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

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 ∈ Submodule.colon I (span {v * a})

Tactic:
rw [Ideal.mem_colon_singleton, mul_comm v, ← mul_assoc]

Result:
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

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}
z : R
hi : z * b * a ∈ I
⊢ z * (a * b) = z * b * a

Tactic:
ring

Result:
no goals

Proof state:
case neg.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}
⊢ ¬Submodule.IsPrincipal (Submodule.colon I (span {y}))

Tactic:
rintro ⟨b, hb⟩

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}
⊢ False

Proof state:
case neg.mk.intro.mk.intro.refine_1.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
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
hucolon : ∃ a, a * b = u
⊢ u * a ∈ Submodule.span R {a * b}

Tactic:
obtain ⟨z, rfl⟩ := hucolon

Result:
case neg.mk.intro.mk.intro.refine_1.intro.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
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}
z : R
hi : z * b * a ∈ I
⊢ z * b * a ∈ Submodule.span R {a * b}

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 : ∃ a_1, a_1 * a = i
this : ∃ a_1, a_1 * a = y
⊢ i ∈ Submodule.span R {a * b}

Tactic:
obtain ⟨v, rfl⟩ := this

Result:
case neg.mk.intro.mk.intro.refine_1.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 a b i : R
hi : i ∈ I
hisup : ∃ a_1, a_1 * a = i
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}
⊢ i ∈ Submodule.span R {a * b}

Proof state:
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
Imax' : ∀ {J : Ideal R}, I < J → Submodule.IsPrincipal J
⊢ False

Tactic:
by_cases hI1 : I = ⊤

Result:
case pos
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 = ⊤
⊢ False

case neg
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 = ⊤
⊢ False

Proof state:
case neg.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}
⊢ x ∈ I

Tactic:
suffices He : ¬(I.colon (span {y})).IsPrincipal by
  rw [hI.eq_of_le ((nonPrincipals_def R).2 He) fun a ha ↦
    Ideal.mem_colon_singleton.2 (mul_mem_right _ _ ha)]
  exact Ideal.mem_colon_singleton.2 hxy

Result:
case neg.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}
⊢ ¬Submodule.IsPrincipal (Submodule.colon I (span {y}))

Proof state:
case pos
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 = ⊤
⊢ False

Tactic:
subst hI1

Result:
case pos
R : Type u_1
inst✝ : CommRing R
H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
hJI : J ≤ ⊤
hI : Maximal (fun x => x ∈ nonPrincipals R) ⊤
Imax' : ∀ {J : Ideal R}, ⊤ < J → Submodule.IsPrincipal J
⊢ False