awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
n : ℕ
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
| iteratedDerivWithin k (fun (t : ℂ) ↦ cotTerm t n) ℍₒ z

Tactic:
rw [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (by simp [hz])]

Premises used: eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
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
| 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]
    rw [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (by simp [hz])]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
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 : ℤ)
⊢ 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:
conv =>
    enter [1, 2, 1, n]
    rw [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (by simp [hz])]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ (z + (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
simpa using aux_summable_add hk z

Premises used: _private.0.aux_summable_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ (z + (↑(-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
simpa [sub_eq_add_neg] using aux_summable_sub hk z

Premises used: _private.0.aux_summable_sub, sub_eq_add_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 : ℤ) +
      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 : ℤ))
⊢ 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:
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)]

Premises used: _private.0.aux_summable_add, _private.0.aux_summable_sub, tsum_mul_left, tsum_of_add_one_of_neg_add_one, Summable.tsum_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
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 : ℤ))
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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 : ℤ))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
simp :
  Eq (α := ℂ) (iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot - x⁻¹) ℍₒ z)
    (iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cotTerm z n) ℍₒ 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 : ℤ)

Tactic:
simp only [← aux_iteratedDeriv_tsum_cotTerm hk hz, one_div, neg_mul, neg_add_cancel_left]

Premises used: _private.0.aux_iteratedDeriv_tsum_cotTerm, one_div, neg_mul, neg_add_cancel_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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)

Tactic:
iteratedDerivWithin_congr (fun z hz ↦ ?_) hz

Premises used: iteratedDerivWithin_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
refine : ∀ (z : ℂ) (hz : z ∈ ℍₒ), (↑π : ℂ) * ((↑π : ℂ) * z).cot - z⁻¹ = ∑' (n : ℕ), cotTerm z n
⊢ Eq (α := ℂ) (iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot - x⁻¹) ℍₒ z)
    (iteratedDerivWithin k (fun (z : ℂ) ↦ ∑' (n : ℕ), cotTerm z n) ℍₒ z)

Tactic:
refine iteratedDerivWithin_congr (fun z hz ↦ ?_) hz

Premises used: iteratedDerivWithin_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z_1 : ℂ
k : ℕ
hk : 1 ≤ k
hz_1 : z_1 ∈ ℍₒ
z : ℂ
hz : z ∈ ℍₒ
⊢ (↑π : ℂ) * ((↑π : ℂ) * z).cot - z⁻¹ = ∑' (n : ℕ), cotTerm z n

Tactic:
simpa [cotTerm] using (cot_series_rep' (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩))

Premises used: cot_series_rep', UpperHalfPlane.mk, UpperHalfPlane.coe_mem_integerComplement, cotTerm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
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 : ℤ)))
hf : ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z
hg : ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ -(1 / x)) ℍₒ 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 : ℤ)))

Tactic:
rw [iteratedDerivWithin_fun_add hz isOpen_upperHalfPlaneSet.uniqueDiffOn]

Premises used: iteratedDerivWithin_fun_add, IsOpen.uniqueDiffOn, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ 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:
simpa [iteratedDerivWithin_fun_neg] using iteratedDerivWithin_one_div k
      isOpen_upperHalfPlaneSet hz

Premises used: iteratedDerivWithin_one_div, UpperHalfPlane.isOpen_upperHalfPlaneSet, iteratedDerivWithin_fun_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ (↑π : ℂ)) ℍₒ z

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z

Tactic:
exact ContDiffWithinAt.mul (by fun_prop) (cot_pi_mul_contDiffWithinAt k
      (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩))

Premises used: ContDiffWithinAt.mul, UpperHalfPlane.mk, UpperHalfPlane.coe_mem_integerComplement, Nat.cast, cot_pi_mul_contDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
hg : ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ -x⁻¹) ℍₒ z
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ -(1 / x)) ℍₒ z

Tactic:
simp only [one_div]

Premises used: one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
hg : ContDiffWithinAt ℂ (↑k : WithTop ℕ∞) Inv.inv ℍₒ z
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ -x⁻¹) ℍₒ z

Tactic:
apply ContDiffWithinAt.neg

Premises used: ContDiffWithinAt.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞) (fun (x : ℂ) ↦ x) ℍₒ z

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k : WithTop ℕ∞) Inv.inv ℍₒ z

Tactic:
exact ContDiffWithinAt.inv (by fun_prop) (ne_zero ⟨z, hz⟩)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ 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 ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
have h0 := iteratedDerivWithin_cot_pi_mul_sub_inv k hz
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x) ℍₒ z =
    iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ 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 (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
rw [iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum hk hz, add_comm] at h0

Premises used: add_comm, iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  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 (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
rw :
  iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z +
      -HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) =
    iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
rw [← add_left_inj (-(-1) ^ k * k ! * z ^ (-1 - k : ℤ)), h0]

Premises used: HMul.hMul, HSub.hSub, add_left_inj, Nat.cast, HPow.hPow, Nat.factorial, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  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 (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z +
      -HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ) =
    iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z -
      HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * z ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow hk hz

Premises used: iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h : ∀ (n : ℤ), 1 / (z + (↑n : ℂ)) ^ (k + 1) = (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ iteratedDerivWithin k (fun (x : ℂ) ↦ (↑π : ℂ) * ((↑π : ℂ) * x).cot) ℍₒ z =
    HPow.hPow (α := ℂ) (-1) k * (↑k ! : ℂ) * ∑' (n : ℤ), 1 / (z + (↑n : ℂ)) ^ (k + 1)

Tactic:
convert! iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow hk hz with n

Premises used: iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ Int.negSucc 0 - (↑k : ℤ) = Int.negSucc k

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ 0 < k + 1

Tactic:
lia
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
h : 1 / (z + (↑n : ℂ)) ^ (k + 1) = HPow.hPow (β := ℤ) (z + (↑n : ℂ)) (-(↑(k + 1) : ℤ))
h₁ : 1 / (z + (↑n : ℂ)) ^ (k + 1) = ((z + (↑n : ℂ)) ^ (k + 1))⁻¹
h₂ h₃ : ((z + (↑n : ℂ)) ^ (k + 1))⁻¹ = ((z + (↑n : ℂ)) ^ (k + 1))⁻¹
⊢ 1 / (z + (↑n : ℂ)) ^ (k + 1) = (z + (↑n : ℂ)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
rw [show (-1 - k : ℤ) = -(k + 1 :) by norm_cast; lia, zpow_neg_coe_of_pos _ (by lia),
    one_div]

Premises used: zpow_neg_coe_of_pos, one_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ HasStrictDerivAt
    (fun (y : ℂ) ↦
      HSub.hSub (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (x : ℂ) ↦ cexp (-id x * I)) (fun (x : ℂ) ↦ cexp (id x * I)) y * I * 2⁻¹)
    ((cexp (-id x * I) * (-1 * I) - cexp (id x * I) * (1 * I)) * I * 2⁻¹) x

Tactic:
((((hasStrictDerivAt_id x).fun_neg.mul_const I).cexp.sub
              ((hasStrictDerivAt_id x).mul_const I).cexp).mul_const
          I).mul_const
      (2 : ℂ)⁻¹

Premises used: HasStrictDerivAt.mul_const, HasStrictDerivAt.cexp, HasStrictDerivAt.sub, Inv.inv, HasStrictDerivAt.fun_neg, OfNat.ofNat, hasStrictDerivAt_id, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-id x * I) * (-1 * I) - cexp (id x * I) * (1 * I)) * I * 2⁻¹
⊢ HasStrictDerivAt sin ((cexp (x * I) + cexp (-x * I)) * 2⁻¹) x

Tactic:
convert!
    ((((hasStrictDerivAt_id x).fun_neg.mul_const I).cexp.sub
              ((hasStrictDerivAt_id x).mul_const I).cexp).mul_const
          I).mul_const
      (2 : ℂ)⁻¹ using 1

Premises used: HasStrictDerivAt.mul_const, HasStrictDerivAt.cexp, HasStrictDerivAt.sub, Inv.inv, HasStrictDerivAt.fun_neg, OfNat.ofNat, hasStrictDerivAt_id, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-id x * I) * (-1 * I) - cexp (id x * I) * (1 * I)) * I * 2⁻¹

Tactic:
simp only [id]

Premises used: id
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
h : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) * I - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₂ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * (I * I)) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₃ :
  (cexp (x * I) + cexp (-x * I)) * 2⁻¹ =
    (cexp (-x * I) * HMul.hMul (α := ℂ) (-1) (-1) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₄ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₅ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * 1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₆ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (1 * I) * I) * 2⁻¹
h₇ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * I * I) * 2⁻¹
h₈ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * (I * I)) * 2⁻¹
h₉ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - cexp (x * I) * -1) * 2⁻¹
h₁₀ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) - -cexp (x * I)) * 2⁻¹
h₁₁ : (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) + cexp (x * I)) * 2⁻¹
h₁₂ h₁₃ : (cexp (-x * I) + cexp (x * I)) * 2⁻¹ = (cexp (-x * I) + cexp (x * I)) * 2⁻¹
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * I) - cexp (x * I) * (1 * I)) * I * 2⁻¹

