awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
r : ℝ
z : ℂ
hz : (↑r : ℂ) ≤ z
rw : (↑z.re : ℂ) = z
rw₁ : (starRingEnd ℂ : (a : ℂ) → ℂ) z = z
rw₂ : z.im = 0
rw₃ : (↑r : ℂ).im = 0
⊢ z = (↑z.re : ℂ)
have rw₄ : Eq (α := ℝ) 0 0
Tactic: rw [eq_comm, ← conj_eq_iff_re, conj_eq_iff_im, ← (Complex.le_def.1 hz).2, Complex.ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z : ℂ
this : 0 ≤ ‖z‖
h : 0 ≤ z
h₁ : re 0 ≤ z.re
h₂ : im 0 = z.im
⊢ z.re = ‖z‖
have rw : z.re = |z.re|
Tactic: rw [← abs_re_eq_norm.2 h₂.symm, abs_of_nonneg h₁]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z : ℂ
this : 0 ≤ ‖z‖
h : 0 ≤ z
h₁ : re 0 ≤ z.re
h₂ : im 0 = z.im
rw : z.re = |z.re|
⊢ z.re = ‖z‖
have rw₁ : z.re = z.re
Tactic: rw [← abs_re_eq_norm.2 h₂.symm, abs_of_nonneg h₁]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z : ℂ
⊢ -z.re = ‖z‖ ↔ z ≤ 0
have rw : 0 ≤ -z ↔ z ≤ 0
Tactic: rw [← neg_re, ← norm_neg z, re_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z : ℂ
⊢ z.re = -‖z‖ ↔ z ≤ 0
have rw : -z.re = ‖z‖ ↔ z ≤ 0
Tactic: rw [← neg_eq_iff_eq_neg, neg_re_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Order (goal)
Goal:
z : ℂ
rw : -z.re = ‖z‖ ↔ z ≤ 0
⊢ z.re = -‖z‖ ↔ z ≤ 0
have rw₁ : z ≤ 0 ↔ z ≤ 0
Tactic: rw [← neg_eq_iff_eq_neg, neg_re_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
⊢ ∃ (m : ℤ), (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
have obtain : ∀ (m : ℤ)
  (hm : log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = 2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)),
  ∃ (m : ℤ), (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
Tactic: obtain ⟨m, hm⟩ := log_exp_exists (2 * ↑π * I * z / ↑h)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = 2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)
⊢ (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
have rw : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
  z + (↑m : ℂ) * (↑h : ℂ)
Tactic: rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
    div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = 2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)
rw :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
⊢ (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
have rw₁ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
  z + (↑m : ℂ) * (↑h : ℂ)
Tactic: rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
    div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = 2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)
rw :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₁ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
⊢ (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
have rw₂ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + 2 * (↑π : ℂ) * I * (↑m : ℂ)) =
  z + (↑m : ℂ) * (↑h : ℂ)
Tactic: rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
    div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = 2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)
rw :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₁ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₂ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + 2 * (↑π : ℂ) * I * (↑m : ℂ)) =
    z + (↑m : ℂ) * (↑h : ℂ)
⊢ (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
have rw₃ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ) + (↑m : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
Tactic: rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
    div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = 2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)
rw :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₁ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₂ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + 2 * (↑π : ℂ) * I * (↑m : ℂ)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₃ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ) + (↑m : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
⊢ (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
have rw₄ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I) * (z / (↑h : ℂ) + (↑m : ℂ)) = z + (↑m : ℂ) * (↑h : ℂ)
Tactic: rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
    div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = 2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)
rw :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₁ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₂ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + 2 * (↑π : ℂ) * I * (↑m : ℂ)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₃ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ) + (↑m : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
rw₄ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I) * (z / (↑h : ℂ) + (↑m : ℂ)) = z + (↑m : ℂ) * (↑h : ℂ)
⊢ (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
have rw₅ : (↑h : ℂ) * (z / (↑h : ℂ) + (↑m : ℂ)) = z + (↑m : ℂ) * (↑h : ℂ)
Tactic: rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
    div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = 2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)
