-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem le_rank_iff_exists_linearIndependent_finset
    [Module.Free K V] {n : ℕ} : ↑n ≤ Module.rank K V ↔
    ∃ s : Finset V, s.card = n ∧ LinearIndependent K ((↑) : ↥(s : Set V) → V)

Proof state:
case mpr.intro.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
s : Finset V
si : LinearIndependent K Subtype.val
⊢ ∃ s_1, (∃ t, ↑t = s_1 ∧ t.card = s.card) ∧ LinearIndepOn K id s_1

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

Result:
no goals

Proof state:
case mp.intro.intro.intro.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
t : Finset V
si : LinearIndepOn K id ↑t
⊢ ∃ s, s.card = t.card ∧ LinearIndependent K Subtype.val

Tactic:
exact ⟨t, rfl, si⟩

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K id s) ↔ ∃ s, s.card = n ∧ LinearIndependent K Subtype.val

Tactic:
constructor

Result:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K id s) → ∃ s, s.card = n ∧ LinearIndependent K Subtype.val

case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent K Subtype.val) → ∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K id s

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ ↑n ≤ Module.rank K V ↔ ∃ s, s.card = n ∧ LinearIndependent K Subtype.val

Tactic:
simp only [le_rank_iff_exists_linearIndependent, mk_set_eq_nat_iff_finset]

Result:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K id s) ↔ ∃ s, s.card = n ∧ LinearIndependent K Subtype.val

Proof state:
case mp
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ (∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K id s) → ∃ s, s.card = n ∧ LinearIndependent K Subtype.val

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

Result:
case mp.intro.intro.intro.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
t : Finset V
si : LinearIndepOn K id ↑t
⊢ ∃ s, s.card = t.card ∧ LinearIndependent K Subtype.val

Proof state:
case mpr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
n : ℕ
⊢ (∃ s, s.card = n ∧ LinearIndependent K Subtype.val) → ∃ s, (∃ t, ↑t = s ∧ t.card = n) ∧ LinearIndepOn K id s

Tactic:
rintro ⟨s, rfl, si⟩

Result:
case mpr.intro.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
s : Finset V
si : LinearIndependent K Subtype.val
⊢ ∃ s_1, (∃ t, ↑t = s_1 ∧ t.card = s.card) ∧ LinearIndepOn K id s_1