-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem linearIndependent_le_basis {ι : Type w} (b : Basis ι R M) {κ : Type w} (v : κ → M)
    (i : LinearIndependent R v) : #κ ≤ #ι

Proof state:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ #κ ≤ ↑(Fintype.card ↑(range ⇑b))

Tactic:
exact linearIndependent_le_span v i (range b) b.span_eq

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
⊢ #κ ≤ #ι

Tactic:
cases fintypeOrInfinite ι

Result:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ #κ ≤ #ι

case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Infinite ι
⊢ #κ ≤ #ι

Proof state:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ #κ ≤ #ι

Tactic:
rw [Cardinal.mk_fintype ι]

Result:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ #κ ≤ ↑(Fintype.card ι)

Proof state:
case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Infinite ι
⊢ #κ ≤ #ι

Tactic:
exact linearIndependent_le_infinite_basis b v i

Result:
no goals

Proof state:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ #κ ≤ ↑(Fintype.card ι)

Tactic:
rw [Fintype.card_congr (Equiv.ofInjective b b.injective)]

Result:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ #κ ≤ ↑(Fintype.card ↑(range ⇑b))

Proof state:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
⊢ #κ ≤ ↑(Fintype.card ι)

Tactic:
haveI : Nontrivial R := nontrivial_of_invariantBasisNumber R

Result:
case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ #κ ≤ ↑(Fintype.card ι)