awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ 0 ≤ dist (↑z : ℂ) (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
have hy : 0 < -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det →
  0 ≤ dist (↑z : ℂ) (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
Tactic: positivity [neg_pos.mpr h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
⊢ (∃ (z : ℍ), g • z = z) ↔ (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
have mp : (∃ (z : ℍ), g • z = z) → (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
mp : (∃ (z : ℍ), g • z = z) → (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
⊢ (∃ (z : ℍ), g • z = z) ↔ (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
have mpr : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0 → ∃ (z : ℍ), g • z = z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
z : ℍ
hz : g • z = z
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
have a : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace +
      (HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (denom g (↑z : ℂ))).im / z.im -
    (0 + (num g (↑z : ℂ)).im / z.im) =
  0
Tactic: linear_combination
      (norm := { simp [σ, h.not_gt, num, denom, z.im_ne_zero, Matrix.trace_fin_two, field] })
      congr($(gl_smul_eq_iff_num_eq.mp hz).im / z.im)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
hadd : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
⊢ ∃ (z : ℍ), g • z = z
have pos : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0), ∃ (z : ℍ), g • z = z
Tactic: by_cases hc : g 1 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
hadd : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
pos : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0), ∃ (z : ℍ), g • z = z
⊢ ∃ (z : ℍ), g • z = z
have neg : ∀ (hc : ¬(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0), ∃ (z : ℍ), g • z = z
Tactic: by_cases hc : g 1 0 = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
hadd : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ ∃ (z : ℍ), g • z = z
have h₁ : g •
    { coe := { re := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1), im := 1 : ℂ },
      coe_im_pos := sorry : ℍ } =
  { coe := { re := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1), im := 1 },
    coe_im_pos := sorry }
Tactic: use ⟨⟨g 0 1 / (2 * g 1 1), 1⟩, one_pos⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
hadd : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hc : ¬(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ ∃ (z : ℍ), g • z = z
have h₁ : g •
    {
      coe :=
        { re := -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
          im := √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0| : ℂ },
      coe_im_pos := sorry : ℍ } =
  {
    coe :=
      { re := -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
        im := √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0| },
    coe_im_pos := sorry }
Tactic: use ⟨⟨-g 1 1 / g 1 0, √(-g.val.det) / |g 1 0|⟩, by simp [*]⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
⊢ g • z = z ↔
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * ((↑z : ℂ) * (↑z : ℂ)) +
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) * (↑z : ℂ) +
        -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) =
      0
have simp : (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) =
    (↑z : ℂ) *
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ↔
  (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * ((↑z : ℂ) * (↑z : ℂ)) +
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) * (↑z : ℂ) +
      -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) =
    0
Tactic: simp [gl_smul_eq_iff_num_eq, σ, h, num, denom]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hfix : ∃ (z : ℍ), g • z = z
⊢ g.IsElliptic
have rcases : ∀ (z : ℍ) (hz : g • z = z), g.IsElliptic
Tactic: rcases hfix with ⟨z, hz⟩
Cleared hypotheses: hfix
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ False
have hgc₁ : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 → ¬0 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1
Tactic: simp [GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, ← Matrix.ext_iff, hc] at hgc
Cleared hypotheses: hgc
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
z : ℍ
hz : g • z = z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hgc :
  (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 → ¬0 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1
⊢ False
have hz₁ : z.re * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 =
    z.re * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ∧
  (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
Tactic: simp [gl_smul_eq_iff_num_eq, Complex.ext_iff, σ, h, num, denom, hc, mul_comm, z.im_ne_zero]
      at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
⊢ g.IsElliptic
have hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
Tactic: have hc : g 1 0 ≠ 0 := by
    intro hc
    simp [GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, ← Matrix.ext_iff, hc] at hgc
    simp [gl_smul_eq_iff_num_eq, Complex.ext_iff, σ, h, num, denom, hc, mul_comm, z.im_ne_zero]
      at hz
    grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ g.IsElliptic
have refine : ∀ (hge : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℝ).discr), False
Tactic: refine lt_of_not_ge fun hge ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
hge : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℝ).discr
⊢ discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ) * (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ)
have rw : discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
    (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
  (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ)
Tactic: rw [← Complex.ofReal_mul, Real.mul_self_sqrt hge]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
hge : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℝ).discr
⊢ discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ)
have simp : HPow.hPow (β := ℕ) ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) 2 +
    4 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) =
  HPow.hPow (β := ℕ) ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) 2 -
    4 *
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) -
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
Tactic: simp [discrim, Matrix.discr_fin_two, Matrix.trace_fin_two, Matrix.det_fin_two]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
hge : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℝ).discr
⊢ False
have hd : discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
    (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
  (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ) * (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ)
Tactic: have hd : discrim (g 1 0 : ℂ) (g 1 1 - g 0 0) (-g 0 1) = √g.val.discr * √g.val.discr := by
    rw [← Complex.ofReal_mul, Real.mul_self_sqrt hge]
    simp [discrim, Matrix.discr_fin_two, Matrix.trace_fin_two, Matrix.det_fin_two]
    ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
hge : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℝ).discr
hd :
  discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ) * (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ)
