awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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
⊢ 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)
have 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
Tactic: rw [← sub_scalar_sq_eq_discr, hm, trace_add, scalar_apply, trace_diagonal]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
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
⊢ False
have hm₁ : 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
Cleared hypotheses: hm, hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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
have refine : 0 ≤ HPow.hPow (β := ℕ) (m 0 0 + m 1 1) 2 - 4 * (m 0 0 * m 1 1 - 0)
Tactic: refine hm.not_ge ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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)
have 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
Tactic: refine (injective_iff_map_eq_zero (upperRightHom (R := R)).toAddMonoidHom).mpr ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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)
⊢ 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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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)
have 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)
Tactic: refine fun hP ↦ ⟨g 0 0, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
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
⊢ (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)
have hb : (↑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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
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
⊢ (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)
have hc : (↑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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (hypothesis)
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
⊢ (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)
have hd : (↑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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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) =
    (↑g : Matrix (Fin 2) (Fin 2) R)
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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
⊢ (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
have 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, sorry⟩) j =
  (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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
⊢ (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
have 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, sorry⟩) j =
  (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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
⊢ (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
have 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, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) =
  (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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))
⊢ (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
have 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, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) =
  (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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
⊢ (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
have 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, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) =
  (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
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))
⊢ (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
have 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, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) =
  (↑g : Matrix (Fin 2) (Fin 2) R) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))
Tactic: fin_cases j
Cleared hypotheses: j
-- 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 : NeZero.{u_2} (R := K) 2
hg : g.IsParabolic
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).parabolicEigenvalue ≠ 0
have this : 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
-- 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 : 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
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).parabolicEigenvalue ≠ 0
have rw : ¬Eq.{u_2 + 1} (α := K) 2 0 ∧ ¬(↑g : Matrix (Fin 2) (Fin 2) K).det = 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo (goal)
Goal:
K : Type u_2
inst : Field K
g : GL (Fin 2) K
hg : g.IsParabolic
inst_1 : CharZero K
n : ℕ
hn : n ≠ 0
⊢ (g ^ n).IsParabolic
have 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
Tactic: rw [IsParabolic, isParabolic_iff_exists] at hg ⊢
Cleared hypotheses: hg, inst_1, n, 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
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
⊢ ∃ (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 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
Tactic: obtain ⟨a, m, hg, hm0, hmsq⟩ := hg
Cleared hypotheses: 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
⊢ ∃ (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_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)
Tactic: refine ⟨a ^ n, (n * a ^ (n - 1)) • m, ?_, ?_, by simp [smul_pow, hmsq]⟩