awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
j : Fin 2
a :
  ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₁ :
  ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
j : Fin 2
a :
  ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₁ :
  ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a :
  (m 0 0 - (m 0 0 + m 1 1) / 2) * (m 0 0 - (m 0 0 + m 1 1) / 2) + m 0 1 * m 1 0 =
    ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
      HMul.hMul (α := K) 2 2
⊢ ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
⊢ (m 0 0 - (m 0 0 + m 1 1) / 2) * (m 0 0 - (m 0 0 + m 1 1) / 2) + m 0 1 * m 1 0 =
    ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
      HMul.hMul (α := K) 2 2

Tactic:
field
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : (m 0 0 - (m 0 0 + m 1 1) / 2) * m 0 1 + m 0 1 * (m 1 1 - (m 0 0 + m 1 1) / 2) = 0
⊢ ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
⊢ (m 0 0 - (m 0 0 + m 1 1) / 2) * m 0 1 + m 0 1 * (m 1 1 - (m 0 0 + m 1 1) / 2) = 0

Tactic:
field
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : m 1 0 * (m 0 0 - (m 0 0 + m 1 1) / 2) + (m 1 1 - (m 0 0 + m 1 1) / 2) * m 1 0 = 0
⊢ ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
⊢ m 1 0 * (m 0 0 - (m 0 0 + m 1 1) / 2) + (m 1 1 - (m 0 0 + m 1 1) / 2) * m 1 0 = 0

Tactic:
field
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a :
  m 1 0 * m 0 1 + (m 1 1 - (m 0 0 + m 1 1) / 2) * (m 1 1 - (m 0 0 + m 1 1) / 2) =
    ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
      HMul.hMul (α := K) 2 2
⊢ ((m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun (x : Fin 2) ↦ (m 0 0 + m 1 1) / 2))
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    diagonal
      (fun (x : Fin 2) ↦
        ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
          HMul.hMul (α := K) 2 2)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [Matrix.mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
⊢ m 1 0 * m 0 1 + (m 1 1 - (m 0 0 + m 1 1) / 2) * (m 1 1 - (m 0 0 + m 1 1) / 2) =
    ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - HMul.hMul (α := K) 2 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) /
      HMul.hMul (α := K) 2 2

Tactic:
field
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
hm : m.IsParabolic
⊢ HPow.hPow (β := ℕ)
      (HSub.hSub (β := Matrix (Fin 2) (Fin 2) K) m
        ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) m.parabolicEigenvalue : Matrix (Fin 2) (Fin 2) K))
      2 =
    0

Tactic:
simp [parabolicEigenvalue, -scalar_apply, sub_scalar_sq_eq_discr, hm.2]

Premises used: And.right, Matrix.parabolicEigenvalue, Matrix.scalar_apply, Matrix.sub_scalar_sq_eq_discr
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
mp :
  m.IsParabolic →
    ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
      m =
          HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
            ((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
mpr :
  (∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
      m =
          HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
            ((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) →
    m.IsParabolic
⊢ m.IsParabolic ↔
    ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
      m =
          HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
            ((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

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
⊢ m.IsParabolic →
    ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
      m =
          HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
            ((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

Tactic:
fun hm ↦ ⟨_, _, (add_sub_cancel ..).symm, sub_ne_zero.mpr fun h ↦ hm.1 ⟨_, h.symm⟩,
      hm.sub_eigenvalue_sq_eq_zero⟩

Premises used: Iff.mpr, Matrix.scalar, sub_ne_zero, Matrix.IsParabolic.sub_eigenvalue_sq_eq_zero, HSub.hSub, add_sub_cancel, And.left, And.intro, Exists.intro, Matrix.parabolicEigenvalue, OfNat.ofNat, Eq.symm, Fin, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
⊢ m.IsParabolic →
    ∃ (a : K) (n : Matrix (Fin 2) (Fin 2) K),
      m =
          HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
            ((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

Tactic:
exact fun hm ↦ ⟨_, _, (add_sub_cancel ..).symm, sub_ne_zero.mpr fun h ↦ hm.1 ⟨_, h.symm⟩,
      hm.sub_eigenvalue_sq_eq_zero⟩
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
mpr : m ∉ Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
mpr₁ : m.discr = 0
⊢ m.IsParabolic

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
⊢ m ∉ Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)

Tactic:
fun ⟨b, hb⟩ ↦ hn0 ?_

Premises used: False, _private.0.Matrix.isParabolic_iff_exists.match_1, Not
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
mpr :
  Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) K))
      (Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)) m →
    ∀ (b : K) (hb : (scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) b = m), n = 0
⊢ m ∉ Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)

Tactic:
refine fun ⟨b, hb⟩ ↦ hn0 ?_
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
h :
  Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) K))
    (Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)) m
