awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ m 0 1 ≠ 0

Tactic:
left_ne_zero_of_mul hm.bc_ne_zero

Premises used: left_ne_zero_of_mul, Matrix.IsElliptic.bc_ne_zero
-- 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
⊢ m 1 0 ≠ 0

Tactic:
right_ne_zero_of_mul hm.bc_ne_zero

Premises used: right_ne_zero_of_mul, Matrix.IsElliptic.bc_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : Ring R
x : R
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) R) (β := Matrix (Fin 2) (Fin 2) R) (!![1, x; 0, 1] : Matrix (Fin 2) (Fin 2) R)
      (!![1, -x; 0, 1] : Matrix (Fin 2) (Fin 2) R) =
    1

Tactic:
simp [one_fin_two]

Premises used: Matrix.one_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : Ring R
x : R
⊢ HMul.hMul (α := Matrix (Fin 2) (Fin 2) R) (β := Matrix (Fin 2) (Fin 2) R) (!![1, -x; 0, 1] : Matrix (Fin 2) (Fin 2) R)
      (!![1, x; 0, 1] : Matrix (Fin 2) (Fin 2) R) =
    1

Tactic:
simp [one_fin_two]

Premises used: Matrix.one_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : Ring R
⊢ Eq.{u_1 + 1} (α := GL (Fin 2) R)
    ({ val := !![1, 0; 0, 1], inv := !![1, -0; 0, 1], val_inv := ⋯, inv_val := ⋯ } : (Matrix (Fin 2) (Fin 2) R)ˣ)
    (1 : GL (Fin 2) R)

Tactic:
simp [Units.ext_iff, one_fin_two]

Premises used: Units.ext_iff, Matrix.one_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : Ring R
a b : R
⊢ { val := !![1, a + b; 0, 1], inv := !![1, -(a + b); 0, 1], val_inv := ⋯, inv_val := ⋯ } =
    HMul.hMul (α := GL (Fin 2) R) (β := GL (Fin 2) R)
      ({ val := !![1, a; 0, 1], inv := !![1, -a; 0, 1], val_inv := ⋯, inv_val := ⋯ } : (Matrix (Fin 2) (Fin 2) R)ˣ)
      ({ val := !![1, b; 0, 1], inv := !![1, -b; 0, 1], val_inv := ⋯, inv_val := ⋯ } : (Matrix (Fin 2) (Fin 2) R)ˣ)

Tactic:
simp [Units.ext_iff, add_comm]

Premises used: Units.ext_iff, add_comm
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : Ring R
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R) (β := GL (Fin 2) R) (⇑upperRightHom : (a : R) → GL (Fin 2) R)

Tactic:
(injective_iff_map_eq_zero (upperRightHom (R := R)).toAddMonoidHom).mpr ?_

Premises used: Iff.mpr, AddChar.toAddMonoidHom, Additive, injective_iff_map_eq_zero, Matrix.GeneralLinearGroup.upperRightHom
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : Ring R
refine :
  ∀ (a : R),
    Eq (α := Additive (GL (Fin 2) R))
        ((AddChar.toAddMonoidHom upperRightHom : (a : R) → Additive (GL (Fin 2) R)) a : Additive (GL (Fin 2) R))
        (0 : Additive (GL (Fin 2) R)) →
      a = 0
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := R) (β := GL (Fin 2) R) (⇑upperRightHom : (a : R) → GL (Fin 2) R)

Tactic:
refine (injective_iff_map_eq_zero (upperRightHom (R := R)).toAddMonoidHom).mpr ?_

Premises used: Iff.mpr, AddChar.toAddMonoidHom, injective_iff_map_eq_zero, Matrix.GeneralLinearGroup.upperRightHom
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : Ring R
⊢ ∀ (a : R),
    Eq (α := Additive (GL (Fin 2) R))
        ((AddChar.toAddMonoidHom upperRightHom : (a : R) → Additive (GL (Fin 2) R)) a : Additive (GL (Fin 2) R))
        (0 : Additive (GL (Fin 2) R)) →
      a = 0

Tactic:
simp [Units.ext_iff, one_fin_two]

Premises used: Units.ext_iff, Matrix.one_fin_two
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g h : GL (Fin 2) R
⊢ (g * h * g⁻¹).IsParabolic ↔ h.IsParabolic

Tactic:
simp [IsParabolic]

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

Tactic:
simp [IsParabolic]

Premises used: Matrix.GeneralLinearGroup.IsParabolic
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
mp :
  HSub.hSub (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X])
            ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
        ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
      0 →
    Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) R))
      (Set.range (ι := R) (⇑(Matrix.scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R))
      (↑g : Matrix (Fin 2) (Fin 2) R)
mpr :
  Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) R))
      (Set.range (ι := R) (⇑(Matrix.scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R))
      (↑g : Matrix (Fin 2) (Fin 2) R) →
    HSub.hSub (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X])
            ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
        ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
      0
