-- Mathlib/LinearAlgebra/Dimension/LinearMap.lean
theorem le_rank_iff_exists_linearIndependent_finset {n : ℕ} {f : V →ₗ[K] V'} :
    ↑n ≤ rank f ↔ ∃ s : Finset V, s.card = n ∧ LinearIndependent K fun x : (s : Set V) => f x

Proof state:
case mp.intro.intro.intro.intro
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
t : Finset V
si : LinearIndepOn K ⇑f ↑t
⊢ ∃ s, s.card = t.card ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x

Tactic:
exact ⟨t, rfl, si⟩

Result:
no goals

Proof state:
case mp
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s) →
    ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x

Tactic:
rintro ⟨s, ⟨t, rfl, rfl⟩, si⟩

Result:
case mp.intro.intro.intro.intro
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
t : Finset V
si : LinearIndepOn K ⇑f ↑t
⊢ ∃ s, s.card = t.card ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x

Proof state:
case mpr.intro.intro
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
s : Finset V
si : LinearIndependent K fun (x : ↑↑s) => f ↑x
⊢ ∃ s_1, (∃ t, ↑t = s_1 ∧ t.card = s.card) ∧ LinearIndepOn K (⇑f) s_1

Tactic:
exact ⟨s, ⟨s, rfl, rfl⟩, si⟩

Result:
no goals

Proof state:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s) ↔
    ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x

Tactic:
constructor

Result:
case mp
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s) →
    ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x

case mpr
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x) →
    ∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s

Proof state:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ ↑n ≤ f.rank ↔ ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x

Tactic:
simp only [le_rank_iff_exists_linearIndependent, Cardinal.lift_natCast, Cardinal.lift_eq_nat_iff,
  Cardinal.mk_set_eq_nat_iff_finset]

Result:
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s) ↔
    ∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x

Proof state:
case mpr
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
n : ℕ
f : V →ₗ[K] V'
⊢ (∃ s, s.card = n ∧ LinearIndependent K fun (x : ↑↑s) => f ↑x) →
    ∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K (⇑f) s

Tactic:
rintro ⟨s, rfl, si⟩

Result:
case mpr.intro.intro
K : Type u
V : Type v
V' : Type v'
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V'
inst✝ : Module K V'
f : V →ₗ[K] V'
s : Finset V
si : LinearIndependent K fun (x : ↑↑s) => f ↑x
⊢ ∃ s_1, (∃ t, ↑t = s_1 ∧ t.card = s.card) ∧ LinearIndepOn K (⇑f) s_1