awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
diff_L₁ :
  let L := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne;
  DifferentiableAt ℂ L q
⊢ let L := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne;
  𝕢 h ∘ L =ᶠ[𝓝 q] id

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))
diff_L₁ :
  let L := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne;
  DifferentiableAt ℂ L q
hL₁ :
  let L := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne;
  𝕢 h ∘ L =ᶠ[𝓝 q] id
⊢ let L := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne;
  f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id

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))
diff_L₁ :
  let L := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne;
  DifferentiableAt ℂ L q
hL₁ :
  let L := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne;
  𝕢 h ∘ L =ᶠ[𝓝 q] id
hF₁ :
  let L := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne;
  f ∘ L =ᶠ[𝓝 q] cuspFunction h f ∘ id
⊢ let L := HasStrictDerivAt.localInverse (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z qdiff diff_ne;
  cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L

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 : ℂ
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z
diff_ne : q * (2 * (↑π : ℂ) * I / (↑h : ℂ)) ≠ 0
hol_z :
  DifferentiableAt ℂ f
    (HasStrictFDerivAt.localInverse (𝕢 h)
      ((ContinuousLinearEquiv.unitsEquivAut ℂ : (a : ℂˣ) → ℂ ≃L[ℂ] ℂ)
        (Units.mk0 (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) diff_ne))
      z ⋯ (𝕢 h z))
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)

Tactic:
(hol_z.comp q diff_L).congr_of_eventuallyEq hF.symm

Premises used: DifferentiableAt.congr_of_eventuallyEq, DifferentiableAt.comp, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f (↑h : ℂ)
z : ℂ
q : ℂ := 𝕢 h z
qdiff : HasStrictDerivAt (𝕢 h) (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) z
diff_ne : q * (2 * (↑π : ℂ) * I / (↑h : ℂ)) ≠ 0
hol_z :
  DifferentiableAt ℂ f
    (HasStrictFDerivAt.localInverse (𝕢 h)
      ((ContinuousLinearEquiv.unitsEquivAut ℂ : (a : ℂˣ) → ℂ ≃L[ℂ] ℂ)
        (Units.mk0 (q * (2 * (↑π : ℂ) * I / (↑h : ℂ))) diff_ne))
      z ⋯ (𝕢 h z))
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)

Tactic:
exact (hol_z.comp q diff_L).congr_of_eventuallyEq hF.symm

Premises used: DifferentiableAt.congr_of_eventuallyEq, DifferentiableAt.comp, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Complex.Periodic
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

Tactic:
((invQParam_tendsto hh).eventually h_hol).mp ?_

Premises used: Filter.Eventually.mp, Function.Periodic.invQParam_tendsto, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
refine : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ f (invQParam h x) → DifferentiableAt ℂ (cuspFunction h f) x
⊢ ∀ᶠ (q : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) q

Tactic:
refine ((invQParam_tendsto hh).eventually h_hol).mp ?_

Premises used: Filter.Eventually.mp, Function.Periodic.invQParam_tendsto, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Complex.Periodic
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

Tactic:
eventually_nhdsWithin_of_forall (fun q hq h_diff ↦ ?_)

Premises used: eventually_nhdsWithin_of_forall
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
refine :
  ∀ (q : ℂ) (hq : Membership.mem (γ := Set ℂ) {0}ᶜ q) (h_diff : DifferentiableAt ℂ f (invQParam h q)),
    DifferentiableAt ℂ (cuspFunction h f) q
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ f (invQParam h x) → DifferentiableAt ℂ (cuspFunction h f) x

Tactic:
refine eventually_nhdsWithin_of_forall (fun q hq h_diff ↦ ?_)

Premises used: eventually_nhdsWithin_of_forall
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
q : ℂ
hq : Membership.mem (γ := Set ℂ) {0}ᶜ q
h_diff : DifferentiableAt ℂ f (invQParam h q)
rw : DifferentiableAt ℂ (cuspFunction h f) (𝕢 h (invQParam h q))
⊢ DifferentiableAt ℂ (cuspFunction h f) q

Tactic:
rw [← qParam_right_inv hh.ne' hq]

Premises used: Function.Periodic.qParam_right_inv, LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
q : ℂ
hq : Membership.mem (γ := Set ℂ) {0}ᶜ q
h_diff : DifferentiableAt ℂ f (invQParam h q)
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h (invQParam h q))

Tactic:
differentiableAt_cuspFunction hh.ne' hf h_diff

Premises used: Function.Periodic.differentiableAt_cuspFunction, LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
q : ℂ
hq : Membership.mem (γ := Set ℂ) {0}ᶜ q
h_diff : DifferentiableAt ℂ f (invQParam h q)
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h (invQParam h q))

Tactic:
exact differentiableAt_cuspFunction hh.ne' hf h_diff

