Theorem: FiniteDimensional.exists_finset_card_eq_finrank_and_linearIndependent (FltRegular/NumberTheory/Finrank.lean)

State before:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
by_cases H : finrank R M = 0
State after:
case pos
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : finrank R M = 0
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val

case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val

State before:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
haveI := nonempty_linearIndependent_set R M
State after:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val

State before:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
have := (Cardinal.toNat_eq_iff H).mp rfl
State after:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : Module.rank R M = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val

State before:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : Module.rank R M = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
rw [Module.rank_def] at this
State after:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : ⨆ ι, #↑↑ι = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val

State before:
case neg
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : ⨆ ι, #↑↑ι = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
obtain ⟨⟨s, hs⟩, hι : #s = _⟩ :=
  Cardinal.exists_eq_natCast_of_iSup_eq _ (Cardinal.bddAbove_range.{v, v} _) _ this
State after:
case neg.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val

State before:
case neg.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
have : Finite s := Cardinal.lt_aleph0_iff_finite.mp (hι ▸ nat_lt_aleph0 (finrank R M))
State after:
case neg.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val

State before:
case neg.intro.mk
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
cases nonempty_fintype s
State after:
case neg.intro.mk.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val

State before:
case neg.intro.mk.intro
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
exact ⟨s.toFinset,
  Cardinal.natCast_injective (by rwa [Set.toFinset_card, ← Cardinal.mk_fintype]),
  by convert hs <;> simp only [Set.mem_toFinset]⟩
State after:
no goals

State before:
case pos
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : finrank R M = 0
⊢ ∃ s, s.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
use ∅
State after:
case h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : finrank R M = 0
⊢ ∅.card = finrank R M ∧ LinearIndependent R Subtype.val

State before:
case h
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : finrank R M = 0
⊢ ∅.card = finrank R M ∧ LinearIndependent R Subtype.val
Tactic:
simp only [Finset.card_empty, H, linearIndependent_empty_type, and_self]
State after:
no goals

State before:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ↑s.toFinset.card = ↑(finrank R M)
Tactic:
rwa [Set.toFinset_card, ← Cardinal.mk_fintype]
State after:
no goals

State before:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ¬finrank R M = 0
this✝¹ : Nonempty { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }
this✝ : ⨆ ι, #↑↑ι = ↑(finrank R M)
s : Set M
hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val
hι : #↑s = ↑(finrank R M)
this : Finite ↑s
val✝ : Fintype ↑s
⊢ LinearIndependent R Subtype.val
Tactic:
convert hs <;> simp only [Set.mem_toFinset]
State after:
no goals