mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: h_diff : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ Gamma s
h_diff' : ∀ {s : ℝ}, 0 < s → DifferentiableAt ℝ (fun s ↦ Gamma (2 * s)) s
⊢ DifferentiableAt ℝ Gamma (2 * (1 / 2))

Tactic:
by apply h_diff; simp

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -log ↑π / 2 / ↑√π * ↑π ^ (1 / 2) + ↑π ^ (-1 / 2) * (-↑√π * (↑γ + 2 * log 2) / 2) = -(↑γ + log (4 * ↑π)) / 2

Tactic:
aux,

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -log ↑π / 2 / ↑√π * ↑√π + ↑π ^ (-1 / 2) * (-↑√π * (↑γ + 2 * log 2) / 2) = -(↑γ + log (4 * ↑π)) / 2
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -log ↑π / 2 + (↑π ^ (1 / 2))⁻¹ * (-↑√π * (↑γ + 2 * log 2) / 2) = -(↑γ + log (4 * ↑π)) / 2

Tactic:
aux,

Goal state after:
f : ℂ → ℂ := fun s ↦ ↑π ^ (-s / 2)
g : ℂ → ℂ := fun s ↦ Gamma (s / 2)
aux : ↑π ^ (1 / 2) = ↑√π
aux2 : ↑√π ≠ 0
hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1
hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1
⊢ -log ↑π / 2 + (↑√π)⁻¹ * (-↑√π * (↑γ + 2 * log 2) / 2) = -(↑γ + log (4 * ↑π)) / 2
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : 1 ≤ r
⊢ -↑(Nat.log b ⌊r⁻¹⁻¹⌋₊) = -log b r

Tactic:
log_of_one_le_right _ hr,

Goal state after:
case inl.inl
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : 1 ≤ r
⊢ -↑(Nat.log b ⌊r⁻¹⁻¹⌋₊) = -↑(Nat.log b ⌊r⌋₊)
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case a
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
hb : 1 < b
hb1' : 1 < ↑b
⊢ Int.clog b r ≤ ⌈logb (↑b) r⌉

Tactic:
rw [← Int.le_zpow_iff_clog_le hb hr, ← rpow_intCast b]
      refine (rpow_logb (zero_lt_one.trans hb1') hb1'.ne' hr).symm.trans_le ?_
      exact rpow_le_rpow_of_exponent_le hb1'.le (Int.le_ceil _)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case neg.inr
b : ℕ
r : ℝ
hr✝ : 0 ≤ r
hr : 0 < r
h✝ : b = 1
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
· simp_all only [Nat.cast_one, logb_one_left, Int.ceil_zero, Int.clog_one_left]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.RegularityCompacts

Goal state before:
pp: case inr
α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : SecondCountableTopology α
inst✝² : IsCompletelyPseudoMetrizableSpace α
inst✝¹ : OpensMeasurableSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
ε : ℝ≥0∞
hε : 0 < ε
this : UpgradedIsCompletelyPseudoMetrizableSpace α := upgradeIsCompletelyPseudoMetrizable α
h✝ : Nonempty α
⊢ ∃ K, IsCompact (closure K) ∧ P Kᶜ < ε

Tactic:
case inr =>
    let seq := TopologicalSpace.denseSeq α
    have hseq_dense : DenseRange seq := TopologicalSpace.denseRange_denseSeq α
    obtain ⟨t : ℕ → SetRel α α,
        ht : ∀ i, t i ∈ 𝓤 α ∧ IsOpen (t i) ∧ (t i).IsSymm,
        h_basis : (uniformity α).HasAntitoneBasis t⟩ :=
      (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
    choose htu hto _ using ht
    let f : ℕ → ℕ → Set α := fun n m ↦ UniformSpace.ball (seq m) (t n)
    have h_univ n : (⋃ m, f n m) = univ := hseq_dense.iUnion_uniformity_ball (htu n)
    have h3 n (ε : ℝ≥0∞) (hε : 0 < ε) : ∃ m, P (⋂ m' ≤ m, (f n m')ᶜ) < ε := by
      refine exists_measure_iInter_lt (fun m ↦ ?_) hε ⟨0, measure_ne_top P _⟩ ?_
      · exact (measurable_prodMk_left (hto n).measurableSet).compl.nullMeasurableSet
      · rw [← compl_iUnion, h_univ, compl_univ]
    choose! s' s'bound using h3
    rcases ENNReal.exists_pos_sum_of_countable' (ne_of_gt hε) ℕ with ⟨δ, hδ1, hδ2⟩
    let u : ℕ → ℕ := fun n ↦ s' n (δ n)
    refine ⟨interUnionBalls seq u t, isCompact_closure_interUnionBalls h_basis.toHasBasis seq u, ?_⟩
    rw [interUnionBalls, Set.compl_iInter]
    refine ((measure_iUnion_le _).trans ?_).trans_lt hδ2
    refine ENNReal.tsum_le_tsum (fun n ↦ ?_)
    have h'' n : Prod.swap ⁻¹' t n = t n := by ext; exact (t n).comm
    simp only [h'', compl_iUnion, ge_iff_le]
    exact (s'bound n (δ n) (hδ1 n)).le

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
    ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))

Tactic:
← key,

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_nn : 0 ≤ᵐ[μ] f
f_mble : AEMeasurable f μ
p : ℝ
p_pos : 0 < p
one_lt_p : -1 < p - 1
g : ℝ → ℝ := fun t ↦ t ^ (p - 1)
obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p
g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t
g_intble : ∀ (t : ℝ), 0 < t → IntervalIntegrable g volume 0 t
key :
  ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)