rw :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₁ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₂ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + 2 * (↑π : ℂ) * I * (↑m : ℂ)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₃ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ) + (↑m : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
rw₄ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I) * (z / (↑h : ℂ) + (↑m : ℂ)) = z + (↑m : ℂ) * (↑h : ℂ)
rw₅ : (↑h : ℂ) * (z / (↑h : ℂ) + (↑m : ℂ)) = z + (↑m : ℂ) * (↑h : ℂ)
⊢ (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
have rw₆ : (↑h : ℂ) * (z / (↑h : ℂ)) + (↑h : ℂ) * (↑m : ℂ) = z + (↑m : ℂ) * (↑h : ℂ)
Tactic: rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
    div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = 2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)
rw :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₁ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₂ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + 2 * (↑π : ℂ) * I * (↑m : ℂ)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₃ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ) + (↑m : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
rw₄ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I) * (z / (↑h : ℂ) + (↑m : ℂ)) = z + (↑m : ℂ) * (↑h : ℂ)
rw₅ : (↑h : ℂ) * (z / (↑h : ℂ) + (↑m : ℂ)) = z + (↑m : ℂ) * (↑h : ℂ)
rw₆ : (↑h : ℂ) * (z / (↑h : ℂ)) + (↑h : ℂ) * (↑m : ℂ) = z + (↑m : ℂ) * (↑h : ℂ)
⊢ (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
have rw₇ : z + (↑h : ℂ) * (↑m : ℂ) = z + (↑m : ℂ) * (↑h : ℂ)
Tactic: rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
    div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
m : ℤ
hm : log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = 2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)
rw :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * z / (↑h : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₁ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + (↑m : ℂ) * (2 * (↑π : ℂ) * I)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₂ :
  (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ)) + 2 * (↑π : ℂ) * I * (↑m : ℂ)) =
    z + (↑m : ℂ) * (↑h : ℂ)
