awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z w : ℂ
rw : ¬(z.re < w.re ∧ z.im = w.im) ↔ w.re ≤ z.re ∨ z.im ≠ w.im
rw₁ : ¬z.re < w.re ∨ ¬z.im = w.im ↔ w.re ≤ z.re ∨ z.im ≠ w.im
rw₂ rw₃ : w.re ≤ z.re ∨ ¬z.im = w.im ↔ w.re ≤ z.re ∨ z.im ≠ w.im
⊢ ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im

Tactic:
rw [lt_def, not_and_or, not_lt]

Premises used: not_lt, not_and_or, Complex.lt_def
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ ¬z ≤ 0 ↔ 0 < z.re ∨ z.im ≠ 0

Tactic:
not_le_iff

Premises used: Complex.not_le_iff
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ ¬z < 0 ↔ 0 ≤ z.re ∨ z.im ≠ 0

Tactic:
not_lt_iff

Premises used: Complex.not_lt_iff
-- Module: Mathlib.Analysis.Complex.Order
Goal:
r : ℝ
z : ℂ
hz : (↑r : ℂ) ≤ z
rw : (↑z.re : ℂ) = z
rw₁ : (starRingEnd ℂ : (a : ℂ) → ℂ) z = z
rw₂ : z.im = 0
rw₃ : (↑r : ℂ).im = 0
rw₄ rw₅ : Eq (α := ℝ) 0 0
⊢ z = (↑z.re : ℂ)

Tactic:
rw [eq_comm, ← conj_eq_iff_re, conj_eq_iff_im, ← (Complex.le_def.1 hz).2, Complex.ofReal_im]

Premises used: Complex.conj_eq_iff_re, eq_comm, And.right, Iff.mp, Complex.conj_eq_iff_im, Complex.ofReal_im, Complex.le_def
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
this : 0 ≤ ‖z‖
h : 0 ≤ z
h₁ : re 0 ≤ z.re
h₂ : im 0 = z.im
rw : z.re = |z.re|
rw₁ rw₂ : z.re = z.re
⊢ z.re = ‖z‖

Tactic:
rw [← abs_re_eq_norm.2 h₂.symm, abs_of_nonneg h₁]

Premises used: Iff.mpr, Complex.abs_re_eq_norm, abs_of_nonneg, Eq.symm
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
rw : 0 ≤ -z ↔ z ≤ 0
⊢ -z.re = ‖z‖ ↔ z ≤ 0

Tactic:
rw [← neg_re, ← norm_neg z, re_eq_norm]

Premises used: Complex.neg_re, norm_neg, Complex.re_eq_norm
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ 0 ≤ -z ↔ z ≤ 0

Tactic:
neg_nonneg.and <| eq_comm.trans neg_eq_zero

Premises used: neg_eq_zero, eq_comm, neg_nonneg, Iff.and, Iff.trans
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
⊢ 0 ≤ -z ↔ z ≤ 0

Tactic:
exact neg_nonneg.and <| eq_comm.trans neg_eq_zero

Premises used: neg_eq_zero, eq_comm, neg_nonneg, Iff.and, Iff.trans
-- Module: Mathlib.Analysis.Complex.Order
Goal:
z : ℂ
rw : -z.re = ‖z‖ ↔ z ≤ 0
rw₁ rw₂ : z ≤ 0 ↔ z ≤ 0
⊢ z.re = -‖z‖ ↔ z ≤ 0

Tactic:
rw [← neg_eq_iff_eq_neg, neg_re_eq_norm]

Premises used: neg_eq_iff_eq_neg, Complex.neg_re_eq_norm
-- Module: Mathlib.Analysis.Complex.Order
Goal:
x y : ℝ
hxy : x ≤ y
⊢ (↑x : ℂ) ≤ (↑y : ℂ)

Tactic:
simp only [real_le_real, hxy]

