-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem nonPrincipals_zorn (c : Set (Ideal R)) (hs : c ⊆ nonPrincipals R)
    (hchain : IsChain (· ≤ ·) c) {K : Ideal R} (hKmem : K ∈ c) :
    ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I

Proof state:
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
⊢ sSup c ≤ J

Tactic:
simp [hx, Ideal.span_le, hxJ]

Result:
no goals

Proof state:
case mk.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
⊢ False

Tactic:
have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x

Result:
case mk.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
⊢ False

Proof state:
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
hs : J ∈ nonPrincipals R
⊢ False

Tactic:
rw [← hsSupJ, hx, nonPrincipals_def] at hs

Result:
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
hs : ¬(Submodule.span R {x}).IsPrincipal
⊢ False

Proof state:
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
⊢ ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I

Tactic:
refine ⟨sSup c, ?_, fun J hJ => le_sSup hJ⟩

Result:
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
⊢ sSup c ∈ nonPrincipals R

Proof state:
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
⊢ sSup c ∈ nonPrincipals R

Tactic:
rintro ⟨x, hx⟩

Result:
case mk.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
⊢ False

Proof state:
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
⊢ False

Tactic:
have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)

Result:
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
⊢ False

Proof state:
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
⊢ False

Tactic:
specialize hs hJc

Result:
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
hs : J ∈ nonPrincipals R
⊢ False

Proof state:
case mk.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
⊢ False

Tactic:
obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem

Result:
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
⊢ False

Proof state:
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
c : Set (Ideal R)
hchain : IsChain (fun x1 x2 => x1 ≤ x2) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
hs : ¬(Submodule.span R {x}).IsPrincipal
⊢ False

Tactic:
exact hs ⟨⟨x, rfl⟩⟩

Result:
no goals