Tactic:
rw [sub_mul, mul_assoc, mul_assoc, I_mul_I, neg_one_mul, neg_neg, mul_one, one_mul, mul_assoc,
    I_mul_I, mul_neg_one, sub_neg_eq_add, add_comm]

Premises used: mul_assoc, neg_one_mul, neg_neg, add_comm, sub_mul, Complex.I_mul_I, mul_neg_one, mul_one, one_mul, sub_neg_eq_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ HasDerivAt sin (cos x) x

Tactic:
(hasStrictDerivAt_sin x).hasDerivAt

Premises used: Complex.hasStrictDerivAt_sin, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ sin ~[𝓝 0] id

Tactic:
simpa using (hasDerivAt_sin 0).isLittleO

Premises used: HasDerivAt.isLittleO, Complex.hasDerivAt_sin, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
n : WithTop ℕ∞
⊢ ContDiff ℂ n sin

Tactic:
(((contDiff_neg.mul contDiff_const).cexp.sub (contDiff_id.mul contDiff_const).cexp).mul
    contDiff_const).div_const _

Premises used: ContDiff.sub, ContDiff.div_const, contDiff_id, ContDiff.cexp, Complex.sin, contDiff_const, contDiff_neg, ContDiff.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ Differentiable ℂ sin

Tactic:
fun x => (hasDerivAt_sin x).differentiableAt

Premises used: Differentiable, HasDerivAt.differentiableAt, Complex.hasDerivAt_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ DifferentiableAt ℂ sin x

Tactic:
differentiable_sin x

Premises used: Complex.differentiable_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ AnalyticAt ℂ sin x

Tactic:
contDiff_sin.contDiffAt.analyticAt

Premises used: ContDiffAt.analyticAt, Complex.contDiff_sin, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
s : Set ℂ
⊢ AnalyticWithinAt ℂ sin s x

Tactic:
contDiff_sin.contDiffWithinAt.analyticWithinAt

Premises used: ContDiff.contDiffWithinAt, Complex.contDiff_sin, ContDiffWithinAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
s : Set ℂ
⊢ AnalyticOnNhd ℂ sin s

Tactic:
fun _ _ ↦ analyticAt_sin

Premises used: Complex.analyticAt_sin, AnalyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
s : Set ℂ
⊢ AnalyticOn ℂ sin s

Tactic:
contDiff_sin.contDiffOn.analyticOn

Premises used: ContDiff.contDiffOn, ContDiffOn.analyticOn, Complex.contDiff_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
⊢ deriv sin = cos

Tactic:
funext fun x => (hasDerivAt_sin x).deriv

Premises used: HasDerivAt.deriv, funext, Complex.hasDerivAt_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
simp : HasStrictDerivAt cos (-(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹) x
⊢ HasStrictDerivAt cos (-sin x) x

Tactic:
simp only [sin, div_eq_mul_inv, neg_mul_eq_neg_mul]

Premises used: Complex.sin, div_eq_mul_inv, neg_mul_eq_neg_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
⊢ HasStrictDerivAt
    (fun (y : ℂ) ↦
      HAdd.hAdd (α := ℂ → ℂ) (β := ℂ → ℂ) (fun (x : ℂ) ↦ cexp (id x * I)) (fun (x : ℂ) ↦ cexp (-id x * I)) y * 2⁻¹)
    ((cexp (id x * I) * (1 * I) + cexp (-id x * I) * (-1 * I)) * 2⁻¹) x

Tactic:
(((hasStrictDerivAt_id x).mul_const I).cexp.add
          ((hasStrictDerivAt_id x).fun_neg.mul_const I).cexp).mul_const
      (2 : ℂ)⁻¹

Premises used: HasStrictDerivAt.mul_const, HasStrictDerivAt.cexp, HasStrictDerivAt.add, Inv.inv, HasStrictDerivAt.fun_neg, OfNat.ofNat, hasStrictDerivAt_id, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Goal:
x : ℂ
h : -(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹ = (cexp (id x * I) * (1 * I) + cexp (-id x * I) * (-1 * I)) * 2⁻¹
⊢ HasStrictDerivAt cos (-(cexp (-x * I) - cexp (x * I)) * I * 2⁻¹) x

Tactic:
convert!
    (((hasStrictDerivAt_id x).mul_const I).cexp.add
          ((hasStrictDerivAt_id x).fun_neg.mul_const I).cexp).mul_const
      (2 : ℂ)⁻¹ using 1

Premises used: HasStrictDerivAt.mul_const, HasStrictDerivAt.cexp, HasStrictDerivAt.add, Inv.inv, HasStrictDerivAt.fun_neg, OfNat.ofNat, hasStrictDerivAt_id, Complex.I