awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
this :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
j : Fin 2
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have h : (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) =
  (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
this :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = 1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = 1 ∨
    (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0 = -1 ∧ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1 = -1
j : Fin 2
h :
  (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j
have h₁ : (↑A : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) =
  (↑1 : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
⊢ Eq (α := Subgroup SL(2, ℤ)) (closure {S, T}) ⊤
have rw : ∀ (x : SL(2, ℤ)), Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) x
Tactic: rw [eq_top_iff']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : FixedDetMatrix (Fin 2) ℤ 1
a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0
a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0
h : 0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1
a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) A
have h0 : Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) 1
Tactic: rw [reps_one_id A a1 a4 a6]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : SL(2, ℤ)
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) A
have h0 : ∀ (A : FixedDetMatrix (Fin 2) ℤ 1) (a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0)
  (a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0),
  0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
    ∀ (a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|),
      Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) A
Tactic: induction A using (induction_on one_ne_zero) with
  | h0 A a1 a4 _ a6 =>
    rw [reps_one_id A a1 a4 a6]
    exact one_mem _
  | hS B hb =>
    exact mul_mem (subset_closure (Set.mem_insert S {T})) hb
  | hT B hb =>
    exact mul_mem (subset_closure (Set.mem_insert_of_mem S rfl)) hb
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : SL(2, ℤ)
h0 :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ 1) (a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0)
    (a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0),
    0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
      ∀ (a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|),
        Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) A
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) A
have hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ 1) (hb : Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) B),
  Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) (S • B)
Tactic: induction A using (induction_on one_ne_zero) with
  | h0 A a1 a4 _ a6 =>
    rw [reps_one_id A a1 a4 a6]
    exact one_mem _
  | hS B hb =>
    exact mul_mem (subset_closure (Set.mem_insert S {T})) hb
  | hT B hb =>
    exact mul_mem (subset_closure (Set.mem_insert_of_mem S rfl)) hb
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.FixedDetMatrices (goal)
Goal:
A : SL(2, ℤ)
h0 :
  ∀ (A : FixedDetMatrix (Fin 2) ℤ 1) (a1 : (↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0)
    (a4 : 0 < (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 0),
    0 ≤ (↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1 →
      ∀ (a6 : |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 0 1| < |(↑A : Matrix (Fin 2) (Fin 2) ℤ) 1 1|),
        Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) A
hS :
  ∀ (B : FixedDetMatrix (Fin 2) ℤ 1) (hb : Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) B),
    Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) (S • B)
⊢ Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) A
have hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ 1) (hb : Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) B),
  Membership.mem (γ := Subgroup SL(2, ℤ)) (closure {S, T}) (T • B)
Tactic: induction A using (induction_on one_ne_zero) with
  | h0 A a1 a4 _ a6 =>
    rw [reps_one_id A a1 a4 a6]
    exact one_mem _
  | hS B hb =>
    exact mul_mem (subset_closure (Set.mem_insert S {T})) hb
  | hT B hb =>
    exact mul_mem (subset_closure (Set.mem_insert_of_mem S rfl)) hb
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
⊢ Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g ↔
    Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(Matrix.scalar n) : (a : R) → Matrix n n R))
      (↑g : Matrix n n R)
have mp : Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g →
  Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(Matrix.scalar n) : (a : R) → Matrix n n R))
    (↑g : Matrix n n R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
mp :
  Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g →
    Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(Matrix.scalar n) : (a : R) → Matrix n n R))
      (↑g : Matrix n n R)
⊢ Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g ↔
    Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(Matrix.scalar n) : (a : R) → Matrix n n R))
      (↑g : Matrix n n R)
have mpr : Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(Matrix.scalar n) : (a : R) → Matrix n n R))
    (↑g : Matrix n n R) →
  Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
hg : Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
⊢ Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(Matrix.scalar n) : (a : R) → Matrix n n R))
    (↑g : Matrix n n R)
have mp : ∀ (t : TransvectionStruct n R), Commute t.toMatrix (↑g : Matrix n n R)
Tactic: refine Matrix.mem_range_scalar_of_commute_transvectionStruct fun t ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
⊢ Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(Matrix.scalar n) : (a : R) → Matrix n n R))
      (↑g : Matrix n n R) →
    Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
have mpr : Membership.mem (γ := Set (Matrix n n R)) (Set.range (ι := R) (⇑(Matrix.scalar n) : (a : R) → Matrix n n R))
    (↑g : Matrix n n R) →
  ∀ (a : R) (ha : (Matrix.scalar n : (a : R) → Matrix n n R) a = (↑g : Matrix n n R)) (h : GL n R), h * g = g * h
Tactic: refine fun ⟨a, ha⟩ ↦ Subgroup.mem_center_iff.mpr fun h ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
⊢ Eq (α := Subgroup (GL n R)) (Subgroup.center (GL n R)) (MonoidHom.range (scalar n))
have h : ∀ (g : GL n R),
  Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g ↔
    Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
⊢ Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g ↔
    Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
