awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
h : cos x ≠ -1
⊢ cos x = (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)

Tactic:
mod_cast @Complex.cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq x (mod_cast h)

Premises used: Int.cast_neg, Complex.cos, Real.cos, Complex.cos_eq_two_mul_tan_half_div_one_sub_tan_half_sq, congrArg, Complex.ofReal_sub._simp_1, Int.cast_negSucc._simp_1, Complex.ofReal_div._simp_1, HSub.hSub, Complex.ofReal_neg, cast, HDiv.hDiv, Ne, Complex.ofReal_pow._simp_1, Complex.ofReal, Nat.cast, HPow.hPow, Complex.ofReal_cos._simp_1, HAdd.hAdd, Complex.tan, congr, congrFun', Complex.ofReal_tan._simp_1, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Not, Complex.ofReal_add._simp_1, Neg.neg, Int.cast_one, Complex.ofReal_inj._simp_1, Eq.trans, Real.tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
⊢ sin x = 2 * tan (x / 2) / (1 + HPow.hPow (β := ℕ) (tan (x / 2)) 2)

Tactic:
mod_cast @Complex.sin_eq_two_mul_tan_half_div_one_add_tan_half_sq x

Premises used: HMul.hMul, congrArg, Complex.sin, Complex.ofReal_div._simp_1, cast, HDiv.hDiv, Complex.ofReal_pow._simp_1, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, HPow.hPow, HAdd.hAdd, Complex.tan, Complex.sin_eq_two_mul_tan_half_div_one_add_tan_half_sq, congr, Complex.ofReal_sin._simp_1, congrFun', Complex.ofReal_tan._simp_1, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Real.sin, Complex.ofReal_add._simp_1, Complex.ofReal_inj._simp_1, Eq.trans, Real.tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Goal:
x : ℝ
⊢ tan x = 2 * tan (x / 2) / (1 - HPow.hPow (β := ℕ) (tan (x / 2)) 2)

Tactic:
mod_cast @Complex.tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq x

Premises used: HMul.hMul, congrArg, Complex.ofReal_sub._simp_1, Complex.ofReal_div._simp_1, HSub.hSub, cast, HDiv.hDiv, Complex.ofReal_pow._simp_1, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, HPow.hPow, Complex.tan, congr, congrFun', Complex.ofReal_tan._simp_1, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Complex.ofReal_inj._simp_1, Eq.trans, Complex.tan_eq_one_sub_tan_half_sq_div_one_add_tan_half_sq, Real.tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
h : cos x ≠ 0
⊢ HasStrictDerivAt (sin / cos) ((cos x * cos x - sin x * -sin x) / HPow.hPow (β := ℕ) (cos x) 2) x

Tactic:
(hasStrictDerivAt_sin x).div (hasStrictDerivAt_cos x) h

Premises used: HasStrictDerivAt.div, Complex.hasStrictDerivAt_cos, Complex.hasStrictDerivAt_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
h : cos x ≠ 0
h₁ : 1 / HPow.hPow (β := ℕ) (cos x) 2 = (cos x * cos x - sin x * -sin x) / HPow.hPow (β := ℕ) (cos x) 2
⊢ HasStrictDerivAt tan (1 / HPow.hPow (β := ℕ) (cos x) 2) x

Tactic:
convert! (hasStrictDerivAt_sin x).div (hasStrictDerivAt_cos x) h using 1

Premises used: HasStrictDerivAt.div, Complex.hasStrictDerivAt_cos, Complex.hasStrictDerivAt_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
h : cos x ≠ 0
h₁ :
  ∀ (h : ¬cos x = 0),
    (HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2) / HPow.hPow (β := ℕ) (cos x) 2 =
      (cos x * cos x - sin x * -sin x) / HPow.hPow (β := ℕ) (cos x) 2
⊢ 1 / HPow.hPow (β := ℕ) (cos x) 2 = (cos x * cos x - sin x * -sin x) / HPow.hPow (β := ℕ) (cos x) 2

Tactic:
rw_mod_cast [← sin_sq_add_cos_sq x]

Premises used: Complex.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
h : ¬cos x = 0
⊢ (HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2) / HPow.hPow (β := ℕ) (cos x) 2 =
    (cos x * cos x - sin x * -sin x) / HPow.hPow (β := ℕ) (cos x) 2

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
h : cos x ≠ 0
⊢ HasDerivAt tan (1 / HPow.hPow (β := ℕ) (cos x) 2) x

Tactic:
(hasStrictDerivAt_tan h).hasDerivAt

Premises used: Complex.hasStrictDerivAt_tan, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
hx : cos x = 0
simp : Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖tan x‖) (𝓝[≠] x) atTop