⊢ ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0..f ω, g t) ∂μ
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ μ.toSphere univ = ↑(dim E) * μ (ball 0 1)

Tactic:
by
  nontriviality E
  rw [toSphere_apply_univ', measure_sdiff_null (measure_singleton _)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
⊢ IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) (Ioo 0 r) volume

Tactic:
have h_rpow : IntegrableOn (fun y ↦ y ^ ((Module.finrank ℝ E : ℝ) - 1 - α)) (Ioo 0 r) := by
      by_cases! hr : 0 < r
      · rw [intervalIntegral.integrableOn_Ioo_rpow_iff hr]
        linarith
      · simp [hr]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow : IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume
⊢ IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) * (C * y ^ (-α))) (Ioo 0 r) volume
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬ContinuousAt (fun z ↦ ℘[L] z) x

Tactic:
simp_rw [← L.weierstrassPExcept_add ⟨x, hx⟩]

Goal state after:
L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
⊢ ¬ContinuousAt (fun z ↦ ℘[L - x] z + (1 / (z - x) ^ 2 - 1 / x ^ 2)) x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ ℘'[L - 0] 0 = 0

Tactic:
by
  simpa [CharZero.eq_neg_self_iff] using L.derivWeierstrassPExcept_neg 0 0

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

Goal state before:
pp: x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ 0 < 1 - x ^ 2

Tactic:
by nlinarith [h₁, h₂]

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

Goal state before:
pp: x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Iic (- -x)) (- -x)
⊢ x ≠ 1

Tactic:
← image_neg_Ici

Goal state after:
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ x ≠ 1
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hab : a ≤ b
h : ContDiffOn ℝ 1 f (Icc a b)
⊢ ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Tactic:
exact integral_deriv_of_contDiffOn_Icc h hab

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
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 : ℝ) in Icc a b, deriv (⇑g ∘ f) x ∂volume‖ₑ ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ

Tactic:
apply (enorm_integral_le_lintegral_enorm _).trans

Goal state after:
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 := ⋯
this : ‖(⇑g ∘ f) b - (⇑g ∘ f) a‖ₑ = ‖f b - f a‖ₑ
⊢ ∫⁻ (a : ℝ) in Icc a b, ‖deriv (⇑g ∘ f) a‖ₑ ∂volume ≤ ∫⁻ (x : ℝ) in Icc a b, ‖deriv f x‖ₑ
Module: Mathlib.Analysis.SpecialFunctions.Stirling

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

Tactic:
set r := ((1 : ℝ) / (2 * (n + 1) + 1)) ^ 2 with hr

Goal state after:
case succ
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 1 + 1)) ≤ 1 / (12 * ↑(n + 1) * (↑(n + 1) + 1))
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κ : κ > 0
hκ' : Metric.ball 1 κ ⊆ (fun x_1 ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' (↑L.lattice \ {l₀}))))ᶜ
l : ↥L.lattice
hl : ↑l ≠ l₀
⊢ ‖z - x‖ * (κ / 2 + 1) < ‖↑l - x‖