b : K
hb : (scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) b = m
mpr :
  ∀
    (hm :
      HSub.hSub (β := Matrix (Fin 2) (Fin 2) K) m
          ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) =
        n)
    (hn0 : n ≠ 0) (hnsq : HPow.hPow (β := ℕ) n 2 = 0),
    Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) K))
        (Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)) m →
      ∀ (b : K) (hb : (scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) b = m), n = 0
⊢ n = 0

Tactic:
rw [← sub_eq_iff_eq_add'] at hm

Premises used: sub_eq_iff_eq_add'
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  HSub.hSub (β := Matrix (Fin 2) (Fin 2) K) m
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) =
    n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
h :
  Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) K))
    (Set.range (ι := K) (⇑(scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)) m
b : K
hb : (scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) b = m
⊢ n = 0

Tactic:
simpa only [← hm, ← hb, ← map_sub, ← map_pow, ← map_zero (scalar (Fin 2)), scalar_inj,
        sq_eq_zero_iff] using hnsq

Premises used: Matrix.scalar_inj, Matrix.scalar, map_sub, map_zero, map_pow, OfNat.ofNat, Fin, sq_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
this :
  Eq (α := Matrix (Fin 2) (Fin 2) K)
    ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (m.discr / 4) : Matrix (Fin 2) (Fin 2) K)
    (0 : Matrix (Fin 2) (Fin 2) K)
⊢ m.discr = 0 ∨ Eq.{u_1 + 1} (α := K) 4 0

Tactic:
rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this

Premises used: Matrix.scalar_inj, Matrix.scalar, map_zero, OfNat.ofNat, Fin, div_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
this : m.discr = 0 ∨ Eq.{u_1 + 1} (α := K) 4 0
⊢ 4 = HPow.hPow (α := K) (β := ℕ) 2 2

Tactic:
norm_num
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
this : m.discr = 0 ∨ Eq.{u_1 + 1} (α := K) 4 0
⊢ Ne.{u_1 + 1} (α := K) 4 0

Tactic:
simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _

Premises used: NeZero.ne
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
this : m.discr = 0 ∨ Eq.{u_1 + 1} (α := K) 4 0
⊢ Ne.{u_1 + 1} (α := K) 4 0

Tactic:
have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
this_1 : m.discr = 0 ∨ Eq.{u_1 + 1} (α := K) 4 0
this : Ne.{u_1 + 1} (α := K) 4 0
inl : ∀ (this : m.discr = 0), m.discr = 0
inr : ∀ (this : Eq.{u_1 + 1} (α := K) 4 0), m.discr = 0
inl₁ inl₂ : ∀ (this : m.discr = 0), m.discr = 0
⊢ m.discr = 0

Tactic:
tauto
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
mpr :
  Eq (α := Matrix (Fin 2) (Fin 2) K)
    ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (m.discr / 4) : Matrix (Fin 2) (Fin 2) K)
    (0 : Matrix (Fin 2) (Fin 2) K)
⊢ m.discr = 0

Tactic:
suffices scalar (Fin 2) (m.discr / 4) = 0 by
        rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this
        have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
        tauto
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
mpr :
  HPow.hPow (β := ℕ)
      (HSub.hSub (β := Matrix (Fin 2) (Fin 2) K) ((diagonal fun (x : Fin 2) ↦ a) + n)
        ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) ((∑ i : Fin 2, a + n.trace) / 2) :
          Matrix (Fin 2) (Fin 2) K))
      2 =
    0
⊢ Eq (α := Matrix (Fin 2) (Fin 2) K)
    ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) (m.discr / 4) : Matrix (Fin 2) (Fin 2) K)
    (0 : Matrix (Fin 2) (Fin 2) K)

Tactic:
rw [← sub_scalar_sq_eq_discr, hm, trace_add, scalar_apply, trace_diagonal]

Premises used: Matrix.trace_diagonal, Matrix.trace_add, Matrix.scalar_apply, Matrix.sub_scalar_sq_eq_discr
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
K : Type u_1
inst : Field K
m : Matrix (Fin 2) (Fin 2) K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm :
  m =
    HAdd.hAdd (α := Matrix (Fin 2) (Fin 2) K)
      ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) a : Matrix (Fin 2) (Fin 2) K) n
hn0 : n ≠ 0
hnsq : HPow.hPow (β := ℕ) n 2 = 0
⊢ HPow.hPow (β := ℕ)
      (HSub.hSub (β := Matrix (Fin 2) (Fin 2) K) ((diagonal fun (x : Fin 2) ↦ a) + n)
        ((scalar (Fin 2) : (a : K) → Matrix (Fin 2) (Fin 2) K) ((∑ i : Fin 2, a + n.trace) / 2) :
          Matrix (Fin 2) (Fin 2) K))
      2 =
    0

