∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)) (P' : Ideal R) (M : Submonoid (R ⧸ P'))
  (φ : R ⧸ P' →+* Polynomial R ⧸ P),
  let M' := Submonoid.map φ M;
  ∀ (motive : 0 ∈ M' → Prop) (hM' : 0 ∈ M'), (∀ (z : R ⧸ P') (zM : z ∈ ↑M) (z0 : φ z = 0), motive ⋯) → motive hM'