-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem linearIndependent_le_span'' {ι : Type v} {v : ι → M} (i : LinearIndependent R v) (w : Set M)
    (s : span R w = ⊤) : #ι ≤ #w

Proof state:
case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f g : ι →₀ R
h : (linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩) g
⊢ f = g

Tactic:
apply_fun linearCombination R ((↑) : w → M) at h

Result:
case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f g : ι →₀ R
h :
  (linearCombination R Subtype.val) ((linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩) f) =
    (linearCombination R Subtype.val) ((linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩) g)
⊢ f = g

Proof state:
case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f g : ι →₀ R
h : (linearCombination R fun b => v b) f = (linearCombination R fun b => v b) g
⊢ f = g

Tactic:
exact i h

Result:
no goals

Proof state:
case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f g : ι →₀ R
h :
  (linearCombination R Subtype.val) ((linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩) f) =
    (linearCombination R Subtype.val) ((linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩) g)
⊢ f = g

Tactic:
simp only [linearCombination_linearCombination, Submodule.coe_mk,
           Span.finsupp_linearCombination_repr] at h

Result:
case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f g : ι →₀ R
h : (linearCombination R fun b => v b) f = (linearCombination R fun b => v b) g
⊢ f = g

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ #ι ≤ #↑w

Tactic:
fapply card_le_of_injective'' (R := R)

Result:
case f
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ (ι →₀ R) →ₗ[R] ↑w →₀ R

case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ Injective ⇑?f

Proof state:
case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ Injective ⇑(linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩)

Tactic:
intro f g h

Result:
case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f g : ι →₀ R
h : (linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩) g
⊢ f = g

Proof state:
case f.v
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ ι → ↑w →₀ R

Tactic:
exact fun i ↦ Span.repr R w ⟨v i, s ▸ trivial⟩

Result:
no goals

Proof state:
case f
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ (ι →₀ R) →ₗ[R] ↑w →₀ R

Tactic:
apply Finsupp.linearCombination

Result:
case f.v
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
⊢ ι → ↑w →₀ R