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‖
⊢ 0 ≤ fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ∫ (x : ℝ), eval x (T ℝ ↑n) * eval x (T ℝ ↑n) ∂measureT = π / 2

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 0 < π

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 0 < (↑n)⁻¹

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ StrictAntiOn (fun x ↦ node n x) ↑(Finset.range (n + 1))

Tactic:
by

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

Goal state before:
pp: n i j : ℕ
hj : j ≤ n
hij : i < j
⊢ i ≤ n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
this :
  (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (-1) ^ k - 1
s a b t : ℂ
h : s * a⁻¹ * b = t
ha : a ≠ 0
hb : b ≠ 0
⊢ s = a / b * t

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
this :
  (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (-1) ^ k - 1
hf : ∀ {s a b t : ℂ}, s * a⁻¹ * b = t → a ≠ 0 → b ≠ 0 → s = a / b * t
⊢ Complex.exp (↑k / ↑n * ↑π * I) - 1 ≠ 0

Tactic:
by

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

Goal state before:
pp: n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j)
⊢ (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
x : α
h₁ : IsIntegral ℤ x
x✝ : ∃ k, x = ↑k
w : ℤ
h : x = ↑w
⊢ x = ↑↑w

Tactic:
by

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

Goal state before:
pp: n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j)
union : (Finset.range (n + 1)).erase i = Finset.range i ∪ Finset.Ioc i n
⊢ Disjoint (Finset.range i) (Finset.Ioc i n)

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
this :
  (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * Complex.exp (-(↑k / (2 * ↑n) * ↑π * I)) *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (-1) ^ k - 1
⊢ ∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I) =
    Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
x : α
h₁ : IsIntegral ℤ x
⊢ (∃ q, x = ↑q) ↔ ∃ k, x = ↑k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ cexp (↑q * ↑π * I) ^ (2 * q.den) = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (cexp (↑q * ↑π * I))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (cexp (-(↑q * ↑π) * I))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (2 * sin (↑q * ↑π))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (2 * cos (↑q * ↑π))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ (algebraMap ℤ ℂ) ↑2 ∈ nonZeroDivisors ℂ

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ ∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I) =
    Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ ((algebraMap ℝ ℂ) (2 * sin (↑q * π)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ ((algebraMap ℝ ℂ) (2 * cos (↑q * π)))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ (algebraMap ℤ ℝ) ↑2 ∈ nonZeroDivisors ℝ

Tactic:
by

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

Goal state before:
pp: n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
⊢ sumZeroes n (∑ i ∈ s, P i) = ∑ i ∈ s, sumZeroes n (P i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsAlgebraic ℤ ((algebraMap ℝ ℂ) (tan (↑q * π)))

Tactic:
by

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

Goal state before:
pp: α : ℝ
i : ℕ
hα : |α| ≤ 1
⊢ (-1) ^ i * α ≤ 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : ℝ
P : ℝ[X]
⊢ sumZeroes n (c • P) = c * sumZeroes n P

Tactic:
by

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

Goal state before:
pp: α β : ℝ
i : ℕ
⊢ (-1) ^ i * α * ((-1) ^ i * β) = (-1) ^ i * (-1) ^ i * α * β

Tactic:
by

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ sumZeroes n (T ℝ 0) = π

Tactic:
by

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

Goal state before:
pp: α β : ℝ
i : ℕ
⊢ (-1) ^ i * (-1) ^ i * α * β = α * β

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : ∑ i ∈ range n, 2 * cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π)) = 0
⊢ π / ↑n ≠ 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : 2 * ∑ i ∈ range n, cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π)) = 0
⊢ 2 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : ∑ i ∈ range n, 2 * cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π)) = 0
⊢ sumZeroes n (T ℝ k) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : ∑ i ∈ range n, 2 * ↑(cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π))) = 0
⊢ ∑ i ∈ range n, 2 * cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π)) = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : ∑ i ∈ range n, 2 * Complex.cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π)) = 0
⊢ ∑ i ∈ range n, 2 * ↑(cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π))) = 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ ¬2 * ↑n ∣ -k

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
⊢ k ∈ Finset.Icc (-2) 2

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‖
κ : ℝ
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₀
h : ‖↑p.2 - x‖ = 0
⊢ ↑p.2 = x

