awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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 : ℂ)))))
have simp : (↑π : ℂ) * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 1) * I * (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)))⁻¹) =
  (↑π : ℂ) * I * ((cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) + 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
z : ℍ
⊢ (↑π : ℂ) * ((↑π : ℂ) * (↑z : ℂ)).cot =
    (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
have h1 : (↑π : ℂ) * ((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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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 : ℂ)))))
⊢ (↑π : ℂ) * ((↑π : ℂ) * (↑z : ℂ)).cot =
    (↑π : ℂ) * I - 2 * (↑π : ℂ) * I * ∑' (n : ℕ), cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
have rw : -(↑π : ℂ) * I * (HMul.hMul (α := ℂ) 2 (∑' (i : ℕ), cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ i) - 1) =
  (↑π : ℂ) * 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 _)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬1 + -HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 = 0
have rw : ¬1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 = - -HPow.hPow (β := ℕ) x 2
Tactic: rw [add_eq_zero_iff_eq_neg, neg_div', eq_div_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
rw : ¬1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 = - -HPow.hPow (β := ℕ) x 2
⊢ ¬1 + -HPow.hPow (β := ℕ) x 2 / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 = 0
have rw₁ : HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 ≠ 0
Tactic: rw [add_eq_zero_iff_eq_neg, neg_div', eq_div_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬1 * HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 = - -HPow.hPow (β := ℕ) x 2
have this : HPow.hPow (β := ℕ) x 2 ≠ HPow.hPow (α := ℂ) (β := ℕ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 2
Tactic: have := (integerComplement_pow_two_ne_pow_two hx (n + 1 : ℤ))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
h0 : x ≠ 0
⊢ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop
    (𝓝 (Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)))
have rw : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop
  (𝓝 (Complex.sin ((↑π : ℂ) * x) * (1 / ((↑π : ℂ) * x))))
Tactic: rw [show (sin (π * x) / (π * x)) = sin (π * x) * (1 / (π * x)) by ring]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
h0 : x ≠ 0
⊢ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop
    (𝓝 (Complex.sin ((↑π : ℂ) * x) * (1 / ((↑π : ℂ) * x))))
have 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)
Tactic: apply (Filter.Tendsto.mul_const (b := 1 / (π * x)) (tendsto_euler_sin_prod x)).congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
h0 : x ≠ 0
n : ℕ
⊢ ((↑π : ℂ) * 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)
have 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)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
⊢ Multipliable (α := ℂ) fun (i : ℕ) ↦ 1 + sineTerm x i
have hf : Summable (α := ℝ) fun (i : ℕ) ↦ ‖sineTerm x i‖
Tactic: apply multipliable_one_add_of_summable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
x : ℂ
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖sineTerm x i‖
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ ∏' (i : ℕ), (1 + sineTerm x i) = Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)
have rw : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop (𝓝 (Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)))
Tactic: rw [← Multipliable.hasProd_iff (multipliable_sineTerm x),
    Multipliable.hasProd_iff_tendsto_nat (multipliable_sineTerm x)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
Z : Set ℂ
hZ : IsCompact Z
⊢ ∃ (u : ℕ → ℝ), Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
have hf : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖-HPow.hPow (β := ℕ) x 2‖) Z
Tactic: have hf : ContinuousOn (fun x : ℂ => ‖-x ^ 2‖) Z := by
    fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (Y := ℝ) (fun (x : ℂ) ↦ ‖-HPow.hPow (β := ℕ) x 2‖) Z
⊢ ∃ (u : ℕ → ℝ), Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
have 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
Tactic: obtain ⟨s, hs⟩ := bddAbove_def.mp (IsCompact.bddAbove_image hZ hf)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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
have refine_1 : Summable (α := ℝ) fun (n : ℕ) ↦ ‖(↑s : ℂ) / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2‖
Tactic: refine ⟨fun n : ℕ => ‖(s : ℂ) / (n + 1) ^ 2‖, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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‖
⊢ ∃ (u : ℕ → ℝ), Summable u ∧ ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
have refine_2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ (fun (n : ℕ) ↦ ‖(↑s : ℂ) / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2‖) j
Tactic: refine ⟨fun n : ℕ => ‖(s : ℂ) / (n + 1) ^ 2‖, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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
⊢ ∀ (j : ℕ),
    ∀ z ∈ Z, ‖sineTerm z j‖ ≤ (fun (n : ℕ) ↦ ‖(↑s : ℂ) / HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2‖) j
have 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
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 *
Cleared hypotheses: hf, hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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 / HPow.hPow (β := ℕ) ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖ 2 ≤
    |s| / HPow.hPow (β := ℕ) ‖HAdd.hAdd (α := ℂ) (↑n : ℂ) 1‖ 2
have refine_2 : HPow.hPow (β := ℕ) ‖x‖ 2 ≤ |s|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
Z : Set ℂ
hZC : IsCompact Z
⊢ MultipliableUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n) Z
have obtain : ∀ (u : ℕ → ℝ) (hu : Summable u) (hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j),
  MultipliableUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n) Z
Tactic: obtain ⟨u, hu, hu2⟩ := sineTerm_bound_aux hZC
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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
have refine_1 : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ Z, ‖sineTerm x n‖ ≤ u n
Tactic: refine Summable.multipliableUniformlyOn_nat_one_add hZC hu ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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
⊢ MultipliableUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n) Z
have refine_2 : ∀ (n : ℕ), ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ sineTerm z n) Z
Tactic: refine Summable.multipliableUniformlyOn_nat_one_add hZC hu ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ Z, ‖sineTerm x n‖ ≤ u n
have refine_1 : ∀ (a : ℕ), Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ ∀ x ∈ Z, ‖sineTerm x n‖ ≤ u n) x} a
Tactic: filter_upwards with n z hz using hu2 n z hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
Z : Set ℂ
hZC : IsCompact Z
u : ℕ → ℝ
hu : Summable u
hu2 : ∀ (j : ℕ), ∀ z ∈ Z, ‖sineTerm z j‖ ≤ u j
⊢ ∀ (n : ℕ), ContinuousOn (Y := ℂ) (fun (z : ℂ) ↦ sineTerm z n) Z
have funProp : ∀ (n : ℕ), ∀ x ∈ Z, HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) 2 ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
Z : Set ℂ
hZ2 : Z ⊆ ℂ_ℤ
hZC : IsCompact Z
⊢ HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n)
    (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) Z
have apply : Set.EqOn (β := ℂ) (fun (x : ℂ) ↦ ∏' (i : ℕ), (1 + sineTerm x i))
  (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) Z
Tactic: apply (multipliableUniformlyOn_euler_sin_prod_on_compact hZC).hasProdUniformlyOn.congr_right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
⊢ HasProdLocallyUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n)
    (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) ℂ_ℤ
have apply : ∀ K ⊆ (Set.range Int.cast)ᶜ,
  IsCompact K →
    HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (z : ℂ) ↦ 1 + sineTerm z n)
      (fun (x : ℂ) ↦ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x)) K
Tactic: apply hasProdLocallyUniformlyOn_of_forall_compact Complex.isOpen_compl_range_intCast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Complex.sin ((↑π : ℂ) * x) ≠ 0
have apply : ∀ (k : ℤ), (↑π : ℂ) * x ≠ (↑k : ℂ) * (↑π : ℂ)
Tactic: apply Complex.sin_ne_zero_iff.2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
k : ℤ
⊢ (↑π : ℂ) * x ≠ (↑k : ℂ) * (↑π : ℂ)
have nth_rw : (↑π : ℂ) * x ≠ (↑π : ℂ) * (↑k : ℂ)
Tactic: nth_rw 2 [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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))
have refine_1 : ∀ᶠ (n : ℕ) in atTop,
  DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ
Tactic: refine logDeriv_tendsto isOpen_compl_range_intCast hx
      HasProdLocallyUniformlyOn_euler_sin_prod.tendstoLocallyUniformlyOn_finsetRange ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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)ᶜ
⊢ Tendsto (β := ℂ) (fun (n : ℕ) ↦ logDeriv (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) atTop
    (𝓝 (logDeriv (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) x))
have refine_2 : Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x) ≠ 0
Tactic: refine logDeriv_tendsto isOpen_compl_range_intCast hx
      HasProdLocallyUniformlyOn_euler_sin_prod.tendstoLocallyUniformlyOn_finsetRange ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ ∀ᶠ (n : ℕ) in atTop,
    DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ
have 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
Tactic: filter_upwards with n using by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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
⊢ ∀ᶠ (n : ℕ) in atTop,
    DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ
have refine_1₁ : ∀ (a : ℕ), DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ∏ j ∈ Finset.range a, (1 + sineTerm z j)) (Set.range Int.cast)ᶜ
Tactic: filter_upwards with n using by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Complex.sin ((↑π : ℂ) * x) / ((↑π : ℂ) * x) ≠ 0
have refine_2 : ¬Complex.sin ((↑π : ℂ) * x) = 0 ∧ ¬π = 0 ∧ ¬x = 0
Tactic: simp only [ne_eq, div_eq_zero_iff, mul_eq_zero, ofReal_eq_zero, not_or]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
⊢ logDeriv (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) x = (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
⊢ logDeriv (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) x = (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x
have rw : ((↑π : ℂ) * x).cot * (↑π : ℂ) - 1 / 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']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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
⊢ logDeriv (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) x = (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x
have ha : (↑π : ℂ) ≠ 0
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']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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
⊢ logDeriv (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) x = (↑π : ℂ) * ((↑π : ℂ) * x).cot - 1 / x
have rw₁ : (↑π : ℂ) * x ≠ 0
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']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hz : x ∈ ℂ_ℤ
this :
  Eq (α := (t : ℂ) → ℂ) (fun (t : ℂ) ↦ Complex.sin ((↑π : ℂ) * t) / ((↑π : ℂ) * t)) fun (z : ℂ) ↦
    (Complex.sin ∘ fun (t : ℂ) ↦ (↑π : ℂ) * t) z / ((↑π : ℂ) * z)
⊢ (↑π : ℂ) * x ≠ 0
have simp : ¬π = 0 ∧ ¬x = 0
Tactic: simp only [ne_eq, mul_eq_zero, ofReal_eq_zero, not_or]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
⊢ logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x = cotTerm x i
have h1 : x + (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) ≠ 0
Tactic: have h1 := integerComplement_add_ne_zero hx (i + 1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) ≠ 0
⊢ logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x = cotTerm x i
have h2 : 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))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
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
have this : HPow.hPow (β := ℕ) x 2 ≠ HPow.hPow (α := ℂ) (β := ℕ) (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) 2
Tactic: have := (integerComplement_pow_two_ne_pow_two hx ((i + 1) : ℤ))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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 ≠ 0
have rw : HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1) 2 ≠ HPow.hPow (β := ℕ) x 2
Tactic: rw [← sub_eq_add_neg, sub_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (hypothesis)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + (↑(HAdd.hAdd (α := ℤ) (↑i : ℤ) 1) : ℂ) ≠ 0
h2 : x - HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 ≠ 0
⊢ logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x = cotTerm x i
have h3 : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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
⊢ logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x = cotTerm x i
have 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)
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 *
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
Goal:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ Eq (α := ℂ) (logDeriv (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) (∑ j ∈ Finset.range n, cotTerm x j)
have rw : Eq (α := ℂ) (∑ i ∈ Finset.range n, logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x) (∑ j ∈ Finset.range n, cotTerm x j)
Tactic: rw [logDeriv_prod]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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)
⊢ Eq (α := ℂ) (logDeriv (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) (∑ j ∈ Finset.range n, cotTerm x j)
have hf : ∀ i ∈ Finset.range n, 1 + sineTerm x i ≠ 0
Tactic: rw [logDeriv_prod]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent (goal)
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
⊢ Eq (α := ℂ) (logDeriv (fun (z : ℂ) ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) (∑ j ∈ Finset.range n, cotTerm x j)
have hd : ∀ i ∈ Finset.range n, DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ 1 + sineTerm z i) x
Tactic: rw [logDeriv_prod]