awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
rw : (↑z : ℂ) ≠ 0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)

Tactic:
rw [Complex.normSq_pos]

Premises used: Complex.normSq_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ (↑z : ℂ) ≠ 0

Tactic:
z.ne_zero

Premises used: UpperHalfPlane.ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ (↑z : ℂ) ≠ 0

Tactic:
exact z.ne_zero

Premises used: UpperHalfPlane.ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ Ne (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (0 : ℝ)

Tactic:
(normSq_pos z).ne'

Premises used: UpperHalfPlane.normSq_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ 0 < (-(↑z : ℂ))⁻¹.im

Tactic:
simpa [neg_div] using div_pos z.im_pos (normSq_pos z)

Premises used: UpperHalfPlane.normSq_pos, neg_div, UpperHalfPlane.im_pos, div_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
n : ℕ
inst : NeZero n
z : ℍ
this : 0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
⊢ 0 < (-(↑n : ℂ) / (↑z : ℂ)).im

Tactic:
simpa [Complex.div_im, neg_div]

Premises used: neg_div, Complex.div_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
n : ℕ
inst : NeZero n
z : ℍ
suffices : 0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
⊢ 0 < (-(↑n : ℂ) / (↑z : ℂ)).im

Tactic:
suffices 0 < n * z.im / Complex.normSq z by simpa [Complex.div_im, neg_div]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
n : ℕ
inst : NeZero n
z : ℍ
positivity positivity₁ positivity₂ :
  n ≠ 0 → 0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
positivity₃ positivity₄ :
  n ≠ 0 →
    LT.lt (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) →
      0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
⊢ 0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)

Tactic:
positivity [NeZero.ne n, z.normSq_pos]

Premises used: UpperHalfPlane.normSq_pos, NeZero.ne
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
x : ℝ
⊢ (↑z : ℂ).im ≠ (↑x : ℂ).im

Tactic:
simp [im_ne_zero]

Premises used: UpperHalfPlane.im_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
n : ℤ
⊢ (↑z : ℂ) ≠ (↑n : ℂ)

Tactic:
mod_cast ne_ofReal z n

Premises used: Int.cast, UpperHalfPlane.coe, cast, Ne, Eq.refl, UpperHalfPlane.ne_ofReal
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
n : ℕ
⊢ (↑z : ℂ) ≠ (↑n : ℂ)

Tactic:
mod_cast ne_intCast z n