Tactic:
by

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

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) ≤ 1 * ((-1) ^ i * c i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
hk_values : k ∈ Finset.Icc (-2) 2
⊢ cos (↑r * π) ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
show cos (r * π) = k / 2 by grind

Goal state after:
r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
k : ℤ
hk : 2 * cos (↑r * π) = ↑k
hk_values : k ∈ Finset.Icc (-2) 2
⊢ ↑k / 2 ∈ {-1, -1 / 2, 0, 1 / 2, 1}
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ 1 * ((-1) ^ i * c i) = eval (node n i) (T ℝ ↑n) * c i

Tactic:
by

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

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

Tactic:
by

Goal state after:
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) = z ^ 2

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‖
κ : ℝ
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₀
h : ‖↑p.2 - x‖ = 0
⊢ False

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
⊢ P = T ℝ ↑n → sumNodes n c P = sumNodes n c (T ℝ ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
⊢ cos θ ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
by

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
⊢ sumZeroes n (T ℝ k) = 0

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
⊢ P ∈ degreeLT ℝ (2 * n)

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
hmem : P ∈ degreeLT ℝ (2 * n)
⊢ ∀ i < 2 * n, IsUnit (↑(chebyshevTsequence ℝ) i).leadingCoeff

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ sin θ ∈ {-1, -1 / 2, 0, 1 / 2, 1}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

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‖
κ : ℝ
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
⊢ ‖((↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id p)).1 +
              1) *
            (↑((Equiv.prodCongrLeft fun x ↦
                        { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                          right_inv := ⋯ })
                      (Prod.map some id p)).2 -
                x) ^
              (-(↑((Equiv.prodCongrLeft fun x ↦
                          { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                            right_inv := ⋯ })
                        (Prod.map some id p)).1 +
                  2)) -
          Nat.rec
            (↑((Equiv.prodCongrLeft fun x ↦
                      { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯,
                        right_inv := ⋯ })
                    (Prod.map some id p)).2 ^
              (-2))
            (fun n n_ih ↦ 0)
            ((Equiv.prodCongrLeft fun x ↦
                  { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
                (Prod.map some id p)).1) *
        (z - x) ^
          ((Equiv.prodCongrLeft fun x ↦
                { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
              (Prod.map some id p)).1‖ =
    ‖↑p.1 + 2‖ * ‖↑p.2 - x‖ ^ (-3 - ↑p.1) * ‖z - x‖ ^ (p.1 + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1
h₂ : cos π = -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‖
κ : ℝ
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.2 - x‖ ^ (-3 - ↑p.1) * ‖z - x‖ ^ (p.1 + 1) =
    ‖↑p.1 + 2‖ * ((‖↑p.2 - x‖ / ‖z - x‖) ^ p.1)⁻¹ * ((‖↑p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

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

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 : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
⊢ 0 < 2 * ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 1 / 2
h₂ : cos (π / 3) = 1 / 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‖
κ : ℝ
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
⊢ 0 < ‖z - x‖

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ ∈ {1}
h₂ : cos 0 = 1
⊢ 0 ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ ∈ {1}
h₂ : cos 0 = 1
⊢ 0 ≤ π

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 : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
⊢ 2 * ↑n * 0 < ↑i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
⊢ θ ∈ {0, π / 3, π / 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‖
κ : ℝ
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.2 - x‖ / ‖z - x‖) ^ 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.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 : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
⊢ ¬2 * ↑n ∣ ↑i

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
this :
  ∑ i ≤ n, (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) <
    ∑ i ≤ n, (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
⊢ ∑ i ≤ n, eval (node n i) P * c i < ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * 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 : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
this : ¬2 * ↑n ∣ ↑i
⊢ ↑i ≠ 0

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 * π ∈ Set.Icc (0 * π) (1 * π)

Tactic:
by

Goal state after: