awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
hf : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (1 + k))⁻¹‖
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 ^ HSub.hSub (α := ℤ) (-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

Premises used: zpow_natCast, zpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
hf : Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) (1 + k))⁻¹
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(HPow.hPow (α := ℝ) (↑(n + 1) : ℝ) (1 + k))⁻¹‖

Tactic:
rw [summable_norm_iff, summable_nat_add_iff (f := fun n : ℕ ↦ ((n : ℝ) ^ (1 + k))⁻¹)]

Premises used: summable_nat_add_iff, summable_norm_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ 1 < 1 + k

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (HPow.hPow (α := ℝ) (↑n : ℝ) (1 + k))⁻¹

Tactic:
exact summable_nat_pow_inv.mpr <| by lia

Premises used: Iff.mpr, Real.summable_nat_pow_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℂ
ha : a ∈ K
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
⊢ 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⟩

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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
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 : ℤ))
⊢ Norm.norm (E := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ (↑a : ℂ)) ≤ cotTermUpperBound k A B hB n

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]

Premises used: one_pow, add_mul, UpperHalfPlane.im_pos, _private.0.cotTermUpperBound, norm_pow, Int.reduceNeg, Complex.norm_natCast, two_mul, NormOneClass.norm_one, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet, norm_neg, norm_zpow, Complex.norm_mul, one_mul, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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
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 : ℤ)
⊢ (↑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:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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
⊢ ‖(↑(![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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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)
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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)
⊢ ‖(↑(![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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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 : ℤ)
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 : ℤ)

Tactic:
apply norm_add_le_of_le

Premises used: norm_add_le_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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 : ℤ)‖ ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
      |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
simpa (disch := positivity) [sub_eq_add_neg, ← Real.rpow_intCast, abs_norm_eq_max_natAbs,
      abs_of_nonneg] using h1

Premises used: sub_eq_add_neg, abs_of_nonneg, EisensteinSeries.abs_norm_eq_max_natAbs, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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 : ℤ)‖ ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) *
      |HAdd.hAdd (α := ℝ) (↑n : ℝ) 1| ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
simpa (disch := positivity) [sub_eq_add_neg, ← Real.rpow_intCast, abs_norm_eq_max_natAbs,
      abs_of_nonneg] using h2

Premises used: sub_eq_add_neg, abs_of_nonneg, EisensteinSeries.abs_norm_eq_max_natAbs, Real.rpow_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
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
⊢ SummableLocallyUniformlyOn (α := ℂ) (fun (n : ℕ) ↦ iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ) ℍₒ

Tactic:
apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet

Premises used: SummableLocallyUniformlyOn_of_locally_bounded, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
⊢ ∀ x ∈ K, 0 < x.im

Tactic:
hK

Premises used: Set.Mem, Set.Subset
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
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
⊢ ∃ (u : ℕ → ℝ),
    Summable u ∧
      ∀ (n : ℕ), ∀ k_1 ∈ K, Norm.norm (E := ℂ) (iteratedDerivWithin k (fun (z : ℂ) ↦ cotTerm z n) ℍₒ k_1) ≤ u n

Tactic:
lift K to Set ℍ using hK

Premises used: UpperHalfPlane, Set
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
K : Set ℍ
hKc : IsCompact (UpperHalfPlane.coe '' K)
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
⊢ ∃ (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)

Premises used: Iff.mpr, UpperHalfPlane.subset_verticalStrip_of_isCompact, Topology.IsEmbedding.isCompact_iff, UpperHalfPlane.isEmbedding_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
K : Set ℍ
hKc : IsCompact (UpperHalfPlane.coe '' K)
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
⊢ UpperHalfPlane.coe '' K ⊆ UpperHalfPlane.coe '' verticalStrip A B

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
K : Set ℍ
hKc : IsCompact (UpperHalfPlane.coe '' K)
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:
exact ⟨cotTermUpperBound k A B hB, summable_cotTermUpperBound A B hB hk,
    iteratedDerivWithin_cotTerm_bounded_uniformly A B hB <| by gcongr⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
this :
  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 : ℤ)))
    ℍₒ
⊢ DifferentiableOn ℂ (F := ℂ) (iteratedDerivWithin l (fun (z : ℂ) ↦ cotTerm z n) ℍₒ) ℍₒ

Tactic:
this.congr fun z hz ↦ eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet l n hz

Premises used: DifferentiableOn.congr, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
this :
  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 : ℤ)))
    ℍₒ
⊢ DifferentiableOn ℂ (F := ℂ) (iteratedDerivWithin l (fun (z : ℂ) ↦ cotTerm z n) ℍₒ) ℍₒ

Tactic:
exact this.congr fun z hz ↦ eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet l n hz