Premises used: Complex.real_le_real
-- Module: Mathlib.Analysis.Complex.Order
Goal:
x : ℝ
hx : 0 < x
⊢ 0 < (↑x : ℂ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Order
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 0 ≤ (↑x : ℂ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Order
Goal:
x : ℝ
hx : x ≠ 0
⊢ (↑x : ℂ) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
z : ℂ
⊢ ‖𝕢 h z‖ = rexp (-2 * π * z.im / h)

Tactic:
simp only [qParam, norm_exp, div_ofReal_re, mul_re, re_ofNat, ofReal_re, im_ofNat, ofReal_im,
    mul_zero, sub_zero, I_re, mul_im, zero_mul, add_zero, I_im, mul_one, sub_self, zero_sub,
    neg_mul]

Premises used: Complex.mul_im, Complex.div_ofReal_re, Function.Periodic.qParam, Complex.mul_re, sub_self, sub_zero, MulZeroClass.zero_mul, Complex.I_re, Complex.I_im, MulZeroClass.mul_zero, Complex.re_ofNat, Complex.norm_exp, Complex.ofReal_re, neg_mul, Complex.ofReal_im, mul_one, add_zero, zero_sub, Complex.im_ofNat
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
q : ℂ
⊢ (invQParam h q).im = -h / (2 * π) * Real.log ‖q‖

Tactic:
simp only [invQParam, ← div_div, div_I, neg_mul, neg_im, mul_im, mul_re, div_ofReal_re,
    div_ofNat_re, ofReal_re, I_re, mul_zero, div_ofReal_im, div_ofNat_im, ofReal_im, zero_div, I_im,
    mul_one, sub_self, zero_mul, add_zero, log_re, zero_add, neg_div]

Premises used: Complex.mul_im, Complex.div_ofReal_re, Complex.log_re, Complex.div_ofNat_im, neg_div, Complex.mul_re, sub_self, Function.Periodic.invQParam, MulZeroClass.zero_mul, zero_div, Complex.I_re, zero_add, Complex.I_im, MulZeroClass.mul_zero, Complex.div_ofNat_re, Complex.div_I, Complex.ofReal_re, Complex.div_ofReal_im, neg_mul, Complex.ofReal_im, div_div, mul_one, add_zero, Complex.neg_im
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : h ≠ 0
q : ℂ
hq : q ≠ 0
⊢ 𝕢 h (invQParam h q) = q

Tactic:
simp only [qParam, invQParam, ← mul_assoc, mul_div_cancel₀ _ two_pi_I_ne_zero,
    mul_div_cancel_left₀ _ (ofReal_ne_zero.mpr hh), exp_log hq]

Premises used: Iff.mpr, Function.Periodic.qParam, Function.Periodic.invQParam, Complex.two_pi_I_ne_zero, mul_assoc, Complex.ofReal_ne_zero, mul_div_cancel_left₀, mul_div_cancel₀, Complex.exp_log
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
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 : ℂ)
⊢ ∃ (m : ℤ), (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))) = z + (↑m : ℂ) * (↑h : ℂ)

Tactic:
obtain ⟨m, hm⟩ := log_exp_exists (2 * ↑π * I * z / ↑h)

