awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
coe :
  (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * HPow.hPow (β := ℕ) c 2 +
          ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c -
        (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
      0 ↔
    (↑c : OnePoint K) = g.parabolicFixedPoint
⊢ g • (↑c : OnePoint K) = (↑c : OnePoint K) ↔ (↑c : OnePoint K) = g.parabolicFixedPoint

Tactic:
suffices g 1 0 * c ^ 2 + (g 1 1 - g 0 0) * c - g 0 1 = 0 ↔ c = g.parabolicFixedPoint by
      simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial]
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
pos :
  ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0),
    (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * HPow.hPow (β := ℕ) c 2 +
            ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
        0 ↔
      (↑c : OnePoint K) = g.parabolicFixedPoint
neg :
  ∀ (hc : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0),
    (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * HPow.hPow (β := ℕ) c 2 +
            ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
        0 ↔
      (↑c : OnePoint K) = g.parabolicFixedPoint
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * HPow.hPow (β := ℕ) c 2 +
          ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c -
        (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
      0 ↔
    (↑c : OnePoint K) = g.parabolicFixedPoint

Tactic:
by_cases hc : g 1 0 = 0

Premises used: Units.val, OfNat.ofNat
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) K) 0 0

Tactic:
grind
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) K) 0 0

Tactic:
have hd : g 1 1 = g 0 0 := by grind
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) K) 0 0
this : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * HPow.hPow (β := ℕ) c 2 +
          ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c -
        (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
      0 ↔
    (↑c : OnePoint K) = g.parabolicFixedPoint

Tactic:
simpa [parabolicFixedPoint, hc, hd]

Premises used: Matrix.GeneralLinearGroup.parabolicFixedPoint
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) K) 0 0
pos : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * HPow.hPow (β := ℕ) c 2 +
          ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c -
        (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
      0 ↔
    (↑c : OnePoint K) = g.parabolicFixedPoint

Tactic:
suffices g 0 1 ≠ 0 by simpa [parabolicFixedPoint, hc, hd]
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) K) 0 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0

Tactic:
fun hb ↦ fixpointPolynomial_eq_zero_iff.not.mpr hg ?_

Premises used: Iff.mpr, Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff, Iff.not, Not
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) K) 0 0
pos : ∀ (hb : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 = 0), g.fixpointPolynomial = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0

Tactic:
refine fun hb ↦ fixpointPolynomial_eq_zero_iff.not.mpr hg ?_

Premises used: Iff.mpr, Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff, Iff.not
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
hd : (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) K) 0 0
hb : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 = 0
⊢ g.fixpointPolynomial = 0

Tactic:
simp [fixpointPolynomial, hb, hc, hd]

Premises used: Matrix.GeneralLinearGroup.fixpointPolynomial
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
rw :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0) 2 -
      4 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
    0
⊢ discrim ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0)
      ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0)
      (-(↑g : Matrix (Fin 2) (Fin 2) K) 0 1) =
    0

Tactic:
rw [discrim]

Premises used: discrim
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0) 2 -
      4 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
    0

Tactic:
grind
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ discrim ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0)
      ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0)
      (-(↑g : Matrix (Fin 2) (Fin 2) K) 0 1) =
    0

Tactic:
have : discrim (g 1 0) (g 1 1 - g 0 0) (-g 0 1) = 0 := by rw [discrim]; grind
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
c : K
hc : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
this :
  discrim ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0)
      ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0)
      (-(↑g : Matrix (Fin 2) (Fin 2) K) 0 1) =
    0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * HPow.hPow (β := ℕ) c 2 +
          ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c -
        (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
      0 ↔
    (↑c : OnePoint K) = g.parabolicFixedPoint

Tactic:
simpa [parabolicFixedPoint, if_neg hc, sq, sub_eq_add_neg]
        using quadratic_eq_zero_iff_of_discrim_eq_zero hc this c

Premises used: sub_eq_add_neg, quadratic_eq_zero_iff_of_discrim_eq_zero, sq, Matrix.GeneralLinearGroup.parabolicFixedPoint, if_neg
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
inst_2 : NeZero.{u_1} (R := K) 2
c : OnePoint K
hg :
  (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
hdisc :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    0
infty : HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint
coe : ∀ (c : K), g • (↑c : OnePoint K) = (↑c : OnePoint K) ↔ (↑c : OnePoint K) = g.parabolicFixedPoint
⊢ g • c = c ↔ c = g.parabolicFixedPoint

Tactic:
cases c with
  | infty => by_cases h : g 1 0 = 0 <;> simp [parabolicFixedPoint, smul_infty_eq_ite, h]
  | coe c =>
    suffices g 1 0 * c ^ 2 + (g 1 1 - g 0 0) * c - g 0 1 = 0 ↔ c = g.parabolicFixedPoint by
      simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial]
    by_cases hc : g 1 0 = 0
    · have hd : g 1 1 = g 0 0 := by grind
      suffices g 0 1 ≠ 0 by simpa [parabolicFixedPoint, hc, hd]
      -- can't have `g 0 1 ≠ 0` since that would force `g` to be scalar
      refine fun hb ↦ fixpointPolynomial_eq_zero_iff.not.mpr hg ?_
      simp [fixpointPolynomial, hb, hc, hd]
    · have : discrim (g 1 0) (g 1 1 - g 0 0) (-g 0 1) = 0 := by rw [discrim]; grind
      simpa [parabolicFixedPoint, if_neg hc, sq, sub_eq_add_neg]
        using quadratic_eq_zero_iff_of_discrim_eq_zero hc this c

Premises used: Iff.mpr, Units.val, OnePoint.infty, sub_eq_add_neg, Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff, Iff.not, sq, OnePoint.smul_infty_eq_ite, Matrix.GeneralLinearGroup.fixpointPolynomial, Matrix.GeneralLinearGroup.parabolicFixedPoint, OfNat.ofNat
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst_2 : CharZero K
n : ℕ
hn : n ≠ 0
rw : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
⊢ (g ^ n).parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
rw [eq_comm, ← IsParabolic.smul_eq_self_iff (hg.pow hn)]

Premises used: Matrix.GeneralLinearGroup.IsParabolic.pow, eq_comm, Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst_2 : CharZero K
⊢ HPow.hPow (β := ℕ) g 0 • g.parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst_2 : CharZero K
n : ℕ
IH : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
succ : (g ^ n * g) • g.parabolicFixedPoint = g.parabolicFixedPoint
succ₁ : g ^ n • g • g.parabolicFixedPoint = g.parabolicFixedPoint
succ₂ : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
succ₃ succ₄ : g.parabolicFixedPoint = g.parabolicFixedPoint
⊢ g ^ (n + 1) • g.parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
rw [pow_succ, mul_smul, hg.smul_eq_self_iff.mpr rfl, IH]

Premises used: Iff.mpr, pow_succ, Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff, SemigroupAction.mul_smul, rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst_2 : CharZero K
n : ℕ
zero : HPow.hPow (β := ℕ) g 0 • g.parabolicFixedPoint = g.parabolicFixedPoint
succ :
  ∀ (n : ℕ) (IH : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint),
    g ^ (n + 1) • g.parabolicFixedPoint = g.parabolicFixedPoint
⊢ g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
induction n with
  | zero => simp
  | succ n IH => rw [pow_succ, mul_smul, hg.smul_eq_self_iff.mpr rfl, IH]

Premises used: Iff.mpr, pow_succ, Matrix.zero, Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff, SemigroupAction.mul_smul, rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
infty : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ HSMul.hSMul (β := OnePoint K) g ∞ ≠ ∞

Tactic:
rw [Ne, smul_infty_eq_self_iff]

Premises used: OnePoint.smul_infty_eq_self_iff, Ne
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
⊢ ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0

Tactic:
fun h ↦ not_le_of_gt hg ?_

Premises used: not_le_of_gt, Not
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
infty : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0), 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) K).discr
⊢ ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0

Tactic:
refine fun h ↦ not_le_of_gt hg ?_

Premises used: not_le_of_gt
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
simp :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2

Tactic:
simp only [discr_fin_two, trace_fin_two, det_fin_two]

Premises used: Matrix.trace_fin_two, Matrix.det_fin_two, Matrix.discr_fin_two
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2 -
      4 *
        ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 -
          (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2

Tactic:
grind
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2

Tactic:
have : g.val.discr = (g 0 0 - g 1 1) ^ 2 := by
      simp only [discr_fin_two, trace_fin_two, det_fin_two]
      grind
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
this :
  (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
infty : 0 ≤ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
⊢ 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) K).discr

Tactic:
rw [this]
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
this :
  (↑g : Matrix (Fin 2) (Fin 2) K).discr =
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2
⊢ 0 ≤ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 - (↑g : Matrix (Fin 2) (Fin 2) K) 1 1) 2

Tactic:
apply sq_nonneg

Premises used: sq_nonneg
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
⊢ g • (↑c : OnePoint K) ≠ (↑c : OnePoint K)

Tactic:
fun h ↦ not_le_of_gt hg ?_

Premises used: not_le_of_gt, Not
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
coe : ∀ (h : g • (↑c : OnePoint K) = (↑c : OnePoint K)), 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) K).discr
⊢ g • (↑c : OnePoint K) ≠ (↑c : OnePoint K)

Tactic:
refine fun h ↦ not_le_of_gt hg ?_

Premises used: not_le_of_gt
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • (↑c : OnePoint K) = (↑c : OnePoint K)
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * (c * c) +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c +
      -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
    0

Tactic:
simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial, sq, sub_eq_add_neg]
          using h

Premises used: sub_eq_add_neg, sq, Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, Matrix.GeneralLinearGroup.fixpointPolynomial
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
inst_2 : LinearOrder K
inst_3 : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • (↑c : OnePoint K) = (↑c : OnePoint K)
⊢ (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * (c * c) +
        ((↑g : Matrix (Fin 2) (Fin 2) K) 1 1 + -(↑g : Matrix (Fin 2) (Fin 2) K) 0 0) * c +
      -(↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
    0

Tactic:
replace h : g 1 0 * (c * c) + (g 1 1 + -g 0 0) * c + -g 0 1 = 0 := by
        simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial, sq, sub_eq_add_neg]
          using h