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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
⊢ (ι →₀ R) →ₗ[R] ↑w →₀ 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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
⊢ Injective ↑?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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
⊢ Fintype.card ι ≤ Fintype.card ↑w
fapply card_le_of_injective' R
case f.v
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
⊢ ι → ↑w →₀ R
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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
⊢ (ι →₀ R) →ₗ[R] ↑w →₀ R
apply Finsupp.total
no goals
case f.v
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
⊢ ι → ↑w →₀ R
exact fun i => Span.repr R w ⟨v i, s (mem_range_self i)⟩
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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
f g : ι →₀ R
h :
  ↑(Finsupp.total ι (↑w →₀ R) R fun i => Span.repr R w { val := v i, property := (_ : v i ∈ ↑(span R w)) }) f =
    ↑(Finsupp.total ι (↑w →₀ R) R fun i => Span.repr R w { val := v i, property := (_ : v i ∈ ↑(span R w)) }) g
⊢ f = g
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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
⊢ Injective ↑(Finsupp.total ι (↑w →₀ R) R fun i => Span.repr R w { val := v i, property := (_ : v i ∈ ↑(span R w)) })
intro f g h
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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
f g : ι →₀ R
h :
  ↑(Finsupp.total (↑w) M R Subtype.val)
      (↑(Finsupp.total ι (↑w →₀ R) R fun i => Span.repr R w { val := v i, property := (_ : v i ∈ ↑(span R w)) }) f) =
    ↑(Finsupp.total (↑w) M R Subtype.val)
      (↑(Finsupp.total ι (↑w →₀ R) R fun i => Span.repr R w { val := v i, property := (_ : v i ∈ ↑(span R w)) }) g)
⊢ f = g
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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
f g : ι →₀ R
h :
  ↑(Finsupp.total ι (↑w →₀ R) R fun i => Span.repr R w { val := v i, property := (_ : v i ∈ ↑(span R w)) }) f =
    ↑(Finsupp.total ι (↑w →₀ R) R fun i => Span.repr R w { val := v i, property := (_ : v i ∈ ↑(span R w)) }) g
⊢ f = g
apply_fun Finsupp.total w M R (↑) at h
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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
f g : ι →₀ R
h : ↑(Finsupp.total ι M R fun b => v b) f = ↑(Finsupp.total ι M R fun b => v b) g
⊢ f = g
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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
f g : ι →₀ R
h :
  ↑(Finsupp.total (↑w) M R Subtype.val)
      (↑(Finsupp.total ι (↑w →₀ R) R fun i => Span.repr R w { val := v i, property := (_ : v i ∈ ↑(span R w)) }) f) =
    ↑(Finsupp.total (↑w) M R Subtype.val)
      (↑(Finsupp.total ι (↑w →₀ R) R fun i => Span.repr R w { val := v i, property := (_ : v i ∈ ↑(span R w)) }) g)
⊢ f = g
simp only [Finsupp.total_total, Submodule.coe_mk, Span.finsupp_total_repr] at h
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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
f g : ι →₀ R
h✝ : ↑(Finsupp.total ι M R fun b => v b) f = ↑(Finsupp.total ι M R fun b => v b) g
h : ↑(Finsupp.total ι M R fun b => v b) (f - g) = 0
⊢ f = g
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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
f g : ι →₀ R
h : ↑(Finsupp.total ι M R fun b => v b) f = ↑(Finsupp.total ι M R fun b => v b) g
⊢ f = g
rw [← sub_eq_zero, ← LinearMap.map_sub] at h
no goals
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.336435
R : Type u
inst✝⁵ : Ring R
inst✝⁴ : StrongRankCondition R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
f g : ι →₀ R
h✝ : ↑(Finsupp.total ι M R fun b => v b) f = ↑(Finsupp.total ι M R fun b => v b) g
h : ↑(Finsupp.total ι M R fun b => v b) (f - g) = 0
⊢ f = g
exact sub_eq_zero.mp (linearIndependent_iff.mp i _ h)