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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
η : ℝ
hη : η > 0
hη_sub : ball 0 η ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
M : ℝ := max a b
hM_def : M = max a b
hM : 0 < M
t : ℝ
ht_pos : 0 < t
ht_bound : t ∈ Iio (η / M)
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
hx_pos : 0 < x
⊢ max (a * t) (b * t) = max a b * t

Tactic:
max_mul_of_nonneg _ _ ht_pos.le

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
η : ℝ
hη : η > 0
hη_sub : ball 0 η ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
M : ℝ := max a b
hM_def : M = max a b
hM : 0 < M
t : ℝ
ht_pos : 0 < t
ht_bound : t ∈ Iio (η / M)
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
hx_pos : 0 < x
⊢ max (a * t) (b * t) = max (a * t) (b * t)
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
⊢ ∀ δ > 0, ∀ᶠ (t : ℝ) in atTop, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - R‖ ≤ δ

Tactic:
intro δ

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
⊢ δ > 0 → ∀ᶠ (t : ℝ) in atTop, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - R‖ ≤ δ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

Tactic:
by_cases hx_zero : x = 0
  case pos =>
    simp only [rpowIntegrand₀₁, hx_zero, add_zero, sub_self, mul_zero]
    positivity
  case neg =>
    calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
    _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
    _ = t ^ (p - 1) * (x / x) := by ring
    _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
    _ = _ := by simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case hbc
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 1 / 2 * (1 / t) ≤ 1 / (t + 1)

Tactic:
one_div_mul_one_div,

Goal state after:
case hbc
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 1 / (2 * t) ≤ 1 / (t + 1)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s ↦ s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)

Tactic:
have h' : Tendsto (fun s : ℂ ↦ 2 * (π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2) := by
    rw [(by simp : 𝓝 2 = 𝓝 (2 * (π : ℂ) ^ (-(0 : ℂ) / 2)))]
    refine Tendsto.mono_left (ContinuousAt.tendsto ?_) nhdsWithin_le_nhds
    exact continuousAt_const.mul ((continuousAt_const_cpow (ofReal_ne_zero.mpr pi_ne_zero)).comp
      (by fun_prop))

Goal state after:
h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
h' : Tendsto (fun s ↦ 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)
⊢ Tendsto (fun s ↦ s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ rexp (107 / 60) < 6

Tactic:
refine lt_trans this ?_

Goal state after:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)
⊢ 2.7182818286 ^ (107 / 60) < 6
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s / (cos (↑π * s / 2))⁻¹ = s.Gammaℂ * cos (↑π * s / 2)

Tactic:
rw [Gammaℂ_def, div_eq_mul_inv, inv_inv]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = 1 / ↑π * sin (↑π / 2) * (↑π ^ (-1) * 1)⁻¹

Tactic:
Complex.sin_pi_div_two,

Goal state after:
case pos
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 1⁻¹ = 1 / ↑π * 1 * (↑π ^ (-1) * 1)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
⊢ y ∈ Ici (rexp 1) → x ≤ y → (fun x ↦ log x / x) y ≤ (fun x ↦ log x / x) x

Tactic:
hey

Goal state after:
x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
⊢ x ≤ y → (fun x ↦ log x / x) y ≤ (fun x ↦ log x / x) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case inl
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
hb₁ : b < 1
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_logb_nhdsNE_zero_of_base_lt_one hb₀ hb₁)
        _ (h.tendsto.mono_left inf_le_left)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: case h0
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
i : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ∈ (Finset.range (n + 1)).erase i
⊢ 0 ≤ a - ↑j

Tactic:
rw [Finset.mem_erase, Finset.mem_range] at hj

Goal state after:
case h0
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
a : ℝ
ha : ↑n < a
b : ℝ
hb : ↑n < b
hab : a ≤ b
i : ℕ
hi : i ∈ Finset.range (n + 1)
j : ℕ
hj : j ≠ i ∧ j < n + 1
⊢ 0 ≤ a - ↑j
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
hs : ‖↑l‖ < r
⊢ False

