R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
⊢ FG s ↔ CompleteLattice.IsCompactElement s
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
⊢ FG s ↔ CompleteLattice.IsCompactElement s
let sp : M → Submodule R M := fun a => span R {a}
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
⊢ FG s ↔ CompleteLattice.IsCompactElement s
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
⊢ FG s ↔ CompleteLattice.IsCompactElement s
have supr_rw : ∀ t : Finset M, (⨆ x ∈ t, sp x) = ⨆ x ∈ (↑t : Set M), sp x := fun t => by rfl
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
⊢ FG s → CompleteLattice.IsCompactElement s

case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
⊢ CompleteLattice.IsCompactElement s → FG s
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
⊢ FG s ↔ CompleteLattice.IsCompactElement s
constructor
no goals
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
t : Finset M
⊢ (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
rfl
case mp.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
t : Finset M
⊢ CompleteLattice.IsCompactElement (span R ↑t)
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
⊢ FG s → CompleteLattice.IsCompactElement s
rintro ⟨t, rfl⟩
case mp.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
t : Finset M
⊢ CompleteLattice.IsCompactElement (Finset.sup t sp)
case mp.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
t : Finset M
⊢ CompleteLattice.IsCompactElement (span R ↑t)
rw [span_eq_iSup_of_singleton_spans, ← supr_rw, ← Finset.sup_eq_iSup t sp]
case mp.intro.h
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
t : Finset M
⊢ ∀ (x : M), x ∈ t → CompleteLattice.IsCompactElement (sp x)
case mp.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
t : Finset M
⊢ CompleteLattice.IsCompactElement (Finset.sup t sp)
apply CompleteLattice.finset_sup_compact_of_compact
no goals
case mp.intro.h
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
t : Finset M
⊢ ∀ (x : M), x ∈ t → CompleteLattice.IsCompactElement (sp x)
exact fun n _ => singleton_span_isCompactElement n
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
⊢ FG s
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
⊢ CompleteLattice.IsCompactElement s → FG s
intro h
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
⊢ FG s
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
⊢ FG s
have sSup' : s = sSup (sp '' ↑s) := by
  rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
case mpr.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
⊢ FG s
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
⊢ FG s
obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup')
case mpr.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
ssup : s = Finset.sup u id
⊢ FG s
case mpr.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
⊢ FG s
have ssup : s = u.sup id := by
  suffices : u.sup id ≤ s
  exact le_antisymm husup this
  rw [sSup', Finset.sup_id_eq_sSup]
  exact sSup_le_sSup huspan
case mpr.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
ssup : s = Finset.sup u id
this : ∃ s', ↑s' ⊆ ↑s ∧ Finset.image sp s' = u
⊢ FG s
case mpr.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
ssup : s = Finset.sup u id
⊢ FG s
have := Finset.subset_image_iff.mp huspan
case mpr.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ Finset.sup (Finset.image sp t) id
ssup : s = Finset.sup (Finset.image sp t) id
⊢ FG s
case mpr.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
ssup : s = Finset.sup u id
this : ∃ s', ↑s' ⊆ ↑s ∧ Finset.image sp s' = u
⊢ FG s
obtain ⟨t, ⟨-, rfl⟩⟩ := this
case mpr.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ Finset.sup (Finset.image sp t) id
ssup : span R ↑t = s
⊢ FG s
case mpr.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ Finset.sup (Finset.image sp t) id
ssup : s = Finset.sup (Finset.image sp t) id
⊢ FG s
rw [Finset.sup_image, Function.comp.left_id, Finset.sup_eq_iSup, supr_rw, ←
  span_eq_iSup_of_singleton_spans, eq_comm] at ssup
no goals
case mpr.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ Finset.sup (Finset.image sp t) id
ssup : span R ↑t = s
⊢ FG s
exact ⟨t, ssup⟩
no goals
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
⊢ s = sSup (sp '' ↑s)
rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
this : Finset.sup u id ≤ s
⊢ s = Finset.sup u id

case this
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
⊢ Finset.sup u id ≤ s
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
⊢ s = Finset.sup u id
suffices : u.sup id ≤ s
case this
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
⊢ Finset.sup u id ≤ s
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
this : Finset.sup u id ≤ s
⊢ s = Finset.sup u id

case this
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
⊢ Finset.sup u id ≤ s
exact le_antisymm husup this
case this
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
⊢ sSup ↑u ≤ sSup (sp '' ↑s)
case this
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
⊢ Finset.sup u id ≤ s
rw [sSup', Finset.sup_id_eq_sSup]
no goals
case this
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
P : Type ?u.314027
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
sp : M → Submodule R M := fun a => span R {a}
supr_rw : ∀ (t : Finset M), (⨆ (x : M) (_ : x ∈ t), sp x) = ⨆ (x : M) (_ : x ∈ ↑t), sp x
h : CompleteLattice.IsCompactElement s
sSup' : s = sSup (sp '' ↑s)
u : Finset (Submodule R M)
huspan : ↑u ⊆ sp '' ↑s
husup : s ≤ Finset.sup u id
⊢ sSup ↑u ≤ sSup (sp '' ↑s)
exact sSup_le_sSup huspan