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

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x else (↑i + 1) * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹)).coeff
      (i + 1) =
    (↑i + 2) * (L.sumInvPow x (i + 3) - ∑' (l : ↥L.lattice), if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0)

pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (↑i + 2) * (L.sumInvPow x (i + 3) - ∑' (l : ↥L.lattice), if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
·

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x else (↑i + 1) * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹)).coeff
      (i + 1) =
    (↑i + 2) * (L.sumInvPow x (i + 3) - ∑' (l : ↥L.lattice), if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
this :
  HasSum (fun i ↦ (1 / (2 * ↑(n + 1) + 1)) ^ 2 * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ i)
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 * (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))

pp: case refine_1
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ (1 / (2 * ↑(n + 1) + 1)) ^ 2 < 1

Tactic:
·

Goal state after:
case refine_2
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
this :
  HasSum (fun i ↦ (1 / (2 * ↑(n + 1) + 1)) ^ 2 * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ i)
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 * (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)⁻¹)
⊢ HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

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

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‖ₑ

Tactic:
·

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

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (↑i + 2) * (L.sumInvPow x (i + 3) - ∑' (l : ↥L.lattice), if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
·

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (↑i + 2) * (L.sumInvPow x (i + 3) - ∑' (l : ↥L.lattice), if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

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

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‖ₑ

Tactic:
·

Goal state after:
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: case zero
⊢ log (stirlingSeq 0) - log (stirlingSeq (0 + 1)) ≤ 1 / (12 * ↑0 * (↑0 + 1))

pp: case succ
n : ℕ
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤ 1 / (12 * ↑(n + 1) * (↑(n + 1) + 1))

Tactic:
·

Goal state after:
case zero
⊢ log (stirlingSeq 0) - log (stirlingSeq (0 + 1)) ≤ 1 / (12 * ↑0 * (↑0 + 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ ∑' (x_1 : ↥L.lattice), (↑i + 2) * (((↑x_1 - x) ^ (i + 3))⁻¹ - if x_1 = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ Summable fun l ↦ if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0

Tactic:
·

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ ∑' (x_1 : ↥L.lattice), (↑i + 2) * (((↑x_1 - x) ^ (i + 3))⁻¹ - if x_1 = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

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 i

Tactic:
·

Goal state after:
case pos
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ↑l = l₀
⊢ (↑i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - ((l₀ - x) ^ ↑(i + 3))⁻¹) = 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 i

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 i
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ Summable fun l ↦ if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0

Tactic:
·

Goal state after:
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ Summable fun l ↦ if l = ⟨l₀, hl₀⟩ then (l₀ - x) ^ (-↑(i + 3)) else 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∉ L.lattice
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x else (↑i + 1) * (L.sumInvPow x (i + 2) - 0)).coeff
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
·

Goal state after:
case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∉ L.lattice
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x else (↑i + 1) * (L.sumInvPow x (i + 2) - 0)).coeff
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹ = ∫ (x : ℝ) in 1..-1, ((fun θ ↦ f (cos θ)) ∘ arccos) x * -(1 / √(1 - x ^ 2))

pp: case hf
f : ℝ → ℝ
⊢ ContinuousOn arccos (uIcc 1 (-1))

pp: case hff'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), HasDerivAt arccos (-(1 / √(1 - x ^ 2))) x

pp: case hf'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), -(1 / √(1 - x ^ 2)) ≤ 0

Tactic:
·

Goal state after:
f : ℝ → ℝ
⊢ ∫ (x : ℝ) in 1..-1, f x * -√(1 - x ^ 2)⁻¹ = ∫ (x : ℝ) in 1..-1, ((fun θ ↦ f (cos θ)) ∘ arccos) x * -(1 / √(1 - x ^ 2))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: case hf
f : ℝ → ℝ
⊢ ContinuousOn arccos (uIcc 1 (-1))

pp: case hff'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), HasDerivAt arccos (-(1 / √(1 - x ^ 2))) x

pp: case hf'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), -(1 / √(1 - x ^ 2)) ≤ 0

Tactic:
·

Goal state after:
case hf
f : ℝ → ℝ
⊢ ContinuousOn arccos (uIcc 1 (-1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: case hff'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), HasDerivAt arccos (-(1 / √(1 - x ^ 2))) x

pp: case hf'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), -(1 / √(1 - x ^ 2)) ≤ 0

Tactic:
·

Goal state after:
case hff'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), HasDerivAt arccos (-(1 / √(1 - x ^ 2))) x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case h₁
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 := ⋯
⊢ Summable (((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm) ∘ Sum.inl)

pp: case h₂
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 := ⋯
⊢ Summable (((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm) ∘ Sum.inr)

Tactic:
·

Goal state after:
case h₁
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 := ⋯
⊢ Summable (((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm) ∘ Sum.inl)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: case hf'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), -(1 / √(1 - x ^ 2)) ≤ 0

Tactic:
·

Goal state after:
case hf'
f : ℝ → ℝ
⊢ ∀ x ∈ Ioo (min 1 (-1)) (max 1 (-1)), -(1 / √(1 - x ^ 2)) ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case inl
⊢ √(2 * π * ↑0) * (↑0 / rexp 1) ^ 0 ≤ ↑0!

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) * (↑n / rexp 1) ^ n ≤ ↑n !

Tactic:
·

Goal state after:
case inl
⊢ √(2 * π * ↑0) * (↑0 / rexp 1) ^ 0 ≤ ↑0!
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case h₂
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 := ⋯
⊢ Summable (((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm) ∘ Sum.inr)

Tactic:
·

Goal state after:
case h₂
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 := ⋯
⊢ Summable (((Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b) ∘ ⇑e.symm) ∘ Sum.inr)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, cos θ = ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ

pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ = 0

Tactic:
·

Goal state after:
n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ∫ (θ : ℝ) in 0..↑n * π, cos θ = ∫ (θ : ℝ) in 0..↑n * π, deriv sin θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

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

pp: n : ℤ
hn✝ : n ≠ 0
hn' : ↑n ≠ 0
hn : n < 0
⊢ ↑n * π ≤ 0

Tactic:
·

Goal state after:
n : ℤ
hn✝ : n ≠ 0
hn' : ↑n ≠ 0
hn : n < 0
⊢ -(sin 0 - sin (↑n * π)) = 0
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:
·

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

Goal state before:
pp: case inl
⊢ StrictAntiOn (fun x ↦ node 0 x) ↑(Finset.range (0 + 1))

pp: case inr
n : ℕ
hn : n ≠ 0
⊢ StrictAntiOn (fun x ↦ node n x) ↑(Finset.range (n + 1))

Tactic:
·

Goal state after:
case inl
⊢ StrictAntiOn (fun x ↦ node 0 x) ↑(Finset.range (0 + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: ⊢ ∫ (x : ℝ), eval x (T ℝ 0) * eval x (T ℝ 0) ∂measureT = π

Tactic:
simp_rw [← eval_mul, show (T ℝ 0) * (T ℝ 0) = T ℝ 0 by simp]

Goal state after:
⊢ ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT = π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case inr.refine_1
n : ℕ
hn : n ≠ 0
⊢ StrictMonoOn (fun x ↦ ↑x * π / ↑n) ↑(Finset.range (n + 1))

pp: case inr.refine_2
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ∈ ↑(Finset.range (n + 1))
⊢ ↑x * π / ↑n ≤ π

Tactic:
·

Goal state after:
case inr.refine_1
n : ℕ
hn : n ≠ 0
⊢ StrictMonoOn (fun x ↦ ↑x * π / ↑n) ↑(Finset.range (n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

pp: case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)

Tactic:
·

Goal state after:
case inl
i : ℕ
hi : i ≤ 0
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (0 + 1)).erase i, (node 0 i - node 0 j)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case e'_2
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) =
    (∑ i ∈ range n, Complex.exp (↑k / ↑n * ↑π * I) ^ i) * (Complex.exp (↑k / ↑n * ↑π * I) - 1)

pp: case e'_3
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (-1) ^ k - 1 = Complex.exp (↑k / ↑n * ↑π * I) ^ n - 1

Tactic:
·

Goal state after:
case e'_2
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) =
    (∑ i ∈ range n, Complex.exp (↑k / ↑n * ↑π * I) ^ i) * (Complex.exp (↑k / ↑n * ↑π * I) - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

Tactic:
·

Goal state after:
case e'_3
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
⊢ (-1) ^ k - 1 = Complex.exp (↑k / ↑n * ↑π * I) ^ n - 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

pp: case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ sumZeroes n (T ℝ k) = 0

Tactic:
·

Goal state after:
case inl
k : ℤ
hk : ¬2 * ↑0 ∣ k
⊢ sumZeroes 0 (T ℝ k) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case ha
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
⊢ 0 ≤ (-1) ^ i * c i

pp: case hbc
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

Tactic:
·

Goal state after:
case ha
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
⊢ 0 ≤ (-1) ^ i * c i
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

Tactic:
·

Goal state after:
case hbc
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
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: case inr.h
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)
hz₂ : Complex.exp (↑k / ↑n * ↑π * I) = z ^ 2
⊢ z / (z ^ 2 - 1) + z⁻¹ / (z⁻¹ ^ 2 - 1) = 0

Tactic:
field [show z ≠ 0 by grind [Complex.exp_ne_zero],
    show (z ^ 2 - 1 ≠ 0) ∧ (1 - z ^ 2 ≠ 0) by grind [exp_sub_one_ne_zero]]

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

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

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

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

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

Tactic:
·

Goal state after:
case convert_2
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ ∃ q, cos (θ - π / 2) = ↑q
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case degree_f_lt
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 : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ P.degree < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card

pp: case degree_g_lt
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 : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ (T ℝ ↑n).degree < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card

pp: case eval_fg
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 : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ ∀ x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1)), eval x P = eval x (T ℝ ↑n)

Tactic:
·

Goal state after:
case degree_f_lt
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 : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ P.degree < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card
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 ∈ range (2 * n), ∫ (a : ℝ), c i • eval a (↑(chebyshevTsequence ℝ) i) ∂measureT =
    ∑ i ∈ range (2 * n), sumZeroes n (c i • ↑(chebyshevTsequence ℝ) i)

pp: case hf
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
⊢ ∀ i ∈ range (2 * n), MeasureTheory.Integrable (fun x ↦ c i • eval x (↑(chebyshevTsequence ℝ) i)) measureT

Tactic:
·

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
⊢ ∑ i ∈ range (2 * n), ∫ (a : ℝ), c i • eval a (↑(chebyshevTsequence ℝ) i) ∂measureT =
    ∑ i ∈ range (2 * n), sumZeroes n (c i • ↑(chebyshevTsequence ℝ) i)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case degree_g_lt
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 : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ (T ℝ ↑n).degree < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card

pp: case eval_fg
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 : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ ∀ x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1)), eval x P = eval x (T ℝ ↑n)

Tactic:
·

Goal state after:
case degree_g_lt
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 : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ (T ℝ ↑n).degree < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card