awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : NeZero.{u_2} (R := K) 2
hg : g.IsParabolic
this : HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K).trace 2 = 4 * (↑g : Matrix (Fin 2) (Fin 2) K).det
rw : ¬Eq.{u_2 + 1} (α := K) 2 0 ∧ ¬(↑g : Matrix (Fin 2) (Fin 2) K).det = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).parabolicEigenvalue ≠ 0

Tactic:
rw [parabolicEigenvalue, div_ne_zero_iff, eq_true_intro (two_ne_zero' K), and_true,
    Ne, ← sq_eq_zero_iff, this, show (4 : K) = 2 ^ 2 by norm_num, mul_eq_zero,
    sq_eq_zero_iff, not_or]

Premises used: and_true, eq_true_intro, div_ne_zero_iff, Ne, mul_eq_zero, not_or, two_ne_zero', Matrix.parabolicEigenvalue, sq_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : NeZero.{u_2} (R := K) 2
hg : g.IsParabolic
this : HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K).trace 2 = 4 * (↑g : Matrix (Fin 2) (Fin 2) K).det
⊢ ¬Eq.{u_2 + 1} (α := K) 2 0 ∧ ¬(↑g : Matrix (Fin 2) (Fin 2) K).det = 0

Tactic:
⟨NeZero.ne _, g.det_ne_zero⟩

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, And.intro, NeZero.ne
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : NeZero.{u_2} (R := K) 2
hg : g.IsParabolic
this : HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K).trace 2 = 4 * (↑g : Matrix (Fin 2) (Fin 2) K).det
⊢ ¬Eq.{u_2 + 1} (α := K) 2 0 ∧ ¬(↑g : Matrix (Fin 2) (Fin 2) K).det = 0

Tactic:
exact ⟨NeZero.ne _, g.det_ne_zero⟩
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
hg : g.IsParabolic
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
rw :
  ∀
    (hg :
      ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
        (↑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) n ∧
          n ≠ 0 ∧ HPow.hPow (β := ℕ) n 2 = 0)
    [CharZero K] {n : ℕ} (hn : n ≠ 0),
    ∃ (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
⊢ (g ^ n).IsParabolic

Tactic:
rw [IsParabolic, isParabolic_iff_exists] at hg ⊢

Premises used: Matrix.isParabolic_iff_exists, Matrix.GeneralLinearGroup.IsParabolic
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
hg :
  ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
    (↑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) n ∧
      n ≠ 0 ∧ HPow.hPow (β := ℕ) n 2 = 0
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
obtain :
  ∀ (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 : 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
⊢ ∃ (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

Tactic:
obtain ⟨a, m, hg, hm0, hmsq⟩ := hg
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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
⊢ HPow.hPow (β := ℕ) (((↑n : K) * a ^ (n - 1)) • m) 2 = 0

Tactic:
simp [smul_pow, hmsq]

Premises used: smul_pow
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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)
refine_2 : ((↑n : K) * a ^ (n - 1)) • m ≠ 0
⊢ ∃ (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

Tactic:
refine ⟨a ^ n, (n * a ^ (n - 1)) • m, ?_, ?_, by simp [smul_pow, hmsq]⟩
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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 :
  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)
⊢ (↑(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)

Tactic:
rw [Units.val_pow_eq_pow_val, hg]

Premises used: Units.val_pow_eq_pow_val
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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 :
  ∀ (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)
⊢ 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

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
inst_1 : CharZero K
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
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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)
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)
⊢ 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:
simp only [pow_succ, IH, add_mul, Nat.add_sub_cancel, mul_add, ← map_mul, add_assoc]

Premises used: add_mul, pow_succ, add_assoc, map_mul, Nat.add_sub_cancel, mul_add
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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)
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
⊢ 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 [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]

Premises used: add_mul, smul_zero, sq, Matrix.smul_eq_mul_diagonal, add_smul, Matrix.smul_mul, Matrix.scalar_apply, add_zero, Nat.cast_add_one, Matrix.smul_eq_diagonal_mul, SemigroupAction.mul_smul, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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)
⊢ n = n - 1 + 1

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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)
⊢ n - 1 + 1 = n

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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)
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
⊢ (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:
rw [(by lia : n = n - 1 + 1), pow_succ, (by lia : n - 1 + 1 = n)]

Premises used: pow_succ
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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 - 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:
ring_nf
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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)
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)
⊢ 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:
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

Premises used: add_mul, pow_succ, add_assoc, smul_zero, sq, Matrix.smul_eq_mul_diagonal, map_mul, add_smul, Matrix.smul_mul, Nat.add_sub_cancel, mul_add, Matrix.scalar_apply, add_zero, Nat.cast_add_one, Matrix.smul_eq_diagonal_mul, SemigroupAction.mul_smul, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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
this : a ≠ 0
⊢ ((↑n : K) * a ^ (n - 1)) • m ≠ 0

Tactic:
simp [this, hm0, hn]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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_2 : a ≠ 0
⊢ ((↑n : K) * a ^ (n - 1)) • m ≠ 0

Tactic:
suffices a ≠ 0 by simp [this, hm0, hn]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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

Tactic:
fun ha ↦ (g ^ 2).det_ne_zero ?_

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, HPow.hPow, OfNat.ofNat, Not
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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_2 : ∀ (ha : a = 0), (↑(HPow.hPow (β := ℕ) g 2) : Matrix (Fin 2) (Fin 2) K).det = 0
⊢ a ≠ 0

Tactic:
refine fun ha ↦ (g ^ 2).det_ne_zero ?_

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) = m

Tactic:
rw [ha, map_zero, zero_add] at hg

Premises used: map_zero, zero_add
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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
hg₁ : (↑g : Matrix (Fin 2) (Fin 2) K) = m
⊢ m ≠ 0

Tactic:
rw [ha, map_zero, zero_add] at hg

Premises used: map_zero, zero_add
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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
hg₁ : (↑g : Matrix (Fin 2) (Fin 2) K) = m
hm0₁ : m ≠ 0
⊢ HPow.hPow (β := ℕ) m 2 = 0

Tactic:
rw [ha, map_zero, zero_add] at hg

Premises used: map_zero, zero_add
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
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
hg₁ : (↑g : Matrix (Fin 2) (Fin 2) K) = m
hm0₁ : m ≠ 0
hmsq₁ : HPow.hPow (β := ℕ) m 2 = 0
⊢ a = 0

Tactic:
rw [ha, map_zero, zero_add] at hg

Premises used: map_zero, zero_add