awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ 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:
simpa using tendsto_logDeriv_euler_sin_div hx

Premises used: tendsto_logDeriv_euler_sin_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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
hb : 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)))

Tactic:
rw [one_div_add_one_div]

Premises used: one_div_add_one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ (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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0

Tactic:
simpa [sub_eq_add_neg] using integerComplement_add_ne_zero hz (-(n + 1) : ℤ)

Premises used: sub_eq_add_neg, Complex.integerComplement_add_ne_zero, Nat.cast, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0

Tactic:
simpa using (integerComplement_add_ne_zero hz ((n : ℤ) + 1))

Premises used: Complex.integerComplement_add_ne_zero, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
rw :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (fun (n : ℕ) ↦ 2 * x * (1 / ((x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)))) n
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ cotTerm x n

Tactic:
rw [funext fun n ↦ cotTerm_identity hz n]

Premises used: funext, cotTerm_identity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
hf : Summable (α := ℂ) fun (i : ℕ) ↦ 1 / ((x + HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1))
⊢ Summable (α := ℂ) fun (n : ℕ) ↦
    (fun (n : ℕ) ↦ 2 * x * (1 / ((x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)))) n

Tactic:
apply Summable.mul_left

Premises used: Summable.mul_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable (α := ℂ) fun (i : ℕ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ (x - (↑(n + 1) : ℂ))⁻¹ * (x + (↑(n + 1) : ℂ))⁻¹

Tactic:
rw [← summable_nat_add_iff 1] at this

Premises used: summable_nat_add_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable (α := ℂ) fun (n : ℕ) ↦ (x - (↑(n + 1) : ℂ))⁻¹ * (x + (↑(n + 1) : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ 1 / ((x + HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1))

Tactic:
simpa using this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
hf : Summable (α := ℂ) fun (i : ℕ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ 1 / ((x + HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) * (x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1))

Tactic:
suffices Summable fun i : ℕ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹ by
    rw [← summable_nat_add_iff 1] at this
    simpa using this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable (α := ℂ) fun (i : ℤ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹

Tactic:
apply this.comp_injective CharZero.cast_injective

Premises used: CharZero.cast_injective, Summable.comp_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
hf : Summable (α := ℂ) fun (i : ℤ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹

Tactic:
suffices Summable fun i : ℤ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹ by
    apply this.comp_injective CharZero.cast_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
hf : ∀ (b : ℤ), (((↑1 : ℂ) * x - (↑b : ℂ)) * ((↑1 : ℂ) * x + (↑b : ℂ)))⁻¹ = (x - (↑b : ℂ))⁻¹ * (x + (↑b : ℂ))⁻¹
⊢ Summable (α := ℂ) fun (i : ℤ) ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹

Tactic:
apply (EisensteinSeries.summable_linear_sub_mul_linear_add x 1 1).congr

Premises used: EisensteinSeries.summable_linear_sub_mul_linear_add, Summable.congr, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ ∀ (b : ℤ), (((↑1 : ℂ) * x - (↑b : ℂ)) * ((↑1 : ℂ) * x + (↑b : ℂ)))⁻¹ = (x - (↑b : ℂ))⁻¹ * (x + (↑b : ℂ))⁻¹

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
rw :
  HasSum (fun (n : ℕ) ↦ 1 / (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
    ((↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x)
⊢ (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x =
    ∑' (n : ℕ), (1 / (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))

Tactic:
rw [HasSum.tsum_eq]

Premises used: HasSum.tsum_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ HasSum (fun (n : ℕ) ↦ 1 / (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))
    ((↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x)

Tactic:
apply (Summable.hasSum_iff_tendsto_nat (summable_cotTerm hz)).mpr
    (tendsto_logDeriv_euler_cot_sub hz)

Premises used: Iff.mpr, Summable.hasSum_iff_tendsto_nat, tendsto_logDeriv_euler_cot_sub, summable_cotTerm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ 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))
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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 - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1))

Tactic:
have h1 := cot_series_rep' hz
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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))
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 : ℕ) : ℂ))⁻¹)
⊢ (↑π : ℂ) * ((↑π : ℂ) * x).cot = 1 / x + ∑' (n : ℕ+), (1 / (x - (↑(↑n : ℕ) : ℂ)) + 1 / (x + (↑(↑n : ℕ) : ℂ)))

Tactic:
simp only [one_div, Nat.cast_add, Nat.cast_one] at *

Premises used: Nat.cast_add, one_div, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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)⁻¹)
rw : (↑π : ℂ) * ((↑π : ℂ) * x).cot = x⁻¹ + ((↑π : ℂ) * ((↑π : ℂ) * x).cot - x⁻¹)
⊢ (↑π : ℂ) * ((↑π : ℂ) * x).cot = x⁻¹ + ∑' (n : ℕ+), ((x - (↑(↑n : ℕ) : ℂ))⁻¹ + (x + (↑(↑n : ℕ) : ℂ))⁻¹)

