awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
refine_1 :
  (↑(g ^ n) : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
      (((↑n : K) * a ^ (n - 1)) • m)
⊢ ∃ (a : K) (n_1 : Matrix (Fin 2) (Fin 2) K),
    (↑(g ^ n) : Matrix (Fin 2) (Fin 2) K) =
        HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
          ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n_1 ∧
      n_1 ≠ 0 ∧ HPow.hPow (β := ℕ) n_1 2 = 0
have refine_2 : ((↑n : K) * a ^ (n - 1)) • m ≠ 0
Tactic: refine ⟨a ^ n, (n * a ^ (n - 1)) • m, ?_, ?_, by simp [smul_pow, hmsq]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
⊢ (↑(g ^ n) : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
      (((↑n : K) * a ^ (n - 1)) • m)
have refine_1 : HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
    n =
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
    ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
    (((↑n : K) * a ^ (n - 1)) • m)
Tactic: rw [Units.val_pow_eq_pow_val, hg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
⊢ HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
      n =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
      (((↑n : K) * a ^ (n - 1)) • m)
have refine_1 : ∀ (hn : 1 ≤ n) (a : K) (m : Matrix (Fin 2) (Fin 2) K)
  (hg :
    (↑g : Matrix (Fin 2) (Fin 2) K) =
      HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m)
  (hm0 : m ≠ 0) (hmsq : HPow.hPow (β := ℕ) m 2 = 0),
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
      n =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
      (((↑n : K) * a ^ (n - 1)) • m)
Tactic: rw [← Nat.one_le_iff_ne_zero] at hn
Cleared hypotheses: hn, a, m, hg, hm0, hmsq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n_1 : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
n : ℕ
hn : 1 ≤ n
IH :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
      n =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
      (((↑n : K) * a ^ (n - 1)) • m)
⊢ HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
      (n + 1) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ (n + 1)) : Matrix (Fin 2) (Fin 2) K)
      (((↑(n + 1) : K) * a ^ (n + 1 - 1)) • m)
have refine_1 : HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
    ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n * a) : Matrix (Fin 2) (Fin 2) K)
    (HMul.hMul (β := Matrix (Fin 2) (Fin 2) K) (((↑n : K) * a ^ (n - 1)) • m)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) +
      (HMul.hMul (α := Matrix (Fin 2) (Fin 2) K)
          ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K) m +
        ((↑n : K) * a ^ (n - 1)) • m * m)) =
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
    ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n * a) : Matrix (Fin 2) (Fin 2) K)
    (((↑(n + 1) : K) * a ^ n) • m)
Tactic: simp only [pow_succ, IH, add_mul, Nat.add_sub_cancel, mul_add, ← map_mul, add_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n_1 : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
n : ℕ
hn : 1 ≤ n
IH :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
      n =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
      (((↑n : K) * a ^ (n - 1)) • m)
⊢ HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n * a) : Matrix (Fin 2) (Fin 2) K)
      (HMul.hMul (β := Matrix (Fin 2) (Fin 2) K) (((↑n : K) * a ^ (n - 1)) • m)
          ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) +
        (HMul.hMul (α := Matrix (Fin 2) (Fin 2) K)
            ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K) m +
          ((↑n : K) * a ^ (n - 1)) • m * m)) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n * a) : Matrix (Fin 2) (Fin 2) K)
      (((↑(n + 1) : K) * a ^ n) • m)
have refine_1 : (diagonal fun (x : Fin 2) ↦ a ^ n * a) + (a * ((↑n : K) * a ^ (n - 1)) + a ^ n) • m =
  (diagonal fun (x : Fin 2) ↦ a ^ n * a) + ((↑n : K) * a ^ n + a ^ n) • m