Tactic:
simp only [tan_eq_sin_div_cos, norm_div]

Premises used: Complex.tan_eq_sin_div_cos, norm_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
hx : cos x = 0
h : sin x = 0
⊢ False

Tactic:
simpa [*, sq] using sin_sq_add_cos_sq x

Premises used: sq, Complex.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
hx : cos x = 0
⊢ sin x ≠ 0

Tactic:
have A : sin x ≠ 0 := fun h => by simpa [*, sq] using sin_sq_add_cos_sq x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
⊢ Tendsto cos (𝓝[≠] x) (𝓝[≠] 0)

Tactic:
have B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0) :=
    hx ▸ (hasDerivAt_cos x).tendsto_nhdsNE (neg_ne_zero.2 A)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0)
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop

Tactic:
continuous_sin.continuousWithinAt.norm.pos_mul_atTop (norm_pos_iff.2 A)
    (tendsto_norm_nhdsNE_zero.comp B).inv_tendsto_nhdsGT_zero

Premises used: Iff.mpr, norm_pos_iff, Complex.continuous_sin, Filter.Tendsto.pos_mul_atTop, ContinuousWithinAt.norm, DivInvMonoid.div', Filter.Tendsto.inv_tendsto_nhdsGT_zero, tendsto_norm_nhdsNE_zero, Filter.Tendsto.comp, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
hx : cos x = 0
A : sin x ≠ 0
B : Tendsto cos (𝓝[≠] x) (𝓝[≠] 0)
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖sin x‖ / ‖cos x‖) (𝓝[≠] x) atTop

Tactic:
exact continuous_sin.continuousWithinAt.norm.pos_mul_atTop (norm_pos_iff.2 A)
    (tendsto_norm_nhdsNE_zero.comp B).inv_tendsto_nhdsGT_zero

Premises used: Iff.mpr, norm_pos_iff, Complex.continuous_sin, Filter.Tendsto.pos_mul_atTop, ContinuousWithinAt.norm, Filter.Tendsto.inv_tendsto_nhdsGT_zero, tendsto_norm_nhdsNE_zero, Filter.Tendsto.comp, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
k : ℤ
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ‖tan x‖) (𝓝[≠] ((HMul.hMul (α := ℂ) 2 (↑k : ℂ) + 1) * (↑π : ℂ) / 2)) atTop

Tactic:
tendsto_norm_tan_of_cos_eq_zero <| cos_eq_zero_iff.2 ⟨k, rfl⟩

Premises used: Iff.mpr, Complex.cos_eq_zero_iff, Complex.tendsto_norm_tan_of_cos_eq_zero, Exists.intro, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
⊢ ContinuousAt tan x ↔ cos x ≠ 0

Tactic:
⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩

Premises used: HasDerivAt.continuousAt, Iff.intro, Complex.hasDerivAt_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
refine : ∀ (hc : ContinuousAt tan x) (h₀ : cos x = 0), False
⊢ ContinuousAt tan x ↔ cos x ≠ 0

Tactic:
refine ⟨fun hc h₀ => ?_, fun h => (hasDerivAt_tan h).continuousAt⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False

Tactic:
not_tendsto_nhds_of_tendsto_atTop (tendsto_norm_tan_of_cos_eq_zero h₀) _
    (hc.norm.tendsto.mono_left inf_le_left)

Premises used: not_tendsto_nhds_of_tendsto_atTop, Complex.tendsto_norm_tan_of_cos_eq_zero, ContinuousAt.tendsto, ContinuousAt.norm, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
hc : ContinuousAt tan x
h₀ : cos x = 0
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_norm_tan_of_cos_eq_zero h₀) _
    (hc.norm.tendsto.mono_left inf_le_left)

Premises used: not_tendsto_nhds_of_tendsto_atTop, Complex.tendsto_norm_tan_of_cos_eq_zero, ContinuousAt.tendsto, ContinuousAt.norm, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
⊢ DifferentiableAt ℂ tan x ↔ cos x ≠ 0

Tactic:
⟨fun h => continuousAt_tan.1 h.continuousAt, fun h => (hasDerivAt_tan h).differentiableAt⟩

Premises used: HasDerivAt.differentiableAt, DifferentiableAt.continuousAt, Iff.intro, Iff.mp, Complex.hasDerivAt_tan, Complex.continuousAt_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
h : cos x = 0
⊢ ¬DifferentiableAt ℂ tan x

Tactic:
have : ¬DifferentiableAt ℂ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
h : cos x = 0
this : ¬DifferentiableAt ℂ tan x
⊢ deriv tan x = 1 / HPow.hPow (β := ℕ) (cos x) 2

