awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine_1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑s : ℂ) / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2‖
refine_2 :
  ∀ (j : ℕ),
    ∀ z ∈ Z, ‖sineTerm z j‖ ≤ (fun (n : ℕ) ↦ ‖(↑s : ℂ) / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2‖) j
⊢ ∃ (u : ℕ → ℝ), Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j

Tactic:
refine ⟨fun n : ℕ => ‖(s : ℂ) / (n + 1) ^ 2‖, ?_, ?_⟩
-- 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
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑s : ℂ) / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2‖

Tactic:
simpa using summable_pow_div_add (s : ℂ) 2 1 (Nat.one_lt_two)

Premises used: Nat.one_lt_two, summable_pow_div_add, Complex.ofReal, OfNat.ofNat
-- 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
refine_2 :
  ∀ (hf : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) Z) (hs : ∀ a ∈ Z, HPow.hPow (β := ℕ) ‖a‖ 2 ≤ s)
    (j : ℕ),
    ∀ z ∈ Z,
      HPow.hPow (β := ℕ) ‖z‖ 2 / HPow.hPow (β := ℕ) ‖HAdd.hAdd (α := ℂ) (↑j : ℂ) 1‖ 2 ≤
        |s| / HPow.hPow (β := ℕ) ‖HAdd.hAdd (α := ℂ) (↑j : ℂ) 1‖ 2
⊢ ∀ (j : ℕ),
    ∀ z ∈ Z, ‖sineTerm z j‖ ≤ (fun (n : ℕ) ↦ ‖(↑s : ℂ) / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2‖) j

Tactic:
simp only [norm_neg, norm_pow, Set.mem_image, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂, sineTerm, norm_div, norm_real, norm_eq_abs] at *

Premises used: norm_pow, and_imp, Set.mem_image, forall_exists_index, Complex.norm_real, norm_div, sineTerm, norm_neg, forall_apply_eq_imp_iff₂, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZ : IsCompact Z
s : ℝ
hf : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) Z
hs : ∀ a ∈ Z, HPow.hPow (β := ℕ) ‖a‖ 2 ≤ s
n : ℕ
x : ℂ
hx : x ∈ Z
refine_2 : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ |s|
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 / HPow.hPow (β := ℕ) ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖ 2 ≤
    |s| / HPow.hPow (β := ℕ) ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖ 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZ : IsCompact Z
s : ℝ
hf : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ HPow.hPow (β := ℕ) ‖x‖ 2) Z
hs : ∀ a ∈ Z, HPow.hPow (β := ℕ) ‖a‖ 2 ≤ s
n : ℕ
x : ℂ
hx : x ∈ Z
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 ≤ |s|

Tactic:
apply le_trans (hs x hx) (le_abs_self s)

Premises used: le_abs_self, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZC : IsCompact Z
obtain :
  ∀ (u : ℕ → ℝ) (hu : Summable u) (hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j),
    MultipliableUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n) Z
⊢ MultipliableUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n) Z

Tactic:
obtain ⟨u, hu, hu2⟩ := sineTerm_bound_aux hZC

Premises used: _private.0.sineTerm_bound_aux
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ MultipliableUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n) Z

Tactic:
Summable.multipliableUniformlyOn_nat_one_add hZC hu ?_ ?_

Premises used: Summable.multipliableUniformlyOn_nat_one_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
refine_1 : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ Z, ‖sineTerm x n‖ ≤ u n
refine_2 : ∀ (n : ℕ), ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ sineTerm z n) Z
⊢ MultipliableUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n) Z

Tactic:
refine Summable.multipliableUniformlyOn_nat_one_add hZC hu ?_ ?_

Premises used: Summable.multipliableUniformlyOn_nat_one_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
n : ℕ
z : ℂ
hz : z ∈ Z
⊢ ‖sineTerm z n‖ ≤ u n

Tactic:
hu2 n z hz
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
refine_1 : ∀ (a : ℕ), Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ ∀ x ∈ Z, ‖sineTerm x n‖ ≤ u n) x} a
refine_1₁ refine_1₂ : ∀ (n : ℕ) (z : ℂ) (hz : z ∈ Z), ‖sineTerm z n‖ ≤ u n
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ Z, ‖sineTerm x n‖ ≤ u n

Tactic:
filter_upwards with n z hz using hu2 n z hz
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
funProp : ∀ (n : ℕ), ∀ x ∈ Z, HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 ≠ 0
⊢ ∀ (n : ℕ), ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ sineTerm z n) Z

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZ2 : Z ⊆ ℂ_ℤ
hZC : IsCompact Z
apply :
  Set.EqOn (β := ℂ) (fun (x : ℂ) ↦ ∏' (i : ℕ), (1 + sineTerm x i))
    (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) Z
⊢ HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n)
    (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) Z