Tactic:
rw [h0, ← h1]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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⁻¹ + ((↑π : ℂ) * ((↑π : ℂ) * x).cot - x⁻¹)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
d : ℤ
⊢ ContDiffOn ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ x + (↑d : ℂ)) ℂ_ℤ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
d : ℤ
⊢ ContDiffOn ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (z : ℂ) ↦ 1 / (z + (↑d : ℂ))) ℂ_ℤ

Tactic:
simpa using ContDiffOn.inv (by fun_prop) (fun x hx ↦ integerComplement_add_ne_zero hx d)

Premises used: Complex.integerComplement_add_ne_zero, ContDiffOn.inv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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
hg : 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)

Tactic:
rw [← Pi.add_def, iteratedDeriv_add]

Premises used: iteratedDeriv_add, Pi.add_def
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ 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 : ℂ))
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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 : ℤ)
⊢ 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 : ℂ)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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 : ℤ)
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 : ℤ))
⊢ 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:
simp only [one_div, one_mul, one_pow, mul_one, Int.reduceNeg, iteratedDeriv_eq_iterate] at *

Premises used: one_pow, Int.reduceNeg, iteratedDeriv_eq_iterate, one_div, mul_one, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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 : ℤ)
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 : ℤ))
⊢ 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:
rw [h2, h3]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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 (α := ℂ)
      ((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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (z : ℂ) ↦ 1 / (z - HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z

Tactic:
simpa [sub_eq_add_neg] using (contDiffOn_inv_linear k (-(d + 1))).contDiffAt
      (isOpen_compl_range_intCast.mem_nhds hz)

Premises used: sub_eq_add_neg, Complex.isOpen_compl_range_intCast, Nat.cast, HAdd.hAdd, IsOpen.mem_nhds, ContDiffOn.contDiffAt, OfNat.ofNat, Neg.neg, _private.0.contDiffOn_inv_linear
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (z : ℂ) ↦ 1 / (z + HAdd.hAdd (α := ℂ) (↑d : ℂ) 1)) z

Tactic:
simpa using (contDiffOn_inv_linear k (d + 1)).contDiffAt
      (isOpen_compl_range_intCast.mem_nhds hz)

Premises used: Complex.isOpen_compl_range_intCast, Nat.cast, HAdd.hAdd, IsOpen.mem_nhds, ContDiffOn.contDiffAt, OfNat.ofNat, _private.0.contDiffOn_inv_linear
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k d : ℕ
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)ᶜ
⊢ 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 : ℤ)))
    ℂ_ℤ

Tactic:
apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen Complex.isOpen_compl_range_intCast)

Premises used: Set.EqOn.trans, Complex.isOpen_compl_range_intCast, iteratedDerivWithin_of_isOpen
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k d : ℕ
⊢ 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:
eqOn_iteratedDeriv_cotTerm ..

Premises used: eqOn_iteratedDeriv_cotTerm, Complex.integerComplement
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k d : ℕ
⊢ 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:
exact eqOn_iteratedDeriv_cotTerm ..

Premises used: eqOn_iteratedDeriv_cotTerm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k d : ℕ
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 : ℤ)))
    ℍₒ
⊢ 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 : ℤ)))
    ℍₒ

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

Premises used: Set.EqOn.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k d : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ Eq (α := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z d) (range Int.cast)ᶜ 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:
simpa using eqOn_iteratedDerivWithin_cotTerm_integerComplement k d
    (coe_mem_integerComplement ⟨z, hz⟩)

Premises used: UpperHalfPlane.mk, UpperHalfPlane.coe_mem_integerComplement, eqOn_iteratedDerivWithin_cotTerm_integerComplement
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
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 : ℤ)‖
⊢ Summable (α := ℝ) fun (a : ℕ) ↦ cotTermUpperBound k A B hB a

Tactic:
simp_rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
hf : Summable (α := ℝ) fun (i : ℕ) ↦ ‖HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ HSub.hSub (α := ℤ) (-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 : ℤ)‖

Tactic:
apply Summable.mul_left

Premises used: Summable.mul_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
h : ∀ (n : ℕ), ‖HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖
| Summable (α := ℝ) fun (i : ℕ) ↦ ‖HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖

Tactic:
enter [1, n]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
⊢ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) = -(↑(1 + k) : ℤ)

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
h : ‖(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (1 + k))⁻¹‖
| ‖HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖

Tactic:
rw [show (-1 - k : ℤ) = -(1 + k :) by lia, zpow_neg, zpow_natCast]

Premises used: zpow_natCast, zpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
h : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
| ‖(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (1 + k))⁻¹‖

Tactic:
enter [1, 1, 1]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
h : (↑(n + 1) : ℝ)
| HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
h : ∀ (n : ℕ), (↑(n + 1) : ℝ)
| Summable (α := ℝ) fun (i : ℕ) ↦ ‖HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)‖

Tactic:
enter [1, n]; rw [show (-1 - k : ℤ) = -(1 + k :) by lia, zpow_neg, zpow_natCast];
          enter [1, 1, 1]; norm_cast

Premises used: zpow_natCast, zpow_neg