-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem linearIndependent_le_span_aux' {ι : Type*} [Fintype ι] (v : ι → M)
    (i : LinearIndependent R v) (w : Set M) [Fintype w] (s : range v ≤ span R w) :
    Fintype.card ι ≤ Fintype.card 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 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 :
  (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 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 : (linearCombination R fun b => v b) f = (linearCombination R fun b => v b) 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 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 : (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 f.v
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : 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

Tactic:
exact fun i => Span.repr R w ⟨v i, s (mem_range_self i)⟩

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 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 : (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 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 :
  (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 f
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : 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

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 u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
⊢ ι → ↑w →₀ R

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : 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

Tactic:
fapply card_le_of_injective' R

Result:
case f
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : 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
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : 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

Proof state:
case i
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_1
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(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 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 : (linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i => Span.repr R w ⟨v i, ⋯⟩) g
⊢ f = g