mathlib-initiative/mathlib-tactics huggingface dataset:
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 + 2) * (κ ^ p.1)⁻¹ * ((‖↑p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖) = (↑p.1 + 2) * κ ^ (-↑p.1) * (‖↑p.2 - x‖ ^ (-3) * ‖z - x‖)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
θ : ℝ
h : ↑r * π = θ
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc (0 * π) (1 * π)
⊢ θ ∈ Set.Icc 0 π

Tactic:
by

Goal state after:
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
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i✝ : ℕ
hix : node n i✝ = x
hi✝ : i✝ ∈ Finset.Iic n
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≤ (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hi : i ∈ range (2 * n)
⊢ ContinuousOn (fun x ↦ eval x (c i • ↑(chebyshevTsequence ℝ) i)) (Set.Icc (-1) 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
h_bnd : r ∈ Set.Icc 0 1
⊢ r ∈ {0, 1 / 3, 1 / 2, 2 / 3, 1}

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < 2 * ↑n
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
this : Int.fract r ∈ {0, 1 / 3, 1 / 2, 2 / 3, 1}
⊢ Int.fract r ∈ {0, 1 / 3, 1 / 2, 2 / 3}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
⊢ Int.fract r ∈ Set.Icc 0 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos (↑(Int.fract r) * π) = ↑((-1) ^ ⌊r⌋ * q)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
⊢ Int.fract r ∈ {0, 1 / 3, 1 / 2, 2 / 3}

Tactic:
by

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‖
⊢ Summable (Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)

Tactic:
by

Goal state after:
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
⊢ sumNodes n c P = sumNodes n c (T ℝ ↑n) ↔ P = T ℝ ↑n

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(Finset.range (n + 1)).card

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hr : 3 < r.den
⊢ Irrational (cos (↑r * π))

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ sumNodes n (leadingCoeffC n) P = P.coeff n

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (T ℝ ↑n).degree ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : LocallyFiniteOrder α
m n : ℕ
hmn : m ≤ n
⊢ (fun n ↦ Icc (-↑n) ↑n) m ⊆ (fun n ↦ Icc (-↑n) ↑n) n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : LocallyFiniteOrder α
⊢ Monotone fun n ↦ Icc (-↑n) ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
⊢ box 0 = {0}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ box (n + 1) = Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Disjoint (box (n + 1)) (Icc (-↑n) ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ (box (n + 1)).disjUnion (Icc (-↑n) ↑n) ⋯ = Icc (-↑n.succ) ↑n.succ

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ sumNodes n (leadingCoeffC n) (T ℝ ↑n) = 2 ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
n : ℕ
inst✝ : DecidableEq α
⊢ 0 ∈ box n ↔ n = 0

Tactic:
by

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‖
l : ↥L.lattice
h : ¬↑l = l₀
⊢ ↑l ≠ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
n : ℕ
inst✝ : DecidableEq α
x : α
hx : x ∈ box n
hn : n = 0
⊢ x = 0

Tactic:
by

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‖
l : ↥L.lattice
h : ¬↑l = l₀
⊢ z - x ∈ Metric.eball 0 ‖↑l - x‖ₑ

Tactic:
by

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

Goal state before:
pp: n i : ℕ
hi : i ≤ n
⊢ 0 < (-1) ^ i * leadingCoeffC n i

Tactic:
by

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‖
⊢ ℘[L - l₀] z = ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ P.coeff n ≤ 2 ^ (n - 1)

Tactic:
by

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‖
⊢ HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i) (℘[L - l₀] z)

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ P.leadingCoeff ≤ 2 ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(box (n + 1)) = #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: n : ℕ
x✝ : n + 1 ≠ 0
⊢ #(box (n + 1)) = 8 * (n + 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ P.coeff n = 2 ^ (n - 1) ↔ P = T ℝ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: x : ℤ × ℤ
⊢ x ∈ box 0 ↔ max x.1.natAbs x.2.natAbs = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P = T ℝ ↑n
⊢ P.leadingCoeff = 2 ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: x : ℤ × ℤ
n : ℕ
⊢ x ∈ box (n + 1) ↔ max x.1.natAbs x.2.natAbs = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: x : ℤ × ℤ
⊢ ∃! n, x ∈ box n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x : Fin 2 → ℤ
⊢ ‖x‖ = ↑(max (x 0).natAbs (x 1).natAbs)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x y : ℤ
⊢ ‖![x, y]‖ = ‖![y, x]‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: m n : ℤ
⊢ ↑|n| ≤ ‖![n, m]‖

Tactic:
by

Goal state after:
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 ∈ Metric.eball 0 ↑r
⊢ ‖z‖ < ↑r

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: m n : ℤ
⊢ ↑|m| ≤ ‖![n, m]‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: n : ℕ
⊢ ‖![1, ↑n + 1]‖ = ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: n : ℕ
⊢ ‖![1, -(↑n + 1)]‖ = ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
⊢ z.im ^ 2 ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.leadingCoeff = 2 ^ (n - 1)
hPdeg' : ↑n ≤ P.degree
⊢ P.coeff n = 2 ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
⊢ r1 z = 1 / ((z.re / z.im) ^ 2 + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
⊢ 0 < r1 z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2
⊢ (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 =
    (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2
H2 :
  (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 =
    (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2
⊢ 0 < z.re ^ 2 + z.im ^ 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
hP : ↑d < ↑n
⊢ d - 1 < n - 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
d : ℕ
hd : ↑d = P.degree
hPdeg : ↑d ≤ ↑n
hP : ↑d < ↑n
this : d - 1 < n - 1
⊢ 2 ^ (d - 1) < 2 ^ (n - 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ P.leadingCoeff = 2 ^ (n - 1) ↔ P = T ℝ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
⊢ 0 < r z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 <
    { coe := { re := A, im := B }, coe_im_pos := h }.re ^ 2 / { coe := { re := A, im := B }, coe_im_pos := h }.im ^ 2 +
      1

Tactic:
by

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(Finset.range (n + 1)).card

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 < z.re ^ 2 / z.im ^ 2 + 1

Tactic:
by

Goal state after:
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₀})ᶜ
⊢ HasFPowerSeriesOnBall ℘[L - l₀] (L.weierstrassPExceptSeries l₀ x) x ↑r

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ r { coe := { re := A, im := B }, coe_im_pos := h } ≤ r z

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ z.im ≤ √((c * z.re + d) ^ 2 + (↑c * z).im ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hc : 1 ≤ c ^ 2
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ 0 ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
⊢ r z ≤ ‖↑c * ↑z + ↑d‖

Tactic:
by

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

Goal state before:
pp: L : PeriodPair
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:
by

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
⊢ l₀ ∈ (↑L.lattice \ {l₀})ᶜ

Tactic:
by

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ -1 ≤ x

Tactic:
by

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ x ≤ 1

Tactic:
by

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

Goal state before:
pp: L : PeriodPair
l : ℂ
n : ℕ
⊢ ↑n ! ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ x 0 ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ eval x (T ℝ n) ∈ Set.Icc (-1) 1

Tactic:
by

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : |x| ≤ 1
⊢ |eval x (T ℝ n)| ≤ 1

Tactic:
by

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ eval x (T ℝ n)

Tactic:
by

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
⊢ arcosh x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ x 1 ≠ 0

Tactic:
by

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ sumNodes n (iterateDerivativeC n k x) P = eval x ((⇑derivative)^[k] P)

Tactic:
by

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ ↑n ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ arcosh x ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
⊢ 1 < eval x (T ℝ n)

Tactic:
by

Goal state after:
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

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : x ≤ -1
⊢ 1 ≤ ↑↑n.negOnePow * eval x (T ℝ n)

Tactic:
by

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

Goal state before:
pp: n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
t : Finset ℕ
a : ℕ
x✝ : a ∈ t
⊢ 0 ≤ x - node n a

Tactic:
by

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ 1 < ↑↑n.negOnePow * eval x (T ℝ n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ ↑(x 0) * ↑z + ↑(x 1) = (↑(x 0) / ↑‖x‖ * ↑z + ↑(x 1) / ↑‖x‖) * ↑‖x‖

Tactic:
by

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

Goal state before:
pp: n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ (-1) ^ i * iterateDerivativeC n k x i

Tactic:
by

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

Goal state before:
pp: n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ (-1) ^ i * iterateDerivativeC n k x i

Tactic:
by
  rw [iterateDerivativeC, ← mul_assoc]
  refine mul_nonneg ?_ (Finset.sum_nonneg' ?_)
  · rw [← mul_assoc, mul_comm (a := (-1) ^ i), mul_assoc]
    exact le_of_lt <| mul_pos (Nat.cast_pos.mpr <| Nat.factorial_pos k)
      (negOnePow_mul_leadingCoeffC_pos hi)
  · exact fun t => Finset.prod_nonneg (fun a _ => by grind [show node n a ≤ 1 from cos_le_one _])

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℤ
x : ℝ
hx : 1 ≤ |x|
⊢ 1 ≤ |eval x (T ℝ n)|

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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
⊢ 0 ≤ -x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
t : Finset ℕ
x✝¹ : t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i)
a : ℕ
x✝ : a ∈ t
⊢ 0 ≤ x - node n a

Tactic:
by

Goal state after:
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 Metric.ball_subset_closedBall

Goal state after: