awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
neg : ∀ (hc : ¬(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0), ∃ (z : ℍ), g • z = z
⊢ ∃ (z : ℍ), g • z = z

Tactic:
by_cases hc : g 1 0 = 0

Premises used: Units.val, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
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 := ⋯ : ℍ } =
    { coe := { re := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1), im := 1 },
      coe_im_pos := ⋯ }
⊢ ∃ (z : ℍ), g • z = z

Tactic:
use ⟨⟨g 0 1 / (2 * g 1 1), 1⟩, one_pos⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
⊢ 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 := ⋯ : ℍ } =
    { coe := { re := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1), im := 1 },
      coe_im_pos := ⋯ }

Tactic:
simp [gl_smul_eq_self_iff_re_eq, *]

Premises used: UpperHalfPlane.gl_smul_eq_self_iff_re_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
⊢ 0 <
    { 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| : ℂ }.im

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
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 := ⋯ : ℍ } =
    {
      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 := ⋯ }
⊢ ∃ (z : ℍ), g • z = z

Tactic:
use ⟨⟨-g 1 1 / g 1 0, √(-g.val.det) / |g 1 0|⟩, by simp [*]⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
⊢ 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 := ⋯ : ℍ } =
    {
      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 := ⋯ }

Tactic:
simp [gl_smul_eq_self_iff_dist_sq_eq, *, dist_eq_norm, ← Complex.normSq_eq_norm_sq,
        Complex.normSq_apply, ← pow_two, div_pow, h.le]

Premises used: dist_eq_norm, pow_two, Complex.normSq_eq_norm_sq, LT.lt.le, UpperHalfPlane.gl_smul_eq_self_iff_dist_sq_eq, div_pow, Complex.normSq_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
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
⊢ 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

Tactic:
simp [gl_smul_eq_iff_num_eq, σ, h, num, denom]

Premises used: UpperHalfPlane.denom, UpperHalfPlane.gl_smul_eq_iff_num_eq, UpperHalfPlane.σ, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
⊢ (↑((↑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:
grind
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
rcases : ∀ (z : ℍ) (hz : g • z = z), g.IsElliptic
⊢ g.IsElliptic

Tactic:
rcases hfix with ⟨z, hz⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : 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

Premises used: Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar, Matrix.ext_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
⊢ 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

Premises used: UpperHalfPlane.im_ne_zero, Complex.ext_iff, UpperHalfPlane.denom, mul_comm, UpperHalfPlane.gl_smul_eq_iff_num_eq, UpperHalfPlane.σ, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
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
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
⊢ False

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : 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
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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

Tactic:
lt_of_not_ge fun hge ↦ ?_

Premises used: Matrix.IsElliptic, lt_of_not_ge
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
refine : ∀ (hge : 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℝ).discr), False
⊢ g.IsElliptic

Tactic:
refine lt_of_not_ge fun hge ↦ ?_

Premises used: lt_of_not_ge
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
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 : ℂ)
⊢ 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:
rw [← Complex.ofReal_mul, Real.mul_self_sqrt hge]

Premises used: Real.mul_self_sqrt, Complex.ofReal_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
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) : ℂ)) =
    (↑(↑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 : 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
⊢ 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:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : ℂ)

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
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : ℂ)
⊢ (↑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

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

Tactic:
rw [gl_smul_eq_self_iff_quadratic h, quadratic_eq_zero_iff (mod_cast hc) hd] at hz

Premises used: quadratic_eq_zero_iff, UpperHalfPlane.gl_smul_eq_self_iff_quadratic
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : ℂ)
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
⊢ 0 ≤ (↑g : Matrix (Fin 2) (Fin 2) ℝ).discr

Tactic:
rw [gl_smul_eq_self_iff_quadratic h, quadratic_eq_zero_iff (mod_cast hc) hd] at hz

Premises used: quadratic_eq_zero_iff, UpperHalfPlane.gl_smul_eq_self_iff_quadratic
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : ℂ)
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
⊢ 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:
rw [gl_smul_eq_self_iff_quadratic h, quadratic_eq_zero_iff (mod_cast hc) hd] at hz

Premises used: quadratic_eq_zero_iff, UpperHalfPlane.gl_smul_eq_self_iff_quadratic
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 : ℂ)
⊢ (↑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
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
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 : ℂ)
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)) :
        ℂ)
⊢ False

Tactic:
simp only [z.ne_ofReal, false_or] at hz

Premises used: false_or, UpperHalfPlane.ne_ofReal
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g_1 : GL (Fin 2) ℝ
z w : ℍ
g : GL (Fin 2) ℝ
hell : g.IsElliptic
⊢ 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) : ℂ)) +
        Complex.I *
          ((↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ) / (2 * (↑|(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0| : ℂ)))).im

Tactic:
simpa [div_pos, Complex.div_re, Complex.div_im, hell.c_ne_zero]

Premises used: Matrix.IsElliptic.c_ne_zero, Complex.div_im, Complex.div_re, div_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : (-g).IsElliptic
coe : (↑(fixedPt (-g) hg) : ℂ) = (↑(fixedPt g ⋯) : ℂ)
⊢ fixedPt (-g) hg = fixedPt g ⋯

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : (-g).IsElliptic
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) : ℂ))
⊢ (↑(fixedPt (-g) hg) : ℂ) = (↑(fixedPt g ⋯) : ℂ)

Tactic:
simp [fixedPt, Matrix.discr_fin_two, Matrix.det_neg]

Premises used: Matrix.det_neg, UpperHalfPlane.fixedPt, Matrix.discr_fin_two
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hg : (-g).IsElliptic
⊢ (-(↑((↑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:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
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
⊢ g • z = z ↔ z = fixedPt g hell

Tactic:
wlog hc : 0 < g 1 0 generalizing g

Premises used: Units.val, OfNat.ofNat
-- 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 : ¬0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 < 0

Tactic:
replace hc := hell.c_ne_zero.lt_or_gt.resolve_right hc