-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem le_rank_iff_exists_linearIndependent [Module.Free K V] {c : Cardinal} :
    c ≤ Module.rank K V ↔ ∃ s : Set V, #s = c ∧ LinearIndepOn K id s

Proof state:
case mp.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
have : LinearIndepOn K id (Set.range t') := by
  convert t.linearIndependent.linearIndepOn_id
  ext
  simp [t]

Result:
case mp.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this✝ : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Proof state:
case h.e'_8
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
⊢ range ⇑t' = range ⇑t

Tactic:
ext

Result:
case h.e'_8.h
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
x✝ : V
⊢ x✝ ∈ range ⇑t' ↔ x✝ ∈ range ⇑t

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
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
obtain ⟨κ, t'⟩ := Module.Free.exists_basis (R := K) (M := V)

Result:
case mp.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Proof state:
case mp.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this✝ : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
rw [← t.mk_eq_rank'', le_mk_iff_exists_subset] at h

Result:
case mp.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this✝ : Nontrivial K
κ : Type v
t' : Basis κ K V
h : ∃ p ⊆ range ⇑t', #↑p = c
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
⊢ ∃ s, #↑s = c ∧ 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
c : Cardinal.{v}
⊢ c ≤ Module.rank K V ↔ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
haveI := nontrivial_of_invariantBasisNumber K

Result:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
⊢ c ≤ Module.rank K V ↔ ∃ s, #↑s = c ∧ 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
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
⊢ LinearIndepOn K id (range ⇑t')

Tactic:
convert t.linearIndependent.linearIndepOn_id

Result:
case h.e'_8
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
⊢ range ⇑t' = range ⇑t

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
c : Cardinal.{v}
this : Nontrivial K
⊢ (∃ s, #↑s = c ∧ LinearIndepOn K id s) → c ≤ Module.rank K V

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
this : Nontrivial K
s : Set V
si : LinearIndepOn K id s
⊢ #↑s ≤ Module.rank K V

Proof state:
case mp.intro.mk.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
c : Cardinal.{v}
this✝ : Nontrivial K
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
s : Set V
hst : s ⊆ range ⇑t'
hsc : #↑s = c
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
exact ⟨s, hsc, this.mono hst⟩

Result:
no goals

Proof state:
case mp.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
let t := t'.reindexRange

Result:
case mp.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

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
this : Nontrivial K
s : Set V
si : LinearIndepOn K id s
⊢ #↑s ≤ Module.rank K V

Tactic:
exact si.cardinal_le_rank

Result:
no goals

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
c : Cardinal.{v}
this : Nontrivial K
⊢ c ≤ Module.rank K V → ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
intro h

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
c : Cardinal.{v}
this : Nontrivial K
h : c ≤ Module.rank K V
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Proof state:
case mp.intro.mk
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
c : Cardinal.{v}
this✝ : Nontrivial K
κ : Type v
t' : Basis κ K V
h : ∃ p ⊆ range ⇑t', #↑p = c
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s

Tactic:
rcases h with ⟨s, hst, hsc⟩

Result:
case mp.intro.mk.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
c : Cardinal.{v}
this✝ : Nontrivial K
κ : Type v
t' : Basis κ K V
t : Basis (↑(range ⇑t')) K V := t'.reindexRange
this : LinearIndepOn K id (range ⇑t')
s : Set V
hst : s ⊆ range ⇑t'
hsc : #↑s = c
⊢ ∃ s, #↑s = c ∧ LinearIndepOn K id s