awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Tendsto (fun (n : ℕ) ↦ ∑ j ∈ Finset.range n, cotTerm x j) atTop (𝓝 ((↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x))
have simp_rw : Tendsto (β := ℂ) (fun (n : ℕ) ↦ logDeriv (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) atTop
  (𝓝 (logDeriv (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) x))
Tactic: simp_rw [← logDeriv_sin_div_eq_cot hx, ← logDeriv_prod_sineTerm_eq_sum_cotTerm hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ 1 / (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    2 * x * (1 / ((x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)))
have rw : (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)) /
    ((x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)) =
  2 * x * (1 / ((x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)))
Tactic: rw [one_div_add_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
rw :
  (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)) /
      ((x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)) =
    2 * x * (1 / ((x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)))
⊢ 1 / (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    2 * x * (1 / ((x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)))
have ha : x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
Tactic: rw [one_div_add_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
rw :
  (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 + (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)) /
      ((x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)) =
    2 * x * (1 / ((x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)))
ha : x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ 1 / (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) =
    2 * x * (1 / ((x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)))
have hb : x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
Tactic: rw [one_div_add_one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ cotTerm x n
have rw : Summable (α := ℂ) fun (n : ℕ) ↦
  (fun (n : ℕ) ↦ 2 * x * (1 / ((x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)))) n
Tactic: rw [funext fun n ↦ cotTerm_identity hz n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable (α := ℂ) fun (n : ℕ) ↦
    (fun (n : ℕ) ↦ 2 * x * (1 / ((x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)))) n
have hf : Summable (α := ℂ) fun (i : ℕ) ↦ 1 / ((x + HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1))
Tactic: apply Summable.mul_left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable (α := ℂ) fun (i : ℕ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ 1 / ((x + HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1))
have this₁ : Summable (α := ℂ) fun (n : ℕ) ↦ (x - (↑(n + 1) : ℂ))⁻¹ * (x + (↑(n + 1) : ℂ))⁻¹
Tactic: rw [← summable_nat_add_iff 1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ 1 / ((x + HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1))
have hf : Summable (α := ℂ) fun (i : ℕ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹
Tactic: suffices Summable fun i : ℕ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹ by
    rw [← summable_nat_add_iff 1] at this
    simpa using this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹
have hf : Summable (α := ℂ) fun (i : ℤ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹
Tactic: suffices Summable fun i : ℤ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹ by
    apply this.comp_injective CharZero.cast_injective
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Summable (α := ℂ) fun (i : ℤ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹
have hf : ∀ (b : ℤ), (((↑1 : ℂ) * x - (↑b : ℂ)) * ((↑1 : ℂ) * x + (↑b : ℂ)))⁻¹ = (x - (↑b : ℂ))⁻¹ * (x + (↑b : ℂ))⁻¹
Tactic: apply (EisensteinSeries.summable_linear_sub_mul_linear_add x 1 1).congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x =
    ∑' (n : ℕ), (1 / (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
have rw : HasSum (fun (n : ℕ) ↦ 1 / (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
  ((↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x)
Tactic: rw [HasSum.tsum_eq]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ (↑π : ℂ) * ((↑π : ℂ) * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - (↑(↑n : ℕ) : ℂ)) + 1 / (x + (↑(↑n : ℕ) : ℂ)))
have h0 : Eq (α := ℂ) (∑' (n : ℕ+), (1 / (x - (↑(↑n : ℕ) : ℂ)) + 1 / (x + (↑(↑n : ℕ) : ℂ))))
  (∑' (n : ℕ), (1 / (x - (↑(n + 1) : ℂ)) + 1 / (x + (↑(n + 1) : ℂ))))
Tactic: have h0 := tsum_pnat_eq_tsum_succ (f := fun n ↦ 1 / (x - n) + 1 / (x + n))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
h0 :
  Eq (α := ℂ) (∑' (n : ℕ+), (1 / (x - (↑(↑n : ℕ) : ℂ)) + 1 / (x + (↑(↑n : ℕ) : ℂ))))
    (∑' (n : ℕ), (1 / (x - (↑(n + 1) : ℂ)) + 1 / (x + (↑(n + 1) : ℂ))))
⊢ (↑π : ℂ) * ((↑π : ℂ) * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - (↑(↑n : ℕ) : ℂ)) + 1 / (x + (↑(↑n : ℕ) : ℂ)))
have h1 : (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x =
  ∑' (n : ℕ), (1 / (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
Tactic: have h1 := cot_series_rep' hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
h0 :
  Eq (α := ℂ) (∑' (n : ℕ+), (1 / (x - (↑(↑n : ℕ) : ℂ)) + 1 / (x + (↑(↑n : ℕ) : ℂ))))
    (∑' (n : ℕ), (1 / (x - (↑(n + 1) : ℂ)) + 1 / (x + (↑(n + 1) : ℂ))))
h1 :
  (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x =
    ∑' (n : ℕ), (1 / (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
⊢ (↑π : ℂ) * ((↑π : ℂ) * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - (↑(↑n : ℕ) : ℂ)) + 1 / (x + (↑(↑n : ℕ) : ℂ)))
have simp : ∀
  (h0 :
    Eq (α := ℂ) (∑' (n : ℕ+), ((x - (↑(↑n : ℕ) : ℂ))⁻¹ + (x + (↑(↑n : ℕ) : ℂ))⁻¹))
      (∑' (n : ℕ), ((x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ + (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹)))
  (h1 :
    (↑π : ℂ) * ((↑π : ℂ) * x).cot - x⁻¹ =
      ∑' (n : ℕ), ((x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ + (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹)),
  (↑π : ℂ) * ((↑π : ℂ) * x).cot = x⁻¹ + ∑' (n : ℕ+), ((x - (↑(↑n : ℕ) : ℂ))⁻¹ + (x + (↑(↑n : ℕ) : ℂ))⁻¹)
Tactic: simp only [one_div, Nat.cast_add, Nat.cast_one] at *
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
h0 :
  Eq (α := ℂ) (∑' (n : ℕ+), ((x - (↑(↑n : ℕ) : ℂ))⁻¹ + (x + (↑(↑n : ℕ) : ℂ))⁻¹))
    (∑' (n : ℕ), ((x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ + (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹))
h1 :
  (↑π : ℂ) * ((↑π : ℂ) * x).cot - x⁻¹ =
    ∑' (n : ℕ), ((x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹ + (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)⁻¹)
⊢ (↑π : ℂ) * ((↑π : ℂ) * x).cot = x⁻¹ + ∑' (n : ℕ+), ((x - (↑(↑n : ℕ) : ℂ))⁻¹ + (x + (↑(↑n : ℕ) : ℂ))⁻¹)
have rw : (↑π : ℂ) * ((↑π : ℂ) * x).cot = x⁻¹ + ((↑π : ℂ) * ((↑π : ℂ) * x).cot - x⁻¹)
Tactic: rw [h0, ← h1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ Eq (α := ℂ) (iteratedDeriv k (fun (z : ℂ) ↦ cotTerm z d) z)
    ((fun (z : ℂ) ↦
        HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
          ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
            (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
      z)
have rw : HAdd.hAdd (α := ℂ) (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z)
    (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z) =
  (fun (z : ℂ) ↦
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
        ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
          (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
    z
Tactic: rw [← Pi.add_def, iteratedDeriv_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
rw :
  HAdd.hAdd (α := ℂ) (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z)
      (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z) =
    (fun (z : ℂ) ↦
        HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
          ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
            (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
      z
⊢ Eq (α := ℂ) (iteratedDeriv k (fun (z : ℂ) ↦ cotTerm z d) z)
    ((fun (z : ℂ) ↦
        HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
          ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
            (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
      z)
have hf : ContDiffAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (z : ℂ) ↦ 1 / (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z
Tactic: rw [← Pi.add_def, iteratedDeriv_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
rw :
  HAdd.hAdd (α := ℂ) (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z)
      (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z) =
    (fun (z : ℂ) ↦
        HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
          ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
            (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
      z
hf : ContDiffAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (z : ℂ) ↦ 1 / (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z
⊢ Eq (α := ℂ) (iteratedDeriv k (fun (z : ℂ) ↦ cotTerm z d) z)
    ((fun (z : ℂ) ↦
        HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
          ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
            (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
      z)
have hg : ContDiffAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (z : ℂ) ↦ 1 / (z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z
Tactic: rw [← Pi.add_def, iteratedDeriv_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ HAdd.hAdd (α := ℂ) (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z)
      (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z) =
    (fun (z : ℂ) ↦
        HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
          ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
            (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
      z
have h2 : Eq (α := ℂ → ℂ) (deriv^[k] fun (x : ℂ) ↦ (1 * x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) fun (x : ℂ) ↦
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * HPow.hPow (α := ℂ) 1 k *
    (1 * x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: have h2 := iter_deriv_inv_linear_sub k 1 ((d + 1 : ℂ))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
h2 :
  Eq (α := ℂ → ℂ) (deriv^[k] fun (x : ℂ) ↦ (1 * x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) fun (x : ℂ) ↦
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * HPow.hPow (α := ℂ) 1 k *
      (1 * x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ HAdd.hAdd (α := ℂ) (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z)
      (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z) =
    (fun (z : ℂ) ↦
        HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
          ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
            (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
      z
have h3 : Eq (α := ℂ → ℂ) (deriv^[k] fun (x : ℂ) ↦ (1 * x + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) fun (x : ℂ) ↦
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * HPow.hPow (α := ℂ) 1 k *
    (1 * x + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
Tactic: have h3 := iter_deriv_inv_linear k 1 (d + 1 : ℂ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
h2 :
  Eq (α := ℂ → ℂ) (deriv^[k] fun (x : ℂ) ↦ (1 * x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) fun (x : ℂ) ↦
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * HPow.hPow (α := ℂ) 1 k *
      (1 * x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
h3 :
  Eq (α := ℂ → ℂ) (deriv^[k] fun (x : ℂ) ↦ (1 * x + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) fun (x : ℂ) ↦
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * HPow.hPow (α := ℂ) 1 k *
      (1 * x + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ HAdd.hAdd (α := ℂ) (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z)
      (iteratedDeriv k (fun (z : ℂ) ↦ 1 / (z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z) =
    (fun (z : ℂ) ↦
        HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
          ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
            (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
      z
have simp : ∀
  (h2 :
    Eq (α := ℂ → ℂ) (deriv^[k] fun (x : ℂ) ↦ (x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) fun (x : ℂ) ↦
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * (x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
  (h3 :
    Eq (α := ℂ → ℂ) (deriv^[k] fun (x : ℂ) ↦ (x + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) fun (x : ℂ) ↦
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * (x + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)),
  HAdd.hAdd (α := ℂ) (β := ℂ) (deriv^[k] (fun (z : ℂ) ↦ (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) z : ℂ)
      (deriv^[k] (fun (z : ℂ) ↦ (z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) z : ℂ) =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
      ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
Tactic: simp only [one_div, one_mul, one_pow, mul_one, Int.reduceNeg, iteratedDeriv_eq_iterate] at *
Cleared hypotheses: h2, h3
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
h2 :
  Eq (α := ℂ → ℂ) (deriv^[k] fun (x : ℂ) ↦ (x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) fun (x : ℂ) ↦
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * (x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
h3 :
  Eq (α := ℂ → ℂ) (deriv^[k] fun (x : ℂ) ↦ (x + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) fun (x : ℂ) ↦
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * (x + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ HAdd.hAdd (α := ℂ) (β := ℂ) (deriv^[k] (fun (z : ℂ) ↦ (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) z : ℂ)
      (deriv^[k] (fun (z : ℂ) ↦ (z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)⁻¹) z : ℂ) =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
      ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
have rw : HAdd.hAdd (α := ℂ)
    ((fun (x : ℂ) ↦
        HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * (x - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
      z)
    ((fun (x : ℂ) ↦
        HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * (x + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
      z) =
  HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
    ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
      (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ))
Tactic: rw [h2, h3]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k d : ℕ
⊢ EqOn (β := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z d) ℂ_ℤ)
    (fun (z : ℂ) ↦
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
        ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
          (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
    ℂ_ℤ
have apply : EqOn (β := ℂ) (iteratedDeriv k fun (z : ℂ) ↦ cotTerm z d)
  (fun (z : ℂ) ↦
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
      ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
  (range Int.cast)ᶜ
Tactic: apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen Complex.isOpen_compl_range_intCast)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
k d : ℕ
⊢ EqOn (β := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z d) ℍₒ)
    (fun (z : ℂ) ↦
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
        ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
          (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
    ℍₒ
have apply : EqOn (β := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z d) (range Int.cast)ᶜ)
  (fun (z : ℂ) ↦
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) *
      ((z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) +
        (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)))
  ℍₒ
Tactic: apply Set.EqOn.trans (upperHalfPlane_inter_integerComplement ▸
    iteratedDerivWithin_congr_right_of_isOpen (fun z ↦ cotTerm z d) k
    isOpen_upperHalfPlaneSet (isOpen_compl_range_intCast))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable (α := ℝ) fun (a : ℕ) ↦ cotTermUpperBound k A B hB a
have simp_rw : Summable (α := ℝ) fun (a : ℕ) ↦
  HMul.hMul (α := ℝ) (↑k ! : ℝ) 2 *
      EisensteinSeries.r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
    ‖HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖
Tactic: simp_rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable (α := ℝ) fun (a : ℕ) ↦
    HMul.hMul (α := ℝ) (↑k ! : ℝ) 2 *
        EisensteinSeries.r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^
          HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
      ‖HAdd.hAdd (α := ℝ) (↑a : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖
have hf : Summable (α := ℝ) fun (i : ℕ) ↦ ‖HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖
Tactic: apply Summable.mul_left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
| Summable (α := ℝ) fun (i : ℕ) ↦ ‖HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖
have h : ∀ (n : ℕ), ‖HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖
Tactic: enter [1, n]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ‖HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖
have h : ‖(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (1 + k))⁻¹‖
Tactic: rw [show (-1 - k : ℤ) = -(1 + k :) by lia, zpow_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ‖(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (1 + k))⁻¹‖
have h : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: enter [1, 1, 1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have h : (↑(n + 1) : ℝ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
| Summable (α := ℝ) fun (i : ℕ) ↦ ‖HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖
have h : ∀ (n : ℕ), (↑(n + 1) : ℝ)
Tactic: enter [1, n]; rw [show (-1 - k : ℤ) = -(1 + k :) by lia, zpow_neg, zpow_natCast];
          enter [1, 1, 1]; norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖
have hf : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (1 + k))⁻¹‖
Tactic: conv => enter [1, n]; rw [show (-1 - k : ℤ) = -(1 + k :) by lia, zpow_neg, zpow_natCast];
          enter [1, 1, 1]; norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (1 + k))⁻¹‖
have hf : Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) (1 + k))⁻¹
Tactic: rw [summable_norm_iff, summable_nat_add_iff (f := fun n : ℕ ↦ ((n : ℝ) ^ (1 + k))⁻¹)]
-- 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 : ℂ
ha : a ∈ K
⊢ Norm.norm (E := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ a) ≤ cotTermUpperBound k A B hB n
have rcases : ∀ (a : ℍ) (haAB : a ∈ verticalStrip A B) (ha : (↑a : ℂ) ∈ K),
  Norm.norm (E := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ (↑a : ℂ)) ≤ cotTermUpperBound k A B hB n
Tactic: rcases hKAB ha with ⟨a, haAB, rfl⟩
Cleared hypotheses: a, ha
-- 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
⊢ Norm.norm (E := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ (↑a : ℂ)) ≤ cotTermUpperBound k A B hB n
have simp : (↑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 : ℤ))
Tactic: simp only [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n a.im_pos, Complex.norm_mul,
    norm_pow, norm_neg, norm_one, one_pow, Complex.norm_natCast, one_mul, cotTermUpperBound,
    Int.reduceNeg, norm_zpow, Real.norm_eq_abs, two_mul, add_mul]