awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UnitDisc.Basic (goal)
Goal:
n : ℕ+
⊢ Continuous (Y := 𝔻) fun (x : 𝔻) ↦ x ^ n
have simp : Continuous (Y := ℂ) fun (x : 𝔻) ↦ (↑x : ℂ) ^ (↑n : ℕ)
Tactic: simp only [isEmbedding_coe.continuous_iff, Function.comp_def, coe_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UnitDisc.Basic (goal)
Goal:
z : 𝔻
n : ℕ+
⊢ z ^ n = 0 ↔ z = 0
have rw : (↑z : ℂ) ^ (↑n : ℕ) = (↑0 : ℂ) ↔ z = 0
Tactic: rw [← coe_inj, coe_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UnitDisc.Basic (goal)
Goal:
z : 𝔻
⊢ Tendsto (β := 𝔻) (fun (n : ℕ+) ↦ z ^ n) atTop (𝓝 0)
have simp : Tendsto (fun (x : ℕ+) ↦ (↑z : ℂ) ^ (↑x : ℕ)) atTop (𝓝 (↑0 : ℂ))
Tactic: simp only [isEmbedding_coe.tendsto_nhds_iff, comp_def, coe_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UnitDisc.Basic (goal)
Goal:
z : 𝔻
⊢ star (star z) = z
have a : (↑(star (star z)) : ℂ) = (↑z : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Basic (goal)
Goal:
⊢ HPow.hPow (β := ℕ) (↑ρ : ℂ) 2 = -(↑ρ : ℂ) - 1
have simp : -1 / 2 * (-1 / 2) - √3 / 2 * (√3 / 2) = -(-1 / 2) - 1 ∧ -1 / 2 * (√3 / 2) + √3 / 2 * (-1 / 2) = -(√3 / 2)
Tactic: simp [Complex.ext_iff, pow_two, ρ]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Basic (hypothesis)
Goal:
τ τ' : ℍ
hre : τ.re = τ'.re
hnorm : ‖(↑τ : ℂ)‖ = ‖(↑τ' : ℂ)‖
⊢ τ = τ'
have hnorm₁ : HPow.hPow (β := ℕ) ‖(↑τ : ℂ)‖ 2 = HPow.hPow (β := ℕ) ‖(↑τ' : ℂ)‖ 2
Tactic: apply_fun (· ^ 2) at hnorm
Cleared hypotheses: hnorm
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Basic (goal)
Goal:
z : ℍ
⊢ LT.lt (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
have rw : (↑z : ℂ) ≠ 0
Tactic: rw [Complex.normSq_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
z : ℍ
⊢ 0 < (-(↑n : ℂ) / (↑z : ℂ)).im
have suffices : 0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
Tactic: suffices 0 < n * z.im / Complex.normSq z by simpa [Complex.div_im, neg_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
z : ℍ
⊢ 0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
have positivity : n ≠ 0 → 0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
Tactic: positivity [NeZero.ne n, z.normSq_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
z : ℍ
positivity positivity₁ positivity₂ :
  n ≠ 0 → 0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
⊢ 0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
have positivity₃ : n ≠ 0 →
  LT.lt (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) →
    0 < HDiv.hDiv (β := ℝ) ((↑n : ℝ) * z.im) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
Tactic: positivity [NeZero.ne n, z.normSq_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Basic (goal)
Goal:
⊢ Set.range UpperHalfPlane.coe = ℍₒ
have h : ∀ (x : ℂ), x ∈ Set.range UpperHalfPlane.coe ↔ x ∈ ℍₒ
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
Goal:
ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa : ‖cexp (2 * (↑π : ℂ) * Complex.I * ξ / (↑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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
Goal:
ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
rwa : ‖cexp (2 * (↑π : ℂ) * Complex.I * ξ / (↑1 : ℂ))‖ ≤ rexp (-π)
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₁ : ‖cexp (2 * (↑π : ℂ) * Complex.I * ξ / 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
Goal:
ξ : ℂ
hξ : 1 / 2 ≤ ξ.im
rwa : ‖cexp (2 * (↑π : ℂ) * Complex.I * ξ / (↑1 : ℂ))‖ ≤ rexp (-π)
rwa₁ : ‖cexp (2 * (↑π : ℂ) * Complex.I * ξ / 1)‖ ≤ rexp (-π)
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₂ : ‖cexp (2 * (↑π : ℂ) * Complex.I * ξ)‖ ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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 (-π)
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₃ : rexp (2 * (↑π : ℂ) * Complex.I * ξ).re ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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 (-π)
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₄ : (2 * (↑π : ℂ) * Complex.I * ξ).re ≤ -π
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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 ≤ -π
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₅ : (2 * (↑π : ℂ) * ξ * Complex.I).re ≤ -π
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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 ≤ -π
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₆ : -(2 * (↑π : ℂ) * ξ).im ≤ -π
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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 ≤ -π
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₇ : π ≤ (2 * (↑π : ℂ) * ξ).im
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₈ : π ≤ ((↑2 : ℂ) * (↑π : ℂ) * ξ).im
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₉ : π ≤ ((↑(2 * π) : ℂ) * ξ).im
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₁₀ : π ≤ 2 * π * ξ.im
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₁₁ : π ≤ π * 2 * ξ.im
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₁₂ : π ≤ π * (2 * ξ.im)
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
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)
⊢ ‖𝕢 1 ξ‖ ≤ rexp (-π)
have rwa₁₃ : 1 ≤ 2 * ξ.im
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Exp (goal)
Goal:
n : ℕ
inst : NeZero n
τ : ℍ
⊢ ‖𝕢 (↑n : ℝ) (↑τ : ℂ)‖ < 1
have rw : 0 < 2 * π * τ.im
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 _)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
z w : ℍ
⊢ g • z = w ↔ num g (↑z : ℂ) = HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (↑w : ℂ) : ℂ) (denom g (↑z : ℂ))
have rw : g • z = w ↔
  Eq (α := ℂ) (((σ g).toAlgEquiv : (a : ℂ) → ℂ) (num g (↑z : ℂ)) : ℂ)
    (((σ g).toAlgEquiv : (a : ℂ) → ℂ) (HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (↑w : ℂ) : ℂ) (denom g (↑z : ℂ))) : ℂ)
Tactic: rw [← (σ g).injective.eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
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 • z = z ↔ z.re = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1)
have htrace₁ : (↑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
Cleared hypotheses: htrace, hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
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 • z = z ↔ z.re = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1)
have h₀ : (↑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
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
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 • z = z ↔ z.re = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1)
have h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
Tactic: have h : g.val.det < 0 := by simp [Matrix.det_fin_two, *]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
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
⊢ g • z = z ↔ z.re = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1)
have 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
Tactic: simp [gl_smul_eq_iff_num_eq, Complex.ext_iff, htrace, hc, num, denom, σ, h.not_gt, mul_comm,
    eq_div_iff, h₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
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 • 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
have htrace₁ : (↑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
Cleared hypotheses: htrace, hc
-- 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) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ 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
have 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
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]
-- 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) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ 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
have 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
Tactic: simp [num, denom, Complex.ext_iff, htrace, Matrix.det_fin_two, field]
-- 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
⊢ 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|
have hy : 0 ≤ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2
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]
-- 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
hy : 0 ≤ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2
⊢ 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|
have hx : 0 ≤ -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det / HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2
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]
-- 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
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
⊢ 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|
have hy₁ : 0 ≤ dist (↑z : ℂ) (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) / (↑((↑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]
-- 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 ≤ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2
have hy : 0 < -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det → 0 ≤ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2
Tactic: positivity [neg_pos.mpr h]
-- 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 ≤ -(↑g : Matrix (Fin 2) (Fin 2) ℝ).det / HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2
have 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
Tactic: positivity [neg_pos.mpr h]