Tactic:
apply (multipliableUniformlyOn_euler_sin_prod_on_compact hZC).hasProdUniformlyOn.congr_right

Premises used: MultipliableUniformlyOn.hasProdUniformlyOn, HasProdUniformlyOn.congr_right, multipliableUniformlyOn_euler_sin_prod_on_compact
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZ2 : Z ⊆ ℂ_ℤ
hZC : IsCompact Z
x : ℂ
hx : x ∈ Z
⊢ x ∈ ℂ_ℤ

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
Z : Set ℂ
hZ2 : Z ⊆ ℂ_ℤ
hZC : IsCompact Z
⊢ Set.EqOn (β := ℂ) (fun (x : ℂ) ↦ ∏' (i : ℕ), (1 + sineTerm x i))
    (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) Z

Tactic:
exact fun x hx => euler_sineTerm_tprod (by aesop)

Premises used: euler_sineTerm_tprod
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
apply :
  ∀ K ⊆ (Set.range Int.cast)ᶜ,
    IsCompact K →
      HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n)
        (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) K
⊢ HasProdLocallyUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n)
    (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) ℂ_ℤ

Tactic:
apply hasProdLocallyUniformlyOn_of_forall_compact Complex.isOpen_compl_range_intCast

Premises used: hasProdLocallyUniformlyOn_of_forall_compact, Complex.isOpen_compl_range_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
⊢ ∀ K ⊆ (Set.range Int.cast)ᶜ,
    IsCompact K →
      HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n)
        (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) K

Tactic:
fun _ hZ hZC => HasProdUniformlyOn_sineTerm_prod_on_compact hZ hZC

Premises used: HasProdUniformlyOn_sineTerm_prod_on_compact
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
⊢ ∀ K ⊆ (Set.range Int.cast)ᶜ,
    IsCompact K →
      HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n)
        (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) K

Tactic:
exact fun _ hZ hZC => HasProdUniformlyOn_sineTerm_prod_on_compact hZ hZC

Premises used: HasProdUniformlyOn_sineTerm_prod_on_compact
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
apply : ∀ (k : ℤ), (↑π : ℂ) * x ≠ (↑k : ℂ) * (↑π : ℂ)
⊢ Complex.sin ((↑π : ℂ) * x) ≠ 0

Tactic:
apply Complex.sin_ne_zero_iff.2

Premises used: Iff.mpr, Complex.sin_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
k : ℤ
nth_rw : (↑π : ℂ) * x ≠ (↑π : ℂ) * (↑k : ℂ)
⊢ (↑π : ℂ) * x ≠ (↑k : ℂ) * (↑π : ℂ)

Tactic:
nth_rw 2 [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
k : ℤ
⊢ x ≠ (↑k : ℂ)

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
k : ℤ
⊢ (↑π : ℂ) * x ≠ (↑π : ℂ) * (↑k : ℂ)

Tactic:
exact Injective.ne (mul_right_injective₀ (ofReal_ne_zero.mpr Real.pi_ne_zero)) (by aesop)

Premises used: Iff.mpr, mul_right_injective₀, Complex.ofReal_ne_zero, Function.Injective.ne, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
k : ℕ∞
hx : x ∈ ℂ_ℤ
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞)
    (fun (x : ℂ) ↦ (cexp ((↑π : ℂ) * x * I) + cexp (-((↑π : ℂ) * x) * I)) / 2) ℍₒ x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
k : ℕ∞
hx : x ∈ ℂ_ℤ
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞)
    (fun (x : ℂ) ↦ (cexp (-((↑π : ℂ) * x) * I) - cexp ((↑π : ℂ) * x * I)) * I / 2) ℍₒ x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
k : ℕ∞
hx : x ∈ ℂ_ℤ
⊢ ContDiffWithinAt ℂ (F := ℂ) (↑k : WithTop ℕ∞)
    (fun (x : ℂ) ↦
      (cexp ((↑π : ℂ) * x * I) + cexp (-((↑π : ℂ) * x) * I)) / 2 /
        ((cexp (-((↑π : ℂ) * x) * I) - cexp ((↑π : ℂ) * x * I)) * I / 2))
    ℍₒ x

Tactic:
exact ContDiffWithinAt.div (by fun_prop) (by fun_prop) (sin_pi_mul_ne_zero hx)