Tactic:
simp [deriv_zero_of_not_differentiableAt this, h, sq]

Premises used: deriv_zero_of_not_differentiableAt, sq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Goal:
x : ℂ
n : WithTop ℕ∞
⊢ ContDiffAt ℂ n tan x ↔ cos x ≠ 0

Tactic:
⟨fun h => continuousAt_tan.1 h.continuousAt, contDiff_sin.contDiffAt.div contDiff_cos.contDiffAt⟩

Premises used: ContDiffAt.div, Iff.intro, Iff.mp, ContDiffAt.continuousAt, Complex.contDiff_sin, Complex.contDiff_cos, Complex.continuousAt_tan, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
rw : cexp (z * I) + cexp (-z * I) = cexp (-(z * I) + 2 * I * z) + cexp (-(z * I)) * 1
⊢ cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)

Tactic:
rw [mul_add, ← Complex.exp_add]

Premises used: Complex.exp_add, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
⊢ cexp (z * I) + cexp (-z * I) = cexp (-(z * I) + 2 * I * z) + cexp (-(z * I)) * 1

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
⊢ cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)

Tactic:
have h1 : exp (z * I) + exp (-z * I) = exp (-(z * I)) * (exp (2 * I * z) + 1) := by
    rw [mul_add, ← Complex.exp_add]
    ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
ring_nf : cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I)) * cexp (z * I * 2)
⊢ cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
rw : cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I) + z * (I * 2))
⊢ cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I)) * cexp (z * I * 2)

Tactic:
rw [mul_assoc, ← Complex.exp_add]

Premises used: Complex.exp_add, mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ cexp (-(z * I)) - cexp (z * I) = cexp (-(z * I)) - cexp (-(z * I) + z * (I * 2))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
⊢ cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))

Tactic:
have h2 : (exp (-z * I) - exp (z * I)) = exp (-(z * I)) * ((1 - exp (2 * I * z))) := by
    ring_nf
    rw [mul_assoc, ← Complex.exp_add]
    ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
h2 : cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))
rw :
  cexp (-(z * I)) * (cexp (2 * I * z) + 1) / 2 / (cexp (-(z * I)) * (1 - cexp (2 * I * z)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))
⊢ (cexp (z * I) + cexp (-z * I)) / 2 / ((cexp (-z * I) - cexp (z * I)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Tactic:
rw [h1, h2]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
h1 : cexp (z * I) + cexp (-z * I) = cexp (-(z * I)) * (cexp (2 * I * z) + 1)
h2 : cexp (-z * I) - cexp (z * I) = cexp (-(z * I)) * (1 - cexp (2 * I * z))
⊢ cexp (-(z * I)) * (cexp (2 * I * z) + 1) / 2 / (cexp (-(z * I)) * (1 - cexp (2 * I * z)) * I / 2) =
    (cexp (2 * I * z) + 1) / (I * (1 - cexp (2 * I * z)))

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
rw :
  (cexp (2 * I * ((↑π : ℂ) * z)) + 1) / (I * (1 - cexp (2 * I * ((↑π : ℂ) * z)))) =
    (cexp (2 * (↑π : ℂ) * I * z) + 1) / (I * (1 - cexp (2 * (↑π : ℂ) * I * z)))
⊢ ((↑π : ℂ) * z).cot = (cexp (2 * (↑π : ℂ) * I * z) + 1) / (I * (1 - cexp (2 * (↑π : ℂ) * I * z)))

Tactic:
rw [cot_eq_exp_ratio (π * z)]

Premises used: Real.pi, HMul.hMul, Complex.ofReal, Complex.cot_eq_exp_ratio
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℂ
⊢ (cexp (2 * I * ((↑π : ℂ) * z)) + 1) / (I * (1 - cexp (2 * I * ((↑π : ℂ) * z)))) =
    (cexp (2 * (↑π : ℂ) * I * z) + 1) / (I * (1 - cexp (2 * (↑π : ℂ) * I * z)))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℍ
simp :
  (↑π : ℂ) * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) * I * (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)))⁻¹) =
    (↑π : ℂ) * I * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) * (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)))⁻¹)
⊢ (↑π : ℂ) * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) / (I * (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))))) =
    -(↑π : ℂ) * I * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) * (1 / (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)))))

Tactic:
simp only [div_mul_eq_div_mul_one_div, div_I, one_div, neg_mul, mul_neg, neg_inj]

