R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
⊢ sSup c ∈ nonPrincipals R
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
⊢ ∃ I, I ∈ nonPrincipals R ∧ ∀ (J : Ideal R), J ∈ c → J ≤ I
refine' ⟨sSup c, _, fun J hJ => le_sSup hJ⟩
case mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
⊢ False
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
⊢ sSup c ∈ nonPrincipals R
rintro ⟨x, hx⟩
case mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
⊢ False
case mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
⊢ False
have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) 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
case mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
⊢ False
obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) 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
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) 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
have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hchain : IsChain (fun x x_1 => x ≤ x_1) 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
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) 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
specialize hs hJc
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hchain : IsChain (fun x x_1 => x ≤ x_1) 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 : ¬IsPrincipal (Submodule.span R {x})
⊢ False
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hchain : IsChain (fun x x_1 => x ≤ x_1) 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
rw [← hsSupJ, hx, nonPrincipals_def] at hs
no goals
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hchain : IsChain (fun x x_1 => x ≤ x_1) 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 : ¬IsPrincipal (Submodule.span R {x})
⊢ False
exact hs ⟨⟨x, rfl⟩⟩
no goals
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) 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
simp [hx, Ideal.span_le, hxJ]