Premises used: Int.cast_natCast, UpperHalfPlane.coe, congrArg, cast, Nat.cast, UpperHalfPlane.ne_intCast, Eq, Not
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : { x : ℝ // 0 < x }
z : ℍ
⊢ 0 < ((↑x : ℝ) • (↑z : ℂ)).im

Tactic:
simpa using mul_pos x.2 z.im_pos

Premises used: UpperHalfPlane.im_pos, mul_pos, Subtype.property
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : { x : ℝ // 0 < x }
z : ℍ
⊢ (↑(x • z) : ℂ) = (↑x : ℝ) • (↑z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : { x : ℝ // 0 < x }
z : ℍ
⊢ (x • z).im = (↑x : ℝ) * z.im

Tactic:
Complex.smul_im _ _

Premises used: UpperHalfPlane.im, Complex.smul_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : { x : ℝ // 0 < x }
z : ℍ
⊢ (x • z).re = (↑x : ℝ) * z.re

Tactic:
Complex.smul_re _ _

Premises used: Complex.smul_re, UpperHalfPlane.re
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
x : ℝ
hx : 0 < x
y : ℝ
hy : 0 < y
h :
  Eq (α := ℍ) ((fun (x : { x : ℝ // 0 < x }) ↦ x • z) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) x hx))
    ((fun (x : { x : ℝ // 0 < x }) ↦ x • z) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) y hy))
⊢ Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) x hx = Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) y hy

Tactic:
simp_all [UpperHalfPlane.ext_iff, ne_zero]

Premises used: UpperHalfPlane.ext_iff, UpperHalfPlane.ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : ℝ
z : ℍ
⊢ 0 < ((↑x : ℂ) + (↑z : ℂ)).im

Tactic:
simpa using z.im_pos

Premises used: UpperHalfPlane.im_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x y : ℝ
z : ℍ
⊢ (x + y) +ᵥ z = x +ᵥ y +ᵥ z

Tactic:
simp [HVAdd.hVAdd, add_assoc]

Premises used: add_assoc, HVAdd.hVAdd
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : ℍ
⊢ HVAdd.hVAdd (α := ℝ) 0 x = x

Tactic:
simp [HVAdd.hVAdd]

Premises used: HVAdd.hVAdd
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : ℝ
z : ℍ
⊢ (↑(x +ᵥ z) : ℂ) = (↑x : ℂ) + (↑z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : ℝ
z : ℍ
⊢ (x +ᵥ z).re = x + z.re

Tactic:
rfl

Premises used: UpperHalfPlane.re, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : ℝ
z : ℍ
⊢ (x +ᵥ z).im = z.im

Tactic:
zero_add _

Premises used: zero_add, UpperHalfPlane.im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x y : ℝ
z : ℍ
⊢ x +ᵥ z = y +ᵥ z ↔ x = y

Tactic:
simp [UpperHalfPlane.ext_iff]

Premises used: UpperHalfPlane.ext_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
z : ℍ
⊢ Function.Injective (β := ℍ) fun (x : ℝ) ↦ x +ᵥ z

Tactic:
simp [Function.Injective]

Premises used: Function.Injective
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : ℝ
z : ℍ
⊢ Infinite ℍ

Tactic:
.of_injective _ <| UpperHalfPlane.vadd_left_injective I

Premises used: Infinite.of_injective, UpperHalfPlane.I, UpperHalfPlane.vadd_left_injective
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : ℝ
z : ℍ
⊢ Nontrivial ℍ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
⊢ IsOpen ℍₒ

Tactic:
isOpen_lt continuous_const Complex.continuous_im

Premises used: isOpen_lt, continuous_const, setOf, Complex.continuous_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
h : ∀ (x : ℂ), x ∈ Set.range UpperHalfPlane.coe ↔ x ∈ ℍₒ
⊢ Set.range UpperHalfPlane.coe = ℍₒ

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Goal:
x : ℂ
⊢ x ∈ Set.range UpperHalfPlane.coe ↔ x ∈ ℍₒ

Tactic:
simp [UpperHalfPlane.exists]

Premises used: UpperHalfPlane.exists
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp
Goal:
h : ℝ
hh : 0 < h
q : ℂ
hq : ‖q‖ < 1
hq_ne : q ≠ 0
⊢ 0 < (invQParam h q).im

Tactic:
im_invQParam .. ▸ mul_pos_of_neg_of_neg
    (div_neg_of_neg_of_pos (neg_lt_zero.mpr hh) Real.two_pi_pos)
    ((Real.log_neg_iff (norm_pos_iff.mpr hq_ne)).mpr hq)

Premises used: Iff.mpr, norm_pos_iff, Eq.rec, Function.Periodic.im_invQParam, Real.two_pi_pos, neg_lt_zero, div_neg_of_neg_of_pos, Eq.symm, mul_pos_of_neg_of_neg, Real.log_neg_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp
Goal:
ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
rwa : ‖cexp (2 * (↑π : ℂ) * Complex.I * ξ / (↑1 : ℂ))‖ ≤ rexp (-π)
rwa₁ : ‖cexp (2 * (↑π : ℂ) * Complex.I * ξ / 1)‖ ≤ rexp (-π)
rwa₂ : ‖cexp (2 * (↑π : ℂ) * Complex.I * ξ)‖ ≤ rexp (-π)
rwa₃ : rexp (2 * (↑π : ℂ) * Complex.I * ξ).re ≤ rexp (-π)
rwa₄ : (2 * (↑π : ℂ) * Complex.I * ξ).re ≤ -π
rwa₅ : (2 * (↑π : ℂ) * ξ * Complex.I).re ≤ -π
rwa₆ : -(2 * (↑π : ℂ) * ξ).im ≤ -π
rwa₇ : π ≤ (2 * (↑π : ℂ) * ξ).im
rwa₈ : π ≤ ((↑2 : ℂ) * (↑π : ℂ) * ξ).im
rwa₉ : π ≤ ((↑(2 * π) : ℂ) * ξ).im
rwa₁₀ : π ≤ 2 * π * ξ.im
rwa₁₁ : π ≤ π * 2 * ξ.im
rwa₁₂ : π ≤ π * (2 * ξ.im)
rwa₁₃ : 1 ≤ 2 * ξ.im
rwa₁₄ rwa₁₅ rwa₁₆ rwa₁₇ : HDiv.hDiv (α := ℝ) 1 2 ≤ ξ.im
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)

Tactic:
rwa [Periodic.qParam, ofReal_one, div_one, Complex.norm_exp, Real.exp_le_exp,
    mul_right_comm, mul_I_re, neg_le_neg_iff, ← ofReal_ofNat, ← ofReal_mul, im_ofReal_mul,
    mul_comm _ π, mul_assoc, le_mul_iff_one_le_right Real.pi_pos, ← div_le_iff₀' two_pos]

Premises used: Function.Periodic.qParam, Real.pi, le_mul_iff_one_le_right, mul_assoc, Real.pi_pos, Complex.ofReal_one, Complex.mul_I_re, Real.exp_le_exp, mul_right_comm, Complex.norm_exp, mul_comm, Complex.im_ofReal_mul, Complex.ofReal_ofNat, div_le_iff₀', div_one, Complex.ofReal_mul, neg_le_neg_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp
Goal:
n : ℕ
inst : NeZero n
τ : ℍ
rw : 0 < 2 * π * τ.im
⊢ ‖𝕢 (↑n : ℝ) (↑τ : ℂ)‖ < 1

Tactic:
rw [Periodic.norm_qParam, Real.exp_lt_one_iff, neg_mul, coe_im, neg_mul, neg_div, neg_lt_zero,
    div_pos_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero <| NeZero.ne _)]

Premises used: neg_div, div_pos_iff_of_pos_right, neg_lt_zero, Real.exp_lt_one_iff, Function.Periodic.norm_qParam, neg_mul, UpperHalfPlane.coe_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp
Goal:
n : ℕ
inst : NeZero n
τ : ℍ
⊢ 0 < 2 * π * τ.im

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Exp
Goal:
τ : ℍ
⊢ ‖cexp (2 * (↑π : ℂ) * Complex.I * (↑τ : ℂ))‖ < 1

Tactic:
simpa [Function.Periodic.norm_qParam, Complex.norm_exp] using τ.norm_qParam_lt_one 1

Premises used: UpperHalfPlane.norm_qParam_lt_one, Complex.norm_exp, Function.Periodic.norm_qParam, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z w : ℍ
rw :
  g • z = w ↔
    Eq (α := ℂ) (((σ g).toAlgEquiv : (a : ℂ) → ℂ) (num g (↑z : ℂ)) : ℂ)
      (((σ g).toAlgEquiv : (a : ℂ) → ℂ) (HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (↑w : ℂ) : ℂ) (denom g (↑z : ℂ))) : ℂ)
⊢ g • z = w ↔ num g (↑z : ℂ) = HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (↑w : ℂ) : ℂ) (denom g (↑z : ℂ))

Tactic:
rw [← (σ g).injective.eq_iff]

Premises used: Function.Injective.eq_iff, AlgEquiv.injective, UpperHalfPlane.σ, ContinuousAlgEquiv.toAlgEquiv
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z w : ℍ
⊢ g • z = w ↔
    Eq (α := ℂ) (((σ g).toAlgEquiv : (a : ℂ) → ℂ) (num g (↑z : ℂ)) : ℂ)
      (((σ g).toAlgEquiv : (a : ℂ) → ℂ) (HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (↑w : ℂ) : ℂ) (denom g (↑z : ℂ))) : ℂ)

Tactic:
simp [UpperHalfPlane.ext_iff, coe_smul, div_eq_iff]

Premises used: UpperHalfPlane.ext_iff, UpperHalfPlane.coe_smul, div_eq_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1

Tactic:
rw [Matrix.trace_fin_two, add_eq_zero_iff_eq_neg] at htrace

Premises used: Matrix.trace_fin_two, add_eq_zero_iff_eq_neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
htrace₁ : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0

Tactic:
rw [Matrix.trace_fin_two, add_eq_zero_iff_eq_neg] at htrace

Premises used: Matrix.trace_fin_two, add_eq_zero_iff_eq_neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
h₀ : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 = 0
⊢ False

Tactic:
simpa [Matrix.det_fin_two, hc, h₀] using g.det_ne_zero

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, Matrix.det_fin_two
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ≠ 0

Tactic:
have h₀ : g 1 1 ≠ 0 := by
    intro h₀
    simpa [Matrix.det_fin_two, hc, h₀] using g.det_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
h₀ : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ≠ 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0

Tactic:
simp [Matrix.det_fin_two, *]

Premises used: Matrix.det_fin_two
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
h₀ : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ≠ 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0

Tactic:
have h : g.val.det < 0 := by simp [Matrix.det_fin_two, *]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
h₀ : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ≠ 0
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
simp :
  -(z.re * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 =
      z.re * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ↔
    z.re * (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1
⊢ g • z = z ↔ z.re = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1)

Tactic:
simp [gl_smul_eq_iff_num_eq, Complex.ext_iff, htrace, hc, num, denom, σ, h.not_gt, mul_comm,
    eq_div_iff, h₀]

Premises used: Complex.ext_iff, UpperHalfPlane.denom, mul_comm, LT.lt.not_gt, UpperHalfPlane.gl_smul_eq_iff_num_eq, UpperHalfPlane.σ, UpperHalfPlane.num, eq_div_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
h₀ : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ≠ 0
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
⊢ -(z.re * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 =
      z.re * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ↔
    z.re * (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1

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

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

Premises used: Matrix.trace_fin_two, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
htrace₁ : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0

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

Premises used: Matrix.trace_fin_two, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
rw :
  num g (↑z : ℂ) = HMul.hMul (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (denom g (↑z : ℂ)) ↔
    (((↑z : ℂ) - -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)).re *
            ((↑z : ℂ) -
                -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)).re +
          ((↑z : ℂ) - -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)).im *
            ((↑z : ℂ) -
                -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)).im) *
        HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 =
      -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det
⊢ g • z = z ↔
    HPow.hPow (β := ℕ)
        (dist (↑z : ℂ) (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)))
        2 =
      -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det / HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2

Tactic:
rw [eq_div_iff (by positivity), dist_eq_norm, ← Complex.normSq_eq_norm_sq, Complex.normSq_apply,
    gl_smul_eq_iff_num_eq, σ, g.val_det_apply, if_neg h.not_gt]

Premises used: dist_eq_norm, Complex.normSq_eq_norm_sq, LT.lt.not_gt, UpperHalfPlane.gl_smul_eq_iff_num_eq, UpperHalfPlane.σ, Complex.normSq_apply, eq_div_iff, if_neg, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
simp :
  -((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 * z.re) + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 =
      z.re * (z.re * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) +
        (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * HPow.hPow (β := ℕ) z.im 2 ↔
    HPow.hPow (β := ℕ) (z.re * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 +
        HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 * HPow.hPow (β := ℕ) z.im 2 =
      (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 +
        HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2
⊢ num g (↑z : ℂ) = HMul.hMul (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (denom g (↑z : ℂ)) ↔
    (((↑z : ℂ) - -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)).re *
            ((↑z : ℂ) -
                -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)).re +
          ((↑z : ℂ) - -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)).im *
            ((↑z : ℂ) -
                -(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)).im) *
        HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 =
      -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det

Tactic:
simp [num, denom, Complex.ext_iff, htrace, Matrix.det_fin_two, field]

Premises used: Complex.ext_iff, UpperHalfPlane.denom, Matrix.det_fin_two, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
htrace : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ -((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 * z.re) + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 =
      z.re * (z.re * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) +
        (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * HPow.hPow (β := ℕ) z.im 2 ↔
    HPow.hPow (β := ℕ) (z.re * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 +
        HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 * HPow.hPow (β := ℕ) z.im 2 =
      (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 +
        HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
hy : 0 ≤ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2
hx : 0 ≤ -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det / HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2
hy₁ : 0 ≤ dist (↑z : ℂ) (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
⊢ g • z = z ↔
    dist (↑z : ℂ) (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) =
      √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0|

Tactic:
rw [gl_smul_eq_self_iff_dist_sq_eq h htrace hc, eq_comm, ← Real.sqrt_eq_iff_eq_sq, eq_comm,
    Real.sqrt_div', Real.sqrt_sq_eq_abs]

Premises used: Real.sqrt_eq_iff_eq_sq, Real.sqrt_sq_eq_abs, Real.sqrt_div', eq_comm, UpperHalfPlane.gl_smul_eq_self_iff_dist_sq_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
hy hy₁ hy₂ hy₃ :
  0 < -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det → 0 ≤ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2
⊢ 0 ≤ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2

Tactic:
positivity [neg_pos.mpr h]

Premises used: Iff.mpr, neg_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
hx hx₁ hx₂ hx₃ :
  0 < -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det →
    0 ≤ -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det / HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2
⊢ 0 ≤ -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det / HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2

Tactic:
positivity [neg_pos.mpr h]

Premises used: Iff.mpr, neg_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
hy hy₁ hy₂ 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) : ℂ))
⊢ 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]

Premises used: Iff.mpr, neg_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
mpr : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0 → ∃ (z : ℍ), g • z = z
⊢ (∃ (z : ℍ), g • z = z) ↔ (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 +
        (HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (denom g (↑z : ℂ))).im / z.im -
      (0 + (num g (↑z : ℂ)).im / z.im) =
    0

Tactic:
simp [σ, h.not_gt, num, denom, z.im_ne_zero, Matrix.trace_fin_two, field]

Premises used: UpperHalfPlane.im_ne_zero, Matrix.trace_fin_two, UpperHalfPlane.denom, LT.lt.not_gt, UpperHalfPlane.σ, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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 +
        (HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) (denom g (↑z : ℂ))).im / z.im -
      (0 + (num g (↑z : ℂ)).im / z.im) =
    0

Tactic:
{ simp [σ, h.not_gt, num, denom, z.im_ne_zero, Matrix.trace_fin_two, field] }

Premises used: UpperHalfPlane.im_ne_zero, Matrix.trace_fin_two, UpperHalfPlane.denom, LT.lt.not_gt, UpperHalfPlane.σ, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
z : ℍ
hz : g • z = z
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
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 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)

Premises used: UpperHalfPlane.im_ne_zero, Matrix.trace_fin_two, UpperHalfPlane.denom, UpperHalfPlane.im, LT.lt.not_gt, UpperHalfPlane.σ, UpperHalfPlane.num