Premises used: one_div, neg_inj, Complex.div_I, neg_mul, div_mul_eq_div_mul_one_div, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℍ
⊢ (↑π : ℂ) * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) * I * (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)))⁻¹) =
    (↑π : ℂ) * I * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) * (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)))⁻¹)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℍ
⊢ (↑π : ℂ) * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) / (I * (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))))) =
    -(↑π : ℂ) * I * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) * (1 / (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)))))

Tactic:
have h1 : π * ((exp (2 * π * I * z) + 1) / (I * (1 - exp (2 * π * I * z)))) =
      -π * I * ((exp (2 * π * I * z) + 1) * (1 / (1 - exp (2 * π * I * z)))) := by
    simp only [div_mul_eq_div_mul_one_div, div_I, one_div, neg_mul, mul_neg, neg_inj]
    ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℍ
h1 :
  (↑π : ℂ) * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) / (I * (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))))) =
    -(↑π : ℂ) * I * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) * (1 / (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)))))
rw :
  -(↑π : ℂ) * I * (HMul.hMul (α := ℂ) 2 (∑' (i : ℕ), cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ i) - 1) =
    (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
⊢ (↑π : ℂ) * ((↑π : ℂ) * (↑z : ℂ)).cot =
    (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n

Tactic:
rw [cot_pi_eq_exp_ratio, h1, one_div, (tsum_geometric_of_norm_lt_one
    (UpperHalfPlane.norm_exp_two_pi_I_lt_one z)).symm, add_comm, geom_series_mul_one_add
      (Complex.exp (2 * π * I * (z : ℂ))) (UpperHalfPlane.norm_exp_two_pi_I_lt_one _)]

Premises used: Real.pi, HMul.hMul, UpperHalfPlane.coe, tsum_geometric_of_norm_lt_one, UpperHalfPlane.norm_exp_two_pi_I_lt_one, Complex.cot_pi_eq_exp_ratio, Complex.ofReal, add_comm, geom_series_mul_one_add, one_div, Complex.exp, OfNat.ofNat, Eq.symm, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
z : ℍ
h1 :
  (↑π : ℂ) * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) / (I * (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))))) =
    -(↑π : ℂ) * I * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) * (1 / (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)))))
⊢ -(↑π : ℂ) * I * (HMul.hMul (α := ℂ) 2 (∑' (i : ℕ), cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ i) - 1) =
    (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
rw : ¬1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 = - -HPow.hPow (β := ℕ) x 2
rw₁ : HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 ≠ 0
⊢ ¬1 + -HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 = 0

Tactic:
rw [add_eq_zero_iff_eq_neg, neg_div', eq_div_iff]

Premises used: neg_div', add_eq_zero_iff_eq_neg, eq_div_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ HPow.hPow (β := ℕ) x 2 ≠ HPow.hPow (α := ℂ) (β := ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 2

Tactic:
have := (integerComplement_pow_two_ne_pow_two hx (n + 1 : ℤ))
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
this : HPow.hPow (β := ℕ) x 2 ≠ HPow.hPow (α := ℂ) (β := ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 2
⊢ ¬1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 = - -HPow.hPow (β := ℕ) x 2

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 ≠ 0

Tactic:
simp [Nat.cast_add_one_ne_zero n]

Premises used: Nat.cast_add_one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
h0 : x ≠ 0
⊢ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x) = Complex.sin ((↑π : ℂ) * x) * (1 / ((↑π : ℂ) * x))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
h0 : x ≠ 0
rw :
  Tendsto (fun (n : ℕ) ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop
    (𝓝 (Complex.sin ((↑π : ℂ) * x) * (1 / ((↑π : ℂ) * x))))
⊢ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop
    (𝓝 (Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)))

Tactic:
rw [show (sin (π * x) / (π * x)) = sin (π * x) * (1 / (π * x)) by ring]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
h0 : x ≠ 0
apply :
  ∀ (x_1 : ℕ),
    ((↑π : ℂ) * x *
          ∏ j ∈ Finset.range x_1, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        (1 / ((↑π : ℂ) * x)) =
      ∏ i ∈ Finset.range x_1, (1 + sineTerm x i)
⊢ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop
    (𝓝 (Complex.sin ((↑π : ℂ) * x) * (1 / ((↑π : ℂ) * x))))

Tactic:
apply (Filter.Tendsto.mul_const (b := 1 / (π * x)) (tendsto_euler_sin_prod x)).congr

Premises used: Real.pi, HMul.hMul, Filter.Tendsto.mul_const, HDiv.hDiv, Complex.tendsto_euler_sin_prod, Complex.ofReal, Filter.Tendsto.congr, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
h0 : x ≠ 0
n : ℕ
field_simp :
  Eq (α := ℂ)
    (∏ x_1 ∈ Finset.range n,
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x_1 : ℂ) 1) 2 - HPow.hPow (β := ℕ) x 2) /
        HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x_1 : ℂ) 1) 2)
    (∏ x_1 ∈ Finset.range n,
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x_1 : ℂ) 1) 2 + -HPow.hPow (β := ℕ) x 2) /
        HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x_1 : ℂ) 1) 2)