Premises used: HMul.hMul, HDiv.hDiv, OfNat.ofNat, Complex.log_exp_exists, Complex.I
-- Module: Mathlib.Analysis.Complex.Periodic
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 : ℂ)
rw₈ rw₉ : z + (↑m : ℂ) * (↑h : ℂ) = z + (↑m : ℂ) * (↑h : ℂ)
⊢ (↑h : ℂ) / (2 * (↑π : ℂ) * I) * log (cexp (2 * (↑π : ℂ) * I * z / (↑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]

Premises used: Int.cast, div_mul_cancel₀, Complex.two_pi_I_ne_zero, mul_assoc, mul_div_assoc, mul_div_cancel₀, mul_comm, mul_add
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : h ≠ 0
z : ℂ
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:
refine ⟨m, by 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]⟩
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
A : ℝ
z : ℂ
rw : -2 * π < 0
⊢ ‖𝕢 h z‖ < rexp (-2 * π * A / h) ↔ A < z.im

Tactic:
rw [norm_qParam, Real.exp_lt_exp, div_lt_div_iff_of_pos_right hh, mul_lt_mul_left_of_neg]

Premises used: mul_lt_mul_left_of_neg, div_lt_div_iff_of_pos_right, Real.exp_lt_exp, Function.Periodic.norm_qParam
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
A : ℝ
z : ℂ
⊢ -2 * π < 0

Tactic:
simpa using Real.pi_pos

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
z : ℂ
⊢ 𝕢 h z ≠ 0

Tactic:
simp [qParam, exp_ne_zero]

Premises used: Function.Periodic.qParam, Complex.exp_ne_zero
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
⊢ Continuous (Y := ℂ) fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
m : WithTop ℕ∞
⊢ ContDiff ℂ (F := ℂ) m fun (z : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * z / (↑h : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (𝕢 h) I∞ (𝓝[≠] 0)

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_
    (.of_forall fun q ↦ exp_ne_zero _)

Premises used: Real.pi, HMul.hMul, Complex.exp_ne_zero, HDiv.hDiv, Filter.Eventually.of_forall, Complex.ofReal, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
refine : Tendsto (𝕢 h) I∞ (𝓝 0)
⊢ Tendsto (𝕢 h) I∞ (𝓝[≠] 0)

Tactic:
refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_
    (.of_forall fun q ↦ exp_ne_zero _)

Premises used: Filter.Eventually.of_forall, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
rw : Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖𝕢 h x‖) I∞ (𝓝 0)
⊢ Tendsto (𝕢 h) I∞ (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
simp : Tendsto (β := ℝ) (fun (x : ℂ) ↦ rexp (-2 * π * x.im / h)) I∞ (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖𝕢 h x‖) I∞ (𝓝 0)

Tactic:
simp only [norm_qParam]

Premises used: Function.Periodic.norm_qParam
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
apply : Tendsto (β := ℝ) (fun (y : ℝ) ↦ rexp (-2 * π * y / h)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ rexp (-2 * π * x.im / h)) I∞ (𝓝 0)

Tactic:
apply (tendsto_comap'_iff (m := fun y ↦ Real.exp (-2 * π * y / h)) (range_im ▸ univ_mem)).mpr

Premises used: Iff.mpr, Filter.tendsto_comap'_iff
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ rexp (-2 * π * y / h)) atTop (𝓝 0)

Tactic:
Real.tendsto_exp_atBot.comp (.atBot_div_const hh (tendsto_id.const_mul_atTop_of_neg ?_))

Premises used: Filter.tendsto_id, Real.exp, Real.tendsto_exp_atBot, Filter.Tendsto.atBot_div_const, Filter.Tendsto.const_mul_atTop_of_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
refine : -2 * π < 0
⊢ Tendsto (β := ℝ) (fun (y : ℝ) ↦ rexp (-2 * π * y / h)) atTop (𝓝 0)

Tactic:
refine Real.tendsto_exp_atBot.comp (.atBot_div_const hh (tendsto_id.const_mul_atTop_of_neg ?_))

Premises used: Filter.tendsto_id, Real.tendsto_exp_atBot, Filter.Tendsto.atBot_div_const, Filter.Tendsto.const_mul_atTop_of_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
⊢ -2 * π < 0

Tactic:
simpa using Real.pi_pos

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
simp : Tendsto (β := ℝ) (fun (x : ℂ) ↦ -h / (2 * π) * Real.log ‖x‖) (𝓝[≠] 0) atTop
⊢ Tendsto (invQParam h) (𝓝[≠] 0) I∞

Tactic:
simp only [tendsto_comap_iff, comp_def, im_invQParam]

Premises used: Function.Periodic.im_invQParam, Filter.tendsto_comap_iff, Function.comp_def
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
⊢ 0 < 2 * π

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
apply : Tendsto (β := ℝ) (fun (x : ℂ) ↦ Real.log ‖x‖) (𝓝[≠] 0) atBot
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ -h / (2 * π) * Real.log ‖x‖) (𝓝[≠] 0) atTop

Tactic:
apply Tendsto.const_mul_atBot_of_neg (div_neg_of_neg_of_pos (neg_lt_zero.mpr hh) (by positivity))

Premises used: Iff.mpr, Filter.Tendsto.const_mul_atBot_of_neg, neg_lt_zero, div_neg_of_neg_of_pos
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ Real.log ‖x‖) (𝓝[≠] 0) atBot

Tactic:
Real.tendsto_log_nhdsGT_zero.comp tendsto_norm_nhdsNE_zero

Premises used: Real.tendsto_log_nhdsGT_zero, Real.log, dite, tendsto_norm_nhdsNE_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
hh : 0 < h
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ Real.log ‖x‖) (𝓝[≠] 0) atBot