⊢ False
have hz₁ : (↑z : ℂ) =
    (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) +
        (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ)) /
      (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) ∨
  (↑z : ℂ) =
    (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) -
        (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ)) /
      (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
Tactic: rw [gl_smul_eq_self_iff_quadratic h, quadratic_eq_zero_iff (mod_cast hc) hd] at hz
Cleared hypotheses: hz, hc, hge, hd
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz :
  (↑z : ℂ) =
      (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) +
          (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ)) /
        (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) ∨
    (↑z : ℂ) =
      (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) -
          (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ)) /
        (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
hge : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℝ).discr
hd :
  discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ) * (↑√(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr : ℂ)
⊢ False
have hz₁ : (↑z : ℂ) =
    (↑((-((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) +
            √(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) /
          (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0)) :
      ℂ) ∨
  (↑z : ℂ) =
    (↑((-((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 - (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) -
            √(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) /
          (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0)) :
      ℂ)
Tactic: norm_cast at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
hg : (-g).IsElliptic
⊢ fixedPt (-g) hg = fixedPt g ⋯
have coe : (↑(fixedPt (-g) hg) : ℂ) = (↑(fixedPt g sorry) : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
hg : (-g).IsElliptic
⊢ (↑(fixedPt (-g) hg) : ℂ) = (↑(fixedPt g ⋯) : ℂ)
have coe : (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) /
    -(2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) =
  ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) /
    (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
Tactic: simp [fixedPt, Matrix.discr_fin_two, Matrix.det_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
⊢ g • z = z ↔ z = fixedPt g hell
have inr : ∀
  (this :
    ∀ {g : GL (Fin 2) ℝ} (hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det) (hell : g.IsElliptic)
      (hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0), g • z = z ↔ z = fixedPt g hell)
  (hc : ¬0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0), g • z = z ↔ z = fixedPt g hell
Tactic: wlog hc : 0 < g 1 0 generalizing g
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
inr :
  ∀
    (this :
      ∀ {g : GL (Fin 2) ℝ} (hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det) (hell : g.IsElliptic)
        (hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0), g • z = z ↔ z = fixedPt g hell)
    (hc : ¬0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0), g • z = z ↔ z = fixedPt g hell
⊢ g • z = z ↔ z = fixedPt g hell
have wlog : ∀ {g : GL (Fin 2) ℝ} (hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det) (hell : g.IsElliptic)
  (hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0), g • z = z ↔ z = fixedPt g hell
Tactic: wlog hc : 0 < g 1 0 generalizing g
Cleared hypotheses: hpos, hell
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
this :
  ∀ {g : GL (Fin 2) ℝ} (hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det) (hell : g.IsElliptic)
    (hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0), g • z = z ↔ z = fixedPt g hell
hc : ¬0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
⊢ g • z = z ↔ z = fixedPt g hell
have hc₁ : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 < 0
Tactic: replace hc := hell.c_ne_zero.lt_or_gt.resolve_right hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g_1 : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
⊢ discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    HPow.hPow (β := ℕ) (Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) 2
have rw : discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
    (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
  HPow.hPow (β := ℕ) Complex.I 2 * (↑(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)
Tactic: rw [mul_pow, ← Complex.ofReal_pow, Real.sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g_1 : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
rw :
  discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    HPow.hPow (β := ℕ) Complex.I 2 * (↑(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)
⊢ discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    HPow.hPow (β := ℕ) (Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) 2
have rw₁ : 0 ≤ -(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr
Tactic: rw [mul_pow, ← Complex.ofReal_pow, Real.sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g_1 : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
⊢ discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    HPow.hPow (β := ℕ) Complex.I 2 * (↑(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)
have simp : HPow.hPow (β := ℕ) ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) 2 +
    4 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) =
  HPow.hPow (β := ℕ) ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) 2 -
    4 *
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) -
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
Tactic: simp [discrim, Matrix.discr_fin_two, Matrix.trace_fin_two, Matrix.det_fin_two]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g_1 : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
⊢ g • z = z ↔ z = fixedPt g hell
have hd : discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
    (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
  HPow.hPow (β := ℕ) (Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) 2
Tactic: have hd : discrim (g 1 0 : ℂ) (g 1 1 - g 0 0) (-g 0 1) = (.I * √(-g.val.discr)) ^ 2 := by
    rw [mul_pow, ← Complex.ofReal_pow, Real.sq_sqrt]
    · simp [discrim, Matrix.discr_fin_two, Matrix.trace_fin_two, Matrix.det_fin_two]
      grind
    · simpa using hell.le
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g_1 : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hd :
  discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    HPow.hPow (β := ℕ) (Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) 2
⊢ g • z = z ↔ z = fixedPt g hell
have rw : (↑z : ℂ) =
      (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) +
          Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
        (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) ∨
    (↑z : ℂ) =
      (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) -
          Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
        (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) ↔
  z = fixedPt g hell
Tactic: rw [gl_smul_eq_self_iff_quadratic hpos, quadratic_eq_zero_iff (mod_cast hell.c_ne_zero)
    (hd.trans (pow_two _))]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g_1 : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hd :
  discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    HPow.hPow (β := ℕ) (Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) 2
⊢ (↑z : ℂ) =
        (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) +
            Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
          (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) ∨
      (↑z : ℂ) =
        (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) -
            Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
          (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) ↔
    z = fixedPt g hell
have rw : (↑z : ℂ) =
    (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) +
        Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
      (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) ↔
  z = fixedPt g hell
Tactic: rw [or_iff_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g_1 : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hd :
  discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    HPow.hPow (β := ℕ) (Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) 2
rw :
  (↑z : ℂ) =
      (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) +
          Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
        (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) ↔
    z = fixedPt g hell
⊢ (↑z : ℂ) =
        (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) +
            Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
          (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) ∨
      (↑z : ℂ) =
        (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) -
            Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
          (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) ↔
    z = fixedPt g hell
have rw₁ : ¬(↑z : ℂ) =
    (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) -
        Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
      (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
Tactic: rw [or_iff_left]