mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

Tactic:
[

Goal state after:
case inr
n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
⊢ ∑ i ∈ range n, 2 * Complex.cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π)) = 0
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
⊢ ∫ (x : ℝ), eval x (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i)

Tactic:
[

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
⊢ ∫ (x : ℝ), eval x (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i)
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)

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.ChebyshevGauss

Goal state before:
pp: case a
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
⊢ ∫ (a : ℝ), eval a (↑(chebyshevTsequence ℝ) i) ∂measureT = sumZeroes n (↑(chebyshevTsequence ℝ) i)

Tactic:
[

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

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

Goal state after:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ sumNodes n (leadingCoeffC n) P = P.coeff n
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) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i =
    ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i

Tactic:
[

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ ∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i =
    ∑' (i : ℕ), (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i
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.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ Summable fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i

Tactic:
[

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ Summable fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i
Module: Mathlib.Order.Interval.Finset.Box

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

Tactic:
[

Goal state after:
n : ℕ
x✝ : n + 1 ≠ 0
⊢ #(box (n + 1)) = 8 * (n + 1)
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:
[

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ sumNodes n (iterateDerivativeC n k x) P = eval x ((⇑derivative)^[k] P)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
i : ℕ
⊢ (L.weierstrassPSeries x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l

Tactic:
[

Goal state after:
L : PeriodPair
x : ℂ
i : ℕ
⊢ (L.weierstrassPSeries x).coeff i = ∑' (l : ↥L.lattice), L.weierstrassPSummand x i l
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ Summable (Function.uncurry fun b c ↦ L.weierstrassPSummand x b c * (z - x) ^ b)

Tactic:
[

Goal state after:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ Summable (Function.uncurry fun b c ↦ L.weierstrassPSummand x b c * (z - x) ^ b)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ HasSum (fun i ↦ (L.weierstrassPSeries x).coeff i * (z - x) ^ i) (℘[L] z)

Tactic:
[

Goal state after:
L : PeriodPair
z x : ℂ
hx : ∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖
⊢ HasSum (fun i ↦ (L.weierstrassPSeries x).coeff i * (z - x) ^ i) (℘[L] z)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L] (L.weierstrassPSeries x) x ↑r

Tactic:
[

Goal state after:
L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L] (L.weierstrassPSeries x) x ↑r
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ MeromorphicAt ℘[L] x

Tactic:
[

Goal state after:
case pos
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ MeromorphicAt ℘[L] x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ meromorphicOrderAt ℘[L] l₀ = ↑(-2)

Tactic:
meromorphicOrderAt_eq_int_iff (L.meromorphic_weierstrassP l₀)

Goal state after:
L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ ∃ g, AnalyticAt ℂ g l₀ ∧ g l₀ ≠ 0 ∧ ∀ᶠ (z : ℂ) in 𝓝[≠] l₀, ℘[L] z = (z - l₀) ^ (-2) • g z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case hΘ
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ (fun c ↦ ↑c * z) =Θ[cofinite] fun n ↦ ↑n

Tactic:
[

Goal state after:
case hΘ
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ (fun c ↦ ↑c * z) =Θ[cofinite] fun n ↦ ↑n
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: case succ
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable fun n ↦ f n t
m : ℕ
hm :
  ∀ {x : 𝕜},
    x ∈ s →
      (∀ (k : ℕ), 1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s) →
        (∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r) →
          iteratedDerivWithin m (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin m (f n) s x
x : 𝕜
hx : x ∈ s
h : ∀ (k : ℕ), 1 ≤ k → k ≤ m + 1 → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m + 1 → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r
⊢ iteratedDerivWithin (m + 1) (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin (m + 1) (f n) s x

Tactic:
[

Goal state after:
case succ
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hsum : ∀ t ∈ s, Summable fun n ↦ f n t
m : ℕ
hm :
  ∀ {x : 𝕜},
    x ∈ s →
      (∀ (k : ℕ), 1 ≤ k → k ≤ m → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s) →
        (∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r) →
          iteratedDerivWithin m (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin m (f n) s x
x : 𝕜
hx : x ∈ s
h : ∀ (k : ℕ), 1 ≤ k → k ≤ m + 1 → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι) (k : ℕ) (r : 𝕜), k ≤ m + 1 → r ∈ s → DifferentiableAt 𝕜 (iteratedDerivWithin k (fun z ↦ f n z) s) r
⊢ iteratedDerivWithin (m + 1) (fun z ↦ ∑' (n : ι), f n z) s x = ∑' (n : ι), iteratedDerivWithin (m + 1) (f n) s x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ iteratedDeriv 6
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0

Tactic:
[

Goal state after:
L : PeriodPair
⊢ iteratedDeriv 6
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
⊢ IsLocalMin (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
have k_pos : 0 < k := hk₂.pos
  have zero_lt : 0 < k * π / n := by positivity
  have lt_pi : k * π / n < π := calc
    k * π / n < n * π / n := by gcongr
    _ = π := mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr hn)
  refine eventually_nhds_iff.mpr ⟨Set.Ioo (-1) 1, ?_, isOpen_Ioo, ?_, ?_⟩
  · intro x hx
    dsimp
    rw [(eval_T_real_eq_neg_one_iff hn _).mpr ⟨k, le_of_lt hk₁, hk₂, rfl⟩]
    refine (abs_le.mp (abs_eval_T_real_le_one n (by grind))).1
  · rw [← cos_pi]
    exact cos_lt_cos_of_nonneg_of_le_pi (le_of_lt zero_lt) (le_refl π) lt_pi
  · rw [← cos_zero]
    exact cos_lt_cos_of_nonneg_of_le_pi (le_refl 0) (le_of_lt lt_pi) zero_lt

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

Goal state before:
pp: case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ iteratedDeriv i
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0

Tactic:
[

Goal state after:
case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
hi₄ : ¬i = 6
⊢ iteratedDeriv i
      (fun z ↦
        (℘'[L - 0] z * z ^ 3 - 2) ^ 2 - 4 * (℘[L - 0] z * z ^ 2 + 1) ^ 3 + L.g₂ * (℘[L - 0] z * z ^ 6 + z ^ 4) +
          L.g₃ * z ^ 6)
      0 =
    0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_2
Z : Set ℂ
hZ : IsCompact Z
s : ℝ
hf : ContinuousOn (fun x ↦ ‖x‖ ^ 2) Z
hs : ∀ a ∈ Z, ‖a‖ ^ 2 ≤ s
⊢ ∀ (j : ℕ), ∀ z ∈ Z, ‖z‖ ^ 2 / ‖↑j + 1‖ ^ 2 ≤ |s| / ‖↑j + 1‖ ^ 2

Tactic:
intro n x hx

Goal state after:
case refine_2
Z : Set ℂ
hZ : IsCompact Z
s : ℝ
hf : ContinuousOn (fun x ↦ ‖x‖ ^ 2) Z
hs : ∀ a ∈ Z, ‖a‖ ^ 2 ≤ s
n : ℕ
x : ℂ
hx : x ∈ Z
⊢ ‖x‖ ^ 2 / ‖↑n + 1‖ ^ 2 ≤ |s| / ‖↑n + 1‖ ^ 2
Module: Mathlib.Tactic.NormNum.NatFib

Goal state before:
pp: n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ fib n' = a'

Tactic:
by rw [← hn, fib_two_mul, H.1, H.2, ← h1]

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℕ
hn0 : n = 0
⊢ fib (-↑n + 1) = (-1) ^ (n + 1) * ↑(Nat.fib n) + (-1) ^ (1 + (n + 1)) * ↑(Nat.fib (n + 1))

Tactic:
simp [hn0]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
k : ℕ∞
hx : x ∈ ℂ_ℤ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ (↑π * x).cot) ℍₒ x

Tactic:
[

Goal state after:
x : ℂ
k : ℕ∞
hx : x ∈ ℂ_ℤ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ (↑π * x).cot) ℍₒ x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
y : ℝ
⊢ ∑ p ∈ f.support, f p • eval y p = ∑ i ∈ f.support, eval y (f i • i)

Tactic:
[

Goal state after:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
y : ℝ
⊢ ∑ p ∈ f.support, f p • eval y p = ∑ i ∈ f.support, eval y (f i • i)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∑ i ∈ Finset.range n, logDeriv (fun z ↦ 1 + sineTerm z i) x = ∑ j ∈ Finset.range n, cotTerm x j

Tactic:
[

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ∑ i ∈ Finset.range n, logDeriv (fun z ↦ 1 + sineTerm z i) x = ∑ j ∈ Finset.range n, cotTerm x j
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Tendsto (fun n ↦ ∑ j ∈ Finset.range n, cotTerm x j) atTop (𝓝 (↑π * (↑π * x).cot - 1 / x))

Tactic:
[

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Tendsto (fun n ↦ ∑ j ∈ Finset.range n, cotTerm x j) atTop (𝓝 (↑π * (↑π * x).cot - 1 / x))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun a ↦ cotTermUpperBound k A B hB a

Tactic:
[

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
⊢ Summable fun a ↦ cotTermUpperBound k A B hB a
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ ψ * φ = -1

Tactic:
by
  rw [mul_comm]
  exact goldenRatio_mul_goldenConj

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
K : Set ℍ
hKc : IsCompact (UpperHalfPlane.coe '' K)
⊢ ∃ u,
    Summable u ∧ ∀ (n : ℕ), ∀ k_1 ∈ UpperHalfPlane.coe '' K, ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ k_1‖ ≤ u n

Tactic:
obtain ⟨A, B, hB, HABK⟩ := subset_verticalStrip_of_isCompact
    (isEmbedding_coe.isCompact_iff.mpr hKc)

Goal state after:
k : ℕ
hk : 1 ≤ k
K : Set ℍ
hKc : IsCompact (UpperHalfPlane.coe '' K)
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
⊢ ∃ u,
    Summable u ∧ ∀ (n : ℕ), ∀ k_1 ∈ UpperHalfPlane.coe '' K, ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ k_1‖ ≤ u n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot - 1 / x) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)

Tactic:
[

Goal state after:
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot - 1 / x) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, x ^ (↑k + 1 - 1) * rexp (-(c * x)) = ↑k ! / c ^ (k + 1)

Tactic:
[

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, x ^ (↑k + 1 - 1) * rexp (-(c * x)) = ↑k ! / c ^ (k + 1)
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
⊢ e ∈ S ↔ ∀ y ∈ S.commutant, (↑e).range ∈ Module.End.invtSubmodule ↑y

Tactic:
[

Goal state after:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
e : H →L[ℂ] H
he : IsStarProjection e
S : VonNeumannAlgebra H
⊢ e ∈ S ↔ ∀ y ∈ S.commutant, (↑e).range ∈ Module.End.invtSubmodule ↑y
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i ∈ Finset.Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x

Tactic:
[

Goal state after:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i ∈ Finset.Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i ∈ Finset.Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x

Tactic:
simp_rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range, add_assoc]

Goal state after:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.range (b - a), f ↑(a + (x + 1)) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ d < u n / ↑n

Tactic:
[

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : ↑n * l - u n ≤ ε * (1 + l) * ↑n
npos : n ∈ Set.Ioi 0
⊢ d < u n / ↑n
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (ConcreteCategory.hom ((colimit.ι F i).app (Opposite.op A.left))) y
y' : CostructuredArrow yoneda (F.obj i) := CostructuredArrow.mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ (CostructuredArrow.map (colimit.ι F i)).obj (j i y') ∈ ⋃ i, (CostructuredArrow.map (colimit.ι F i)).obj '' s i

Tactic:
simp only [Set.mem_iUnion, Set.mem_image]
    exact ⟨i, j i y', hjs _ _, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (ConcreteCategory.hom ((colimit.ι F i).app (Opposite.op A.left))) y
y' : CostructuredArrow yoneda (F.obj i) := CostructuredArrow.mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ A ⟶ (CostructuredArrow.map (colimit.ι F i)).obj (j i y')

Tactic:
refine ?_ ≫ (map (colimit.ι F i)).map x

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} ↑(s i)
j : (i : I) → CostructuredArrow yoneda (F.obj i) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy : yonedaEquiv A.hom = (ConcreteCategory.hom ((colimit.ι F i).app (Opposite.op A.left))) y
y' : CostructuredArrow yoneda (F.obj i) := CostructuredArrow.mk (yonedaEquiv.symm y)
x : y' ⟶ j i y'
⊢ A ⟶ (CostructuredArrow.map (colimit.ι F i)).obj y'