awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
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)
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)
⊢ 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

Premises used: OneMemClass.one_mem
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
Goal:
R : Type u_1
inst : Field R
a b : R
hab : HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 ≠ 0
⊢ Ne.{u_1 + 1} (α := R) (det (n := Fin 2) !![a, -b; b, a]) 0

Tactic:
simpa [det_fin_two, sq] using hab

Premises used: sq, Matrix.det_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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)
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
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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)

Tactic:
Matrix.mem_range_scalar_of_commute_transvectionStruct fun t ↦ ?_

Premises used: Matrix.mem_range_scalar_of_commute_transvectionStruct
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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
mp : ∀ (t : TransvectionStruct n R), Commute t.toMatrix (↑g : Matrix n 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)

Tactic:
refine Matrix.mem_range_scalar_of_commute_transvectionStruct fun t ↦ ?_

Premises used: Matrix.mem_range_scalar_of_commute_transvectionStruct
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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
t : TransvectionStruct n R
⊢ Commute t.toMatrix (↑g : Matrix n n R)

Tactic:
simpa [Units.ext_iff] using Subgroup.mem_center_iff.mp hg (.mk _ _ t.mul_inv t.inv_mul)

Premises used: Units.ext_iff, Subgroup.mem_center_iff, Matrix.TransvectionStruct.inv_mul, Units.mk, Iff.mp, Matrix.TransvectionStruct.mul_inv
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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

Tactic:
fun ⟨a, ha⟩ ↦ Subgroup.mem_center_iff.mpr fun h ↦ ?_

Premises used: Iff.mpr, _private.0.Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar.match_1, Subgroup.mem_center_iff, Membership.mem, Subgroup.center, Matrix.GeneralLinearGroup
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
g : GL n R
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
⊢ 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:
refine fun ⟨a, ha⟩ ↦ Subgroup.mem_center_iff.mpr fun h ↦ ?_
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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_1 :
  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:
simpa [Units.ext_iff, ← ha] using (scalar_commute a (mul_comm a ·) h.val).symm

Premises used: Units.val, Units.ext_iff, Matrix.scalar_commute, Commute.symm, mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
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
⊢ Eq (α := Subgroup (GL n R)) (Subgroup.center (GL n R)) (MonoidHom.range (scalar n))

Tactic:
ext g
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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
h₁ :
  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)) (Subgroup.center (GL n R)) g ↔
    Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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 : IsEmpty n
⊢ Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g

Tactic:
simp [nontriviality]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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
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
⊢ Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g

Tactic:
obtain ⟨a, ha⟩ := mem_center_iff_val_mem_range_scalar.mp hg

Premises used: Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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)
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
⊢ 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)

Premises used: Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, Subgroup.inv_mem, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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)
⊢ a * b = 1

Tactic:
simpa [-mul_inv_cancel, ← ha, ← hb, ← diagonal_one, Units.ext_iff] using mul_inv_cancel g

Premises used: Units.ext_iff, Matrix.diagonal_one, mul_inv_cancel
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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

Tactic:
⟨⟨a, b, hab, mul_comm a b ▸ hab⟩, ?_⟩

Premises used: Set.Mem, setOf, Eq.rec, Units.mk, Exists.intro, mul_comm, Set.range
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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
h : (scalar n : (a : Rˣ) → GL n R) { val := a, inv := b, val_inv := hab, inv_val := ⋯ } = g
⊢ Membership.mem (γ := Subgroup (GL n R)) (MonoidHom.range (scalar n)) g

Tactic:
refine ⟨⟨a, b, hab, mul_comm a b ▸ hab⟩, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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
⊢ (scalar n : (a : Rˣ) → GL n R) { val := a, inv := b, val_inv := hab, inv_val := ⋯ } = g

Tactic:
simp [Units.ext_iff, ← ha]

Premises used: Units.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
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
⊢ 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]

Premises used: Units.ext_iff, Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, isEmpty_or_nonempty, Subgroup.inv_mem, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
a : Rˣ
⊢ Membership.mem (α := GL n R) (γ := Subgroup (GL n R)) (Subgroup.center (GL n R))
    ((scalar n : (a : Rˣ) → GL n R) a : GL n R)

Tactic:
mem_center_iff_val_mem_range_scalar.mpr ⟨a, rfl⟩

Premises used: Iff.mpr, Units.val, Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
Goal:
R : Type u_1
n : Type u_2
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing R
a : Rˣ
⊢ Membership.mem (α := GL n R) (γ := Subgroup (GL n R)) (Subgroup.center (GL n R))
    ((scalar n : (a : Rˣ) → GL n R) a : GL n R)

Tactic:
exact mem_center_iff_val_mem_range_scalar.mpr ⟨a, rfl⟩

Premises used: Iff.mpr, Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, Exists.intro
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
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
rw : card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))
⊢ Nat.card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))