Tactic:
exfalso

Goal state after:
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
hs : ‖↑l‖ < r
⊢ False
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : StandardBorelSpace α
inst✝ : Finite α
⊢ ∃ n, Nonempty (α ≃ᵐ ↑(range fun x ↦ ↑↑x))

Tactic:
obtain ⟨n, ⟨n_equiv⟩⟩ := Finite.exists_equiv_fin α
  refine ⟨n, ⟨PolishSpace.Equiv.measurableEquiv (n_equiv.trans ?_)⟩⟩
  exact Equiv.ofInjective _ (Nat.cast_injective.comp Fin.val_injective)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ μ.toSphere.real univ • ∫ (x : ↑(Ioi 0)), f ↑x ∂Measure.volumeIoiPow (dim E - 1) =
    dim E • μ.real (ball 0 1) • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

Tactic:
simp only [Measure.volumeIoiPow, ENNReal.ofReal]
      rw [integral_withDensity_eq_integral_smul, μ.toSphere_real_apply_univ,
        ← nsmul_eq_mul, smul_assoc,
        integral_subtype_comap measurableSet_Ioi fun a ↦ Real.toNNReal (a ^ (dim E - 1)) • f a,
        setIntegral_congr_fun measurableSet_Ioi fun x hx ↦ ?_]
      · rw [NNReal.smul_def, Real.coe_toNNReal _ (pow_nonneg hx.out.le _)]
      · exact (measurable_subtype_coe.pow_const _).real_toNNReal

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1))
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹

Tactic:
grw [hf]

Goal state after:
n : ℕ
f : ℕ → ℝ := fun k ↦ log (stirlingSeq (k + 1))
g : ℕ → ℝ := fun k ↦ 1 / (12 * (↑k + 1))
hf : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1))
⊢ 1 / (12 * (↑0 + 1)) - 1 / (12 * (↑n + 1)) ≤ 12⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

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

Tactic:
simp [sumZeroes, show π / n * n = π by field]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: k : ℝ
hk : 2 < k
⊢ ∀ᶠ (i : ℕ) in atTop, ‖↑(#(box i)) * ↑i ^ (-k)‖ ≤ 8 * ↑i ^ (1 - k)

Tactic:
filter_upwards [Filter.eventually_gt_atTop 0] with n hn

Goal state after:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ ‖↑(#(box n)) * ↑n ^ (-k)‖ ≤ 8 * ↑n ^ (1 - k)
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ SummableLocallyUniformlyOn f s

Tactic:
apply SummableLocallyUniformlyOn.of_locally_bounded_eventually hs
  intro K hK hKc
  obtain ⟨u, hu1, hu2⟩ := hu K hK hKc
  exact ⟨u, hu1, by filter_upwards using hu2⟩

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

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

Tactic:
cases k.even_or_odd

Goal state after:
case inl
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
h✝ : Even k
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

case inr
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
h✝ : Odd k
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: case pos
ι : 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
r : 𝕜
hr : r ∈ s
hm2 : m = 0
⊢ Summable fun n ↦ iteratedDerivWithin m (fun z ↦ f n z) s r

pp: case neg
ι : 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
r : 𝕜
hr : r ∈ s
hm2 : ¬m = 0
⊢ Summable fun n ↦ iteratedDerivWithin m (fun z ↦ f n z) s r

Tactic:
· simp [hm2, hsum r hr]

Goal state after:
case neg
ι : 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
r : 𝕜
hr : r ∈ s
hm2 : ¬m = 0
⊢ Summable fun n ↦ iteratedDerivWithin m (fun z ↦ f n z) s r
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk : k ≤ n
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) (cos (↑k * π / ↑n))

Tactic:
cases k.even_or_odd

Goal state after:
case inl
n k : ℕ
hn : n ≠ 0
hk : k ≤ n
h✝ : Even k
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) (cos (↑k * π / ↑n))