Premises used: Function.Periodic.differentiableAt_cuspFunction, LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_zer : I∞.ZeroAtFilter f
⊢ cuspFunction h f 0 = 0

Tactic:
simpa only [cuspFunction, update_self] using (h_zer.comp (invQParam_tendsto hh)).limUnder_eq

Premises used: Function.Periodic.cuspFunction, Function.Periodic.invQParam_tendsto, Filter.Tendsto.comp, Function.update_self, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
obtain :
  ∀ (c : ℝ) (t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, ‖cuspFunction h f x‖ ≤ c * norm (E := ℝ) (1 x)),
    DifferentiableAt ℂ (cuspFunction h f) 0
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

Tactic:
obtain ⟨c, t⟩ := (boundedAtFilter_cuspFunction hh h_bd).bound

Premises used: Function.Periodic.boundedAtFilter_cuspFunction, Asymptotics.IsBigO.bound
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, ‖cuspFunction h f x‖ ≤ c * norm (E := ℝ) (1 x)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c * norm (E := ℝ) (1 x)

Tactic:
replace t := (eventually_differentiableAt_cuspFunction_nhds_ne_zero hh hf h_hol).and t
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c * norm (E := ℝ) (1 x)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c

Tactic:
simp only [norm_one, Pi.one_apply, mul_one] at t

Premises used: Pi.one_apply, NormOneClass.norm_one, mul_one
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
obtain :
  ∀ (S : Set ℂ)
    (hS1 :
      ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c)
    (hS2 : IsOpen S) (hS3 : 0 ∈ S), DifferentiableAt ℂ (cuspFunction h f) 0
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

Tactic:
obtain ⟨S, hS1, hS2, hS3⟩ := eventually_nhds_iff.mp (eventually_nhdsWithin_iff.mp t)

Premises used: eventually_nhds_iff, eventually_nhdsWithin_iff, Iff.mp
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
⊢ DifferentiableOn ℂ (cuspFunction h f) (S \ {0})

Tactic:
have h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0}) :=
    fun x hx ↦ (hS1 x hx.1 hx.2).1.differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
h₁ : c ∈ upperBounds (norm ∘ cuspFunction h f '' (S \ {0}))
⊢ BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))

Tactic:
use c
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
h₁ : ∀ (x : ℝ), ∀ x_1 ∈ S, x_1 ∉ {0} → (norm ∘ cuspFunction h f) x_1 = x → x ≤ c
⊢ c ∈ upperBounds (norm ∘ cuspFunction h f '' (S \ {0}))

Tactic:
simp only [mem_upperBounds, Set.mem_image, Set.mem_diff, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_image, forall_exists_index, Set.mem_diff, mem_upperBounds
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
y : ℝ
q : ℂ
hq : q ∈ S
hq2 : q ∉ {0}
hy : (norm ∘ cuspFunction h f) q = y
⊢ y ≤ c

Tactic:
simpa only [← hy, norm_one, mul_one] using (hS1 q hq hq2).2

Premises used: NormOneClass.norm_one, And.right, mul_one
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
⊢ BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))

Tactic:
have hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0})) := by
    use c
    simp only [mem_upperBounds, Set.mem_image, Set.mem_diff, forall_exists_index, and_imp]
    intro y q hq hq2 hy
    simpa only [← hy, norm_one, mul_one] using (hS1 q hq hq2).2
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))
⊢ DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (limUnder (𝓝[≠] 0) (cuspFunction h f))) S

Tactic:
have := differentiableOn_update_limUnder_of_bddAbove (IsOpen.mem_nhds hS2 hS3) h_diff hF_bd
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))
this : DifferentiableOn ℂ (update (β := fun (a : ℂ) ↦ ℂ) (cuspFunction h f) 0 (limUnder (𝓝[≠] 0) (cuspFunction h f))) S
⊢ DifferentiableOn ℂ (cuspFunction h f) S

Tactic:
rw [← cuspFunction_zero_eq_limUnder_nhds_ne, update_eq_self] at this

Premises used: Function.update_eq_self, Function.Periodic.cuspFunction_zero_eq_limUnder_nhds_ne
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))
this : DifferentiableOn ℂ (cuspFunction h f) S
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

Tactic:
this.differentiableAt (IsOpen.mem_nhds hS2 hS3)

Premises used: DifferentiableOn.differentiableAt, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
c : ℝ
t : ∀ᶠ (x : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (cuspFunction h f) x ∧ ‖cuspFunction h f x‖ ≤ c
S : Set ℂ
hS1 : ∀ y ∈ S, Membership.mem (γ := Set ℂ) {0}ᶜ y → DifferentiableAt ℂ (cuspFunction h f) y ∧ ‖cuspFunction h f y‖ ≤ c
hS2 : IsOpen S
hS3 : 0 ∈ S
h_diff : DifferentiableOn ℂ (cuspFunction h f) (S \ {0})
hF_bd : BddAbove (norm ∘ cuspFunction h f '' (S \ {0}))
this : DifferentiableOn ℂ (cuspFunction h f) S
⊢ DifferentiableAt ℂ (cuspFunction h f) 0

Tactic:
exact this.differentiableAt (IsOpen.mem_nhds hS2 hS3)

Premises used: DifferentiableOn.differentiableAt, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
this : Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))
⊢ Tendsto f I∞ (𝓝 (cuspFunction h f 0))

Tactic:
simpa only [Function.comp_def, eq_cuspFunction hh.ne' hf] using this.comp (qParam_tendsto hh)

Premises used: Function.Periodic.eq_cuspFunction, LT.lt.ne', Function.comp_def, Function.Periodic.qParam_tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
suffices : Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))
⊢ Tendsto f I∞ (𝓝 (cuspFunction h f 0))

Tactic:
suffices Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 <| cuspFunction h f 0) by
    simpa only [Function.comp_def, eq_cuspFunction hh.ne' hf] using this.comp (qParam_tendsto hh)
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
⊢ Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds
    (differentiableAt_cuspFunction_zero hh hf h_hol h_bd).continuousAt.tendsto

Premises used: DifferentiableAt.continuousAt, tendsto_nhdsWithin_of_tendsto_nhds, ContinuousAt.tendsto, Function.Periodic.differentiableAt_cuspFunction_zero
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
⊢ Tendsto (cuspFunction h f) (𝓝[≠] 0) (𝓝 (cuspFunction h f 0))

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds
    (differentiableAt_cuspFunction_zero hh hf h_hol h_bd).continuousAt.tendsto

Premises used: DifferentiableAt.continuousAt, tendsto_nhdsWithin_of_tendsto_nhds, ContinuousAt.tendsto, Function.Periodic.differentiableAt_cuspFunction_zero
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_bd : I∞.BoundedAtFilter f
⊢ IsBigO (E := ℂ) (F := ℝ) I∞ (fun (z : ℂ) ↦ f z - cuspFunction h f 0) fun (z : ℂ) ↦ rexp (-2 * π * z.im / h)

Tactic:
simpa [comp_def, eq_cuspFunction hh.ne' hf, norm_qParam] using
    differentiableAt_cuspFunction_zero hh hf h_hol h_bd |>.isBigO_sub.mono
      nhdsWithin_le_nhds |>.comp_tendsto (qParam_tendsto hh) |>.norm_right

Premises used: DifferentiableAt.isBigO_sub, Function.Periodic.eq_cuspFunction, LT.lt.ne', Function.comp_def, nhdsWithin_le_nhds, Function.Periodic.qParam_tendsto, Asymptotics.IsBigO.mono, Function.Periodic.norm_qParam, Asymptotics.IsBigO.comp_tendsto, Asymptotics.IsBigO.norm_right, Function.Periodic.differentiableAt_cuspFunction_zero
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
hf : Periodic f (↑h : ℂ)
h_hol : ∀ᶠ (z : ℂ) in I∞, DifferentiableAt ℂ f z
h_zer : I∞.ZeroAtFilter f
⊢ IsBigO (F := ℝ) I∞ f fun (z : ℂ) ↦ rexp (-2 * π * z.im / h)

Tactic:
simpa [cuspFunction_zero_of_zero_at_inf hh h_zer, sub_zero] using
    exp_decay_sub_of_bounded_at_inf hh hf h_hol h_zer.boundedAtFilter

Premises used: sub_zero, Function.Periodic.cuspFunction_zero_of_zero_at_inf, Filter.ZeroAtFilter.boundedAtFilter, Function.Periodic.exp_decay_sub_of_bounded_at_inf
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
a : ℂ
h₁ :
  ∀ (y : ℂ),
    update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) y =
      (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) y
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) =
    a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))

Tactic:
ext y
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
a y : ℂ
h₁ :
  update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) 0 =
    (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
h₂ :
  ∀ (hy : y ≠ 0),
    update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) y =
      (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) y
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) y =
    (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) y

Tactic:
obtain rfl | hy := eq_or_ne y 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
a : ℂ
⊢ Tendsto (fun (x : ℂ) ↦ f (invQParam h x)) (𝓝[≠] 0) (𝓝 (limUnder (𝓝[≠] 0) (f ∘ invQParam h)))

Tactic:
simpa using hfcts
-- Module: Mathlib.Analysis.Complex.Periodic
Goal:
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0
a : ℂ
⊢ update (β := fun (a : ℂ) ↦ ℂ) ((a • f) ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) ((a • f) ∘ invQParam h)) 0 =
    (a • update (β := fun (a : ℂ) ↦ ℂ) (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))) 0

Tactic:
simpa using (Tendsto.const_mul _ (by simpa using hfcts)).limUnder_eq

Premises used: Filter.Tendsto.const_mul, Filter.Tendsto.limUnder_eq