awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 < 0
⊢ 0 < (↑(-g) : Matrix (Fin 2) (Fin 2) ℝ).det

Tactic:
simpa [Matrix.det_neg]

Premises used: Matrix.det_neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 < 0
⊢ 0 < (↑(-g) : Matrix (Fin 2) (Fin 2) ℝ) 1 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 < 0
⊢ g • z = z ↔ z = fixedPt g hell

Tactic:
simpa using @this (-g) (by simpa [Matrix.det_neg]) hell.neg (by simpa)

Premises used: Matrix.IsElliptic.neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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) : ℂ)
rw₁ : 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) : ℂ)) =
    HPow.hPow (β := ℕ) (Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) 2

Tactic:
rw [mul_pow, ← Complex.ofReal_pow, Real.sq_sqrt]

Premises used: Real.sq_sqrt, mul_pow, Complex.ofReal_pow
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
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) : ℂ))
⊢ 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:
simp [discrim, Matrix.discr_fin_two, Matrix.trace_fin_two, Matrix.det_fin_two]

Premises used: Matrix.trace_fin_two, discrim, Matrix.det_fin_two, Matrix.discr_fin_two
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
⊢ 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:
grind
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
⊢ 0 ≤ -(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr

Tactic:
simpa using hell.le

Premises used: LT.lt.le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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

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
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : ℂ) =
        (-((↑((↑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
⊢ g • z = z ↔ 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 _))]

Premises used: pow_two, quadratic_eq_zero_iff, UpperHalfPlane.gl_smul_eq_self_iff_quadratic, Eq.trans
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
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 : ℂ) =
        (-((↑((↑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]

Premises used: or_iff_left
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 = fixedPt g hell

Tactic:
simp [fixedPt, UpperHalfPlane.ext_iff, abs_of_pos hc, field]

Premises used: UpperHalfPlane.ext_iff, abs_of_pos, UpperHalfPlane.fixedPt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
h :
  (↑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) : ℂ))
⊢ False

Tactic:
z.im_pos.not_ge ?_

Premises used: UpperHalfPlane.im_pos, LT.lt.not_ge
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
h :
  (↑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) : ℂ))
refine : z.im ≤ 0
⊢ False

Tactic:
refine z.im_pos.not_ge ?_

Premises used: UpperHalfPlane.im_pos, LT.lt.not_ge
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
h :
  (↑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) : ℂ))
rw :
  ((-((↑((↑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) : ℂ))).im ≤
    0
⊢ z.im ≤ 0

Tactic:
rw [← coe_im, h]

Premises used: UpperHalfPlane.coe_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
h :
  (↑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) : ℂ))