Tactic:
exact Real.tendsto_log_nhdsGT_zero.comp tendsto_norm_nhdsNE_zero

Premises used: Real.tendsto_log_nhdsGT_zero, tendsto_norm_nhdsNE_zero, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
q : ℂ
hq : q ≠ 0
⊢ cuspFunction h f q = f (invQParam h q)

Tactic:
update_of_ne hq ..

Premises used: Function.Periodic.cuspFunction, Function.update_of_ne
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
simp : limUnder (𝓝[≠] 0) (f ∘ invQParam h)
| cuspFunction h f 0

Tactic:
simp only [cuspFunction, update_self]

Premises used: Function.Periodic.cuspFunction, Function.update_self
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
conv_lhs : limUnder (𝓝[≠] 0) (f ∘ invQParam h) = limUnder (𝓝[≠] 0) (cuspFunction h f)
⊢ cuspFunction h f 0 = limUnder (𝓝[≠] 0) (cuspFunction h f)

Tactic:
conv_lhs => simp only [cuspFunction, update_self]

Premises used: Function.Periodic.cuspFunction, Function.update_self
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
⊢ limUnder (𝓝[≠] 0) (f ∘ invQParam h) = limUnder (𝓝[≠] 0) (cuspFunction h f)

Tactic:
congr_arg lim (Filter.map_congr <| eventuallyEq_nhdsWithin_of_eqOn fun r hr ↦ ?_)

Premises used: Filter.map_congr, congr_arg, Filter.lim, Filter.limUnder, eventuallyEq_nhdsWithin_of_eqOn
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
refine : ∀ (r : ℂ) (hr : Membership.mem (γ := Set ℂ) {0}ᶜ r), (f ∘ invQParam h) r = cuspFunction h f r
⊢ limUnder (𝓝[≠] 0) (f ∘ invQParam h) = limUnder (𝓝[≠] 0) (cuspFunction h f)

Tactic:
refine congr_arg lim (Filter.map_congr <| eventuallyEq_nhdsWithin_of_eqOn fun r hr ↦ ?_)

Premises used: Filter.map_congr, congr_arg, Filter.lim, eventuallyEq_nhdsWithin_of_eqOn
-- Module: Mathlib.Analysis.Complex.Periodic
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
rw₁ rw₂ : (f ∘ invQParam h) r = (f ∘ invQParam h) r
⊢ (f ∘ invQParam h) r = cuspFunction h f r

Tactic:
rw [cuspFunction, update_of_ne hr]

Premises used: Function.Periodic.cuspFunction, Function.update_of_ne
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
h₁ : 𝕢 h z ≠ 0
⊢ cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))

Tactic:
rw [cuspFunction, update_of_ne, comp_apply]

Premises used: Function.Periodic.cuspFunction, Function.comp_apply, Function.update_of_ne
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
⊢ 𝕢 h z ≠ 0

Tactic:
exp_ne_zero _

Premises used: Function.Periodic.qParam, Complex.exp_ne_zero
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
⊢ 𝕢 h z ≠ 0

Tactic:
exact exp_ne_zero _

Premises used: Complex.exp_ne_zero
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
⊢ 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 _
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
this : cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
obtain : ∀ (m : ℤ) (hm : invQParam h (𝕢 h z) = z + (↑m : ℂ) * (↑h : ℂ)), cuspFunction h f (𝕢 h z) = f z
⊢ cuspFunction h f (𝕢 h z) = f z

Tactic:
obtain ⟨m, hm⟩ := qParam_left_inv_mod_period hh z

Premises used: Function.Periodic.qParam_left_inv_mod_period
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
this : cuspFunction h f (𝕢 h z) = f (invQParam h (𝕢 h z))
m : ℤ
hm : invQParam h (𝕢 h z) = z + (↑m : ℂ) * (↑h : ℂ)
⊢ cuspFunction h f (𝕢 h z) = f z

Tactic:
simpa only [this, hm] using hf.int_mul m z

Premises used: Function.Periodic.int_mul
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hcts : ContinuousAt (cuspFunction h f) 0
apply : cuspFunction h f =ᶠ[𝓝[≠] 0] fun (x : ℂ) ↦ f (invQParam h x)
⊢ Tendsto (fun (x : ℂ) ↦ f (invQParam h x)) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))

