awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
p : ℙ K (Fin 2 → K)
h :
  ∀ (w : Fin 2 → K) (hw : w ≠ 0),
    Eq (α := ℙ K (Fin 2 → K))
      ((fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K)))
        ((fun (p : ℙ K (Fin 2 → K)) ↦
            (Projectivization.lift
                (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
                  if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
                ⋯ p :
              OnePoint K))
          (mk K w hw)))
      (mk K w hw)
⊢ (fun (p : OnePoint K) ↦ (p.elim (mk K ![1, 0] ⋯) fun (t : K) ↦ mk K ![t, 1] ⋯ : ℙ K (Fin 2 → K)))
      ((fun (p : ℙ K (Fin 2 → K)) ↦
          (Projectivization.lift
              (fun (u : { v : Fin 2 → K // v ≠ 0 }) ↦
                if (↑u : Fin 2 → K) 1 = 0 then ∞ else (↑(((↑u : Fin 2 → K) 1)⁻¹ * (↑u : Fin 2 → K) 0) : OnePoint K))
              ⋯ p :
            OnePoint K))
        p) =
    p

Tactic:
induction p using ind with | h w hw =>
    by_cases h₀ : w 1 = 0 <;> simp only [mk_eq_mk_iff', h₀, Projectivization.lift_mk, if_true,
        if_false, OnePoint.elim_infty, OnePoint.elim_some]
    · have : w 0 ≠ 0 := fun h ↦ hw <| funext <| by simp_all
      use (w 0)⁻¹
      ext i
      fin_cases i <;> simp_all
    · exact ⟨(w 1)⁻¹, funext <| by simp [inv_mul_cancel₀ h₀]⟩

Premises used: if_true, if_false, OnePoint.elim_some, OnePoint.elim_infty, Projectivization.lift_mk, Projectivization.mk_eq_mk_iff'
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
⊢ Ne.{u_1 + 1} (α := Fin (Nat.succ 0).succ → K) ![1, 0] 0

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
⊢ Eq (α := ℙ K (Fin 2 → K)) ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) ∞ : ℙ K (Fin 2 → K))
    (mk K ![1, 0] ⋯ : ℙ K (Fin (Nat.succ 0).succ → K))

Tactic:
rfl

Premises used: Projectivization.mk, Set.Mem, rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
t : K
⊢ ![t, 1] ≠ 0

Tactic:
simp
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
t : K
⊢ Eq (α := ℙ K (Fin 2 → K))
    ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) (↑t : OnePoint K) : ℙ K (Fin 2 → K))
    (mk K ![t, 1] ⋯ : ℙ K (Fin (Nat.succ 0).succ → K))

Tactic:
rfl

Premises used: Projectivization.mk, Set.Mem, rfl
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : DivisionRing K
inst_1 : DecidableEq K
v : Fin 2 → K
h : v ≠ 0
⊢ (Equiv.symm (equivProjectivization K) : (a : ℙ K (Fin 2 → K)) → OnePoint K) (mk K v h) =
    if v 1 = 0 then ∞ else (↑((v 1)⁻¹ * v 0) : OnePoint K)

Tactic:
simp [equivProjectivization]

Premises used: OnePoint.equivProjectivization
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
x : OnePoint K
rw :
  (equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K))
      ((Equiv.symm (equivProjectivization K) : (a : ℙ K (Fin 2 → K)) → OnePoint K)
        (HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
          ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K)))) =
    HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
      ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K))
rw₁ rw₂ :
  HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
      ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K)) =
    HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
      ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K))
⊢ (equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) (g • x) =
    HSMul.hSMul (β := ℙ K (Fin 2 → K)) g
      ((equivProjectivization K : (a : OnePoint K) → ℙ K (Fin 2 → K)) x : ℙ K (Fin 2 → K))

Tactic:
rw [Equiv.smul_def, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, Equiv.smul_def
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
h : ![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 0] = 0
⊢ False

Tactic:
simpa [det_fin_two, show g 0 0 = 0 from congr_fun h 0, show g 1 0 = 0 from congr_fun h 1]
        using g.det_ne_zero

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, congr_fun, Matrix.det_fin_two, 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
⊢ HSMul.hSMul (β := OnePoint K) g ∞ =
    (Equiv.symm (equivProjectivization K) : (a : ℙ K (Fin 2 → K)) → OnePoint K)
      (mk K ![(↑g : Matrix (Fin 2) (Fin 2) K) 0 0, (↑g : Matrix (Fin 2) (Fin 2) K) 1 0] ⋯ : ℙ K (Fin 2 → K))

Tactic:
simp [Equiv.smul_def, mulVec_eq_sum, Units.smul_def]

Premises used: Equiv.smul_def, Matrix.mulVec_eq_sum, Units.smul_def
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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)
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)
⊢ 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

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
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:
simp [h, div_eq_inv_mul, smul_infty_def]

Premises used: OnePoint.smul_infty_def, div_eq_inv_mul
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
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:
simp [h, div_eq_inv_mul, smul_infty_def]

Premises used: OnePoint.smul_infty_def, div_eq_inv_mul
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
⊢ HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0

Tactic:
simp [smul_infty_eq_ite]

Premises used: OnePoint.smul_infty_eq_ite
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
g : GL (Fin 2) K
k : K
⊢ g • (↑k : OnePoint K) =
    if (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * k + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1 = 0 then ∞
    else
      (↑(((↑g : Matrix (Fin 2) (Fin 2) K) 0 0 * k + (↑g : Matrix (Fin 2) (Fin 2) K) 0 1) /
            ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * k + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1)) :
        OnePoint K)

Tactic:
simp [Equiv.smul_def, mulVec_eq_sum, div_eq_inv_mul, mul_comm, Units.smul_def]

Premises used: Equiv.smul_def, Matrix.mulVec_eq_sum, Units.smul_def, mul_comm, div_eq_inv_mul
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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
⊢ 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:
simp [smul_infty_eq_ite, apply_ite]

Premises used: apply_ite, OnePoint.smul_infty_eq_ite
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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 : 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:
simp [smul_some_eq_ite, ← map_mul, ← map_add, apply_ite]

Premises used: OnePoint.smul_some_eq_ite, apply_ite, map_add, map_mul
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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) ∞)
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))
⊢ 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)

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]

Premises used: OnePoint.infty, OnePoint.smul_some_eq_ite, apply_ite, map_add, map_mul, OnePoint.smul_infty_eq_ite
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
c : K
g : GL (Fin 2) K
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)
⊢ Eq (α := K) ((aeval c : (a : K[X]) → K) g.fixpointPolynomial : K) (0 : K) ↔ g • (↑c : 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]

Premises used: Algebra.algebraMap_self_apply, map_sub, Polynomial.aeval_X_pow, OnePoint.smul_some_eq_ite, map_add, map_mul, Matrix.GeneralLinearGroup.fixpointPolynomial, Polynomial.aeval_C, Polynomial.aeval_X
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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)
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)
⊢ (↑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:
split_ifs with h
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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)

Tactic:
⟨fun hg ↦ (g.det_ne_zero ?_).elim, fun hg ↦ (infty_ne_coe _ hg).elim⟩

Premises used: False.elim, Matrix.GeneralLinearGroup.det_ne_zero, Iff.intro, OnePoint.infty_ne_coe
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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
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
⊢ (↑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:
refine ⟨fun hg ↦ (g.det_ne_zero ?_).elim, fun hg ↦ (infty_ne_coe _ hg).elim⟩
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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
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
⊢ (↑g : Matrix (Fin 2) (Fin 2) K).det = 0

Tactic:
rw [det_fin_two]

Premises used: Matrix.det_fin_two
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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) 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:
grind
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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
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)
⊢ (↑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:
rw [coe_eq_coe, div_eq_iff h]

Premises used: div_eq_iff, OnePoint.coe_eq_coe
-- Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
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 =
      c * ((↑g : Matrix (Fin 2) (Fin 2) K) 1 0 * c + (↑g : Matrix (Fin 2) (Fin 2) K) 1 1)

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
hg : g.IsParabolic
inst_2 : NeZero.{u_1} (R := K) 2
c : OnePoint K
⊢ (↑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⟩
-- 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 : 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 : Matrix (Fin 2) (Fin 2) K).discr = 0

Tactic:
rcases hg with ⟨hg, hdisc⟩
-- 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 : (↑g : Matrix (Fin 2) (Fin 2) K).discr = 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) =
    0

Tactic:
rw [discr_fin_two, trace_fin_two, det_fin_two] at hdisc

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
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
neg :
  ∀ (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

Tactic:
by_cases h : 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
h : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint

Tactic:
simp [parabolicFixedPoint, smul_infty_eq_ite, h]

Premises used: OnePoint.smul_infty_eq_ite, 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
h : ¬(↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ HSMul.hSMul (β := OnePoint K) g ∞ = ∞ ↔ ∞ = g.parabolicFixedPoint

Tactic:
simp [parabolicFixedPoint, smul_infty_eq_ite, h]

Premises used: OnePoint.smul_infty_eq_ite, 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
this :
  (↑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:
simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial]

Premises used: Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff, Matrix.GeneralLinearGroup.fixpointPolynomial