-- Mathlib/RingTheory/PrincipalIdealDomainOfPrime.lean
theorem IsPrincipalIdealRing.of_prime (H : ∀ P : Ideal R, P.IsPrime → P.IsPrincipal) :
    IsPrincipalIdealRing R

Proof state:
case neg.mk.intro.mk.intro.refine_1
R : Type u_1
inst✝ : CommRing R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
hJI : J ≤ I
hI : Maximal (fun x => x ∈ nonPrincipals R) I
Imax' : ∀ {J : Ideal R}, I < J → Submodule.IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : y ∉ I
a : R
ha : I ⊔ span {y} = Submodule.span R {a}
b : R
hb : Submodule.colon I (span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ span {y}
this : y ∈ I ⊔ span {y}
⊢ i ∈ Submodule.span R {a * b}

Tactic:
erw [ha, mem_span_singleton'] at hisup this

Result:
case neg.mk.intro.mk.intro.refine_1
R : Type u_1
inst✝ : CommRing R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
hJI : J ≤ I
hI : Maximal (fun x => x ∈ nonPrincipals R) I
Imax' : ∀ {J : Ideal R}, I < J → Submodule.IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : y ∉ I
a : R
ha : I ⊔ span {y} = Submodule.span R {a}
b : R
hb : Submodule.colon I (span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : ∃ a_1, a_1 * a = i
this : ∃ a_1, a_1 * a = y
⊢ i ∈ Submodule.span R {a * b}

Proof state:
R : Type u_1
inst✝ : CommRing R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
⊢ False

Tactic:
obtain ⟨I, hJI, hI⟩ := zorn_le_nonempty₀ (nonPrincipals R) nonPrincipals_zorn _ hJ

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
hJI : J ≤ I
hI : Maximal (fun x => x ∈ nonPrincipals R) I
⊢ False

Proof state:
case neg.mk.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
hJI : J ≤ I
hI : Maximal (fun x => x ∈ nonPrincipals R) I
Imax' : ∀ {J : Ideal R}, I < J → Submodule.IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : y ∉ I
a : R
ha : I ⊔ span {y} = Submodule.span R {a}
b : R
hb : Submodule.colon I (span {y}) = Submodule.span R {b}
⊢ False

Tactic:
refine (nonPrincipals_def _).1 hI.prop ⟨a * b, ?_⟩

Result:
case neg.mk.intro.mk.intro
R : Type u_1
inst✝ : CommRing R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
hJI : J ≤ I
hI : Maximal (fun x => x ∈ nonPrincipals R) I
Imax' : ∀ {J : Ideal R}, I < J → Submodule.IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : y ∉ I
a : R
ha : I ⊔ span {y} = Submodule.span R {a}
b : R
hb : Submodule.colon I (span {y}) = Submodule.span R {b}
⊢ I = Submodule.span R {a * b}

Proof state:
R : Type u_1
inst✝ : CommRing R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
hJI : J ≤ I
hI : Maximal (fun x => x ∈ nonPrincipals R) I
K : Ideal R
hK : I < K
⊢ Submodule.IsPrincipal K

Tactic:
simpa [nonPrincipals] using hI.not_prop_of_gt hK

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
hJI : J ≤ I
hI : Maximal (fun x => x ∈ nonPrincipals R) I
Imax' : ∀ {J : Ideal R}, I < J → Submodule.IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : v * a ∉ I
ha : I ⊔ span {v * a} = Submodule.span R {a}
hb : Submodule.colon I (span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
⊢ u * a * v ∈ I

Tactic:
exact mul_mem_right _ _ hi

Result:
no goals