R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
⊢ p = sSup {T | ∃ m x x, T = span R {m}}
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
⊢ p = sSup {T | ∃ m x x, T = span R {m}}
let S := { T : Submodule R M | ∃ (m : M) (_ : m ∈ p) (_ : m ≠ 0), T = span R {m} }
case a
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
⊢ p ≤ sSup {T | ∃ m x x, T = span R {m}}

case a
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
⊢ sSup {T | ∃ m x x, T = span R {m}} ≤ p
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
⊢ p = sSup {T | ∃ m x x, T = span R {m}}
apply le_antisymm
case a
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
m : M
hm : m ∈ p
⊢ m ∈ sSup {T | ∃ m x x, T = span R {m}}
case a
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
⊢ p ≤ sSup {T | ∃ m x x, T = span R {m}}
intro m hm
case pos
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
m : M
hm : m ∈ p
h : m = 0
⊢ m ∈ sSup {T | ∃ m x x, T = span R {m}}

case neg
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
m : M
hm : m ∈ p
h : ¬m = 0
⊢ m ∈ sSup {T | ∃ m x x, T = span R {m}}
case a
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
m : M
hm : m ∈ p
⊢ m ∈ sSup {T | ∃ m x x, T = span R {m}}
by_cases h : m = 0
case pos
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
m : M
hm : m ∈ p
h : m = 0
⊢ 0 ∈ sSup {T | ∃ m x x, T = span R {m}}
case pos
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
m : M
hm : m ∈ p
h : m = 0
⊢ m ∈ sSup {T | ∃ m x x, T = span R {m}}
rw [h]
no goals
case pos
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
m : M
hm : m ∈ p
h : m = 0
⊢ 0 ∈ sSup {T | ∃ m x x, T = span R {m}}
simp
no goals
case neg
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
m : M
hm : m ∈ p
h : ¬m = 0
⊢ m ∈ sSup {T | ∃ m x x, T = span R {m}}
exact @le_sSup _ _ S _ ⟨m, ⟨hm, ⟨h, rfl⟩⟩⟩ m (mem_span_singleton_self m)
case a
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
⊢ ∀ (b : Submodule R M), b ∈ {T | ∃ m x x, T = span R {m}} → b ≤ p
case a
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
⊢ sSup {T | ∃ m x x, T = span R {m}} ≤ p
rw [sSup_le_iff]
case a.intro.intro.intro
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
w✝² : M
w✝¹ : w✝² ∈ p
w✝ : w✝² ≠ 0
⊢ span R {w✝²} ≤ p
case a
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
⊢ ∀ (b : Submodule R M), b ∈ {T | ∃ m x x, T = span R {m}} → b ≤ p
rintro S ⟨_, ⟨_, ⟨_, rfl⟩⟩⟩
no goals
case a.intro.intro.intro
R : Type u_1
R₂ : Type ?u.227879
K : Type ?u.227882
M : Type u_2
M₂ : Type ?u.227888
V : Type ?u.227891
S✝ : Type ?u.227894
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
x : M
p✝ p' : Submodule R M
inst✝² : Semiring R₂
σ₁₂ : R →+* R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
s t : Set M
p : Submodule R M
S : Set (Submodule R M) := {T | ∃ m x x, T = span R {m}}
w✝² : M
w✝¹ : w✝² ∈ p
w✝ : w✝² ≠ 0
⊢ span R {w✝²} ≤ p
rwa [span_singleton_le_iff_mem]