Premises used: sin_pi_mul_ne_zero, ContDiffWithinAt.div
-- 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:
logDeriv_tendsto isOpen_compl_range_intCast hx
      HasProdLocallyUniformlyOn_euler_sin_prod.tendstoLocallyUniformlyOn_finsetRange ?_ ?_

Premises used: Complex.logDeriv_tendsto, Complex.isOpen_compl_range_intCast, HasProdLocallyUniformlyOn_euler_sin_prod, HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
refine_1 :
  ∀ᶠ (n : ℕ) in atTop,
    DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ
refine_2 : Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x) ≠ 0
⊢ 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:
refine logDeriv_tendsto isOpen_compl_range_intCast hx
      HasProdLocallyUniformlyOn_euler_sin_prod.tendstoLocallyUniformlyOn_finsetRange ?_ ?_

Premises used: Complex.logDeriv_tendsto, Complex.isOpen_compl_range_intCast, HasProdLocallyUniformlyOn_euler_sin_prod, HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
refine_1 :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ |
        (fun (n : ℕ) ↦
            DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ)
          x}
      a
refine_1₁ refine_1₂ :
  ∀ (n : ℕ), DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ
⊢ ∀ᶠ (n : ℕ) in atTop,
    DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ

Tactic:
filter_upwards with n using by fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
refine_2 : ¬Complex.sin ((↑π : ℂ) * x) = 0 ∧ ¬π = 0 ∧ ¬x = 0
⊢ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x) ≠ 0

Tactic:
simp only [ne_eq, div_eq_zero_iff, mul_eq_zero, ofReal_eq_zero, not_or]

Premises used: mul_eq_zero, ne_eq, not_or, Complex.ofReal_eq_zero, div_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ ¬Complex.sin ((↑π : ℂ) * x) = 0 ∧ ¬π = 0 ∧ ¬x = 0

Tactic:
⟨sin_pi_mul_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩

Premises used: Complex.integerComplement.ne_zero, sin_pi_mul_ne_zero, And.intro, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ ¬Complex.sin ((↑π : ℂ) * x) = 0 ∧ ¬π = 0 ∧ ¬x = 0

Tactic:
exact ⟨sin_pi_mul_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)

Tactic:
have : (fun t ↦ (Complex.sin (π * t) / (π * t))) = fun z ↦
    (Complex.sin ∘ fun t ↦ π * t) z / (π * z) := by simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
⊢ (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) x ≠ 0

Tactic:
apply sin_pi_mul_ne_zero hz

Premises used: sin_pi_mul_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (t : ℂ) ↦ (↑π : ℂ) * t) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
⊢ DifferentiableAt ℂ (HMul.hMul (↑π : ℂ)) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
rw : ((↑π : ℂ) * x).cot * (↑π : ℂ) - 1 / x = (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x
ha : (↑π : ℂ) ≠ 0
rw₁ : (↑π : ℂ) * x ≠ 0
⊢ logDeriv (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) x = (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x

Tactic:
rw [this, logDeriv_div _ (by apply sin_pi_mul_ne_zero hz) ?_
    (DifferentiableAt.comp _ (Complex.differentiableAt_sin) (by fun_prop)) (by fun_prop),
    logDeriv_comp (Complex.differentiableAt_sin) (by fun_prop), Complex.logDeriv_sin,
    deriv_const_mul_id, logDeriv_const_mul, logDeriv_id']

Premises used: Complex.differentiableAt_sin, logDeriv_comp, logDeriv_div, Complex.logDeriv_sin, deriv_const_mul_id, logDeriv_id', logDeriv_const_mul, DifferentiableAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
⊢ ((↑π : ℂ) * x).cot * (↑π : ℂ) - 1 / x = (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
⊢ (↑π : ℂ) ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
simp : ¬π = 0 ∧ ¬x = 0
⊢ (↑π : ℂ) * x ≠ 0

Tactic:
simp only [ne_eq, mul_eq_zero, ofReal_eq_zero, not_or]

Premises used: mul_eq_zero, ne_eq, not_or, Complex.ofReal_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
⊢ ¬π = 0 ∧ ¬x = 0

Tactic:
⟨Real.pi_ne_zero, integerComplement.ne_zero hz⟩

Premises used: Complex.integerComplement.ne_zero, And.intro, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
⊢ ¬π = 0 ∧ ¬x = 0

Tactic:
exact ⟨Real.pi_ne_zero, integerComplement.ne_zero hz⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
⊢ x + (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) ≠ 0

Tactic:
have h1 := integerComplement_add_ne_zero hx (i + 1)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) ≠ 0
⊢ x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 ≠ 0

Tactic:
simpa [sub_eq_add_neg] using integerComplement_add_ne_zero hx (-(i + 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 : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) ≠ 0
⊢ x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 ≠ 0

Tactic:
have h2 : ((x : ℂ) - (i + 1)) ≠ 0 := by
    simpa [sub_eq_add_neg] using integerComplement_add_ne_zero hx (-(i + 1))
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) ≠ 0
h2 : x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 ≠ 0
⊢ HPow.hPow (β := ℕ) x 2 ≠ HPow.hPow (α := ℂ) (β := ℕ) (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) 2

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

Tactic:
rw [← sub_eq_add_neg, sub_ne_zero]

Premises used: sub_ne_zero, sub_eq_add_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) ≠ 0
h2 : x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 ≠ 0
this : HPow.hPow (β := ℕ) x 2 ≠ HPow.hPow (α := ℂ) (β := ℕ) (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) 2
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2 ≠ HPow.hPow (β := ℕ) x 2

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

Tactic:
have h3 : (i + 1) ^ 2 + - x ^ 2 ≠ 0 := by
      have := (integerComplement_pow_two_ne_pow_two hx ((i + 1) : ℤ))
      rw [← sub_eq_add_neg, sub_ne_zero]
      aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) ≠ 0
h2 : x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 ≠ 0
h3 : HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2 + -HPow.hPow (β := ℕ) x 2 ≠ 0
simp :
  ∀ (h1 : ¬x + HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 = 0),
    -(2 * x ^ HSub.hSub (α := ℕ) 2 1 * 1) / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2 /
        (1 + -HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2) =
      1 / (x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑i : ℂ) 1)