Tactic:
simp [mul_div_cancel_left₀ _ (NeZero.ne (2 : K)),
        (Matrix.isNilpotent_trace_of_isNilpotent ⟨2, hnsq⟩).eq_zero, hnsq]

Premises used: mul_div_cancel_left₀, Exists.intro, Matrix.isNilpotent_trace_of_isNilpotent, IsNilpotent.eq_zero, OfNat.ofNat, NeZero.ne
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsHyperbolic ↔ m.IsHyperbolic

Tactic:
simp [IsHyperbolic]

Premises used: Matrix.IsHyperbolic
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ * m * (↑g : Matrix (Fin 2) (Fin 2) R)).IsHyperbolic ↔ m.IsHyperbolic

Tactic:
simpa using isHyperbolic_conj_iff g⁻¹

Premises used: Matrix.isHyperbolic_conj_iff, Inv.inv
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R) * m * (↑g : Matrix (Fin 2) (Fin 2) R)⁻¹).IsElliptic ↔ m.IsElliptic

Tactic:
simp [IsElliptic]

Premises used: Matrix.IsElliptic
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g : Matrix (Fin 2) (Fin 2) R)⁻¹ * m * (↑g : Matrix (Fin 2) (Fin 2) R)).IsElliptic ↔ m.IsElliptic

Tactic:
simpa using isElliptic_conj_iff g⁻¹

Premises used: Matrix.isElliptic_conj_iff, Inv.inv
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Preorder R
m : Matrix (Fin 2) (Fin 2) R
⊢ (-m).IsHyperbolic ↔ m.IsHyperbolic

Tactic:
simp [IsHyperbolic, discr_fin_two, det_neg]

Premises used: Matrix.det_neg, Matrix.IsHyperbolic, Matrix.discr_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Preorder R
m : Matrix (Fin 2) (Fin 2) R
⊢ (-m).IsElliptic ↔ m.IsElliptic

Tactic:
simp [IsElliptic, discr_fin_two, det_neg]

Premises used: Matrix.IsElliptic, Matrix.det_neg, Matrix.discr_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : m.IsElliptic
hc : m 0 1 * m 1 0 = 0
⊢ HPow.hPow (β := ℕ) (m 0 0 + m 1 1) 2 - 4 * (m 0 0 * m 1 1 - 0) < 0

Tactic:
rw [IsElliptic, discr_fin_two, trace_fin_two, det_fin_two, hc] at hm

Premises used: Matrix.IsElliptic, Matrix.trace_fin_two, Matrix.det_fin_two, Matrix.discr_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : m.IsElliptic
hc : m 0 1 * m 1 0 = 0
hm₁ : HPow.hPow (β := ℕ) (m 0 0 + m 1 1) 2 - 4 * (m 0 0 * m 1 1 - 0) < 0
⊢ m 0 1 * m 1 0 = 0

Tactic:
rw [IsElliptic, discr_fin_two, trace_fin_two, det_fin_two, hc] at hm

Premises used: Matrix.IsElliptic, Matrix.trace_fin_two, Matrix.det_fin_two, Matrix.discr_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : HPow.hPow (β := ℕ) (m 0 0 + m 1 1) 2 - 4 * (m 0 0 * m 1 1 - 0) < 0
hc : m 0 1 * m 1 0 = 0
⊢ False

Tactic:
hm.not_ge ?_

Premises used: LT.lt.not_ge
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : HPow.hPow (β := ℕ) (m 0 0 + m 1 1) 2 - 4 * (m 0 0 * m 1 1 - 0) < 0
hc : m 0 1 * m 1 0 = 0
refine : 0 ≤ HPow.hPow (β := ℕ) (m 0 0 + m 1 1) 2 - 4 * (m 0 0 * m 1 1 - 0)
⊢ False

Tactic:
refine hm.not_ge ?_

Premises used: LT.lt.not_ge
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : HPow.hPow (β := ℕ) (m 0 0 + m 1 1) 2 - 4 * (m 0 0 * m 1 1 - 0) < 0
hc : m 0 1 * m 1 0 = 0
⊢ 0 ≤ HPow.hPow (β := ℕ) (m 0 0 + m 1 1) 2 - 4 * (m 0 0 * m 1 1 - 0)

Tactic:
linear_combination sq_nonneg (m 0 0 - m 1 1)

Premises used: HSub.hSub, sq_nonneg, OfNat.ofNat