Tactic:
apply (tendsto_nhdsWithin_of_tendsto_nhds hcts.tendsto).congr'

Premises used: tendsto_nhdsWithin_of_tendsto_nhds, ContinuousAt.tendsto, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hcts : ContinuousAt (cuspFunction h f) 0
a : ℂ
⊢ Membership.mem (γ := Set ℂ) {0}ᶜ a → cuspFunction h f a = f (invQParam h a)

Tactic:
cuspFunction_eq_of_nonzero h f

Premises used: Set.Mem, setOf, Function.Periodic.cuspFunction_eq_of_nonzero, Set.singleton, Not
-- Module: Mathlib.Analysis.Complex.Periodic
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
h₂ h₃ : ∀ (a : ℂ), Membership.mem (γ := Set ℂ) {0}ᶜ a → cuspFunction h f a = f (invQParam h a)
⊢ cuspFunction h f =ᶠ[𝓝[≠] 0] fun (x : ℂ) ↦ f (invQParam h x)

Tactic:
filter_upwards [self_mem_nhdsWithin] with a using cuspFunction_eq_of_nonzero h f

Premises used: Function.Periodic.cuspFunction_eq_of_nonzero, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
⊢ HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z

Tactic:
simpa only [id_eq, mul_one] using (((hasStrictDerivAt_id z).const_mul _).div_const _).cexp

Premises used: HasStrictDerivAt.const_mul, HasStrictDerivAt.cexp, HasStrictDerivAt.div_const, mul_one, hasStrictDerivAt_id, id_eq
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
⊢ 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
-- Module: Mathlib.Analysis.Complex.Periodic
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
⊢ 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)
-- Module: Mathlib.Analysis.Complex.Periodic
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 ℂ L q

Tactic:
have diff_L : DifferentiableAt ℂ L q :=
    (qdiff.to_localInverse diff_ne).hasStrictFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Complex.Periodic
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
⊢ 𝕢 h ∘ L =ᶠ[𝓝 q] id

Tactic:
have hL : 𝕢 h ∘ L =ᶠ[𝓝 q] (id : ℂ → ℂ) :=
    (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_right_inverse
-- Module: Mathlib.Analysis.Complex.Periodic
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
⊢ cuspFunction h f ∘ 𝕢 h ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id

Tactic:
have hF := hL.fun_comp (cuspFunction h f)
-- Module: Mathlib.Analysis.Complex.Periodic
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
⊢ 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)
-- Module: Mathlib.Analysis.Complex.Periodic
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
⊢ f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id

Tactic:
rw [this] at hF
-- Module: Mathlib.Analysis.Complex.Periodic
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
hF₁ : f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
⊢ cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L

Tactic:
rw [this] at hF
-- Module: Mathlib.Analysis.Complex.Periodic
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 ℂ f
    (HasStrictFDerivAt.localInverse (𝕢 h)
      ((ContinuousLinearEquiv.unitsEquivAut ℂ : (a : ℂˣ) → ℂ ≃L[ℂ] ℂ)
        (Units.mk0 (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) diff_ne))
      z ⋯ (𝕢 h z))

Tactic:
rw [← EventuallyEq.eq_of_nhds (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_left_inverse]
    at hol_z

Premises used: Filter.EventuallyEq.eq_of_nhds, HasStrictFDerivAt.eventually_left_inverse, HasStrictDerivAt.hasStrictFDerivAt_equiv
-- Module: Mathlib.Analysis.Complex.Periodic
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
hol_z₁ :
  DifferentiableAt ℂ f
    (HasStrictFDerivAt.localInverse (𝕢 h)
      ((ContinuousLinearEquiv.unitsEquivAut ℂ : (a : ℂˣ) → ℂ ≃L[ℂ] ℂ)
        (Units.mk0 (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) diff_ne))
      z ⋯ (𝕢 h z))
⊢ let L := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne;
  DifferentiableAt ℂ L q

Tactic:
rw [← EventuallyEq.eq_of_nhds (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_left_inverse]
    at hol_z

Premises used: Filter.EventuallyEq.eq_of_nhds, HasStrictFDerivAt.eventually_left_inverse, HasStrictDerivAt.hasStrictFDerivAt_equiv