Tactic: simp only [scalar_apply, ← smul_eq_mul_diagonal, ← mul_smul,
        ← smul_eq_diagonal_mul, smul_mul, ← sq, hmsq, smul_zero, add_zero, ← add_smul,
        Nat.cast_add_one, add_mul, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n_1 : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
n : ℕ
hn : 1 ≤ n
IH :
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
      n =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
      (((↑n : K) * a ^ (n - 1)) • m)
⊢ (diagonal fun (x : Fin 2) ↦ a ^ n * a) + (a * ((↑n : K) * a ^ (n - 1)) + a ^ n) • m =
    (diagonal fun (x : Fin 2) ↦ a ^ n * a) + ((↑n : K) * a ^ n + a ^ n) • m
have refine_1 : (diagonal fun (x : Fin 2) ↦ a ^ (n - 1) * a * a) + (a * ((↑n : K) * a ^ (n - 1)) + a ^ (n - 1) * a) • m =
  (diagonal fun (x : Fin 2) ↦ a ^ (n - 1) * a * a) + ((↑n : K) * (a ^ (n - 1) * a) + a ^ (n - 1) * a) • m
Tactic: rw [(by lia : n = n - 1 + 1), pow_succ, (by lia : n - 1 + 1 = n)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : 1 ≤ n
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
⊢ HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
      n =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
      (((↑n : K) * a ^ (n - 1)) • m)
have refine_1 : HPow.hPow (β := ℕ)
    (HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m)
    1 =
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
    ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (HPow.hPow (β := ℕ) a 1) : Matrix (Fin 2) (Fin 2) K)
    (((↑1 : K) * a ^ HSub.hSub (α := ℕ) 1 1) • m)
Tactic: induction n, hn using Nat.le_induction with
    | base => simp
    | succ n hn IH =>
      simp only [pow_succ, IH, add_mul, Nat.add_sub_cancel, mul_add, ← map_mul, add_assoc]
      simp only [scalar_apply, ← smul_eq_mul_diagonal, ← mul_smul,
        ← smul_eq_diagonal_mul, smul_mul, ← sq, hmsq, smul_zero, add_zero, ← add_smul,
        Nat.cast_add_one, add_mul, one_mul]
      rw [(by lia : n = n - 1 + 1), pow_succ, (by lia : n - 1 + 1 = n)]
      ring_nf
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : 1 ≤ n
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
refine_1 :
  HPow.hPow (β := ℕ)
      (HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m)
      1 =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (HPow.hPow (β := ℕ) a 1) : Matrix (Fin 2) (Fin 2) K)
      (((↑1 : K) * a ^ HSub.hSub (α := ℕ) 1 1) • m)
⊢ HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
      n =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
      (((↑n : K) * a ^ (n - 1)) • m)
have refine_1₁ : ∀ (n : ℕ) (hn : 1 ≤ n)
  (IH :
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
          ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
        n =
      HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ n) : Matrix (Fin 2) (Fin 2) K)
        (((↑n : K) * a ^ (n - 1)) • m)),
  HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
        ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m ^
      (n + 1) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (a ^ (n + 1)) : Matrix (Fin 2) (Fin 2) K)
      (((↑(n + 1) : K) * a ^ (n + 1 - 1)) • m)