rw₃ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I * (z / (↑h : ℂ) + (↑m : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
rw₄ : (↑h : ℂ) / (2 * (↑π : ℂ) * I) * (2 * (↑π : ℂ) * I) * (z / (↑h : ℂ) + (↑m : ℂ)) = z + (↑m : ℂ) * (↑h : ℂ)
rw₅ : (↑h : ℂ) * (z / (↑h : ℂ) + (↑m : ℂ)) = z + (↑m : ℂ) * (↑h : ℂ)
rw₆ : (↑h : ℂ) * (z / (↑h : ℂ)) + (↑h : ℂ) * (↑m : ℂ) = z + (↑m : ℂ) * (↑h : ℂ)
rw₇ : z + (↑h : ℂ) * (↑m : ℂ) = z + (↑m : ℂ) * (↑h : ℂ)
⊢ (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)
have rw₈ : z + (↑m : ℂ) * (↑h : ℂ) = z + (↑m : ℂ) * (↑h : ℂ)
Tactic: rw [hm, mul_div_assoc, mul_comm (m : ℂ), ← mul_add, ← mul_assoc,
    div_mul_cancel₀ _ two_pi_I_ne_zero, mul_add, mul_div_cancel₀ _ (mod_cast hh), mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : 0 < h
A : ℝ
z : ℂ
⊢ ‖𝕢 h z‖ < rexp (-2 * π * A / h) ↔ A < z.im
have rw : -2 * π < 0
Tactic: rw [norm_qParam, Real.exp_lt_exp, div_lt_div_iff_of_pos_right hh, mul_lt_mul_left_of_neg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (𝕢 h) I∞ (𝓝[≠] 0)
have refine : Tendsto (𝕢 h) I∞ (𝓝 0)
Tactic: refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_
    (.of_forall fun q ↦ exp_ne_zero _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (𝕢 h) I∞ (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖𝕢 h x‖) I∞ (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖𝕢 h x‖) I∞ (𝓝 0)
have simp : Tendsto (β := ℝ) (fun (x : ℂ) ↦ rexp (-2 * π * x.im / h)) I∞ (𝓝 0)
Tactic: simp only [norm_qParam]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ rexp (-2 * π * x.im / h)) I∞ (𝓝 0)
have apply : Tendsto (β := ℝ) (fun (y : ℝ) ↦ rexp (-2 * π * y / h)) atTop (𝓝 0)
Tactic: apply (tendsto_comap'_iff (m := fun y ↦ Real.exp (-2 * π * y / h)) (range_im ▸ univ_mem)).mpr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ rexp (-2 * π * y / h)) atTop (𝓝 0)
have refine : -2 * π < 0
Tactic: refine Real.tendsto_exp_atBot.comp (.atBot_div_const hh (tendsto_id.const_mul_atTop_of_neg ?_))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (invQParam h) (𝓝[≠] 0) I∞
have simp : Tendsto (β := ℝ) (fun (x : ℂ) ↦ -h / (2 * π) * Real.log ‖x‖) (𝓝[≠] 0) atTop
Tactic: simp only [tendsto_comap_iff, comp_def, im_invQParam]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ -h / (2 * π) * Real.log ‖x‖) (𝓝[≠] 0) atTop
have apply : Tendsto (β := ℝ) (fun (x : ℂ) ↦ Real.log ‖x‖) (𝓝[≠] 0) atBot
Tactic: apply Tendsto.const_mul_atBot_of_neg (div_neg_of_neg_of_pos (neg_lt_zero.mpr hh) (by positivity))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
| cuspFunction h f 0
have simp : limUnder (𝓝[≠] 0) (f ∘ invQParam h)
Tactic: simp only [cuspFunction, update_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
⊢ cuspFunction h f 0 = limUnder (𝓝[≠] 0) (cuspFunction h f)
have conv_lhs : limUnder (𝓝[≠] 0) (f ∘ invQParam h) = limUnder (𝓝[≠] 0) (cuspFunction h f)
Tactic: conv_lhs => simp only [cuspFunction, update_self]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
⊢ limUnder (𝓝[≠] 0) (f ∘ invQParam h) = limUnder (𝓝[≠] 0) (cuspFunction h f)
have refine : ∀ (r : ℂ) (hr : Membership.mem (γ := Set ℂ) {0}ᶜ r), (f ∘ invQParam h) r = cuspFunction h f r
Tactic: refine congr_arg lim (Filter.map_congr <| eventuallyEq_nhdsWithin_of_eqOn fun r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
r : ℂ
hr : Membership.mem (γ := Set ℂ) {0}ᶜ r
⊢ (f ∘ invQParam h) r = cuspFunction h f r
have rw : (f ∘ invQParam h) r = update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) r
Tactic: rw [cuspFunction, update_of_ne hr]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
r : ℂ
hr : Membership.mem (γ := Set ℂ) {0}ᶜ r
rw : (f ∘ invQParam h) r = update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)) r
⊢ (f ∘ invQParam h) r = cuspFunction h f r
have rw₁ : (f ∘ invQParam h) r = (f ∘ invQParam h) r
Tactic: rw [cuspFunction, update_of_ne hr]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
⊢ cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
have h₁ : 𝕢 h z ≠ 0
Tactic: rw [cuspFunction, update_of_ne, comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
⊢ cuspFunction h f (𝕢 h z) = f z
have this : cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
Tactic: have : (cuspFunction h f) (𝕢 h z) = f (invQParam h (𝕢 h z)) := by
    rw [cuspFunction, update_of_ne, comp_apply]
    exact exp_ne_zero _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
this : cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
⊢ cuspFunction h f (𝕢 h z) = f z
have obtain : ∀ (m : ℤ) (hm : invQParam h (𝕢 h z) = z + (↑m : ℂ) * (↑h : ℂ)), cuspFunction h f (𝕢 h z) = f z
Tactic: obtain ⟨m, hm⟩ := qParam_left_inv_mod_period hh z
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hcts : ContinuousAt (cuspFunction h f) 0
⊢ Tendsto (fun (x : ℂ) ↦ f (invQParam h x)) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))
have apply : cuspFunction h f =ᶠ[𝓝[≠] 0] fun (x : ℂ) ↦ f (invQParam h x)
Tactic: apply (tendsto_nhdsWithin_of_tendsto_nhds hcts.tendsto).congr'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hcts : ContinuousAt (cuspFunction h f) 0
⊢ cuspFunction h f =ᶠ[𝓝[≠] 0] fun (x : ℂ) ↦ f (invQParam h x)
have h₁ : ∀ (a : ℂ),
  Membership.mem (γ := Set ℂ)
    {x : ℂ |
      Membership.mem (γ := Set ℂ) {0}ᶜ x →
        Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ cuspFunction h f x = (fun (x : ℂ) ↦ f (invQParam h x)) x) x}
          x}
    a