case inr
n k : ℕ
hn : n ≠ 0
hk : k ≤ n
h✝ : Odd k
⊢ IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) (cos (↑k * π / ↑n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp.refine_2
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMaxOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ ↑n)|

Tactic:
refine le_abs.mpr (.inl ?_)
      have := isMaxOn_iff.mp h (cos (0 * π / n)) (by simp)
      rw [(eval_T_real_eq_one_iff hn _).mpr ⟨0, by simp, by simp⟩] at this
      assumption

Goal state after:
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:
Polynomial.eval_smul

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in ↑0..↑M, x ^ k * rexp (-(c * (x - 1))) ≤ ↑k ! / c ^ (k + 1) * rexp c

Tactic:
simp only [mul_sub, mul_one, neg_sub, CharP.cast_eq_zero]
    simp only [sub_eq_add_neg, Real.exp_add, mul_comm (rexp c), ← mul_assoc]
    rw [intervalIntegral.integral_mul_const]
    gcongr
    exact intervalIntegral_pow_mul_exp_neg_le (by simp) hc

Goal state after:
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
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
cNn : c (N - 1) ≤ n
A : a ≤ N - 1
B : N - 1 + 1 = N
this : ↑(c (N - 1 + 1)) ≤ (1 + ε) * ↑(c (N - 1))
⊢ ↑(c N) ≤ (1 + ε) * ↑(c (N - 1))

Tactic:
rwa [B] at this

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
⊢ Integrable (fun x ↦ f x * g (x - 1)) (volume.restrict (Icc ↑a ↑b))

Tactic:
apply (hf.integrableOn_isCompact isCompact_Icc).mul_of_top_left

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
⊢ MemLp (fun x ↦ g (x - 1)) ⊤ (volume.restrict (Icc ↑a ↑b))
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
⊢ ∃ G, Injective G ∧ IsCoseparator G

Tactic:
let T : C := Injective.under (piObj fun P : Subobject (op G) => unop P)

Goal state after:
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))
⊢ ∃ G, Injective G ∧ IsCoseparator G
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
⊢ Tendsto (fun ε ↦ d + ε * (1 + l)) (𝓝 0) (𝓝 (d + 0 * (1 + l)))

Tactic:
exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ Integrable (fun x ↦ f x * g (x - 1)) (volume.restrict (Icc ↑a ↑b))

Tactic:
apply (hf.integrableOn_isCompact isCompact_Icc).mul_of_top_left

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ MemLp (fun x ↦ g (x - 1)) ⊤ (volume.restrict (Icc ↑a ↑b))
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:

Tactic:
d < (n : ℝ)⁻¹ * n * (l - ε * (1 + l)) := by
        rw [inv_mul_cancel₀, one_mul]
        · linarith only [hε]
        · exact Nat.cast_ne_zero.2 (ne_of_gt npos)
      _ = (n : ℝ)⁻¹ * (n * l - ε * (1 + l) * n) := by ring
      _ ≤ (n : ℝ)⁻¹ * u n := by gcongr; linarith only [hn]

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

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ ∑ i ∈ range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2

Tactic:
calc
    (∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (c ^ i) ^ 2) ≤
        ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (1 : ℝ) / (c ^ i) ^ 2 := by
      gcongr
      intro i hi
      simp only [mem_filter, mem_range] at hi
      simp only [hi.1, mem_Ico, and_true]
      apply Nat.floor_le_of_le
      apply le_of_lt
      rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow]
      exact Real.log_lt_log hj hi.2
    _ = ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i := by
      simp [← pow_mul, mul_comm]
    _ ≤ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ / ((1 : ℝ) - c⁻¹ ^ 2) :=
      geom_sum_Ico_le_of_lt_one (sq_nonneg _) C
    _ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / ((1 : ℝ) - c⁻¹ ^ 2) := by
      gcongr
      rw [← Real.rpow_natCast]
      exact Real.rpow_le_rpow_of_exponent_ge A C.le (Nat.sub_one_lt_floor _).le
    _ = c ^ 2 * ((1 : ℝ) - c⁻¹ ^ 2)⁻¹ / j ^ 2 := by
      have I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = (1 : ℝ) / j ^ 2 := by
        apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
        · rw [Set.mem_Ioi]; positivity
        rw [Real.log_rpow A]
        simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]
        field [(Real.log_pos hc).ne']
      rw [Real.rpow_sub A, I]
      simp
      ring
    _ ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2 := by gcongr

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
L : C ⥤ T
R : D ⥤ T
C' : Type u₄
inst✝³ : Category.{v₄, u₄} C'
D' : Type u₅
inst✝² : Category.{v₅, u₅} D'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L' : C' ⥤ T'
R' : D' ⥤ T'
F₁ : C ⥤ C'
F₂ : D ⥤ D'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝ : IsIso β
X : Comma L' R'
Y : StructuredArrow X (Comma.map α β)
⊢ ((map₂ (𝟙 (L'.obj X.left)) α).obj (mk Y.hom.left)).hom ≫ F.map Y.right.hom =
    ((map₂ X.hom (inv β)).obj (mk Y.hom.right)).hom

Tactic:
simpa only [Functor.const_obj_obj, map₂_obj_left, mk_left, map₂_obj_right, mk_right,
        map₂_obj_hom, mk_hom_eq_self, Category.id_comp, Category.assoc, NatIso.isIso_inv_app,
        Functor.comp_obj, Comma.map_obj_right, Comma.map_obj_left, Comma.map_obj_hom,
        IsIso.hom_inv_id, Category.comp_id] using
        congrFun (congrArg CategoryStruct.comp Y.hom.w) (inv (β.app Y.right.right) :)

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
L : C ⥤ T
R : D ⥤ T
C' : Type u₄
inst✝³ : Category.{v₄, u₄} C'
D' : Type u₅
inst✝² : Category.{v₅, u₅} D'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L' : C' ⥤ T'
R' : D' ⥤ T'
F₁ : C ⥤ C'
F₂ : D ⥤ D'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝ : IsIso β
X : Comma L' R'
Y Z : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
f : Y ⟶ Z
⊢ L.map (Hom.right f.left) ≫ (mk { left := Z.left.hom, right := Z.right.hom, w := ⋯ }).right.hom =
    (mk { left := Y.left.hom, right := Y.right.hom, w := ⋯ }).right.hom ≫ R.map (Hom.right f.right)

Tactic:
exact congrArg CommaMorphism.right f.w

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
ι✝ : Type u_2
inst✝⁵ : HasProductsOfShape ι✝ C
inst✝⁴ : HasProducts C
inst✝³ : HasFilteredColimitsOfSize.{w, w, v_1, u_1} C
inst✝² : IsIPC C
ι : Type u_3
inst✝¹ : Small.{w, u_3} ι
inst✝ : HasProductsOfShape ι C
⊢ IsIPCOfShape.{w, u_3, v_1, u_1} ι C

Tactic:
suffices IsIPCOfShape (Shrink.{w} ι) C from .of_equiv (equivShrink ι).symm
  apply IsIPC.isIPCOfShape

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this : PreservesFiniteColimits (F C)
⊢ PreservesFiniteColimits (F C ⋙ G C ⋙ H C)

Tactic:
have : PreservesFiniteColimits (G C) := by rw [G]; apply preservesFiniteColimits_rightOp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
this✝ : PreservesFiniteColimits (F C)
this : PreservesFiniteColimits (G C)
⊢ PreservesFiniteColimits (F C ⋙ G C ⋙ H C)
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ (J.ι ≫ desc f I J).f 0 = ((CochainComplex.single₀ C).map f ≫ I.ι).f 0

Tactic:
simp [desc, descFOne, descFZero]

Goal state after: