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

Proof state:
case intro
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
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k => (b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
i' : LinearIndependent (ι := ↑(Φ ⁻¹' {s})) R v'
⊢ False

Tactic:
have w' : Finite (Φ ⁻¹' {s}) := by
  apply i'.finite_of_le_span_finite v' (s.image b)
  rintro m ⟨⟨p, ⟨rfl⟩⟩, rfl⟩
  simp only [SetLike.mem_coe, Subtype.coe_mk, Finset.coe_image]
  apply Basis.mem_span_repr_support

Result:
case intro
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
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k => (b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
i' : LinearIndependent (ι := ↑(Φ ⁻¹' {s})) R v'
w' : Finite ↑(Φ ⁻¹' {s})
⊢ False

Proof state:
case intro.mk.refl
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
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k => (b.repr (v k)).support
p : κ
w : Infinite ↑(Φ ⁻¹' {Φ p})
v' : ↑(Φ ⁻¹' {Φ p}) → M := fun k => v ↑k
i' : LinearIndependent (ι := ↑(Φ ⁻¹' {Φ p})) R v'
⊢ v' ⟨p, ⋯⟩ ∈ ↑(span R ↑(Finset.image (⇑b) (Φ p)))

Tactic:
simp only [SetLike.mem_coe, Subtype.coe_mk, Finset.coe_image]

Result:
case intro.mk.refl
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
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k => (b.repr (v k)).support
p : κ
w : Infinite ↑(Φ ⁻¹' {Φ p})
v' : ↑(Φ ⁻¹' {Φ p}) → M := fun k => v ↑k
i' : LinearIndependent (ι := ↑(Φ ⁻¹' {Φ p})) R v'
⊢ v' ⟨p, ⋯⟩ ∈ span R (⇑b '' ↑(Φ p))

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
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
⊢ #κ ≤ #ι

Tactic:
classical
by_contra h
rw [not_le, ← Cardinal.mk_finset_of_infinite ι] at h
let Φ := fun k : κ => (b.repr (v k)).support
obtain ⟨s, w : Infinite ↑(Φ ⁻¹' {s})⟩ := Cardinal.exists_infinite_fiber Φ h (by infer_instance)
let v' := fun k : Φ ⁻¹' {s} => v k
have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
have w' : Finite (Φ ⁻¹' {s}) := by
  apply i'.finite_of_le_span_finite v' (s.image b)
  rintro m ⟨⟨p, ⟨rfl⟩⟩, rfl⟩
  simp only [SetLike.mem_coe, Subtype.coe_mk, Finset.coe_image]
  apply Basis.mem_span_repr_support
exact w.false

Result:
no goals

Proof state:
case intro
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
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k => (b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
⊢ False

Tactic:
let v' := fun k : Φ ⁻¹' {s} => v k

Result:
case intro
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
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
Φ : κ → Finset ι := fun k => (b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
⊢ False