Tactic: filter_upwards [self_mem_nhdsWithin] with a using cuspFunction_eq_of_nonzero h f
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hcts : ContinuousAt (cuspFunction h f) 0
h₁ :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {0}ᶜ x →
          Membership.mem (γ := Set ℂ)
            {x : ℂ | (fun (x : ℂ) ↦ cuspFunction h f x = (fun (x : ℂ) ↦ f (invQParam h x)) x) x} x}
      a
⊢ cuspFunction h f =ᶠ[𝓝[≠] 0] fun (x : ℂ) ↦ f (invQParam h x)
have h₂ : ∀ (a : ℂ), Membership.mem (γ := Set ℂ) {0}ᶜ a → cuspFunction h f a = f (invQParam h a)
Tactic: filter_upwards [self_mem_nhdsWithin] with a using cuspFunction_eq_of_nonzero h f
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
have qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z
Tactic: have qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * π * I / h)) z := by
    simpa only [id_eq, mul_one] using (((hasStrictDerivAt_id z).const_mul _).div_const _).cexp
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
have diff_ne : q * (2 * (↑π : ℂ) * I / (↑h : ℂ)) ≠ 0
Tactic: have diff_ne : q * (2 * π * I / h) ≠ 0 :=
    mul_ne_zero (exp_ne_zero _) (div_ne_zero two_pi_I_ne_zero <| mod_cast hh)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z
diff_ne : q * (2 * (↑π : ℂ) * I / (↑h : ℂ)) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
have diff_L : DifferentiableAt ℂ L q
Tactic: have diff_L : DifferentiableAt ℂ L q :=
    (qdiff.to_localInverse diff_ne).hasStrictFDerivAt.differentiableAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z
diff_ne : q * (2 * (↑π : ℂ) * I / (↑h : ℂ)) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
have hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
Tactic: have hL : 𝕢 h ∘ L =ᶠ[𝓝 q] (id : ℂ → ℂ) :=
    (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_right_inverse
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z
diff_ne : q * (2 * (↑π : ℂ) * I / (↑h : ℂ)) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
have hF : cuspFunction h f ∘ 𝕢 h ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
Tactic: have hF := hL.fun_comp (cuspFunction h f)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z
diff_ne : q * (2 * (↑π : ℂ) * I / (↑h : ℂ)) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
hF : cuspFunction h f ∘ 𝕢 h ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
have this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
Tactic: have : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L := funext fun z ↦ eq_cuspFunction hh hf (L z)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z
diff_ne : q * (2 * (↑π : ℂ) * I / (↑h : ℂ)) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
hF : cuspFunction h f ∘ 𝕢 h ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
have hF₁ : f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
Tactic: rw [this] at hF
Cleared hypotheses: hF, this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (hypothesis)
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z
diff_ne : q * (2 * (↑π : ℂ) * I / (↑h : ℂ)) ≠ 0
L : ℂ → ℂ := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne
diff_L : DifferentiableAt ℂ L q
hL : 𝕢 h ∘ L =ᶠ[𝓝 q] id
hF : f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
this : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)
have hol_z₁ : DifferentiableAt ℂ f
  (HasStrictFDerivAt.localInverse (𝕢 h)
    ((ContinuousLinearEquiv.unitsEquivAut ℂ : (a : ℂˣ) → ℂ ≃L[ℂ] ℂ)
      (Units.mk0 (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) diff_ne))
    z sorry (𝕢 h z))
Tactic: rw [← EventuallyEq.eq_of_nhds (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_left_inverse]
    at hol_z
Cleared hypotheses: hol_z, L, diff_L, hL, hF, this
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
⊢ ∀ᶠ (q : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) q
have refine : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ f (invQParam h x) → DifferentiableAt ℂ (cuspFunction h f) x
Tactic: refine ((invQParam_tendsto hh).eventually h_hol).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Periodic (goal)
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ f (invQParam h x) → DifferentiableAt ℂ (cuspFunction h f) x
have refine : ∀ (q : ℂ) (hq : Membership.mem (γ := Set ℂ) {0}ᶜ q) (h_diff : DifferentiableAt ℂ f (invQParam h q)),
  DifferentiableAt ℂ (cuspFunction h f) q
Tactic: refine eventually_nhdsWithin_of_forall (fun q hq h_diff ↦ ?_)