have h : Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g →
  Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
h :
  Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g →
    Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
⊢ Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g ↔
    Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
have h₁ : Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g →
  Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
hg : Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
hn : Nonempty n
⊢ Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
have h : ∀ (a : R) (ha : (Matrix.scalar n : (a : R) → Matrix n n R) a = (↑g : Matrix n n R)),
  Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
Tactic: obtain ⟨a, ha⟩ := mem_center_iff_val_mem_range_scalar.mp hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
hg : Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
hn : Nonempty n
a : R
ha : (Matrix.scalar n : (a : R) → Matrix n n R) a = (↑g : Matrix n n R)
⊢ Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
have h : ∀ (b : R) (hb : (Matrix.scalar n : (a : R) → Matrix n n R) b = (↑g⁻¹ : Matrix n n R)),
  Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
Tactic: obtain ⟨b, hb⟩ := mem_center_iff_val_mem_range_scalar.mp (Subgroup.inv_mem _ hg)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (hypothesis)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
hg : Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
hn : Nonempty n
a : R
ha : (Matrix.scalar n : (a : R) → Matrix n n R) a = (↑g : Matrix n n R)
b : R
hb : (Matrix.scalar n : (a : R) → Matrix n n R) b = (↑g⁻¹ : Matrix n n R)
⊢ Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
have hab : a * b = 1
Tactic: have hab : a * b = 1 := by
        simpa [-mul_inv_cancel, ← ha, ← hb, ← diagonal_one, Units.ext_iff] using mul_inv_cancel g
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
hg : Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
hn : Nonempty n
a : R
ha : (Matrix.scalar n : (a : R) → Matrix n n R) a = (↑g : Matrix n n R)
b : R
hb : (Matrix.scalar n : (a : R) → Matrix n n R) b = (↑g⁻¹ : Matrix n n R)
hab : a * b = 1
⊢ Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
have h : (scalar n : (a : Rˣ) → GL n R) { val := a, inv := b, val_inv := hab, inv_val := sorry } = g
Tactic: refine ⟨⟨a, b, hab, mul_comm a b ▸ hab⟩, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic (hypothesis)
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
hg : Membership.mem (γ := Subgroup (GL n R)) (Subgroup.center (GL n R)) g
⊢ Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g
have x : IsEmpty n ∨ Nonempty n
Tactic: cases isEmpty_or_nonempty n with
    | inl hn => simp [nontriviality]
    | inr hn =>
      obtain ⟨a, ha⟩ := mem_center_iff_val_mem_range_scalar.mp hg
      obtain ⟨b, hb⟩ := mem_center_iff_val_mem_range_scalar.mp (Subgroup.inv_mem _ hg)
      have hab : a * b = 1 := by
        simpa [-mul_inv_cancel, ← ha, ← hb, ← diagonal_one, Units.ext_iff] using mul_inv_cancel g
      refine ⟨⟨a, b, hab, mul_comm a b ▸ hab⟩, ?_⟩
      simp [Units.ext_iff, ← ha]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