Tactic: induction n, hn using Nat.le_induction with
    | base => simp
    | succ n hn IH =>
      simp only [pow_succ, IH, add_mul, Nat.add_sub_cancel, mul_add, ← map_mul, add_assoc]
      simp only [scalar_apply, ← smul_eq_mul_diagonal, ← mul_smul,
        ← smul_eq_diagonal_mul, smul_mul, ← sq, hmsq, smul_zero, add_zero, ← add_smul,
        Nat.cast_add_one, add_mul, one_mul]
      rw [(by lia : n = n - 1 + 1), pow_succ, (by lia : n - 1 + 1 = n)]
      ring_nf
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
⊢ ((↑n : K) * a ^ (n - 1)) • m ≠ 0
have refine_2 : a ≠ 0
Tactic: suffices a ≠ 0 by simp [this, hm0, hn]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
⊢ a ≠ 0
have refine_2 : ∀ (ha : a = 0), (↑(HPow.hPow (β := ℕ) g 2) : Matrix (Fin 2) (Fin 2) K).det = 0
Tactic: refine fun ha ↦ (g ^ 2).det_ne_zero ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((Matrix.scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
ha : a = 0
⊢ (↑(HPow.hPow (β := ℕ) g 2) : Matrix (Fin 2) (Fin 2) K).det = 0
have hg₁ : (↑g : Matrix (Fin 2) (Fin 2) K) = m
Tactic: rw [ha, map_zero, zero_add] at hg
Cleared hypotheses: hg, hm0, hmsq, ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : (↑g : Matrix (Fin 2) (Fin 2) K) = m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) m 2 = 0
ha : a = 0
⊢ (↑(HPow.hPow (β := ℕ) g 2) : Matrix (Fin 2) (Fin 2) K).det = 0
have hmsq₁ : HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2 = 0
Tactic: rw [← hg] at hmsq
Cleared hypotheses: hmsq, ha
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : (↑g : Matrix (Fin 2) (Fin 2) K) = m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2 = 0
ha : a = 0
⊢ (↑(HPow.hPow (β := ℕ) g 2) : Matrix (Fin 2) (Fin 2) K).det = 0
have refine_2 : (HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2).det = 0
Tactic: rw [Units.val_pow_eq_pow_val, hmsq, det_zero ⟨0⟩]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : (↑g : Matrix (Fin 2) (Fin 2) K) = m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2 = 0
ha : a = 0
refine_2 : (HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2).det = 0
⊢ (↑(HPow.hPow (β := ℕ) g 2) : Matrix (Fin 2) (Fin 2) K).det = 0
have refine_2₁ : Eq.{u_2 + 1} (α := K) (Matrix.det (n := Fin 2) 0) 0
Tactic: rw [Units.val_pow_eq_pow_val, hmsq, det_zero ⟨0⟩]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : (↑g : Matrix (Fin 2) (Fin 2) K) = m
hm0 : m ≠ 0
hmsq : HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2 = 0
ha : a = 0
refine_2 : (HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K) 2).det = 0
refine_2₁ : Eq.{u_2 + 1} (α := K) (Matrix.det (n := Fin 2) 0) 0
⊢ (↑(HPow.hPow (β := ℕ) g 2) : Matrix (Fin 2) (Fin 2) K).det = 0
have refine_2₂ : Eq.{u_2 + 1} (α := K) 0 0
Tactic: rw [Units.val_pow_eq_pow_val, hmsq, det_zero ⟨0⟩]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ g.IsParabolic ↔
    (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
      ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
have rw : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0 ↔
  (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
    ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
Tactic: rw [isParabolic_iff_of_upperTriangular hg10]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0 ↔
    (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
      ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
have mp : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0 →
  (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
    ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
mp :
  (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0 →
    (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
      ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0 ↔
    (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
      ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
have mpr : ((∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
    ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x) →
  (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 ∧ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
⊢ (↑((det : (a : GL (Fin 2) K) → Kˣ) g) : K) = HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
have rw : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * 0 =
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
Tactic: rw [val_det_apply, det_fin_two, hg10, hg00]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
have this : (↑((det : (a : GL (Fin 2) K) → Kˣ) g) : K) = HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
Tactic: have : g.det = g 1 1 ^ 2 := by rw [val_det_apply, det_fin_two, hg10, hg00]; ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
this : (↑((det : (a : GL (Fin 2) K) → Kˣ) g) : K) = HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
have h_det₁ : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1 ∨
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = -1
Tactic: simp only [Units.ext_iff, Units.val_one, Units.val_neg, this] at h_det
Cleared hypotheses: h_det
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
Goal:
K : Type u_2
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det :
  Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (1 : Kˣ) ∨
    Eq (α := Kˣ) ((det : (a : GL (Fin 2) K) → Kˣ) g : Kˣ) (-1 : Kˣ)
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hg00 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) K) 1 1
hg01 : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
⊢ (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
    ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x
have this : HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 = 1
Tactic: have : g 1 1 ^ 2 = 1 := by
      have : g.det = g 1 1 ^ 2 := by rw [val_det_apply, det_fin_two, hg10, hg00]; ring
      simp only [Units.ext_iff, Units.val_one, Units.val_neg, this] at h_det
      exact h_det.resolve_right (neg_one_lt_zero.trans_le <| sq_nonneg _).ne'