⊢ HSub.hSub (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X])
            ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
        ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
      0 ↔
    Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) R))
      (Set.range (ι := R) (⇑(Matrix.scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R))
      (↑g : Matrix (Fin 2) (Fin 2) R)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
⊢ HSub.hSub (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X])
            ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
        ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
      0 →
    Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) R))
      (Set.range (ι := R) (⇑(Matrix.scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R))
      (↑g : Matrix (Fin 2) (Fin 2) R)

Tactic:
fun hP ↦ ⟨g 0 0, ?_⟩

Premises used: Units.val, Set.Mem, setOf, Exists.intro, Set.range, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
mp :
  ∀
    (hP :
      HSub.hSub (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) (β := R[X])
              ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X])
              X)
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
        0),
    (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0) =
      (↑g : Matrix (Fin 2) (Fin 2) R)
⊢ HSub.hSub (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
            (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) (β := R[X])
            ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
        ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
      0 →
    Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) R))
      (Set.range (ι := R) (⇑(Matrix.scalar (Fin 2)) : (a : R) → Matrix (Fin 2) (Fin 2) R))
      (↑g : Matrix (Fin 2) (Fin 2) R)

Tactic:
refine fun hP ↦ ⟨g 0 0, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
⊢ (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0

Tactic:
simpa using congr_arg (coeff · 0) hP

Premises used: Polynomial.coeff, congr_arg, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
⊢ (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0

Tactic:
have hb : g 0 1 = 0 := by simpa using congr_arg (coeff · 0) hP
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0

Tactic:
simpa using congr_arg (coeff · 2) hP

Premises used: Polynomial.coeff, congr_arg, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0

Tactic:
have hc : g 1 0 = 0 := by simpa using congr_arg (coeff · 2) hP
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) R) 0 0

Tactic:
simpa [sub_eq_zero] using congr_arg (coeff · 1) hP

Premises used: sub_eq_zero, Polynomial.coeff, congr_arg, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) R) 0 0

Tactic:
have hd : g 1 1 = g 0 0 := by simpa [sub_eq_zero] using congr_arg (coeff · 1) hP
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) R) 0 0
mp :
  ∀ (i j : Fin 2),
    (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0) i j =
      (↑g : Matrix (Fin 2) (Fin 2) R) i j
⊢ (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0) =
    (↑g : Matrix (Fin 2) (Fin 2) R)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) R) 0 0
i j : Fin 2
mp :
  (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j
mp₁ :
  (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j
⊢ (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0) i j =
    (↑g : Matrix (Fin 2) (Fin 2) R) i j

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) R) 0 0
j : Fin 2
mp :
  (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))
mp₁ :
  (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
⊢ (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) R) 0 0
j : Fin 2
mp :
  (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))
mp₁ :
  (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
⊢ (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) R) 0 0
⊢ (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))

Tactic:
simp [hb, hc, hd]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) R) 0 0
⊢ (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))

Tactic:
simp [hb, hc, hd]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) R) 0 0
⊢ (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))

Tactic:
simp [hb, hc, hd]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
hP :
  HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0
hb : (↑g : Matrix (Fin 2) (Fin 2) R) 0 1 = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) R) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) R) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) R) 0 0
⊢ (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) =
    (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))

Tactic:
simp [hb, hc, hd]
-- Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Goal:
R : Type u_1
inst : CommRing R
g : GL (Fin 2) R
a : R
ha : (Matrix.scalar (Fin 2) : (a : R) → Matrix (Fin 2) (Fin 2) R) a = (↑g : Matrix (Fin 2) (Fin 2) R)
⊢ HSub.hSub (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) : R[X])
          (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HMul.hMul (α := R[X]) (β := R[X])
          ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) R) 0 0) : R[X]) X)
      ((C : (a : R) → R[X]) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1) : R[X]) =
    0

Tactic:
simp [← ha]
-- 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
⊢ HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K).trace 2 = 4 * (↑g : Matrix (Fin 2) (Fin 2) K).det

Tactic:
simpa [sub_eq_zero, discr_fin_two] using hg.2

Premises used: sub_eq_zero, And.right, Matrix.discr_fin_two
-- 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
⊢ HPow.hPow (β := ℕ) (↑g : Matrix (Fin 2) (Fin 2) K).trace 2 = 4 * (↑g : Matrix (Fin 2) (Fin 2) K).det

Tactic:
have : g.val.trace ^ 2 = 4 * g.val.det := by simpa [sub_eq_zero, discr_fin_two] using hg.2
-- 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
⊢ 4 = HPow.hPow (α := K) (β := ℕ) 2 2

Tactic:
norm_num