mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < ↑r
this :
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z‖ < ‖↑l - x‖) →
    HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
l : ↥L.lattice
hl : ↑l ≠ l₀
⊢ ↑r < ‖↑l - x‖

Tactic:
simpa using

Goal state after:
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < ↑r
this :
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z‖ < ‖↑l - x‖) →
    HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
l : ↥L.lattice
hl : ↑l ≠ l₀
⊢ ↑r < ‖↑l - x‖
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
r : ℝ
h₁ : 0 < r
h₂ : Metric.closedBall l r ⊆ (↑L.lattice \ {l})ᶜ
⊢ HasFPowerSeriesAt ℘[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ if i = 0 then ℘[L - l] l else (↑i + 1) * L.sumInvPow l (i + 2)) l

Tactic:
lift r to NNReal using h₁.le

Goal state after:
L : PeriodPair
l : ℂ
r : NNReal
h₁ : 0 < ↑r
h₂ : Metric.closedBall l ↑r ⊆ (↑L.lattice \ {l})ᶜ
⊢ HasFPowerSeriesAt ℘[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ if i = 0 then ℘[L - l] l else (↑i + 1) * L.sumInvPow l (i + 2)) l
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
r : NNReal
h₁ : 0 < ↑r
h₂ : Metric.closedBall l ↑r ⊆ (↑L.lattice \ {l})ᶜ
⊢ HasFPowerSeriesAt ℘[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ if i = 0 then ℘[L - l] l else (↑i + 1) * L.sumInvPow l (i + 2)) l

Tactic:
simpa using

Goal state after:
L : PeriodPair
l : ℂ
r : NNReal
h₁ : 0 < ↑r
h₂ : Metric.closedBall l ↑r ⊆ (↑L.lattice \ {l})ᶜ
⊢ HasFPowerSeriesAt ℘[L - l]
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ if i = 0 then ℘[L - l] l else (↑i + 1) * L.sumInvPow l (i + 2)) l
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2)
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Tactic:
simpa using

Goal state after:
z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2)
⊢ z.im ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2) ∨ √(r1 z) ≤ √((c * z.re + d) ^ 2 + (c * z.im) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘[L - l] l / ↑n ! = if n = 0 then ℘[L - l] l else (↑n + 1) * L.sumInvPow l (n + 2)

Tactic:
simpa using

Goal state after:
L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘[L - l] l / ↑n ! = if n = 0 then ℘[L - l] l else (↑n + 1) * L.sumInvPow l (n + 2)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x : Fin 2 → ℤ
hx : x ≠ 0
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2 ∨ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Tactic:
by
  refine (max_choice (x 0).natAbs (x 1).natAbs).imp (fun H0 ↦ ?_) (fun H1 ↦ ?_)
  · have : x 0 ≠ 0 := by
      rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H0, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
    simp only [norm_eq_max_natAbs, H0, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]
  · have : x 1 ≠ 0 := by
      rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
    simp only [norm_eq_max_natAbs, H1, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case inr
n : ℤ
x : ℝ
hx : 1 ≤ |x|
this : ∀ (n : ℤ) {x : ℝ}, 1 ≤ |x| → 0 ≤ x → 1 ≤ |eval x (T ℝ n)|
h : x < 0
⊢ 1 ≤ |eval x (T ℝ n)|

Tactic:
simpa using

Goal state after:
case inr
n : ℤ
x : ℝ
hx : 1 ≤ |x|
this : ∀ (n : ℤ) {x : ℝ}, 1 ≤ |x| → 0 ≤ x → 1 ≤ |eval x (T ℝ n)|
h : x < 0
⊢ 1 ≤ |eval x (T ℝ n)|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case inr
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
this : ∀ {n : ℤ}, n ≠ 0 → ∀ {x : ℝ}, 1 < |x| → 0 ≤ x → 1 < |eval x (T ℝ n)|
h : x < 0
⊢ 1 < |eval x (T ℝ n)|

Tactic:
simpa using

Goal state after:
case inr
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
this : ∀ {n : ℤ}, n ≠ 0 → ∀ {x : ℝ}, 1 < |x| → 0 ≤ x → 1 < |eval x (T ℝ n)|
h : x < 0
⊢ 1 < |eval x (T ℝ n)|
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
⊢ |eval x (T ℝ n)| ≤ 1 → |x| ≤ 1

Tactic:
simpa using

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ |eval x (T ℝ n)| ≤ 1 → |x| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case refine_2
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ Metric.eball x ↑r ⊆ Metric.closedBall x ↑r

Tactic:
simpa using

Goal state after:
case refine_2
L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
⊢ Metric.ball x ↑r ⊆ Metric.closedBall x ↑r
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
r : ℝ
h₁ : 0 < r
h₂ : Metric.closedBall l r ⊆ (↑L.lattice \ {l})ᶜ
⊢ HasFPowerSeriesAt ℘'[L - l] (FormalMultilinearSeries.ofScalars ℂ fun i ↦ (↑i + 1) * (↑i + 2) * L.sumInvPow l (i + 3))
    l

Tactic:
simpa using

Goal state after:
L : PeriodPair
l : ℂ
r : ℝ
h₁ : 0 < r
h₂ : Metric.closedBall l r ⊆ (↑L.lattice \ {l})ᶜ
⊢ HasFPowerSeriesAt ℘'[L - l] (FormalMultilinearSeries.ofScalars ℂ fun i ↦ (↑i + 1) * (↑i + 2) * L.sumInvPow l (i + 3))
    l
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘'[L - l] l / ↑n ! = (↑n + 1) * (↑n + 2) * L.sumInvPow l (n + 3)

Tactic:
simpa using

Goal state after:
L : PeriodPair
l : ℂ
n : ℕ
⊢ iteratedDeriv n ℘'[L - l] l / ↑n ! = (↑n + 1) * (↑n + 2) * L.sumInvPow l (n + 3)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case hbc.inl
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
H1 : 1 ≤ (↑(x 0) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖

Tactic:
simpa using

Goal state after:
case hbc.inl
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
H1 : 1 ≤ (↑(x 0) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ k ≤ n

Tactic:
simpa using

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ k ≤ n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case hbc.inr
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
H2 : 1 ≤ (↑(x 1) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖

Tactic:
simpa using

Goal state after:
case hbc.inr
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 : ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖
H2 : 1 ≤ (↑(x 1) / ‖x‖) ^ 2
⊢ r z ≤ ‖↑(x 0) / ↑↑(max (x 0).natAbs (x 1).natAbs) * ↑z + ↑(x 1) / ↑↑(max (x 0).natAbs (x 1).natAbs)‖
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
hl₀ : l₀ = 0
⊢ AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀

Tactic:
simpa using

Goal state after:
case pos
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
this : AnalyticAt ℂ ℘[L - l₀] l₀
hl₀ : l₀ = 0
⊢ AnalyticAt ℂ (fun z ↦ 0) 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case hΘ
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑c * z) =o[cofinite] fun n ↦ ↑n

Tactic:
simpa using

Goal state after:
case hΘ
c e : ℤ
z : ℂ
⊢ (c = 0 ∨ z = 0) ∨ Tendsto (norm ∘ fun n ↦ ↑n) cofinite atTop
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case ho
c e : ℤ
z : ℂ
⊢ (fun d ↦ ↑e) =o[cofinite] fun n ↦ ↑n

Tactic:
simpa using

Goal state after:
case ho
c e : ℤ
z : ℂ
⊢ e = 0 ∨ Tendsto (norm ∘ fun n ↦ ↑n) cofinite atTop
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
c₁ c₂ : ℤ
⊢ (fun n ↦ ((↑c₁ * z + ↑n + 1) * (↑c₂ * z + ↑n))⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ 2)⁻¹

Tactic:
simpa using

Goal state after:
z : ℂ
c₁ c₂ : ℤ
⊢ ((fun n ↦ (↑c₂ * z + ↑n)⁻¹ * (↑c₁ * z + ↑n + 1)⁻¹) =O[atBot] fun n ↦ (↑n)⁻¹ * (↑n)⁻¹) ∧
    (fun n ↦ (↑c₂ * z + ↑n)⁻¹ * (↑c₁ * z + ↑n + 1)⁻¹) =O[atTop] fun n ↦ (↑n)⁻¹ * (↑n)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ (fun n ↦ ((↑n * z + ↑c₁) * (↑n * z + ↑c₂))⁻¹) =O[cofinite] fun n ↦ (↑n * ↑n)⁻¹

Tactic:
simpa using

Goal state after:
z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ ((fun n ↦ (↑n * z + ↑c₂)⁻¹ * (↑n * z + ↑c₁)⁻¹) =O[atBot] fun n ↦ (↑n)⁻¹ * (↑n)⁻¹) ∧
    (fun n ↦ (↑n * z + ↑c₂)⁻¹ * (↑n * z + ↑c₁)⁻¹) =O[atTop] fun n ↦ (↑n)⁻¹ * (↑n)⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
⊢ ‖((↑(m 0) + ↑a) * ↑z + ↑(m 1) + ↑b)⁻¹‖ ≤ ?m.98

Tactic:
simpa using

Goal state after:
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
⊢ ‖(↑(m 0) + ↑a) * ↑z + (↑(m 1) + ↑b)‖⁻¹ ≤ ?m.98
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: α : Type u_1
a : α
inst✝² : NormedAddCommGroup α
inst✝¹ : DiscreteTopology α
inst✝ : ProperSpace α
⊢ (fun x ↦ a) =o[cofinite] fun x ↦ ‖x‖

Tactic:
simpa using

Goal state after:
α : Type u_1
a : α
inst✝² : NormedAddCommGroup α
inst✝¹ : DiscreteTopology α
inst✝ : ProperSpace α
⊢ a = 0 ∨ Tendsto (fun x ↦ ‖x‖) cofinite atTop
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp.e_a
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ n - 1 + 1 = n

Tactic:
exact Nat.sub_add_cancel (Nat.one_le_of_lt hn)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_c
L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ (x + ↑l ∈ L.lattice) = (x ∈ L.lattice)

Tactic:
simpa using

Goal state after:
case e_c
L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ x + ↑l ∈ L.lattice ↔ x ∈ L.lattice
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
⊢ AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x

Tactic:
have := L.analyticOnNhd_derivWeierstrassP _ hx

Goal state after:
L : PeriodPair
x : ℂ
hx : x ∉ L.lattice
this : AnalyticAt ℂ ℘'[L] x
⊢ AnalyticAt ℂ (fun z ↦ ℘'[L] z ^ 2 - 4 * ℘[L] z ^ 3 + L.g₂ * ℘[L] z + L.g₃) x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
hz : z ∉ L.lattice
⊢ ℘'[L] z ^ 2 = 4 * ℘[L] z ^ 3 - L.g₂ * ℘[L] z - L.g₃

Tactic:
simpa using

Goal state after:
L : PeriodPair
z : ℂ
hz : z ∉ L.lattice
⊢ ℘'[L] z ^ 2 = 4 * ℘[L] z ^ 3 - L.g₂ * ℘[L] z - L.g₃
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)

Tactic:
rw [arithGeom_same_eq_mul_div' ha n, ← neg_sub _ a, div_neg,
    ← neg_sub _ (a ^ (n + 1)), mul_neg, neg_div, neg_neg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ (↑n + 1) ^ 2 ≠ 0

Tactic:
· simp [Nat.cast_add_one_ne_zero n]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
⊢ Summable fun i ↦ ‖sineTerm x i‖

Tactic:
have := summable_pow_div_add (x ^ 2) 2 1 Nat.one_lt_two

Goal state after:
x : ℂ
this : Summable fun n ↦ ‖x ^ 2 / (↑n + ↑1) ^ 2‖
⊢ Summable fun i ↦ ‖sineTerm x i‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
this : Summable fun n ↦ ‖x ^ 2 / (↑n + ↑1) ^ 2‖
⊢ Summable fun i ↦ ‖sineTerm x i‖

Tactic:
simpa using

Goal state after:
x : ℂ
this : Summable fun n ↦ ‖x ^ 2 / (↑n + ↑1) ^ 2‖
⊢ Summable fun i ↦ ‖x‖ ^ 2 / ‖↑i + 1‖ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_1
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ Summable fun n ↦ ‖↑s / (↑n + 1) ^ 2‖

Tactic:
simpa using

Goal state after:
case refine_1
Z : Set ℂ
hZ : IsCompact Z
hf : ContinuousOn (fun x ↦ ‖-x ^ 2‖) Z
s : ℝ
hs : ∀ y ∈ (fun x ↦ ‖-x ^ 2‖) '' Z, y ≤ s
⊢ Summable fun n ↦ |s| / ‖↑n + 1‖ ^ 2
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr
n : ℕ
hn : Odd n
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)

Tactic:
· simp [fib_of_odd, hn]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: 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)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + ↑(↑i + 1) ≠ 0
⊢ x - (↑i + 1) ≠ 0

Tactic:
simpa using

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + ↑(↑i + 1) ≠ 0
⊢ ¬x + (-1 + -↑i) = 0
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: m n : ℤ
⊢ (fib m).gcd (fib n) = Nat.fib (m.gcd n)

Tactic:
by
  obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
    <;> obtain ⟨n, (rfl | rfl)⟩ := n.eq_nat_or_neg
    <;> simp [fib_neg, Nat.fib_gcd, apply_ite, apply_ite_left]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: 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:
simpa using

Goal state after:
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))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case ha
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x - (↑n + 1) ≠ 0

Tactic:
simpa using

Goal state after:
case ha
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬x + (-1 + -↑n) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hb
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x + (↑n + 1) ≠ 0

Tactic:
simpa using

Goal state after:
case hb
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬x + (↑n + 1) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable fun n ↦ (x - ↑(n + 1))⁻¹ * (x + ↑(n + 1))⁻¹
⊢ Summable fun i ↦ 1 / ((x + (↑i + 1)) * (x - (↑i + 1)))

Tactic:
simpa using

Goal state after:
x : ℂ
hz : x ∈ ℂ_ℤ
this : Summable fun n ↦ (x - ↑(n + 1))⁻¹ * (x + ↑(n + 1))⁻¹
⊢ Summable fun i ↦ (x - (↑i + 1))⁻¹ * (x + (↑i + 1))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
d : ℤ
⊢ ContDiffOn ℂ (↑k) (fun z ↦ 1 / (z + ↑d)) ℂ_ℤ

Tactic:
simpa using

Goal state after:
k : ℕ
d : ℤ
⊢ ContDiffOn ℂ (↑k) (fun z ↦ (z + ↑d)⁻¹) ℂ_ℤ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hf
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z - (↑d + 1))) z

Tactic:
simpa using

Goal state after:
case hf
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ (z + (-1 + -↑d))⁻¹) z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hg
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ 1 / (z + (↑d + 1))) z

Tactic:
simpa using

Goal state after:
case hg
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ ContDiffAt ℂ (↑k) (fun z ↦ (z + (↑d + 1))⁻¹) z
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
h3 : 2 ∣ n.minFac
⊢ 2 = n.minFac

Tactic:
simpa using

Goal state after:
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : n.minFac ≠ k
h2✝ : k < n.minFac
h2 : k.succ = n.minFac
h3 : 2 ∣ n.minFac
⊢ 2 = n.minFac
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hbc.h₁
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a + (↑n + 1)) ^ (-1 - ↑k)‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)

Tactic:
simpa using

Goal state after:
case hbc.h₁
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖↑a + (↑n + 1)‖ ^ (-1 + -↑k) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 + -↑k) * (↑n + 1) ^ (-1 + -↑k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case h₂
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖(↑a - (↑n + 1)) ^ (-1 - ↑k)‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 - ↑k) * |↑n + 1| ^ (-1 - ↑k)

Tactic:
simpa using

Goal state after:
case h₂
k : ℕ
K : Set ℂ
A B : ℝ
hB : 0 < B
hKAB : K ⊆ UpperHalfPlane.coe '' verticalStrip A B
n : ℕ
a : ℍ
haAB : a ∈ verticalStrip A B
ha : ↑a ∈ K
h1 :
  ‖↑(![1, ↑n + 1] 0) * ↑a + ↑(![1, ↑n + 1] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * ‖![1, ↑n + 1]‖ ^ (-(↑k + 1))
h2 :
  ‖↑(![1, -(↑n + 1)] 0) * ↑a + ↑(![1, -(↑n + 1)] 1)‖ ^ (-(↑k + 1)) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-(↑k + 1)) * (↑n + 1) ^ (-(↑k + 1))
⊢ ‖↑a + (-1 + -↑n)‖ ^ (-1 + -↑k) ≤
    r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-1 + -↑k) * (↑n + 1) ^ (-1 + -↑k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hf
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x + (↑n + 1) ≠ 0

Tactic:
simpa using

Goal state after:
case hf
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ ¬-1 + -↑n = x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hg
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x - (↑n + 1) ≠ 0

Tactic:
simpa using

Goal state after:
case hg
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ ¬x = ↑n + 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ Summable fun n ↦ (z + ↑(↑n + 1)) ^ (-1 - ↑k)

Tactic:
simpa using

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ Summable fun n ↦ (z + (↑n + 1)) ^ (-1 - ↑k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ Summable fun n ↦ (z + ↑(-(↑n + 1))) ^ (-1 - ↑k)

Tactic:
simpa using

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
⊢ Summable fun n ↦ (z + (-1 + -↑n)) ^ (-1 + -↑k)
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: n : ℕ
⊢ φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    calc
      _ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]; ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z✝ : ℂ
k : ℕ
hk : 1 ≤ k
hz✝ : z✝ ∈ ℍₒ
z : ℂ
hz : z ∈ ℍₒ
⊢ ↑π * (↑π * z).cot - z⁻¹ = ∑' (n : ℕ), cotTerm z n

Tactic:
simpa using

Goal state after:
z✝ : ℂ
k : ℕ
hk : 1 ≤ k
hz✝ : z✝ ∈ ℍₒ
z : ℂ
hz : z ∈ ℍₒ
⊢ ↑π * (↑π * z).cot - z⁻¹ = ∑' (n : ℕ), ((z - (↑n + 1))⁻¹ + (z + (↑n + 1))⁻¹)
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Icc ↑0 ↑M
y : ℝ
hy : y ∈ Icc ↑0 ↑M
hxy : x ≤ y
⊢ 0 ≤ x

Tactic:
simpa using

Goal state after:
k M : ℕ
c : ℝ
hc : 0 < c
x : ℝ
hx : x ∈ Icc ↑0 ↑M
y : ℝ
hy : y ∈ Icc ↑0 ↑M
hxy : x ≤ y
⊢ 0 ≤ x
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hbc
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ |u (c n) / ↑(c n) - l| ≤ ε

Tactic:
simpa using

Goal state after:
case hbc
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ |u (c n) / ↑(c n) - l| ≤ ε