⊢ logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x = cotTerm x i

Tactic:
simp only [Int.cast_add, Int.cast_natCast, Int.cast_one, ne_eq, sineTerm, logDeriv_apply,
    deriv_const_add', deriv_div_const, deriv.fun_neg', differentiableAt_fun_id, deriv_fun_pow,
    Nat.cast_ofNat, deriv_id'', cotTerm] at *

Premises used: Nat.cast_ofNat, Int.cast_natCast, deriv_const_add', deriv.fun_neg', deriv_id'', Int.cast_add, logDeriv_apply, ne_eq, sineTerm, differentiableAt_fun_id, cotTerm, deriv_fun_pow, Int.cast_one, deriv_div_const
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h2 : ¬x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 = 0
h3 : ¬HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2 + -HPow.hPow (β := ℕ) x 2 = 0
h1 : ¬x + HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 = 0
⊢ -(2 * x ^ HSub.hSub (α := ℕ) 2 1 * 1) / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2 /
      (1 + -HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2) =
    1 / (x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) + 1 / (x + HAdd.hAdd (α := ℂ) (↑i : ℂ) 1)

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
rw : Eq (α := ℂ) (∑ i ∈ Finset.range n, logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x) (∑ j ∈ Finset.range n, cotTerm x j)
hf : ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0
hd : ∀ i ∈ Finset.range n, DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ 1 + sineTerm z i) x
⊢ Eq (α := ℂ) (logDeriv (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) (∑ j ∈ Finset.range n, cotTerm x j)

Tactic:
rw [logDeriv_prod]

Premises used: logDeriv_prod
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ Eq (α := ℂ) (∑ i ∈ Finset.range n, logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x) (∑ j ∈ Finset.range n, cotTerm x j)

Tactic:
simp_rw [logDeriv_sineTerm_eq_cotTerm hx]

Premises used: logDeriv_sineTerm_eq_cotTerm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0

Tactic:
fun i _ ↦ sineTerm_ne_zero hx i

Premises used: sineTerm_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0

Tactic:
exact fun i _ ↦ sineTerm_ne_zero hx i

Premises used: sineTerm_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∀ i ∈ Finset.range n, DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ 1 + sineTerm z i) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
simp_rw :
  Tendsto (β := ℂ) (fun (n : ℕ) ↦ logDeriv (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) atTop
    (𝓝 (logDeriv (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) x))
⊢ Tendsto (fun (n : ℕ) ↦ ∑ j ∈ Finset.range n, cotTerm x j) atTop (𝓝 ((↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x))

Tactic:
simp_rw [← logDeriv_sin_div_eq_cot hx, ← logDeriv_prod_sineTerm_eq_sum_cotTerm hx]

Premises used: logDeriv_sin_div_eq_cot, logDeriv_prod_sineTerm_eq_sum_cotTerm