Tactic:
have : ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l := by
      simpa using @hκ' (κ / 2 + 1) (by simp [div_lt_iff₀, abs_eq_self.mpr hκ.le, hκ])

Goal state after:
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : κ > 0
hκ' : Metric.ball 1 κ ⊆ (fun x_1 ↦ x_1 * ‖z - x‖) ⁻¹' (↑(upperClosure (dist x '' (↑L.lattice \ {l₀}))))ᶜ
l : ↥L.lattice
hl : ↑l ≠ l₀
this : ∀ l ∈ L.lattice, l ≠ l₀ → (κ / 2 + 1) * ‖z - x‖ < dist x l
⊢ ‖z - x‖ * (κ / 2 + 1) < ‖↑l - x‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

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

Tactic:
case neg hn =>
    rw [integral_symm, integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn]
    · simp
    exact mul_nonpos_of_nonpos_of_nonneg (Int.cast_nonpos.mpr <| le_of_lt hn) pi_nonneg

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

Goal state before:
pp: n m : ℤ
this :
  ∫ (x : ℝ), eval x (2 * T ℝ n * T ℝ m) ∂measureT =
    ∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2

Tactic:
by
    simp_rw [eval_mul, eval_ofNat, mul_assoc] at this
    rw [MeasureTheory.integral_const_mul] at this
    grind

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
  rcases eq_or_ne n 0 with rfl | hn
  · simp
  refine strictAntiOn_cos.comp_strictMonoOn ?_ (fun x hx => Set.mem_Icc.mpr ⟨by positivity, ?_⟩)
  · apply StrictMono.strictMonoOn
    exact StrictMono.mul_const
      (StrictMono.mul_const Nat.strictMono_cast (by positivity)) (by positivity)
  rw [Finset.mem_coe, Finset.mem_range_succ_iff] at hx
  rw [mul_div_assoc]
  nth_rewrite 2 [← mul_div_cancel₀ π (Nat.cast_ne_zero.mpr hn)]
  gcongr

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
⊢ ∫ (x : ℝ), eval x (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i)

Tactic:
simp_rw [eval_finsetSum, eval_smul]

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

Tactic:
sumNodes_T_eq

Goal state after:
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)
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) = sumNodes n (fun i ↦ leadingCoeffC n i) (T ℝ ↑n)

Tactic:
sumNodes_T_eq

Goal state after:
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)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

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

