-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem linearIndependent_le_span' {ι : Type*} (v : ι → M) (i : LinearIndependent R v) (w : Set M)
    [Fintype w] (s : range v ≤ span R w) : #ι ≤ Fintype.card w

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
this : Finite ι
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
letI := Fintype.ofFinite ι

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ #ι ≤ ↑(Fintype.card ↑w)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
haveI : Finite ι := i.finite_of_le_span_finite v w s

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
this : Finite ι
⊢ #ι ≤ ↑(Fintype.card ↑w)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ ↑(Fintype.card ι) ≤ ↑(Fintype.card ↑w)

Tactic:
simp only [Nat.cast_le]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ Fintype.card ι ≤ Fintype.card ↑w

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
rw [Cardinal.mk_fintype]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ ↑(Fintype.card ι) ≤ ↑(Fintype.card ↑w)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_1
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ≤ ↑(span R w)
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ Fintype.card ι ≤ Fintype.card ↑w

Tactic:
exact linearIndependent_le_span_aux' v i w s

Result:
no goals