awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : (↑a : ℂ) ∈ K
⊢ (↑k ! : ℝ) *
      ‖((↑a : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
          ((↑a : ℂ) - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖ ≤
    (↑k ! : ℝ) *
      (r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
          |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
          |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
have hbc : ‖((↑a : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      ((↑a : ℂ) - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖ ≤
  r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
      |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
      |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : (↑a : ℂ) ∈ K
⊢ ‖((↑a : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        ((↑a : ℂ) - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖ ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
        |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
        |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have h1 : ‖(↑(![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 0) : ℂ) * (↑a : ℂ) + (↑(![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 1) : ℂ)‖ ^
    (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ≤
  r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) *
    ‖![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1]‖ ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
Tactic: have h1 := summand_bound_of_mem_verticalStrip (k := k + 1) (by positivity) ![1, n + 1] hB haAB
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : (↑a : ℂ) ∈ K
h1 :
  ‖(↑(![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 0) : ℂ) * (↑a : ℂ) + (↑(![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 1) : ℂ)‖ ^
      (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) *
      ‖![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1]‖ ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
⊢ ‖((↑a : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        ((↑a : ℂ) - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖ ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
        |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
        |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have h2 : ‖(↑(![1, -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 0) : ℂ) * (↑a : ℂ) + (↑(![1, -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 1) : ℂ)‖ ^
    (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ≤
  r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) *
    HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
Tactic: have h2 := abs_norm_eq_max_natAbs_neg n ▸ summand_bound_of_mem_verticalStrip (k := k + 1)
    (by positivity) ![1, -(n + 1)] hB haAB
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : (↑a : ℂ) ∈ K
h1 :
  ‖(↑(![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 0) : ℂ) * (↑a : ℂ) + (↑(![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 1) : ℂ)‖ ^
      (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) *
      ‖![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1]‖ ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
h2 :
  ‖(↑(![1, -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 0) : ℂ) * (↑a : ℂ) + (↑(![1, -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 1) : ℂ)‖ ^
      (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) *
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
⊢ ‖((↑a : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        ((↑a : ℂ) - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖ ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
        |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
        |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have hbc : ‖((↑a : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖ ≤
  r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
    |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: apply norm_add_le_of_le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : (↑a : ℂ) ∈ K
h1 :
  ‖(↑(![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 0) : ℂ) * (↑a : ℂ) + (↑(![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 1) : ℂ)‖ ^
      (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) *
      ‖![1, HAdd.hAdd (α := ℤ) (↑n : ℤ) 1]‖ ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
h2 :
  ‖(↑(![1, -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 0) : ℂ) * (↑a : ℂ) + (↑(![1, -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1] 1) : ℂ)‖ ^
      (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) *
      HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (-HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hbc :
  ‖((↑a : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖ ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
      |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ ‖((↑a : ℂ) + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        ((↑a : ℂ) - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖ ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
        |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
        |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have hbc₁ : ‖((↑a : ℂ) - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖ ≤
  r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
    |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: apply norm_add_le_of_le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
hk : 1 ≤ k
⊢ SummableLocallyUniformlyOn (α := ℂ) (fun (n : ℕ) ↦ iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ) ℍₒ
have apply : ∀ K ⊆ ℍₒ,
  IsCompact K →
    ∃ (u : ℕ → ℝ),
      Summable u ∧
        ∀ (n : ℕ), ∀ k_1 ∈ K, Norm.norm (E := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ k_1) ≤ u n
Tactic: apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
hk : 1 ≤ k
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
⊢ ∃ (u : ℕ → ℝ),
    Summable u ∧
      ∀ (n : ℕ), ∀ k_1 ∈ K, Norm.norm (E := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ k_1) ≤ u n
have lift : ∀ (K : Set ℍ) (hKc : IsCompact (UpperHalfPlane.coe '' K)),
  ∃ (u : ℕ → ℝ),
    Summable u ∧
      ∀ (n : ℕ),
        ∀ k_1 ∈ UpperHalfPlane.coe '' K,
          Norm.norm (E := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ k_1) ≤ u n
Tactic: lift K to Set ℍ using hK
Cleared hypotheses: K, hK, hKc
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
hk : 1 ≤ k
K : Set ℍ
hKc : IsCompact (UpperHalfPlane.coe '' K)
⊢ ∃ (u : ℕ → ℝ),
    Summable u ∧
      ∀ (n : ℕ),
        ∀ k_1 ∈ UpperHalfPlane.coe '' K,
          Norm.norm (E := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ k_1) ≤ u n
have obtain : ∀ (A B : ℝ) (hB : 0 < B) (HABK : K ⊆ verticalStrip A B),
  ∃ (u : ℕ → ℝ),
    Summable u ∧
      ∀ (n : ℕ),
        ∀ k_1 ∈ UpperHalfPlane.coe '' K,
          Norm.norm (E := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ k_1) ≤ u n
Tactic: obtain ⟨A, B, hB, HABK⟩ := subset_verticalStrip_of_isCompact
    (isEmbedding_coe.isCompact_iff.mpr hKc)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
n l : ℕ
⊢ DifferentiableOn ℂ (F := ℂ) (iteratedDerivWithin l (fun (z : ℂ) ↦ cotTerm z n) ℍₒ) ℍₒ
have suffices : DifferentiableOn ℂ (F := ℂ)
  (fun (z : ℂ) ↦
    HPow.hPow (α := ℂ) (-1) l * (↑l ! : ℂ) *
      ((z + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ) +
        (z - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ)))
  ℍₒ
Tactic: suffices DifferentiableOn ℂ (fun z : ℂ ↦ (-1) ^ l * l ! * ((z + (n + 1)) ^ (-1 - l : ℤ) +
    (z - (n + 1)) ^ (-1 - l : ℤ))) ℍₒ by
    exact this.congr fun z hz ↦ eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet l n hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
n l : ℕ
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      HPow.hPow (α := ℂ) (-1) l * (↑l ! : ℂ) *
        ((z + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ) +
          (z - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ)))
    ℍₒ
have ha : DifferentiableOn ℂ (F := ℂ)
  (fun (y : ℂ) ↦
    (y + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ) +
      (y - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ))
  ℍₒ
Tactic: apply DifferentiableOn.const_mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
n l : ℕ
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (y : ℂ) ↦
      (y + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ) +
        (y - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ))
    ℍₒ
have ha : DifferentiableOn ℂ (F := ℂ) (fun (y : ℂ) ↦ (y + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ)) ℍₒ
Tactic: apply DifferentiableOn.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
n l : ℕ
ha :
  DifferentiableOn ℂ (F := ℂ) (fun (y : ℂ) ↦ (y + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ)) ℍₒ
⊢ DifferentiableOn ℂ (F := ℂ)
    (fun (y : ℂ) ↦
      (y + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ) +
        (y - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ))
    ℍₒ
have ha₁ : DifferentiableOn ℂ (F := ℂ) (fun (y : ℂ) ↦ (y - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ)) ℍₒ
Tactic: apply DifferentiableOn.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
n l : ℕ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (y : ℂ) ↦ (y + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ)) ℍₒ
have ha : ∀ (x : ℂ) (hx : x ∈ ℍₒ), x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
Tactic: refine DifferentiableOn.zpow (by fun_prop) <| .inl fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
n l : ℕ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (y : ℂ) ↦ (y - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ)) ℍₒ
have ha : ∀ (x : ℂ) (hx : x ∈ ℍₒ), x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
Tactic: refine DifferentiableOn.zpow (by fun_prop) <| .inl fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have apply : ∀ (b : ℕ),
  (((↑1 : ℂ) * x + (↑(↑(b + 1) : ℤ) : ℂ)) ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)⁻¹ =
    (x + HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: apply ((summable_nat_add_iff 1).mpr (summable_int_iff_summable_nat_and_neg.mp
        (EisensteinSeries.linear_right_summable x 1 (k := k + 1) (by lia))).1).congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have apply : ∀ (b : ℕ),
  (((↑1 : ℂ) * x + (↑(-(↑(b + 1) : ℤ)) : ℂ)) ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)⁻¹ =
    (x - HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: apply ((summable_nat_add_iff 1).mpr (summable_int_iff_summable_nat_and_neg.mp
        (EisensteinSeries.linear_right_summable x 1 (k := k + 1) (by lia))).2).congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cotTerm z n) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have rw : HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
    ∑' (n : ℕ), iteratedDerivWithin k (fun (t : ℂ) ↦ cotTerm t n) ℍₒ z =
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: rw [iteratedDerivWithin_tsum k isOpen_upperHalfPlaneSet hz
    (fun t ht ↦ summable_cotTerm (coe_mem_integerComplement ⟨t, ht⟩))
    (fun l hl hl2 ↦ summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm hl)
    (fun n l z hl hz ↦ (differentiableOn_iteratedDerivWithin_cotTerm n l).differentiableAt
    (isOpen_upperHalfPlaneSet.mem_nhds hz))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
| HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      ∑' (n : ℕ), iteratedDerivWithin k (fun (t : ℂ) ↦ cotTerm t n) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have h : ∀ (n : ℕ), iteratedDerivWithin k (fun (t : ℂ) ↦ cotTerm t n) ℍₒ z
Tactic: enter [1, 2, 1, n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
| iteratedDerivWithin k (fun (t : ℂ) ↦ cotTerm t n) ℍₒ z
have h : (fun (z : ℂ) ↦
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
      ((z + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        (z - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
  z
Tactic: rw [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (by simp [hz])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
| HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      ∑' (n : ℕ), iteratedDerivWithin k (fun (t : ℂ) ↦ cotTerm t n) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have h : ∀ (n : ℕ),
  (fun (z : ℂ) ↦
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
        ((z + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
          (z - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
    z
Tactic: enter [1, 2, 1, n]
    rw [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (by simp [hz])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      ∑' (n : ℕ), iteratedDerivWithin k (fun (t : ℂ) ↦ cotTerm t n) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have conv : HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
    ∑' (n : ℕ),
      (fun (z : ℂ) ↦
          HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
            ((z + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
              (z - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
        z =
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: conv =>
    enter [1, 2, 1, n]
    rw [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (by simp [hz])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      ∑' (n : ℕ),
        (fun (z : ℂ) ↦
            HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
              ((z + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
                (z - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
          z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have rw : HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
      HAdd.hAdd (α := ℂ) (∑' (b : ℕ), (z + HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
        (∑' (b : ℕ), (z - HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) =
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
    (∑' (n : ℕ), (z + (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        (z + (↑0 : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      ∑' (n : ℕ), (z + (↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
Tactic: rw [tsum_of_add_one_of_neg_add_one (by simpa using aux_summable_add hk z)
    (by simpa [sub_eq_add_neg] using aux_summable_sub hk z),
    tsum_mul_left, Summable.tsum_add (aux_summable_add hk z) (aux_summable_sub hk z)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
        HAdd.hAdd (α := ℂ) (∑' (b : ℕ), (z + HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
          (∑' (b : ℕ), (z - HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
      (∑' (n : ℕ), (z + (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
          (z + (↑0 : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        ∑' (n : ℕ), (z + (↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
have push_cast : HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
      HAdd.hAdd (α := ℂ) (∑' (b : ℕ), (z + HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
        (∑' (b : ℕ), (z - HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) =
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
    (∑' (n : ℕ), (z + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        (z + 0) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      ∑' (n : ℕ), (z + -HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x) ℍₒ z =
    -HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
have simp : Eq (α := ℂ) (iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot - x⁻¹) ℍₒ z)
  (iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cotTerm z n) ℍₒ z)
Tactic: simp only [← aux_iteratedDeriv_tsum_cotTerm hk hz, one_div, neg_mul, neg_add_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ Eq (α := ℂ) (iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot - x⁻¹) ℍₒ z)
    (iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cotTerm z n) ℍₒ z)
have refine : ∀ (z : ℂ) (hz : z ∈ ℍₒ), (↑π : ℂ) * ((↑π : ℂ) * z).cot - z⁻¹ = ∑' (n : ℕ), cotTerm z n
Tactic: refine iteratedDerivWithin_congr (fun z hz ↦ ?_) hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot + -(1 / x)) ℍₒ z =
    iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z +
      -(HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)))
have rw : HAdd.hAdd (α := ℂ) (iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z)
    (iteratedDerivWithin k (fun (x : ℂ) ↦ -(1 / x)) ℍₒ z) =
  iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z +
    -(HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)))
Tactic: rw [iteratedDerivWithin_fun_add hz isOpen_upperHalfPlaneSet.uniqueDiffOn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
rw :
  HAdd.hAdd (α := ℂ) (iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z)
      (iteratedDerivWithin k (fun (x : ℂ) ↦ -(1 / x)) ℍₒ z) =
    iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z +
      -(HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)))
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot + -(1 / x)) ℍₒ z =
    iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z +
      -(HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HAdd.hAdd (α := ℤ) (-1) (-(↑k : ℤ)))
have hf : ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z
Tactic: rw [iteratedDerivWithin_fun_add hz isOpen_upperHalfPlaneSet.uniqueDiffOn]