k : ℕ
hk : k ≤ n
⊢ Nat.card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))
have rw : card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))
Tactic: rw [Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
hk : 0 ≤ n
⊢ card.{u_2} { s : Fin 0 → V // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
have zero : ∀ (this : Unique { s : Fin 0 → V // Eq.{u_1 + 1} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ }),
  card.{u_2} { s : Fin 0 → V // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
Tactic: have : Unique { s : Fin 0 → V // (⊤ : Submodule K (Fin 0 →₀ K)) = ⊥ } :=
        uniqueOfSubsingleton ⟨0, Subsingleton.elim ..⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
hk : 0 ≤ n
this : Unique { s : Fin 0 → V // Eq.{u_1 + 1} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ }
⊢ card.{u_2} { s : Fin 0 → V // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
have zero : card.{u_2} { s : Fin 0 → V // Eq (α := Submodule K (Fin 0 →₀ K)) (ker (Finsupp.linearCombination K s)) ⊥ } =
  ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
Tactic: simp_rw [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
        Finset.univ_eq_empty, Finset.prod_empty, card_unique]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
hk : 0 ≤ n
this : Unique { s : Fin 0 → V // Eq.{u_1 + 1} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ }
zero :
  card.{u_2} { s : Fin 0 → V // Eq (α := Submodule K (Fin 0 →₀ K)) (ker (Finsupp.linearCombination K s)) ⊥ } =
    ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
⊢ card.{u_2} { s : Fin 0 → V // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
have zero₁ : card.{u_2}
    { s : Fin 0 → V //
      Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K))
        (ker.{u_1, u_1, u_1, u_2} (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) 0) ⊥ } =
  ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
Tactic: simp_rw [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
        Finset.univ_eq_empty, Finset.prod_empty, card_unique]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
hk : 0 ≤ n
this : Unique { s : Fin 0 → V // Eq.{u_1 + 1} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ }
zero :
  card.{u_2} { s : Fin 0 → V // Eq (α := Submodule K (Fin 0 →₀ K)) (ker (Finsupp.linearCombination K s)) ⊥ } =
    ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
zero₁ :
  card.{u_2}
      { s : Fin 0 → V //
        Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K))
          (ker.{u_1, u_1, u_1, u_2} (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) 0) ⊥ } =
    ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
⊢ card.{u_2} { s : Fin 0 → V // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
have zero₂ : card.{u_2} { s : Fin 0 → V // Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ } =
  ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
Tactic: simp_rw [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
        Finset.univ_eq_empty, Finset.prod_empty, card_unique]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
hk : 0 ≤ n
this : Unique { s : Fin 0 → V // Eq.{u_1 + 1} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ }
zero :
  card.{u_2} { s : Fin 0 → V // Eq (α := Submodule K (Fin 0 →₀ K)) (ker (Finsupp.linearCombination K s)) ⊥ } =
    ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
zero₁ :
  card.{u_2}
      { s : Fin 0 → V //
        Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K))
          (ker.{u_1, u_1, u_1, u_2} (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) 0) ⊥ } =
    ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
zero₂ :
  card.{u_2} { s : Fin 0 → V // Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ } =
    ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
⊢ card.{u_2} { s : Fin 0 → V // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
have zero₃ : card.{u_2} { s : Fin 0 → V // Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ } =
  ∏ x ∈ ∅, (q ^ n - q ^ (↑x : ℕ))
Tactic: simp_rw [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
        Finset.univ_eq_empty, Finset.prod_empty, card_unique]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
hk : 0 ≤ n
this : Unique { s : Fin 0 → V // Eq.{u_1 + 1} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ }
zero :
  card.{u_2} { s : Fin 0 → V // Eq (α := Submodule K (Fin 0 →₀ K)) (ker (Finsupp.linearCombination K s)) ⊥ } =
    ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
zero₁ :
  card.{u_2}
      { s : Fin 0 → V //
        Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K))
          (ker.{u_1, u_1, u_1, u_2} (R₂ := K) (M₂ := V) (τ₁₂ := RingHom.id K) 0) ⊥ } =
    ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
zero₂ :
  card.{u_2} { s : Fin 0 → V // Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ } =
    ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
zero₃ :
  card.{u_2} { s : Fin 0 → V // Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ } =
    ∏ x ∈ ∅, (q ^ n - q ^ (↑x : ℕ))
⊢ card.{u_2} { s : Fin 0 → V // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
have zero₄ : card.{u_2} { s : Fin 0 → V // Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ } = 1
Tactic: simp_rw [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
        Finset.univ_eq_empty, Finset.prod_empty, card_unique]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
k : ℕ
ih : ∀ (hk : k ≤ n), card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))
hk : k + 1 ≤ n
s : { s : Fin k → V // LinearIndependent K s }
⊢ card.{u_2} (↑(↑(Submodule.span K (Set.range (↑s : Fin k → V))) : Set V)ᶜ : Type u_2) = q ^ n - q ^ k
have rw : card V - q ^ finrank.{u_1, u_2} K (↑(↑(Submodule.span K (Set.range (↑s : Fin k → V))) : Set V) : Type u_2) =
  q ^ n - q ^ k
Tactic: rw [card_compl_set, Module.card_eq_pow_finrank (K := K)
            (V := ((Submodule.span K (Set.range (s : Fin k → V))) : Set (V)))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
k : ℕ
ih : ∀ (hk : k ≤ n), card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))
hk : k + 1 ≤ n
s : { s : Fin k → V // LinearIndependent K s }
⊢ card V - q ^ finrank.{u_1, u_2} K (↑(↑(Submodule.span K (Set.range (↑s : Fin k → V))) : Set V) : Type u_2) =
    q ^ n - q ^ k
have simp : card V - q ^ k = q ^ n - q ^ k
Tactic: simp only [SetLike.coe_sort_coe, finrank_span_eq_card s.2, card_fin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (goal)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
k : ℕ
ih : ∀ (hk : k ≤ n), card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))
hk : k + 1 ≤ n
s : { s : Fin k → V // LinearIndependent K s }
⊢ card V - q ^ k = q ^ n - q ^ k
have rw : q ^ n - q ^ k = q ^ n - q ^ k
Tactic: rw [Module.card_eq_pow_finrank (K := K)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Fintype K
inst_4 : Finite V
k : ℕ
ih : ∀ (hk : k ≤ n), card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))
hk : k + 1 ≤ n
⊢ card.{u_2} { s : Fin (k + 1) → V // LinearIndependent K s } = ∏ i : Fin (k + 1), (q ^ n - q ^ (↑i : ℕ))
have this : ∀ (s : { s : Fin k → V // LinearIndependent K s }),
  card.{u_2} (↑(↑(Submodule.span K (Set.range (↑s : Fin k → V))) : Set V)ᶜ : Type u_2) = q ^ n - q ^ k
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, Module.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 [Module.card_eq_pow_finrank (K := K)]