Tactic:
rw [Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
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
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 : ℕ))
⊢ 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 ..⟩
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
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 : ℕ))
zero₄ : card.{u_2} { s : Fin 0 → V // Eq.{max 1 (u_1 + 1)} (α := Submodule K (Fin 0 →₀ K)) ⊤ ⊥ } = 1
⊢ card.{u_2} { s : Fin 0 → V // LinearIndependent 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]

Premises used: Finset.prod_empty, linearIndependent_iff_ker, Finset.univ_eq_empty, LinearMap.ker_zero, Fintype.card_unique, Finsupp.linearCombination_fin_zero
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
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 }
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
⊢ card.{u_2} (↑(↑(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)))]

Premises used: Module.card_eq_pow_finrank, Fintype.card_compl_set
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
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 }
simp : card V - q ^ k = q ^ n - q ^ k
⊢ 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:
simp only [SetLike.coe_sort_coe, finrank_span_eq_card s.2, card_fin]

Premises used: Fintype.card_fin, SetLike.coe_sort_coe, finrank_span_eq_card, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
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 }
rw rw₁ : q ^ n - q ^ k = q ^ n - q ^ k
⊢ card V - q ^ k = q ^ n - q ^ k

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

Premises used: Module.card_eq_pow_finrank
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
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

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)]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
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
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
⊢ card.{u_2} { s : Fin (k + 1) → V // 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 _ (Fin.last k), -Set.fintypeCard_eq_ncard]

Premises used: Fintype.card_congr, Nat.le_of_succ_le, Fin.prod_univ_succAbove, equiv_linearIndependent, Fintype.sum_congr, Fin.last, mul_comm, Set.fintypeCard_eq_ncard
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
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
zero : ∀ (hk : 0 ≤ n), card.{u_2} { s : Fin 0 → V // LinearIndependent K s } = ∏ i : Fin 0, (q ^ n - q ^ (↑i : ℕ))
succ :
  ∀ (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 : ℕ))
⊢ card.{u_2} { s : Fin k → V // LinearIndependent K s } = ∏ i : Fin k, (q ^ n - q ^ (↑i : ℕ))

Tactic:
induction k with
  | zero =>
      have : Unique { s : Fin 0 → V // (⊤ : Submodule K (Fin 0 →₀ K)) = ⊥ } :=
        uniqueOfSubsingleton ⟨0, Subsingleton.elim ..⟩
      simp_rw [linearIndependent_iff_ker, Finsupp.linearCombination_fin_zero, ker_zero,
        Finset.univ_eq_empty, Finset.prod_empty, card_unique]
  | 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, 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)]
      simp [card_congr (equiv_linearIndependent k), sum_congr _ _ this, ih (Nat.le_of_succ_le hk),
        mul_comm, Fin.prod_univ_succAbove _ (Fin.last k), -Set.fintypeCard_eq_ncard]

Premises used: Fintype.card_congr, Finset.prod_empty, linearIndependent_iff_ker, Fin.prod_univ_succAbove, equiv_linearIndependent, Finset.univ_eq_empty, LinearMap.ker_zero, Fin.last, Fintype.card_unique, Finsupp.linearCombination_fin_zero, mul_comm, Set.fintypeCard_eq_ncard
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
apply : Fintype.card (Fin n) = Set.finrank 𝔽 (Set.range (↑M : Matrix (Fin n) (Fin n) 𝔽).col)
⊢ LinearIndependent 𝔽 (↑M : Matrix (Fin n) (Fin n) 𝔽).col

Tactic:
apply linearIndependent_iff_card_eq_finrank_span.2

Premises used: Iff.mpr, linearIndependent_iff_card_eq_finrank_span
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : GL (Fin n) 𝔽
rw : Fintype.card (Fin n) = finrank 𝔽 ↥(Submodule.span 𝔽 (Set.range (↑M : Matrix (Fin n) (Fin n) 𝔽).col))
rw₁ : Fintype.card (Fin n) = (↑M : Matrix (Fin n) (Fin n) 𝔽).rank
rw₂ rw₃ : Fintype.card (Fin n) = Fintype.card (Fin n)
⊢ Fintype.card (Fin n) = Set.finrank 𝔽 (Set.range (↑M : Matrix (Fin n) (Fin n) 𝔽).col)

Tactic:
rw [Set.finrank, ← rank_eq_finrank_span_cols, rank_unit]

Premises used: Set.finrank, Matrix.rank_unit, Matrix.rank_eq_finrank_span_cols
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
Goal:
𝔽 : Type u_1
inst : Field 𝔽
inst_1 : Fintype 𝔽
n : ℕ
M : { s : Fin n → Fin n → 𝔽 // LinearIndependent 𝔽 s }
b : Basis (Fin n) 𝔽 (Fin n → 𝔽) := basisOfPiSpaceOfLinearIndependent ⋯
have :
  ∀
    (this :
      Invertible (α := Matrix (Fin n) (Fin n) 𝔽)
        (Basis.toMatrix (Pi.basisFun 𝔽 (Fin n)) (⇑b : (a : Fin n) → Fin n → 𝔽))),
    IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det
⊢ IsUnit (↑M : Fin n → Fin n → 𝔽)ᵀ.det

Tactic:
have := (Pi.basisFun 𝔽 (Fin n)).invertibleToMatrix b