awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
pos :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0),
    HSMul.hSMul (β := OnePoint K) g ∞ =
      if (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0 then ∞
      else (↑((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) : OnePoint K)
⊢ HSMul.hSMul (β := OnePoint K) g ∞ =
    if (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0 then ∞
    else (↑((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) : OnePoint K)
have neg : ∀ (h : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0),
  HSMul.hSMul (β := OnePoint K) g ∞ =
    if (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0 then ∞
    else (↑((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) K) 1 0) : OnePoint K)
Tactic: by_cases h : g 1 0 = 0
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
L : Type u_2
inst_2 : Field L
inst_3 : DecidableEq L
f : K →+* L
g : GL (Fin 2) K
c : OnePoint K
⊢ OnePoint.map (⇑f : (a : K) → L) (g • c) =
    HSMul.hSMul (α := GL (Fin 2) L) (β := OnePoint L)
      (((GeneralLinearGroup.map f : MonoidHom.{u_1, u_2} (GL (Fin 2) K) (GL (Fin 2) L)) :
            (a : GL (Fin 2) K) → GL (Fin 2) L)
          g :
        GL (Fin 2) L)
      (OnePoint.map (⇑f : (a : K) → L) c)
have infty : OnePoint.map (⇑f : (a : K) → L) (HSMul.hSMul (β := OnePoint K) g ∞) =
  HSMul.hSMul (α := GL (Fin 2) L) (β := OnePoint L)
    (((GeneralLinearGroup.map f : MonoidHom.{u_1, u_2} (GL (Fin 2) K) (GL (Fin 2) L)) :
          (a : GL (Fin 2) K) → GL (Fin 2) L)
        g :
      GL (Fin 2) L)
    (OnePoint.map.{u_1, u_2} (X := K) (⇑f : (a : K) → L) ∞)
Tactic: cases c with
  | infty => simp [smul_infty_eq_ite, apply_ite]
  | coe c => simp [smul_some_eq_ite, ← map_mul, ← map_add, apply_ite]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
L : Type u_2
inst_2 : Field L
inst_3 : DecidableEq L
f : K →+* L
g : GL (Fin 2) K
c : OnePoint K
infty :
  OnePoint.map (⇑f : (a : K) → L) (HSMul.hSMul (β := OnePoint K) g ∞) =
    HSMul.hSMul (α := GL (Fin 2) L) (β := OnePoint L)
      (((GeneralLinearGroup.map f : MonoidHom.{u_1, u_2} (GL (Fin 2) K) (GL (Fin 2) L)) :
            (a : GL (Fin 2) K) → GL (Fin 2) L)
          g :
        GL (Fin 2) L)
      (OnePoint.map.{u_1, u_2} (X := K) (⇑f : (a : K) → L) ∞)
⊢ OnePoint.map (⇑f : (a : K) → L) (g • c) =
    HSMul.hSMul (α := GL (Fin 2) L) (β := OnePoint L)
      (((GeneralLinearGroup.map f : MonoidHom.{u_1, u_2} (GL (Fin 2) K) (GL (Fin 2) L)) :
            (a : GL (Fin 2) K) → GL (Fin 2) L)
          g :
        GL (Fin 2) L)
      (OnePoint.map (⇑f : (a : K) → L) c)
have coe : ∀ (c : K),
  OnePoint.map (⇑f : (a : K) → L) (g • (↑c : OnePoint K)) =
    HSMul.hSMul (α := GL (Fin 2) L) (β := OnePoint L)
      (((GeneralLinearGroup.map f : MonoidHom.{u_1, u_2} (GL (Fin 2) K) (GL (Fin 2) L)) :
            (a : GL (Fin 2) K) → GL (Fin 2) L)
          g :
        GL (Fin 2) L)
      (OnePoint.map (⇑f : (a : K) → L) (↑c : OnePoint K))
Tactic: cases c with
  | infty => simp [smul_infty_eq_ite, apply_ite]
  | coe c => simp [smul_some_eq_ite, ← map_mul, ← map_add, apply_ite]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
c : K
g : GL (Fin 2) K
⊢ Eq (α := K) ((aeval c : (a : K[X]) → K) g.fixpointPolynomial : K) (0 : K) ↔ g • (↑c : OnePoint K) = (↑c : OnePoint K)
have simp : (↑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 ↔
  (if (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 0 then ∞
    else
      (↑(((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 0 1) /
            ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1)) :
        OnePoint K)) =
    (↑c : OnePoint K)
Tactic: simp only [fixpointPolynomial, map_sub, map_mul, map_add, aeval_X_pow, aeval_C, aeval_X,
    Algebra.algebraMap_self_apply, OnePoint.smul_some_eq_ite]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
c : K
g : GL (Fin 2) K
⊢ (↑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 ↔
    (if (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 0 then ∞
      else
        (↑(((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 0 1) /
              ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1)) :
          OnePoint K)) =
      (↑c : OnePoint K)
have pos : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
c : K
g : GL (Fin 2) K
pos :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 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 : 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 ↔
    (if (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 0 then ∞
      else
        (↑(((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 0 1) /
              ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1)) :
          OnePoint K)) =
      (↑c : OnePoint K)
have neg : ∀ (h : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 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 ↔
    (↑(((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 0 1) /
            ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1)) :
        OnePoint K) =
      (↑c : OnePoint K)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
c : K
g : GL (Fin 2) K
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 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)
have pos : ∀
  (hg :
    (↑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),
  (↑g : Matrix (Fin 2) (Fin 2) K).det = 0
Tactic: refine ⟨fun hg ↦ (g.det_ne_zero ?_).elim, fun hg ↦ (infty_ne_coe _ hg).elim⟩
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
c : K
g : GL (Fin 2) K
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 0
hg :
  (↑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
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).det = 0
have pos : (↑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
Tactic: rw [det_fin_two]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
c : K
g : GL (Fin 2) K
h : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 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 ↔
    (↑(((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 0 1) /
            ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1)) :
        OnePoint K) =
      (↑c : OnePoint K)
have neg : (↑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 ↔
  (↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 =
    c * ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1)
Tactic: rw [coe_eq_coe, div_eq_iff h]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst_2 : NeZero.{u_1} (R := K) 2
c : OnePoint K
⊢ g • c = c ↔ c = g.parabolicFixedPoint
have hg₁ : (↑g : Matrix (Fin 2) (Fin 2) K) ∉ Set.range (ι := K) (⇑(Matrix.scalar (Fin 2)) : (a : K) → Matrix (Fin 2) (Fin 2) K)
Tactic: rcases hg with ⟨hg, hdisc⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
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)
⊢ g • c = c ↔ c = g.parabolicFixedPoint
have hdisc : (↑g : Matrix (Fin 2) (Fin 2) K).discr = 0
Tactic: rcases hg with ⟨hg, hdisc⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (hypothesis)
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 : (↑g : Matrix (Fin 2) (Fin 2) K).discr = 0
⊢ g • c = c ↔ c = g.parabolicFixedPoint
have 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
Tactic: rw [discr_fin_two, trace_fin_two, det_fin_two] at hdisc
Cleared hypotheses: hdisc
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
⊢ HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint
have pos : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0), HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint
Tactic: by_cases h : g 1 0 = 0
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
pos : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0), HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint
⊢ HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint
have neg : ∀ (h : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0), HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint
Tactic: by_cases h : g 1 0 = 0
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
⊢ g • (↑c : OnePoint K) = (↑c : OnePoint K) ↔ (↑c : OnePoint K) = g.parabolicFixedPoint
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
⊢ (↑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
have 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
Tactic: by_cases hc : g 1 0 = 0
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
⊢ (↑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
have 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
Tactic: by_cases hc : g 1 0 = 0
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (hypothesis)
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 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
have hd : (↑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
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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) 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
have pos : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 ≠ 0
Tactic: suffices g 0 1 ≠ 0 by simpa [parabolicFixedPoint, hc, hd]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
have pos : ∀ (hb : (↑g : Matrix (Fin 2) (Fin 2) K) 0 1 = 0), g.fixpointPolynomial = 0
Tactic: refine fun hb ↦ fixpointPolynomial_eq_zero_iff.not.mpr hg ?_
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
have 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
Tactic: rw [discrim]
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (hypothesis)
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 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
have 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
Tactic: have : discrim (g 1 0) (g 1 1 - g 0 0) (-g 0 1) = 0 := by rw [discrim]; grind
-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.ProjectiveLine (goal)
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
⊢ g • c = c ↔ c = g.parabolicFixedPoint
have infty : HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ ∞ = 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
Cleared hypotheses: c