-- Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Card.lean
theorem card_linearIndependent {k : ℕ} (hk : k ≤ n) :
    Nat.card { s : Fin k → V // LinearIndependent K s } =
      ∏ i : Fin k, (q ^ n - q ^ i.val)

Proof state:
case zero
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
hk : 0 ≤ n
⊢ card { s // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ ↑i)

Tactic:
simp only [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
card_ofSubsingleton, Finset.univ_eq_empty, Finset.prod_empty]

Result:
no goals

Proof state:
case succ
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
ih : k ≤ n → card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)
hk : k + 1 ≤ n
this : ∀ (s : { s // LinearIndependent K s }), card ↑(↑(Submodule.span K (Set.range ↑s)))ᶜ = q ^ n - q ^ k
⊢ card { s // LinearIndependent K s } = ∏ i : Fin (k + 1), (q ^ n - q ^ ↑i)

Tactic:
simp [card_congr (equiv_linearIndependent k), sum_congr _ _ this, ih (Nat.le_of_succ_le hk),
  mul_comm, Fin.prod_univ_succAbove _ k]

Result:
no goals

Proof state:
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
ih : k ≤ n → card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)
hk : k + 1 ≤ n
s : { s // LinearIndependent K s }
⊢ card V - q ^ k = q ^ n - q ^ k

Tactic:
rw [card_eq_pow_finrank (K := K)]

Result:
no goals

Proof state:
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
hk : k ≤ n
⊢ card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)

Tactic:
induction k with
| zero => simp only [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
    card_ofSubsingleton, Finset.univ_eq_empty, Finset.prod_empty]
| succ k ih =>
    have (s : { s : Fin k → V // LinearIndependent K s }) :
        card ((Submodule.span K (Set.range (s : Fin k → V)))ᶜ : Set (V)) =
        (q) ^ n - (q) ^ k := by
          rw [card_compl_set, card_eq_pow_finrank (K := K)
          (V := ((Submodule.span K (Set.range (s : Fin k → V))) : Set (V)))]
          simp only [SetLike.coe_sort_coe, finrank_span_eq_card s.2, card_fin]
          rw [card_eq_pow_finrank (K := K)]
    simp [card_congr (equiv_linearIndependent k), sum_congr _ _ this, ih (Nat.le_of_succ_le hk),
      mul_comm, Fin.prod_univ_succAbove _ k]

Result:
no goals

Proof state:
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
ih : k ≤ n → card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)
hk : k + 1 ≤ n
s : { s // LinearIndependent K s }
⊢ card V - q ^ Module.finrank K ↑↑(Submodule.span K (Set.range ↑s)) = q ^ n - q ^ k

Tactic:
simp only [SetLike.coe_sort_coe, finrank_span_eq_card s.2, card_fin]

Result:
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
ih : k ≤ n → card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)
hk : k + 1 ≤ n
s : { s // LinearIndependent K s }
⊢ card V - q ^ k = q ^ n - q ^ k

Proof state:
case succ
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
ih : k ≤ n → card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)
hk : k + 1 ≤ n
⊢ card { s // LinearIndependent K s } = ∏ i : Fin (k + 1), (q ^ n - q ^ ↑i)

Tactic:
have (s : { s : Fin k → V // LinearIndependent K s }) :
    card ((Submodule.span K (Set.range (s : Fin k → V)))ᶜ : Set (V)) =
    (q) ^ n - (q) ^ k := by
      rw [card_compl_set, card_eq_pow_finrank (K := K)
      (V := ((Submodule.span K (Set.range (s : Fin k → V))) : Set (V)))]
      simp only [SetLike.coe_sort_coe, finrank_span_eq_card s.2, card_fin]
      rw [card_eq_pow_finrank (K := K)]

Result:
case succ
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
ih : k ≤ n → card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)
hk : k + 1 ≤ n
this : ∀ (s : { s // LinearIndependent K s }), card ↑(↑(Submodule.span K (Set.range ↑s)))ᶜ = q ^ n - q ^ k
⊢ card { s // LinearIndependent K s } = ∏ i : Fin (k + 1), (q ^ n - q ^ ↑i)

Proof state:
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
hk : k ≤ n
⊢ Nat.card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)

Tactic:
rw [Nat.card_eq_fintype_card]

Result:
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
hk : k ≤ n
⊢ card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)

Proof state:
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
ih : k ≤ n → card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)
hk : k + 1 ≤ n
s : { s // LinearIndependent K s }
⊢ card ↑(↑(Submodule.span K (Set.range ↑s)))ᶜ = q ^ n - q ^ k

Tactic:
rw [card_compl_set, card_eq_pow_finrank (K := K)
(V := ((Submodule.span K (Set.range (s : Fin k → V))) : Set (V)))]

Result:
K : Type u_1
V : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Fintype K
inst✝ : Finite V
k : ℕ
ih : k ≤ n → card { s // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ ↑i)
hk : k + 1 ≤ n
s : { s // LinearIndependent K s }
⊢ card V - q ^ Module.finrank K ↑↑(Submodule.span K (Set.range ↑s)) = q ^ n - q ^ k