⊢ ((↑π : ℂ) * x *
        ∏ j ∈ Finset.range n, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
      (1 / ((↑π : ℂ) * x)) =
    ∏ i ∈ Finset.range n, (1 + sineTerm x i)

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
h0 : x ≠ 0
n : ℕ
⊢ Eq (α := ℂ)
    (∏ x_1 ∈ Finset.range n,
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x_1 : ℂ) 1) 2 - HPow.hPow (β := ℕ) x 2) /
        HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x_1 : ℂ) 1) 2)
    (∏ x_1 ∈ Finset.range n,
      (HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x_1 : ℂ) 1) 2 + -HPow.hPow (β := ℕ) x 2) /
        HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑x_1 : ℂ) 1) 2)

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
h0 : x ≠ 0
⊢ ∀ (x_1 : ℕ),
    ((↑π : ℂ) * x *
          ∏ j ∈ Finset.range x_1, (1 - HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑j : ℂ) 1) 2)) *
        (1 / ((↑π : ℂ) * x)) =
      ∏ i ∈ Finset.range x_1, (1 + sineTerm x i)

Tactic:
exact fun n ↦ by field_simp; rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hf : Summable (α := ℝ) fun (i : ℕ) ↦ ‖sineTerm x i‖
⊢ Multipliable (α := ℂ) fun (i : ℕ) ↦ 1 + sineTerm x i

Tactic:
apply multipliable_one_add_of_summable

Premises used: multipliable_one_add_of_summable
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) (↑1 : ℂ)) 2‖

Tactic:
have := summable_pow_div_add (x ^ 2) 2 1 Nat.one_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
this :
  Summable (α := ℝ) fun (n : ℕ) ↦ ‖HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) (↑1 : ℂ)) 2‖
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖sineTerm x i‖

Tactic:
simpa [sineTerm] using this

Premises used: sineTerm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
rw :
  Tendsto (fun (n : ℕ) ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop
    (𝓝 (Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)))
⊢ ∏' (i : ℕ), (1 + sineTerm x i) = Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)

Tactic:
rw [← Multipliable.hasProd_iff (multipliable_sineTerm x),
    Multipliable.hasProd_iff_tendsto_nat (multipliable_sineTerm x)]

Premises used: Multipliable.hasProd_iff_tendsto_nat, Multipliable.hasProd_iff, multipliable_sineTerm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop
    (𝓝 (Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)))

Tactic:
tendsto_euler_sin_prod' (integerComplement.ne_zero hx)

Premises used: Complex.integerComplement.ne_zero, tendsto_euler_sin_prod'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop
    (𝓝 (Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)))

Tactic:
exact tendsto_euler_sin_prod' (integerComplement.ne_zero hx)

Premises used: Complex.integerComplement.ne_zero, tendsto_euler_sin_prod'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZ : IsCompact Z
⊢ ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖-HPow.hPow (β := ℕ) x 2‖) Z

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZ : IsCompact Z
⊢ ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖-HPow.hPow (β := ℕ) x 2‖) Z

Tactic:
have hf : ContinuousOn (fun x : ℂ => ‖-x ^ 2‖) Z := by
    fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖-HPow.hPow (β := ℕ) x 2‖) Z
obtain :
  ∀ (s : ℝ) (hs : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℂ) ↦ ‖-HPow.hPow (β := ℕ) x 2‖) '' Z) y → y ≤ s),
    ∃ (u : ℕ → ℝ), Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ ∃ (u : ℕ → ℝ), Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j

Tactic:
obtain ⟨s, hs⟩ := bddAbove_def.mp (IsCompact.bddAbove_image hZ hf)

Premises used: IsCompact.bddAbove_image, Iff.mp, bddAbove_def
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖-HPow.hPow (β := ℕ) x 2‖) Z
s : ℝ
hs : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) ((fun (x : ℂ) ↦ ‖-HPow.hPow (β := ℕ) x 2‖) '' Z) y → y ≤ s
⊢ ∃ (u : ℕ → ℝ), Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j

Tactic:
⟨fun n : ℕ => ‖(s : ℂ) / (n + 1) ^ 2‖, ?_, ?_⟩

Premises used: Norm.norm, HDiv.hDiv, Complex.ofReal, Nat.cast, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat