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

Goal state before:
pp: case e_f
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
⊢ ((if ↑w = ↑l₀ then 0 else 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2) + if ↑w = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0) =
    1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2

Tactic:
;

Goal state after:
case e_f
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
⊢ ((if ↑w = ↑l₀ then 0 else 1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2) + if ↑w = ↑l₀ then 1 / (z - ↑l₀) ^ 2 - 1 / ↑l₀ ^ 2 else 0) =
    1 / (z - ↑w) ^ 2 - 1 / ↑w ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l ∉ L.lattice
⊢ False

Tactic:
;

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l ∉ L.lattice
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_5.hnc
L : PeriodPair
l : ↥L.lattice
x✝ : ℂ
⊢ ¬↑l = L.ω₁ / 2

Tactic:
;

Goal state after:
case e'_5.hnc
L : PeriodPair
l : ↥L.lattice
x✝ : ℂ
⊢ ¬↑l = L.ω₁ / 2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
⊢ ∀ (b : ℝ),
    2 * r ≤ b →
      ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = b → ‖if ↑l = l₀ then 0 else -2 / (x - ↑l) ^ 3‖ ≤ 16 * ‖l‖ ^ (-3)

Tactic:
rintro _ h s hs l rfl

Goal state after:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
⊢ ‖if ↑l = l₀ then 0 else -2 / (s - ↑l) ^ 3‖ ≤ 16 * ‖l‖ ^ (-3)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
hs : ‖↑l‖ < r
⊢ False

Tactic:
;

Goal state after:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
hs : ‖↑l‖ < r
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
h : 2 * r ≤ ‖↑0‖
h✝ : ¬↑0 = l₀
this : s ≠ ↑0
⊢ False

Tactic:
;

Goal state after:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
h : 2 * r ≤ ‖↑0‖
h✝ : ¬↑0 = l₀
this : s ≠ ↑0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
s : ℂ
hr : 0 < r
hs : ‖s‖ < r
h : 2 * r ≤ 0
h✝ : ¬0 = l₀
this : ¬s = 0
⊢ False

Tactic:
;

Goal state after:
L : PeriodPair
l₀ : ℂ
r : ℝ
s : ℂ
hr : 0 < r
hs : ‖s‖ < r
h : 2 * r ≤ 0
h✝ : ¬0 = l₀
this : ¬s = 0
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case e_f
n : ℕ
a : Multiset ℂ
hn : n ≠ 0
⊢ (fun x ↦ x + ↑n) = fun j ↦ ↑n * (j / ↑n + 1)

Tactic:
;

Goal state after:
case e_f
n : ℕ
a : Multiset ℂ
hn : n ≠ 0
⊢ (fun x ↦ x + ↑n) = fun j ↦ ↑n * (j / ↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case e_f
n : ℕ
a : Multiset ℂ
hn : n ≠ 0
x✝ : ℂ
⊢ x✝ + ↑n = ↑n * (x✝ / ↑n + 1)

Tactic:
;

Goal state after:
case e_f
n : ℕ
a : Multiset ℂ
hn : n ≠ 0
x✝ : ℂ
⊢ x✝ + ↑n = ↑n * (x✝ / ↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
;

Goal state after:
n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
x✝ : ℕ
⊢ (FormalMultilinearSeries.ofScalars ℂ (regularizedHGFunCoeff a b)).coeff x✝ = regularizedHGFunCoeff a b x✝

Tactic:
;

Goal state after:
a b : Multiset ℂ
x✝ : ℕ
⊢ (FormalMultilinearSeries.ofScalars ℂ (regularizedHGFunCoeff a b)).coeff x✝ = regularizedHGFunCoeff a b x✝
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
hx : ↑i ∈ (↑L.lattice \ {l₀})ᶜ
⊢ False

Tactic:
;

Goal state after:
L : PeriodPair
l₀ : ℂ
s : Finset ↥L.lattice
i : ↥L.lattice
hi : i ∈ s
h✝ : ¬↑i = l₀
hx : ↑i ∈ (↑L.lattice \ {l₀})ᶜ
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b c : ℂ
h : ∀ (k : ℕ), a ≠ -↑k ∧ b ≠ -↑k
⊢ (∀ (k : ℕ), ¬a = -↑k) ∧ ∀ (k : ℕ), ¬b = -↑k

Tactic:
;

Goal state after:
a b c : ℂ
h : ∀ (k : ℕ), a ≠ -↑k ∧ b ≠ -↑k
⊢ (∀ (k : ℕ), ¬a = -↑k) ∧ ∀ (k : ℕ), ¬b = -↑k
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
h₁ : l₀ - ↑l ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
h₂ : l₀ - ↑l + ↑l ∈ ↑L.lattice
h₃ : l₀ - ↑l + ↑l ≠ l₀
⊢ False

Tactic:
;

Goal state after:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
h₁ : l₀ - ↑l ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
h₂ : l₀ - ↑l + ↑l ∈ ↑L.lattice
h₃ : l₀ - ↑l + ↑l ≠ l₀
⊢ False
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: case pos.inr
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : Countable α
h✝ : Infinite α
⊢ MeasurableSet (range Nat.cast)

Tactic:
exact Nat.isClosedEmbedding_coe_real.isClosed_range.measurableSet

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

Goal state before:
pp: L : PeriodPair
z : ℂ
hl : ↑0 / 2 ∉ L.lattice
⊢ False

Tactic:
;

Goal state after:
L : PeriodPair
z : ℂ
hl : ↑0 / 2 ∉ L.lattice
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic

Goal state before:
pp: case one
θ : ℂ
⊢ 2 * cos θ * sin θ = 2 * sin θ * cos θ

Tactic:
;

Goal state after:
case one
θ : ℂ
⊢ 2 * cos θ * sin θ = 2 * sin θ * cos θ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z✝ : ℂ
l : ↥L.lattice
z : ℂ
hz : z ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}
i : ℂ
| (fun x ↦ ℘[L] (x + z)) (i + -z)

Tactic:
;

Goal state after:
L : PeriodPair
z✝ : ℂ
l : ↥L.lattice
z : ℂ
hz : z ∈ {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}
i : ℂ
| (fun x ↦ ℘[L] (x + z)) (i + -z)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e_f
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
⊢ ((if ↑w = ↑l₀ then 0 else -2 / (z - ↑w) ^ 3) + if ↑w = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) = -(2 / (z - ↑w) ^ 3)

Tactic:
;

Goal state after:
case e_f
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
w : ↥L.lattice
⊢ ((if ↑w = ↑l₀ then 0 else -2 / (z - ↑w) ^ 3) + if ↑w = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0) = -(2 / (z - ↑w) ^ 3)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_5.hnc
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ ¬↑l = L.ω₁ / 2

Tactic:
;

Goal state after:
case e'_5.hnc
L : PeriodPair
l : ↥L.lattice
z : ℂ
⊢ ¬↑l = L.ω₁ / 2
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
⊢ ∑' (b : ↥L.lattice), 2 / -(↑b - z) ^ 3 = ∑' (b : ↥L.lattice), 2 / (z - ↑b) ^ 3

Tactic:
congr! with l

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ -(↑l - z) ^ 3 = (z - ↑l) ^ 3
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖(fderiv ℝ (⇑g) (f x)) (deriv f x)‖ₑ ≤ ‖deriv f x‖ₑ

pp: case hl
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ (⇑g) (f x)

pp: case hf
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ f x

Tactic:
;

Goal state after:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ ‖(fderiv ℝ (⇑g) (f x)) (deriv f x)‖ₑ ≤ ‖deriv f x‖ₑ

case hl
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ (⇑g) (f x)

case hf
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
g : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
x : ℝ
hx : x ∈ Ioo a b
⊢ DifferentiableAt ℝ f x
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑0 + 1) + 1)) ^ 2 < 1

Tactic:
;

Goal state after:
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑0 + 1) + 1)) ^ 2 < 1
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
this : HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))
j : ℕ
⊢ 3 ≤ 2 * (j + 1) + 1

Tactic:
;

Goal state after:
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
this : HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))
j : ℕ
⊢ 3 ≤ 2 * (j + 1) + 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬↑l = l₀
⊢ (↑i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - 0) = (↑(i + 1) + 1) * ((↑l - x) ^ (↑i + 1 + 2))⁻¹ - 0

Tactic:
;

Goal state after:
case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬↑l = l₀
⊢ (↑i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - 0) = (↑(i + 1) + 1) * ((↑l - x) ^ (↑i + 1 + 2))⁻¹ - 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬↑l = l₀
⊢ ↑(i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - 0) = ↑(i + 1 + 1) * ((↑l - x) ^ (i + 1 + 2))⁻¹ - 0

Tactic:
;

Goal state after:
case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬↑l = l₀
⊢ ↑(i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - 0) = ↑(i + 1 + 1) * ((↑l - x) ^ (i + 1 + 2))⁻¹ - 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case succ
n✝ : ℕ
⊢ (↑n✝ + 1) * 4 ≤ (↑n✝ + 1 + 1) * 12

Tactic:
;

Goal state after:
case succ
n✝ : ℕ
⊢ (↑n✝ + 1) * 4 ≤ (↑n✝ + 1 + 1) * 12
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
this : 1 - log √2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

pp: n : ℕ
this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ √2 ≠ 0

Tactic:
log_sqrt

Goal state after:
n : ℕ
this : 1 - log 2 / 2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

n : ℕ
this : 1 - log √2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 0 ≤ 2

n : ℕ
this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ √2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
⊢ 0 < ↑(n + 1)! / (√(2 * ↑(n + 1)) * (↑(n + 1) / rexp 1) ^ (n + 1))

Tactic:
;

Goal state after:
n : ℕ
⊢ 0 < ↑(n + 1)! / (√(2 * ↑(n + 1)) * (↑(n + 1) / rexp 1) ^ (n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ √2 * √π * √↑n * (↑n / rexp 1) ^ n = √π * (√2 * √↑n * (↑n / rexp 1) ^ n)

Tactic:
;

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ √2 * √π * √↑n * (↑n / rexp 1) ^ n = √π * (√2 * √↑n * (↑n / rexp 1) ^ n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: ⊢ ∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ 0) = π

Tactic:
;

Goal state after:
⊢ ∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ 0) = π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ sin (↑n * π) - sin 0 = 0

Tactic:
;

Goal state after:
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
h✝ : 0 ≤ n
⊢ sin (↑n * π) - sin 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ↑n * log ↑n - ↑n + log ↑n / 2 + log (2 * π) / 2 ≤ log ↑n !

Tactic:
by
  calc
    _ = (log (2 * π) + log n) / 2 + n * (log n - 1) := by ring
    _ = log (√(2 * π * n) * (n / rexp 1) ^ n) := by
      rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp] <;>
      positivity
    _ ≤ _ := log_le_log (by positivity) (le_factorial_stirling n)

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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
i✝ : ℕ
⊢ 0 i✝ ≤ (fun i ↦ (↑i + 2) * κ ^ (-↑i)) i✝

Tactic:
;

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
i✝ : ℕ
⊢ 0 i✝ ≤ (fun i ↦ (↑i + 2) * κ ^ (-↑i)) i✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case inl
i : ℕ
hi : i ∈ Finset.Iic 0
⊢ eval (node 0 i) (T ℝ ↑0) = (-1) ^ i

pp: case inr
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
⊢ eval (node n i) (T ℝ ↑n) = (-1) ^ i

Tactic:
· simp [show i = 0 by grind]

Goal state after:
case inr
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
⊢ eval (node n i) (T ℝ ↑n) = (-1) ^ i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
⊢ ↑n * (↑i * π / ↑n) = ↑i * π

Tactic:
;

Goal state after:
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
⊢ ↑n * (↑i * π / ↑n) = ↑i * π
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
i✝ : ↥L.lattice
⊢ 0 i✝ ≤ (fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖) i✝

Tactic:
;

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
i✝ : ↥L.lattice
⊢ 0 i✝ ≤ (fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖) i✝
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case a
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (↑k / ↑n * ↑π * I) = 1
m : ℤ
hx : ↑k / ↑n * ↑π * I = ↑m * (2 * ↑π * I)
⊢ ↑k + ↑m * (2 * ↑π * I) * (↑n / ↑π / I) - (2 * ↑n * ↑m + ↑k / ↑n * ↑π * I * (↑n / ↑π / I)) = 0

Tactic:
;