Tactic:
convert! sumNodes_eq_sumNodes_T_iff (fun i hi => negOnePow_mul_leadingCoeffC_pos hi) hPdeg hPbnd
  · rw [sumNodes_eq_coeff hPdeg]
  · rw [sumNodes_T_eq]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: ι : 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
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable fun n ↦ f n y
h : SummableLocallyUniformlyOn (fun n ↦ derivWithin (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
⊢ TendstoLocallyUniformlyOn (fun n a ↦ ∑ i ∈ n, derivWithin (fun z ↦ f i z) s a)
    (fun {x} ↦ ∑' (n : ι), derivWithin (f n) s x) (SummationFilter.unconditional ι).filter s

pp: ι : 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
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable fun n ↦ f n y
h : SummableLocallyUniformlyOn (fun n ↦ derivWithin (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
⊢ ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
    ∀ x ∈ s, HasDerivAt (fun y ↦ ∑ b ∈ n, (fun n ↦ f n y) b) (∑ i ∈ n, derivWithin (fun z ↦ f i z) s x) x

Tactic:
· obtain ⟨g, hg⟩ := h
    apply (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).congr_right
    exact fun _ hb ↦ (hg.tsum_eqOn hb).symm

Goal state after:
ι : 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
x : 𝕜
hx : x ∈ s
hf : ∀ y ∈ s, Summable fun n ↦ f n y
h : SummableLocallyUniformlyOn (fun n ↦ derivWithin (fun z ↦ f n z) s) s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r
⊢ ∀ᶠ (n : Finset ι) in (SummationFilter.unconditional ι).filter,
    ∀ x ∈ s, HasDerivAt (fun y ↦ ∑ b ∈ n, (fun n ↦ f n y) b) (∑ i ∈ n, derivWithin (fun z ↦ f i z) s x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
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_one_iff hn _).mpr ⟨k, le_of_lt hk₁, hk₂, rfl⟩]
    exact (abs_le.mp (abs_eval_T_real_le_one n (by grind))).2
  · 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: L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ L.relation (x - ↑l) = L.relation x

Tactic:
← L.relation_add_coe _ l,

Goal state after:
L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ L.relation (x - ↑l + ↑l) = L.relation x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
⊢ 2 * n / n.gcd (2 * k + 1) = 2 * (n / n.gcd (2 * k + 1))

Tactic:
Nat.mul_div_assoc _ (Nat.gcd_dvd_left ..)

Goal state after:
n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
hn : n ≠ 0
hnz : (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den ≤ 3
⊢ 2 * (n / n.gcd (2 * k + 1)) = 2 * (n / n.gcd (2 * k + 1))
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
hn : 0 ≤ n
⊢ fib n = ↑(Nat.fib n.toNat)

Tactic:
by simp [fib, hn]

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

Goal state before:
pp: case refine_2
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ ¬Complex.sin (↑π * x) = 0 ∧ ¬π = 0 ∧ ¬x = 0

Tactic:
exact ⟨sin_pi_mul_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩

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

Goal state before:
pp: n : ℤ
⊢ fib n = fib (n + 2) - fib (n + 1)

Tactic:
simp only [fib_add_two, add_sub_cancel_right]

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: case inr
n : ℕ
⊢ (if Even n then -↑(Nat.fib n) else ↑(Nat.fib n)) =
    ((if Even n then 1 else -1) * ψ ^ n - (if Even n then 1 else -1) * φ ^ n) / √5

Tactic:
grind [coe_fib_eq]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), f ↑i ≤ g x
hg : IntegrableOn g (Ico ↑a ↑b) volume
⊢ ∑ i ∈ Finset.Ico a b, f ↑i ≤ ∫ (x : ℝ) in ↑a..↑b, g x

Tactic:
by
  have A i (hi : i ∈ Finset.Ico a b) : IntervalIntegrable g volume i ↑(i + 1) := by
    rw [intervalIntegrable_iff_integrableOn_Ico_of_le (by simp)]
    simp only [Finset.mem_Ico, ← Nat.add_one_le_iff] at hi
    rify at hi
    exact hg.mono (by grind) le_rfl
  calc
  _ = ∑ i ∈ .Ico a b, (∫ x in (i : ℝ)..↑(i + 1), f i) := by simp
  _ ≤ ∑ i ∈ .Ico a b, (∫ x in (i : ℝ)..↑(i + 1), g x) := by
    gcongr with i hi
    apply integral_mono_on_of_le_Ioo (by simp) (by simp) (A _ hi) (fun x hx ↦ ?_)
    exact h _ (by simpa using hi) _ (Ioo_subset_Ico_self hx)
  _ = _ := by rw [sum_integral_adjacent_intervals_Ico (a := (↑·)) hab]; grind

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject (op G) := Subobject.mk (factorThruImage (h ≫ f)).op
q₁ : image (h ≫ f) ⟶ unop (Subobject.underlying.obj R) :=
  (Subobject.underlyingIso (factorThruImage (h ≫ f)).op).unop.hom
q₂ : unop (Subobject.underlying.obj R) ⟶ ∏ᶜ fun P ↦ unop (Subobject.underlying.obj P) :=
  section_ (Pi.π (fun P ↦ unop (Subobject.underlying.obj P)) R)
q : image (h ≫ f) ⟶ T := q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
⊢ factorThruImage (h ≫ f) ≫ q = 0

Tactic:
rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
      Category.assoc, hf, comp_zero]

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2)

Tactic:
rw [mul_div_assoc', mul_one, div_le_div_iff₀]

Goal state after:
case h
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 * (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * ↑⌊c ^ i⌋₊ ^ 2

case h.hb
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < ↑⌊c ^ i⌋₊ ^ 2

case h.hd
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
i : ℕ
a✝ : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < (c ^ i) ^ 2
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case min.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ CofilteredClosureSmall.abstractCofilteredClosureRealization f
      ⟨(max n m).succ, ⋯.mpr (CofilteredClosureSmall.InductiveStep.min ⋯ ⋯ x y)⟩ =
    {
        obj :=
          min (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
            (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩),
        property := ⋯ }.obj

Tactic:
simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]

Goal state after:
case min.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure f (max n m).succ).snd
      (⋯.mpr (CofilteredClosureSmall.InductiveStep.min ⋯ ⋯ x y)) =
    min ((CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).snd x)
      ((CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).snd y)