case mp
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
⊢ I < I ⊔ span R {a} → ¬a ∈ I

case mpr
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
⊢ ¬a ∈ I → I < I ⊔ span R {a}
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
⊢ I < I ⊔ span R {a} ↔ ¬a ∈ I
constructor
case mp
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
⊢ ¬a ∈ I
case mp
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
⊢ I < I ⊔ span R {a} → ¬a ∈ I
intro h
case mp
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
⊢ False
case mp
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
⊢ ¬a ∈ I
by_contra akey
case mp
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
h1 : I ⊔ span R {a} ≤ I
h2 : I > I
⊢ False
case mp
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
h1 : I ⊔ span R {a} ≤ I
⊢ False
have h2 := gt_of_ge_of_gt h1 h
no goals
case mp
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
h1 : I ⊔ span R {a} ≤ I
h2 : I > I
⊢ False
exact lt_irrefl I h2
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
⊢ I ≤ I ∧ span R {a} ≤ I
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
⊢ I ⊔ span R {a} ≤ I
simp only [sup_le_iff]
case left
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
⊢ I ≤ I

case right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
⊢ span R {a} ≤ I
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
⊢ I ≤ I ∧ span R {a} ≤ I
constructor
no goals
case left
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
⊢ I ≤ I
exact le_refl I
no goals
case right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : I < I ⊔ span R {a}
akey : a ∈ I
⊢ span R {a} ≤ I
exact (span_singleton_le_iff_mem a I).mpr akey
case mpr
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ I < I ⊔ span R {a}
case mpr
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
⊢ ¬a ∈ I → I < I ⊔ span R {a}
intro h
case mpr
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ I ≤ I ⊔ span R {a} ∧ ∃ x, x ∈ I ⊔ span R {a} ∧ ¬x ∈ I
case mpr
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ I < I ⊔ span R {a}
apply SetLike.lt_iff_le_and_exists.mpr
case mpr.left
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ I ≤ I ⊔ span R {a}

case mpr.right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ ∃ x, x ∈ I ⊔ span R {a} ∧ ¬x ∈ I
case mpr
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ I ≤ I ⊔ span R {a} ∧ ∃ x, x ∈ I ⊔ span R {a} ∧ ¬x ∈ I
constructor
case mpr.right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ ∃ x, x ∈ I ⊔ span R {a} ∧ ¬x ∈ I
case mpr.left
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ I ≤ I ⊔ span R {a}

case mpr.right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ ∃ x, x ∈ I ⊔ span R {a} ∧ ¬x ∈ I
simp only [le_sup_left]
case mpr.right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ a ∈ I ⊔ span R {a} ∧ ¬a ∈ I
case mpr.right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ ∃ x, x ∈ I ⊔ span R {a} ∧ ¬x ∈ I
use a
case mpr.right.left
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ a ∈ I ⊔ span R {a}

case mpr.right.right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ ¬a ∈ I
case mpr.right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ a ∈ I ⊔ span R {a} ∧ ¬a ∈ I
constructor
case mpr.right.right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ ¬a ∈ I

case mpr.right.left
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ a ∈ I ⊔ span R {a}
case mpr.right.left
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ a ∈ I ⊔ span R {a}

case mpr.right.right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ ¬a ∈ I
swap
no goals
case mpr.right.right
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ ¬a ∈ I
assumption
case mpr.right.left
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
this : span R {a} ≤ I ⊔ span R {a}
⊢ a ∈ I ⊔ span R {a}
case mpr.right.left
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
⊢ a ∈ I ⊔ span R {a}
have : (R ∙ a) ≤ I ⊔ R ∙ a := le_sup_right
no goals
case mpr.right.left
R : Type u_1
R₂ : Type ?u.235836
K : Type ?u.235839
M : Type u_2
M₂ : Type ?u.235845
V : Type ?u.235848
S : Type ?u.235851
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
I : Submodule R M
a : M
h : ¬a ∈ I
this : span R {a} ≤ I ⊔ span R {a}
⊢ a ∈ I ⊔ span R {a}
exact this (mem_span_singleton_self a)