case f
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ (↑w →₀ R) →ₗ[R] ι →₀ R

case i
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ↑?f
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Fintype.card ι ≤ Fintype.card ↑w
fapply card_le_of_surjective' R
no goals
case f
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ (↑w →₀ R) →ₗ[R] ι →₀ R
exact b.repr.toLinearMap.comp (Finsupp.total w M R (↑))
case i.hg
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ↑↑b.repr

case i.hf
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective fun x => ↑(Finsupp.total (↑w) M R Subtype.val) x
case i
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ↑(LinearMap.comp (↑b.repr) (Finsupp.total (↑w) M R Subtype.val))
apply Surjective.comp (g := b.repr.toLinearMap)
case i.hf
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective fun x => ↑(Finsupp.total (↑w) M R Subtype.val) x
case i.hg
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective ↑↑b.repr

case i.hf
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective fun x => ↑(Finsupp.total (↑w) M R Subtype.val) x
apply LinearEquiv.surjective
case i.hf
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ span R (range Subtype.val) = ⊤
case i.hf
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ Surjective fun x => ↑(Finsupp.total (↑w) M R Subtype.val) x
rw [← LinearMap.range_eq_top, Finsupp.range_total]
no goals
case i.hf
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.301145
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : RankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
b : Basis ι R M
w : Set M
inst✝ : Fintype ↑w
s : span R w = ⊤
⊢ span R (range Subtype.val) = ⊤
simpa using s