⊢ ((-((↑((↑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) : ℂ))).im ≤
    0

Tactic:
simp [Complex.div_im, div_nonpos_iff, hc.le, mul_nonneg]

Premises used: mul_nonneg, Complex.div_im, LT.lt.le, div_nonpos_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
rw :
  num g (↑I : ℂ) = HMul.hMul (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (↑I : ℂ) : ℂ) (denom g (↑I : ℂ)) ↔
    (↑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
⊢ g • I = I ↔
    (↑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:
rw [gl_smul_eq_iff_num_eq, σ, if_pos hg]

Premises used: if_pos, UpperHalfPlane.gl_smul_eq_iff_num_eq, UpperHalfPlane.σ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ num g (↑I : ℂ) = HMul.hMul (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (↑I : ℂ) : ℂ) (denom g (↑I : ℂ)) ↔
    (↑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 [Complex.ext_iff, num, denom, and_comm]

Premises used: and_comm, Complex.ext_iff, UpperHalfPlane.denom, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
rw :
  num g (↑I : ℂ) = HMul.hMul (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) (↑I : ℂ) : ℂ) (denom g (↑I : ℂ)) ↔
    (↑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
⊢ g • I = I ↔
    (↑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:
rw [gl_smul_eq_iff_num_eq, σ, if_neg (not_lt_of_gt hg)]

Premises used: not_lt_of_gt, UpperHalfPlane.gl_smul_eq_iff_num_eq, UpperHalfPlane.σ, if_neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
⊢ num g (↑I : ℂ) = HMul.hMul (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) (↑I : ℂ) : ℂ) (denom g (↑I : ℂ)) ↔
    (↑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 [num, denom, Complex.ext_iff, and_comm]

Premises used: and_comm, Complex.ext_iff, UpperHalfPlane.denom, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
mp : (∀ (z : ℍ), g • z = z) → Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g
mpr : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g → ∀ (z : ℍ), g • z = z
⊢ (∀ (z : ℍ), g • z = z) ↔ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
mp : ∀ (hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)), False
⊢ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g

Tactic:
by_contra! hgc
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
mp : ∀ (hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0), False
mp₁ : ∀ (hgt : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det), False
⊢ False

Tactic:
rcases g.det_ne_zero.lt_or_gt with hlt | hgt

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1

Tactic:
obtain ⟨ha, hb⟩ := (gl_smul_I_eq_I_iff_of_neg hlt).mp (hg _)

Premises used: UpperHalfPlane.gl_smul_I_eq_I_iff_of_neg, Iff.mp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑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:
obtain ⟨ha, hb⟩ := (gl_smul_I_eq_I_iff_of_neg hlt).mp (hg _)

Premises used: UpperHalfPlane.gl_smul_I_eq_I_iff_of_neg, Iff.mp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0

Tactic:
rw [eq_neg_iff_add_eq_zero, ← Matrix.trace_fin_two] at ha

Premises used: Matrix.trace_fin_two, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
ha₁ : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0

Tactic:
rw [eq_neg_iff_add_eq_zero, ← Matrix.trace_fin_two] at ha

Premises used: Matrix.trace_fin_two, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
mp : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0), False
mp₁ : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0), False
⊢ False

Tactic:
rcases eq_or_ne (g 1 0) 0 with hc | hc

Premises used: Units.val, eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ 0 < (1 + Complex.I).im

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ g • { coe := 1 + Complex.I, coe_im_pos := ⋯ : ℍ } = { coe := 1 + Complex.I, coe_im_pos := ⋯ }

Tactic:
specialize hg ⟨1 + .I, by simp⟩

Premises used: UpperHalfPlane.mk, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hg : g • { coe := 1 + Complex.I, coe_im_pos := ⋯ : ℍ } = { coe := 1 + Complex.I, coe_im_pos := ⋯ }
⊢ { coe := 1 + Complex.I, coe_im_pos := ⋯ : ℍ }.re =
    (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1)

Tactic:
rw [gl_smul_eq_self_iff_re_eq ha hc] at hg

Premises used: UpperHalfPlane.gl_smul_eq_self_iff_re_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hg :
  { coe := 1 + Complex.I, coe_im_pos := ⋯ : ℍ }.re =
    (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1)
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ 0 < 1 + √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0|

Tactic:
simp [add_pos, *]

Premises used: add_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ 0 < 1 + √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0|

Tactic:
have : 0 < 1 + √(-g.val.det) / |g 1 0| := by simp [add_pos, *]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
this : 0 < 1 + √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0|
⊢ g •
      {
        coe :=
          { re := -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
            im := 1 + √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0| : ℂ },
        coe_im_pos := this : ℍ } =
    {
      coe :=
        { re := -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
          im := 1 + √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0| },
      coe_im_pos := this }

Tactic:
specialize hg ⟨⟨-g 1 1 / g 1 0, 1 + √(-g.val.det) / |g 1 0|⟩, this⟩

Premises used: Units.val, abs, UpperHalfPlane.mk, HDiv.hDiv, HAdd.hAdd, Real.sqrt, OfNat.ofNat, Complex.mk, Matrix.det, Neg.neg