Goal state after:
case a
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (↑k / ↑n * ↑π * I) = 1
m : ℤ
hx : ↑k / ↑n * ↑π * I = ↑m * (2 * ↑π * I)
⊢ ↑k + ↑m * (2 * ↑π * I) * (↑n / ↑π / I) - (2 * ↑n * ↑m + ↑k / ↑n * ↑π * I * (↑n / ↑π / I)) = 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ↑((Equiv.prodCongrLeft fun x ↦
            { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
          (Prod.map some id p)).2 =
    l₀
⊢ 0 ≤ (↑p.1 + 2) * (κ ^ p.1)⁻¹ * ((‖↑p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖)

Tactic:
;

Goal state after:
case pos
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ↑((Equiv.prodCongrLeft fun x ↦
            { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
          (Prod.map some id p)).2 =
    l₀
⊢ 0 ≤ (↑p.1 + 2) * (κ ^ p.1)⁻¹ * ((‖↑p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
c : ℝ
P : ℝ[X]
⊢ π / ↑n * (c * ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P) =
    c * (π / ↑n * ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P)

Tactic:
;

Goal state after:
n : ℕ
c : ℝ
P : ℝ[X]
⊢ π / ↑n * (c * ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P) =
    c * (π / ↑n * ∑ x ∈ range n, eval (cos ((2 * ↑x + 1) / (2 * ↑n) * π)) P)
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
⊢ 2 * cos (↑r * π) = 2 * ↑hcos.choose

Tactic:
;

Goal state after:
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
⊢ 2 * cos (↑r * π) = 2 * ↑hcos.choose
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ↑↑(-k).negOnePow = ↑↑k.negOnePow

Tactic:
;

Goal state after:
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ↑↑(-k).negOnePow = ↑↑k.negOnePow
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
⊢ Complex.exp (↑k / ↑n * ↑π * I) = Complex.exp (↑2 * (↑k / (2 * ↑n) * ↑π * I))

Tactic:
;

Goal state after:
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
z : ℂ := Complex.exp (↑k / (2 * ↑n) * ↑π * I)
hz : z = Complex.exp (↑k / (2 * ↑n) * ↑π * I)
⊢ Complex.exp (↑k / ↑n * ↑π * I) = Complex.exp (↑2 * (↑k / (2 * ↑n) * ↑π * I))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : P = T ℝ ↑n
⊢ sumNodes n c P = sumNodes n c (T ℝ ↑n)

Tactic:
;

Goal state after:
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : P = T ℝ ↑n
⊢ sumNodes n c P = sumNodes n c (T ℝ ↑n)
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ cos (θ - π / 2) = sin θ

pp: case convert_1
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ ∃ r, θ - π / 2 = ↑r * π

pp: case convert_2
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ ∃ q, cos (θ - π / 2) = ↑q

Tactic:
· exact cos_sub_pi_div_two θ

Goal state after:
case convert_1
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ ∃ r, θ - π / 2 = ↑r * π

case convert_2
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ ∃ q, cos (θ - π / 2) = ↑q
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
a✝¹ : ℚ
a✝ : θ = ↑a✝¹ * π
⊢ θ - π / 2 = ↑(a✝¹ - 1 / 2) * π

Tactic:
;

Goal state after:
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
a✝¹ : ℚ
a✝ : θ = ↑a✝¹ * π
⊢ θ - π / 2 = ↑(a✝¹ - 1 / 2) * π
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
a✝¹ : ℚ
a✝ : θ = ↑a✝¹ * π
⊢ θ - π / 2 = (↑a✝¹ - 1 / 2) * π

Tactic:
;

Goal state after:
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
a✝¹ : ℚ
a✝ : θ = ↑a✝¹ * π
⊢ θ - π / 2 = (↑a✝¹ - 1 / 2) * π
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ ‖↑p.1 + 1 + 1‖ * ‖↑p.2 - x‖ ^ (-2 + (-1 + -↑p.1)) = ‖↑p.1 + 2‖ * ‖↑p.2 - x‖ ^ (-3 - ↑p.1) ∨ z - x = 0

Tactic:
;

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ ‖↑p.1 + 1 + 1‖ * ‖↑p.2 - x‖ ^ (-2 + (-1 + -↑p.1)) = ‖↑p.1 + 2‖ * ‖↑p.2 - x‖ ^ (-3 - ↑p.1) ∨ z - x = 0
Module: Mathlib.NumberTheory.Niven

Goal state before:

Tactic:
;

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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ True ∨ -x + z = 0

Tactic:
;

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ¬↑((Equiv.prodCongrLeft fun x ↦
              { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
            (Prod.map some id p)).2 =
      l₀
hpx : ‖↑p.2 - x‖ ≠ 0
hxz : z ≠ x
⊢ True ∨ -x + z = 0