-- 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 y : R
hxy : x * y ∈ I
hy : y ∉ I
a : R
ha : I ⊔ span {y} = Submodule.span R {a}
He : ¬Submodule.IsPrincipal (Submodule.colon I (span {y}))
⊢ x ∈ I

Tactic:
rw [hI.eq_of_le ((nonPrincipals_def R).2 He) fun a ha ↦
  Ideal.mem_colon_singleton.2 (mul_mem_right _ _ ha)]

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 y : R
hxy : x * y ∈ I
hy : y ∉ I
a : R
ha : I ⊔ span {y} = Submodule.span R {a}
He : ¬Submodule.IsPrincipal (Submodule.colon I (span {y}))
⊢ x ∈ Submodule.colon I (span {y})

Proof state:
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}

Tactic:
obtain ⟨u, rfl⟩ := hisup

Result:
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
⊢ u * a ∈ Submodule.span R {a * b}

Proof state:
case neg.mk.intro.mk.intro.refine_2
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}
⊢ span {a} * span {b} ≤ I

Tactic:
rw [← Ideal.submodule_span_eq, ← ha, Ideal.sup_mul, sup_le_iff,
  span_singleton_mul_span_singleton, mul_comm y, Ideal.span_singleton_le_iff_mem]

Result:
case neg.mk.intro.mk.intro.refine_2
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 * span {b} ≤ I ∧ b * y ∈ 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
⊢ ∀ {J : Ideal R}, I < J → Submodule.IsPrincipal J

Tactic:
intro K hK

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
K : Ideal R
hK : I < K
⊢ Submodule.IsPrincipal K

Proof state:
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

Tactic:
refine hI.prop (H I ⟨hI1, fun {x y} hxy => or_iff_not_imp_right.mpr fun hy => ?_⟩)

Result:
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 = ⊤
x y : R
hxy : x * y ∈ I
hy : y ∉ I
⊢ x ∈ I

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
⊢ i ∈ Submodule.span R {a * b}

Tactic:
have hisup : i ∈ I ⊔ span {y} := Ideal.mem_sup_left hi

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 : i ∈ I ⊔ span {y}
⊢ i ∈ Submodule.span R {a * b}

Proof state:
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 = ⊤
x y : R
hxy : x * y ∈ I
hy : y ∉ I
⊢ x ∈ I

Tactic:
obtain ⟨a, ha⟩ : (I ⊔ span {y}).IsPrincipal :=
  Imax' (left_lt_sup.mpr (mt I.span_singleton_le_iff_mem.mp hy))

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}
⊢ x ∈ I

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}
⊢ i ∈ Submodule.span R {a * b}

Tactic:
have : y ∈ I ⊔ span {y} := Ideal.mem_sup_right (Ideal.mem_span_singleton_self y)

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 : i ∈ I ⊔ span {y}
this : y ∈ I ⊔ span {y}
⊢ i ∈ Submodule.span R {a * b}