mathlib-initiative/mathlib-tactics huggingface dataset:
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

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
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
Module: Mathlib.NumberTheory.Niven

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

Tactic:
]

Goal state after:
r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ cos (↑(r - ↑⌊r⌋) * π) = ↑((-1) ^ ⌊r⌋ * q)
Module: Mathlib.NumberTheory.Niven

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

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
]

Goal state after:
r : ℚ
hr : 3 < (Int.fract r).den
⊢ Irrational (cos (↑r * π))
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inl
r : ℚ
hr : 3 < Rat.den 0
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 0
⊢ False

Tactic:
]

Goal state after:
case inl
r : ℚ
hr : 3 < Rat.den 0
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 0
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inl
r : ℚ
hr : 3 < (1 / 3).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 3
⊢ False

Tactic:
]

Goal state after:
case inr.inl
r : ℚ
hr : 3 < (1 / 3).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 3
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

Tactic:
]

Goal state after:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

Tactic:
]

Goal state after:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ↑n < ↑(n + 1)
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inl
r : ℚ
hr : 3 < (1 / 2).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 2
⊢ False

Tactic:
]

Goal state after:
case inr.inr.inl
r : ℚ
hr : 3 < (1 / 2).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 2
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inr
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 2 / 3
⊢ False

Tactic:
]

Goal state after:
case inr.inr.inr
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 2 / 3
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inr
r : ℚ
hr : 3 < (2 / 3).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 2 / 3
⊢ False

Tactic:
]

Goal state after:
case inr.inr.inr
r : ℚ
hr : 3 < (2 / 3).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 2 / 3
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

Tactic:
]

Goal state after:
n : ℕ
⊢ (T ℝ ↑n).coeff n = 2 ^ (n - 1)
Module: Mathlib.Order.Interval.Finset.Box

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Icc (-↑(n + 1)) ↑(n + 1) \ Icc (-↑n) ↑n = Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n
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 (Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n) (Icc (-↑n) ↑n)

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Disjoint (Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n) (Icc (-↑n) ↑n)
Module: Mathlib.Order.Interval.Finset.Box

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

Tactic:
]

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 = 0
hn : n = 0
⊢ x = 0

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁴ : Ring α
inst✝³ : PartialOrder α
inst✝² : IsOrderedRing α
inst✝¹ : LocallyFiniteOrder α
n : ℕ
inst✝ : DecidableEq α
x : α
hx : x = 0
hn : n = 0
⊢ x = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n i : ℕ
hi : i ≤ n
this : 0 < (-1) ^ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
⊢ 0 < (-1) ^ i * leadingCoeffC n i

Tactic:
]

Goal state after:
n i : ℕ
hi : i ≤ n
this : 0 < (-1) ^ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹
⊢ 0 < (-1) ^ i * leadingCoeffC n i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

Tactic:
]

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 : ℕ
⊢ #(Icc (-↑n.succ).1 (↑n.succ).1) * #(Icc (-↑n.succ).2 (↑n.succ).2) - #(Icc (-↑n).1 (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
]

Goal state after:
α : 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 : ℕ
⊢ #(Icc (-↑n.succ).1 (↑n.succ).1) * #(Icc (-↑n.succ).2 (↑n.succ).2) - #(Icc (-↑n).1 (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
n : ℕ
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : ↑d = P.degree
hPdeg : d ≤ n
⊢ P.coeff d ≤ 2 ^ (n - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

pp: case ha
n : ℕ
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : ↑d = P.degree
hPdeg : d ≤ n
⊢ 1 ≤ 2

Tactic:
]

Goal state after:
case ha
n : ℕ
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : ¬P = 0
d : ℕ
hd : ↑d = P.degree
hPdeg : d ≤ n
⊢ 1 ≤ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

Tactic:
]

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

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

Tactic:
]

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:
]

Goal state after:
x : Fin 2 → ℤ
⊢ ‖x‖₊ = max ↑(x 0).natAbs ↑(x 1).natAbs
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: m n : ℤ
⊢ ↑↑n.natAbs ≤ ↑n.natAbs

Tactic:
]

Goal state after:
m n : ℤ
⊢ ↑↑n.natAbs ≤ ↑n.natAbs
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: m n : ℤ
⊢ ↑↑m.natAbs ≤ ↑m.natAbs

Tactic:
]

Goal state after:
m n : ℤ
⊢ ↑↑m.natAbs ≤ ↑m.natAbs
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.coeff n = 2 ^ (n - 1)
hPdeg' : P.degree = ↑n
⊢ P.coeff n = 2 ^ (n - 1)

Tactic:
]

Goal state after:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.coeff n = 2 ^ (n - 1)
hPdeg' : P.degree = ↑n
⊢ P.coeff n = 2 ^ (n - 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
]

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.degree = ⊥
⊢ 0 ≠ 2 ^ (n - 1)

Tactic:
]

Goal state after:
n : ℕ
P : ℝ[X]
hn : 2 ≤ n
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
hP : P.degree = ⊥
⊢ 0 ≠ 2 ^ (n - 1)
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 ≤ (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2

Tactic:
]

Goal state after:
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 ≤ (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2
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 < ↑(n + 1)

Tactic:
]

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_5
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))
A : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ↑r < ‖↑l - x‖
i : ℕ
⊢ (if i = 0 then ℘[L - l₀] x
      else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)) *
      z ^ i =
    (if i = 0 then ℘[L - l₀] x
      else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)) *
      z ^ i

Tactic:
]

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
⊢ ↑n < ↑(n + 1)

Tactic:
]

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ↑n < ↑(n + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
]

Goal state after:
case a
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ |z.re| ^ 2 / z.im ^ 2 ≤
    { coe := { re := A, im := B }, coe_im_pos := h }.re ^ 2 / { coe := { re := A, im := B }, coe_im_pos := h }.im ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
]

Goal state after:
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ z.im ^ 2 ≤ (c * z.re + d) ^ 2 + c ^ 2 * z.im ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
]

Goal state after:
n : ℤ
x : ℝ
hx : x ∈ Set.Icc (-1) 1
⊢ eval (cos (arccos x)) (T ℝ n) ∈ Set.Icc (-1) 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
]

Goal state after:
x : Fin 2 → ℤ
hx : x 0 ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ x 0 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case refine_1
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2

Tactic:
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

Goal state after:
case refine_1
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
this : x 0 ≠ 0
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
h₁ : P.degree < ↑(Finset.range (n + 1)).card
⊢ ∑ i ≤ n,
      eval (node n i) P *
        (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)) =
    ∑ i ∈ Finset.range (n + 1),
      ↑k.factorial *
        ((eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
          ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
            ∏ a ∈ t, (x - node n a))

Tactic:
]

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
h₁ : P.degree < ↑(Finset.range (n + 1)).card
⊢ ∑ i ≤ n,
      eval (node n i) P *
        (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)) =
    ∑ i ∈ Finset.range (n + 1),
      ↑k.factorial *
        ((eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
          ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
            ∏ a ∈ t, (x - node n a))
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)) / ↑n !

Tactic:
]

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)) / ↑n !
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
]

Goal state after:
n : ℤ
x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ eval (cosh (arcosh x)) (T ℝ n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
]

Goal state after:
x : Fin 2 → ℤ
hx : x 1 ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ x 1 ≠ 0
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 ∧ arcosh x ≠ 0

Tactic:
]

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ ↑n ≠ 0 ∧ arcosh x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
]

Goal state after:
n : ℤ
x : ℝ
hx : x ≤ -1
⊢ 1 ≤ ↑↑n.negOnePow * (↑↑n.negOnePow * eval (-x) (T ℝ n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤
    (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹) *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)

Tactic:
]

Goal state after:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤
    (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹) *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
]

Goal state after:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
⊢ x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
]

Goal state after:
n : ℤ
x : ℝ
hx : x ≤ -1
⊢ (-1 * -1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
]

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ 1 < ↑↑n.negOnePow * (↑↑n.negOnePow * eval (-x) (T ℝ n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case refine_1
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ ↑k.factorial * ((-1) ^ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

Tactic:
]

Goal state after:
case refine_1
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ ↑k.factorial * ((-1) ^ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
]

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ (-1 * -1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)
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) * ↑z + ↑(x 1)

Tactic:
]

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
⊢ 0 <
    (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹) *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)

Tactic:
]

Goal state after:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 <
    (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹) *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
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:
wlog! h : 0 ≤ x
  · simpa [T_eval_neg, abs_mul, abs_unit_intCast] using @this n hn (-x) (by grind) (by grind)
  · exact one_lt_eval_T_real hn (abs_of_nonneg h ▸ hx) |>.trans_le <| le_abs_self _

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

Goal state before:
pp: case refine_1
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < ↑k.factorial * ((-1) ^ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)

Tactic:
]

Goal state after:
case refine_1
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < ↑k.factorial * ((-1) ^ i * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

Tactic:
]

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

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : ∃ k, ↑k * π = ↑n * arccos x
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
]

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : ∃ k, ↑k * π = ↑n * arccos x
hx : |x| ≤ 1
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)
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 / π)
⊢ 0 ≤ ↑n * (arccos x / π)

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
⊢ 0 ≤ ↑n * (arccos x / π)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case h₂
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∉ L.lattice
z : ℂ
i : ℕ
f : i = 0
⊢ ℘[L] = ℘[L]

Tactic:
]

Goal state after:
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 / π)
⊢ ↑n * (arccos x / π) ≤ ↑n * 1

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
⊢ ↑n * (arccos x / π) ≤ ↑n * 1
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
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ node n a < node n 0

Tactic:
]

Goal state after:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ node n a < node n 0
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
⊢ x = x

Tactic:
]

Goal state after: