-- Mathlib/Analysis/Complex/Periodic.lean
theorem differentiableAt_cuspFunction (hh : h ≠ 0) (hf : Periodic f h)
    {z : ℂ} (hol_z : DifferentiableAt ℂ f z) :
    DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Proof state:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 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

Result:
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)

Proof state:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
let q := 𝕢 h z

Result:
h : ℝ
f : ℂ → ℂ
hh : h ≠ 0
hf : Periodic f ↑h
z : ℂ
hol_z : DifferentiableAt ℂ f z
q : ℂ := 𝕢 h z
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Proof state:
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)

Tactic:
have diff_L : DifferentiableAt ℂ L q := (qdiff.to_localInverse diff_ne).differentiableAt

Result:
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)

Proof state:
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

Result:
no goals

Proof state:
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)

Tactic:
have : cuspFunction h f ∘ 𝕢 h ∘ L = f ∘ L := funext fun z ↦ eq_cuspFunction hh hf (L z)

Result:
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)

Proof state:
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 ℂ) (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

Result:
no goals

Proof state:
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
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Tactic:
let L := (qdiff.localInverse (𝕢 h) _ z) diff_ne

Result:
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)

Proof state:
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)

Tactic:
have hL : 𝕢 h ∘ L =ᶠ[𝓝 q] (id : ℂ → ℂ) :=
  (qdiff.hasStrictFDerivAt_equiv diff_ne).eventually_right_inverse

Result:
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)

Proof state:
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)

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)

Result:
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
⊢ DifferentiableAt ℂ (cuspFunction h f) (𝕢 h z)

Proof state:
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)

Tactic:
have hF := hL.fun_comp (cuspFunction h f)

Result:
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)

Proof state:
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)

Tactic:
rw [this] at hF

Result:
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)