-- Mathlib/LinearAlgebra/Dimension/Finite.lean
lemma exists_finset_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.rank R M) :
    ∃ s : Finset M, s.card = n ∧ LinearIndepOn R id (s : Set M)

Proof state:
case inl
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this :
  ∀ (R : Type ?u.127759) (M : Type ?u.127758) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n = Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
obtain ⟨⟨s, hs⟩, hs'⟩ := Cardinal.exists_eq_natCast_of_iSup_eq _
  (Cardinal.bddAbove_range _) _ (h.trans (Module.rank_def R M)).symm

Result:
case inl.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Proof state:
case inr
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n < Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_set_linearIndependent_of_lt_rank h

Result:
case inr.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this :
  ∀ (R : Type ?u.127759) (M : Type ?u.127758) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
rcases hn.eq_or_lt with h | h

Result:
case inl
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this :
  ∀ (R : Type ?u.127759) (M : Type ?u.127758) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n = Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

case inr
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this :
  ∀ (R : Type ?u.127759) (M : Type ?u.127758) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n < Module.rank R M
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
this : Finite ↑s
val✝ : Fintype ↑s
⊢ LinearIndepOn R id ↑s.toFinset

Tactic:
simpa

Result:
no goals

Proof state:
case inl.intro.mk.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
refine ⟨s.toFinset, by simpa using hs', by simpa⟩

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
this : Finite ↑s
val✝ : Fintype ↑s
⊢ s.toFinset.card = n

Tactic:
simpa using hs

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
val✝ : Fintype ↑s
⊢ s.toFinset.card = n

Tactic:
simpa using hs'

Result:
no goals

Proof state:
case inr.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
this : Finite ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
cases nonempty_fintype s

Result:
case inr.intro.intro.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n < Module.rank R M
s : Set M
hs : #↑s = ↑n
hs' : LinearIndepOn R id s
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Proof state:
case inl.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
have : Finite s := lt_aleph0_iff_finite.mp (hs' ▸ nat_lt_aleph0 n)

Result:
case inl.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Proof state:
case inl.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s

Tactic:
cases nonempty_fintype s

Result:
case inl.intro.mk.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn : ↑n ≤ Module.rank R M
this✝ :
  ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
    Nonempty { s // LinearIndepOn R id s }
h : ↑n = Module.rank R M
s : Set M
hs : LinearIndepOn R id s
hs' : #↑↑⟨s, hs⟩ = ↑n
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = n ∧ LinearIndepOn R id ↑s