Premises used: DifferentiableOn.congr, eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
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 : ℤ)))
    ℍₒ
⊢ DifferentiableOn ℂ (F := ℂ) (iteratedDerivWithin l (fun (z : ℂ) ↦ cotTerm z n) ℍₒ) ℍₒ

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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
ha :
  DifferentiableOn ℂ (F := ℂ)
    (fun (y : ℂ) ↦
      (y + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ) +
        (y - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑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 : ℤ)))
    ℍₒ

Tactic:
apply DifferentiableOn.const_mul

Premises used: DifferentiableOn.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
ha :
  DifferentiableOn ℂ (F := ℂ) (fun (y : ℂ) ↦ (y + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑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 : ℤ))
    ℍₒ

Tactic:
apply DifferentiableOn.add

Premises used: DifferentiableOn.add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (y : ℂ) ↦ y + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ℍₒ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
ha : ∀ (x : ℂ) (hx : x ∈ ℍₒ), x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ DifferentiableOn ℂ (F := ℂ) (fun (y : ℂ) ↦ (y + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ)) ℍₒ

Tactic:
refine DifferentiableOn.zpow (by fun_prop) <| .inl fun x hx ↦ ?_

Premises used: DifferentiableOn.zpow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (y : ℂ) ↦ y - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ℍₒ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
ha : ∀ (x : ℂ) (hx : x ∈ ℍₒ), x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0
⊢ DifferentiableOn ℂ (F := ℂ) (fun (y : ℂ) ↦ (y - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑l : ℤ)) ℍₒ

Tactic:
refine DifferentiableOn.zpow (by fun_prop) <| .inl fun x hx ↦ ?_

Premises used: DifferentiableOn.zpow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0

Tactic:
simpa [add_eq_zero_iff_neg_eq'] using (UpperHalfPlane.ne_intCast (.mk x hx) (-(n + 1))).symm

Premises used: UpperHalfPlane.mk, Ne.symm, Nat.cast, HAdd.hAdd, add_eq_zero_iff_neg_eq', OfNat.ofNat, UpperHalfPlane.ne_intCast, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 ≠ 0

Tactic:
simpa [sub_eq_zero] using (UpperHalfPlane.ne_intCast (.mk x hx) (n + 1))

Premises used: sub_eq_zero, UpperHalfPlane.mk, Nat.cast, HAdd.hAdd, OfNat.ofNat, UpperHalfPlane.ne_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ 2 ≤ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
x : ℂ
apply :
  ∀ (b : ℕ),
    (((↑1 : ℂ) * x + (↑(↑(b + 1) : ℤ) : ℂ)) ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)⁻¹ =
      (x + HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ (x + HAdd.hAdd (α := ℂ) (↑n : ℂ) 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

Premises used: Iff.mpr, summable_nat_add_iff, EisensteinSeries.linear_right_summable, summable_int_iff_summable_nat_and_neg, And.left, Iff.mp, Summable.congr, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ ∀ (b : ℕ),
    (((↑1 : ℂ) * x + (↑(↑(b + 1) : ℤ) : ℂ)) ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)⁻¹ =
      (x + HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
simp [← zpow_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, zpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
x : ℂ
apply :
  ∀ (b : ℕ),
    (((↑1 : ℂ) * x + (↑(-(↑(b + 1) : ℤ)) : ℂ)) ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)⁻¹ =
      (x - HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ (x - HAdd.hAdd (α := ℂ) (↑n : ℂ) 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

Premises used: Iff.mpr, summable_nat_add_iff, EisensteinSeries.linear_right_summable, summable_int_iff_summable_nat_and_neg, And.right, Iff.mp, Summable.congr, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
x : ℂ
⊢ ∀ (b : ℕ),
    (((↑1 : ℂ) * x + (↑(-(↑(b + 1) : ℤ)) : ℂ)) ^ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1)⁻¹ =
      (x - HAdd.hAdd (α := ℂ) (↑b : ℂ) 1) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
simp [← zpow_neg, sub_eq_add_neg]

Premises used: sub_eq_add_neg, zpow_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
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 : ℤ)
⊢ 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 : ℤ)

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

Premises used: differentiableOn_iteratedDerivWithin_cotTerm, summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm, DifferentiableOn.differentiableAt, UpperHalfPlane.mk, UpperHalfPlane.coe_mem_integerComplement, IsOpen.mem_nhds, summable_cotTerm, iteratedDerivWithin_tsum, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
h : ∀ (n : ℕ), iteratedDerivWithin k (fun (t : ℂ) ↦ cotTerm t n) ℍₒ 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 : ℤ)

Tactic:
enter [1, 2, 1, n]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
⊢ z ∈ ℍₒ

Tactic:
simp [hz]