mathlib-initiative/mathlib-tactics huggingface dataset:
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₀₁ (x * t) x = p.rpowIntegrand₀₁ t 1 * x ^ (p - 1)

Tactic:
by
  have hxt : 0 ≤ x * t := by positivity
  rw [rpowIntegrand₀₁_eq_pow_div hp hxt hx, rpowIntegrand₀₁_eq_pow_div hp ht zero_le_one]
  by_cases hx_zero : x = 0
  case neg =>
    calc _ = x ^ (p - 1) * (t ^ (p - 1) * (x / (x * t + x))) := by
              rw [← mul_assoc, mul_div_assoc, Real.mul_rpow hx ht]
      _ = x ^ (p - 1) * (t ^ (p - 1) * 1 / (t + 1)) := by
              have : x * t + x = x * (t + 1) := by ring
              rw [mul_div_assoc, this, div_mul_eq_div_mul_one_div, div_self hx_zero, one_mul]
      _ = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) := by rw [mul_comm]
  case pos =>
    rw [mem_Ioo] at hp
    simp [hx_zero, Real.zero_rpow (by linarith : p - 1 ≠ 0)]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
δ : ℝ
hδ_pos : δ > 0
x : ℝ
hδ : x ∈ {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g x y volume) (log (b / a) • (L - R)) < ε / 2}
hx : x ∈ Ioi 0
hdist : dist x 0 < δ
⊢ dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
rw [mem_ofPred] at hδ

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
δ : ℝ
hδ_pos : δ > 0
x : ℝ
hδ : ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g x y volume) (log (b / a) • (L - R)) < ε / 2
hx : x ∈ Ioi 0
hdist : dist x 0 < δ
⊢ dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ (s + 1).Gammaℝ ≠ 0

Tactic:
simpa only [Ne, Gammaℝ_eq_zero_iff, not_exists, ← eq_sub_iff_add_eq,
      sub_eq_add_neg, ← neg_add]

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

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

Tactic:
mul_div_cancel_right₀ _ this

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ / (1 - s).Gammaℝ
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: case refine_1
⊢ BddAbove (Set.range eulerMascheroniSeq)

Tactic:
· exact ⟨_, fun _ ⟨_, hn⟩ ↦ hn ▸ (eulerMascheroniSeq_lt_eulerMascheroniSeq' _ 1).le⟩

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

Goal state before:
pp: case a
n : ℕ
f : ℝ → ℝ := ⋯
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
⊢ -deriv f 1 ≤ γ

pp: case a
n : ℕ
f : ℝ → ℝ := ⋯
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
⊢ γ ≤ -deriv f 1

Tactic:
· apply ge_of_tendsto tendsto_harmonic_sub_log
    filter_upwards [eventually_gt_atTop 0] with n hn
    rw [le_sub_iff_add_le', ← sub_eq_add_neg, sub_le_iff_le_add', ← hder_nat]
    exact derivLB n hn

Goal state after:
case a
n : ℕ
f : ℝ → ℝ := ⋯
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
hder_nat : ∀ (n : ℕ), deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
derivLB : ∀ (n : ℕ), 0 < n → log ↑n ≤ deriv f (↑n + 1)
derivUB : ∀ (n : ℕ), deriv f (↑n + 1) ≤ log (↑n + 1)
⊢ γ ≤ -deriv f 1
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₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
h₀' : 0 < r₂
⊢ -↑(Nat.clog b ⌈r₁⁻¹⌉₊) ≤ log b r₂

Tactic:
log_of_right_le_one _ h₂,

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₂ : R
h₀ : 0 < r₁
h : r₁ ≤ r₂
h₁ : r₁ ≤ 1
h₂ : r₂ ≤ 1
h₀' : 0 < r₂
⊢ -↑(Nat.clog b ⌈r₁⁻¹⌉₊) ≤ -↑(Nat.clog b ⌈r₂⁻¹⌉₊)
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ < b ∨ b ≤ 1

Tactic:
refine Or.inl (lt_of_le_of_lt ?_ hb)

Goal state after:
case inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
hb : 1 < b
⊢ ⌊r⁻¹⌋₊ ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ 0 ≤ logb b x ↔ 1 ≤ x

Tactic:
← not_lt,

Goal state after:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ ¬logb b x < 0 ↔ 1 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ logb b x ≤ 0 ↔ x ≤ 1

Tactic:
← not_lt,

Goal state after:
b x : ℝ
hb : 1 < b
hx : 0 < x
⊢ ¬0 < logb b x ↔ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ (fun x ↦ log x / x) y ≤ (fun x ↦ log x / x) x

Tactic:
have hlogx : 1 ≤ log x := by rwa [le_log_iff_exp_le x_pos]

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

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ 0 ≤ logb b x ↔ x ≤ 1

Tactic:
← not_lt,

Goal state after:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ ¬logb b x < 0 ↔ x ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ 0 ↔ 1 ≤ x

Tactic:
← not_lt,

Goal state after:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ ¬0 < logb b x ↔ 1 ≤ x
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
⊢ Tendsto (fun n ↦ ∫ (x : E), (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x ∂P) atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq (g x) ∂P))

Tactic:
apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
  · apply Eventually.of_forall
    exact fun n => StronglyMeasurable.aestronglyMeasurable (Continuous.stronglyMeasurable
        (Continuous.mul g.continuous ((1 + ((n : ℝ)⁻¹ • -(ε • g * g))) ^ n).continuous))
  · obtain ⟨N, hgN⟩ := exists_nat_gt (ε * (norm g * norm g))
    use norm g
    rw [eventually_atTop]
    use N
    intro n hn
    have hnpos : 0 < (n : ℝ) := by
      apply lt_of_lt_of_le (lt_of_le_of_lt _ hgN) (Nat.cast_le.mpr hn)
      exact (mul_nonneg (le_of_lt hε) (mul_self_nonneg (norm g)))
    apply Eventually.of_forall
    intro x
    simp only [smul_neg, BoundedContinuousFunction.coe_mul, Pi.mul_apply, pow_apply,
      BoundedContinuousFunction.coe_add, BoundedContinuousFunction.coe_one, coe_neg,
      BoundedContinuousFunction.coe_smul, smul_eq_mul, Pi.add_apply, Pi.one_apply, Pi.neg_apply,
      norm_mul, norm_eq_abs, norm_pow]
    refine (mul_le_mul_of_nonneg_right (norm_coe_le_norm g x) (pow_nonneg (abs_nonneg _) n)).trans
      <| mul_le_of_le_one_right (norm_nonneg _) ?_
    apply pow_le_one₀ (abs_nonneg _)
    rw [mul_assoc, inv_mul_eq_div, abs_le]
    refine ⟨?_, (add_le_iff_nonpos_right 1).mpr (Left.neg_nonpos_iff.mpr
      (div_nonneg (mul_nonneg (le_of_lt hε) (mul_self_nonneg (g x))) (le_of_lt hnpos)))⟩
    apply le_trans (by linarith) (sub_nonneg_of_le ((div_le_one hnpos).mpr _))
    apply le_trans (le_trans _ (le_of_lt hgN)) (Nat.cast_le.mpr hn)
    apply mul_le_mul (le_refl ε) _ (mul_self_nonneg (g x)) (le_of_lt hε)
    rw [← abs_le_iff_mul_self_le, abs_norm]
    exact norm_coe_le_norm g x
  · apply Eventually.of_forall
    intro x
    apply Tendsto.const_mul (g x)
    simpa [mul_assoc, inv_mul_eq_div, ← neg_div] using
      tendsto_one_add_div_pow_exp (-(ε * (g x * g x)))

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
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
n k : ℕ
⊢ (volumeIoiPow n) (Iio ⟨↑k + 1, ⋯⟩) < ∞

Tactic:
by simp [volumeIoiPow_apply_Iio]

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

Goal state before:
pp: n a b : ℕ
hb : b ≠ 0
⊢ (↑n + 1) * ↑a * ↑b ^ n ≤ ↑a ^ (n + 1) + ↑n * ↑b * ↑b ^ n

Tactic:
have h := pow_add_mul_le_add_pow_of_sq_nonneg (a := (b : ℤ)) (b := (a : ℤ) - b)
    (ha := by positivity) (Hsq := by positivity) (Hsq' := by positivity) (H := by omega)
    (n := n + 1)

Goal state after:
n a b : ℕ
hb : b ≠ 0
h : ↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b) ≤ (↑b + (↑a - ↑b)) ^ (n + 1)
⊢ (↑n + 1) * ↑a * ↑b ^ n ≤ ↑a ^ (n + 1) + ↑n * ↑b * ↑b ^ n
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case pos
a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 0
hb : ∀ k ∈ b, k ≠ -↑n
⊢ regularizedHGFunCoeff a b (n + 1) / regularizedHGFunCoeff a b n =
    (Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))

Tactic:
rw [regularizedHGFunCoeff_add_one hb]
    field_simp

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

Goal state before:
pp: case neg
a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 0
j : ℂ
hj : j ∈ b ∧ j = -↑n
h₁ : (Multiset.map (fun x ↦ x + ↑n) b).prod = 0
⊢ regularizedHGFunCoeff a b (n + 1) / regularizedHGFunCoeff a b n =
    (Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))

Tactic:
simp [regularizedHGFunCoeff_eq_zero_right a b n 0, h₁]

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

Goal state before:
pp: a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
h₁ : Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)
this :
  Tendsto
    (fun x ↦
      ‖↑x ^ (↑a.card - ↑b.card - 1) *
          ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) a).prod /
            ((Multiset.map (fun x_1 ↦ x_1 / ↑x + 1) b).prod * (1 + (↑x)⁻¹)))‖)
    atTop (𝓝 0)
h_ne : ∀ᶠ (n : ℕ) in atTop, regularizedHGFunCoeff a b n ≠ 0
n : ℕ
hn₁ : regularizedHGFunCoeff a b n ≠ 0
hn₂ : n ≠ 0
⊢ ‖↑n ^ (↑a.card - ↑b.card - 1) *
        ((Multiset.map (fun x ↦ x / ↑n + 1) a).prod / ((Multiset.map (fun x ↦ x / ↑n + 1) b).prod * (1 + (↑n)⁻¹)))‖ =
    ‖regularizedHGFunCoeff a b (n + 1)‖ / ‖regularizedHGFunCoeff a b n‖

Tactic:
rw [← Complex.norm_div, regularizedHGFunCoeff_add_one_div_self hn₁,
      multiset_prod_div_multiset_prod_mul a b hn₂, mul_div]

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

Goal state before:
pp: case refine_2
L : PeriodPair
l₀ : ℂ
⊢ TendstoLocallyUniformlyOn
    (deriv ∘ fun x1 x2 ↦ ∑ i ∈ x1, (fun l z ↦ if ↑l = l₀ then 0 else 1 / (z - ↑l) ^ 2 - 1 / ↑l ^ 2) i x2) ℘'[L - l₀]
    atTop (↑L.lattice \ {l₀})ᶜ

Tactic:
· refine (L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀).tendstoLocallyUniformlyOn.congr ?_
    intro s l hl
    simp only [Function.comp_apply]
    rw [deriv_fun_sum]
    · congr with x
      split_ifs with hl₁
      · simp
      have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)
      rw [deriv_fun_sub (.fun_div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop),
        deriv_const]
      simp_rw [← zpow_natCast, one_div, ← zpow_neg, Nat.cast_ofNat]
      rw [deriv_comp_sub_const (f := (· ^ (-2 : ℤ))), deriv_zpow]
      simp
      field_simp
    · intros x hxs
      split_ifs with hl₁
      · simp
      have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)
      exact .sub (.div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop)

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

Goal state before:
pp: n : ℕ
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

Tactic:
have := log_stirlingSeq_bounded_aux n

Goal state after:
n : ℕ
this : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n i : ℕ
hi : i ∈ Finset.Iic n
⊢ eval (node n i) (T ℝ ↑n) = (-1) ^ i

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · simp [show i = 0 by grind]
  have : (n : ℤ) * (i * π / n) = i * π := by norm_cast; field
  rw [node, T_real_cos, this, cos_nat_mul_pi]

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

Goal state before:
pp: x y : ℤ
⊢ ‖![x, y]‖ = ‖![y, x]‖

Tactic:
by
  simp [EisensteinSeries.norm_eq_max_natAbs, max_comm]

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

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
⊢ s ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i)

Tactic:
by simp [hs, hscard]

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

Goal state before:
pp: k n : ℕ
hn : n ≠ 0
⊢ eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = ↑↑(↑k).negOnePow

Tactic:
rw [T_real_cos, Int.cast_negOnePow]
  convert! Real.cos_int_mul_pi k using 2
  simp [field]

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

Goal state before:
pp: L : PeriodPair
⊢ Meromorphic ℘'[L]

Tactic:
rw [← deriv_weierstrassP]
  fun_prop

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
d : ℤ
k : ℕ
hk : 2 ≤ ↑k
⊢ (fun n ↦ ((↑n * z + ↑d) ^ ↑k)⁻¹) =O[cofinite] fun n ↦ (|↑n| ^ ↑↑k)⁻¹

Tactic:
simp only [zpow_natCast, Int.cast_natCast, Real.rpow_natCast, ← inv_pow, ← abs_inv]

Goal state after:
z : ℂ
hz : z ≠ 0
d : ℤ
k : ℕ
hk : 2 ≤ ↑k
⊢ (fun n ↦ (↑n * z + ↑d)⁻¹ ^ k) =O[cofinite] fun n ↦ |(↑n)⁻¹| ^ k
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
c₁ c₂ : ℤ
⊢ Summable fun n ↦ ((↑c₁ * z - ↑n) * (↑c₂ * z + ↑n))⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
  simpa [pow_two] using! (linear_inv_isBigO_right c₂ z).mul
      (linear_inv_isBigO_right c₁ z).comp_neg_int

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

Goal state before:
pp: case refine_1
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ eval (cos (↑k * π / ↑n)) (T ℝ ↑n) ≤ eval x (T ℝ ↑n)

Tactic:
(eval_T_real_eq_neg_one_iff hn _).mpr ⟨k, le_of_lt hk₁, hk₂, rfl⟩

Goal state after:
case refine_1
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
x : ℝ
hx : x ∈ Set.Ioo (-1) 1
⊢ -1 ≤ eval x (T ℝ ↑n)
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
⊢ a ^ n * (b - b / (1 - a)) + b / (1 - a) = b * (1 - a ^ (n + 1)) / (1 - a)

Tactic:
field [sub_ne_zero.mpr ha.symm]

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 : (f.sum fun mi r ↦ r • mi) = (⇑derivative)^[k] (T ℝ ↑n)
⊢ |eval x ((⇑derivative)^[k] (T ℝ ↑n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ ↑n))

Tactic:
replace hfderiv : ∑ p ∈ f.support, f p • p = derivative^[k] (T ℝ n) := by rw [← hfderiv]; rfl

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)
⊢ |eval x ((⇑derivative)^[k] (T ℝ ↑n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ ↑n))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
h2 : (deriv^[k] fun x ↦ (x - (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)
h3 : (deriv^[k] fun x ↦ (x + (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x + (↑d + 1)) ^ (-1 - ↑k)
⊢ deriv^[k] (fun z ↦ (z - (↑d + 1))⁻¹) z + deriv^[k] (fun z ↦ (z + (↑d + 1))⁻¹) z =
    (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))

Tactic:
h2,

Goal state after:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
h2 : (deriv^[k] fun x ↦ (x - (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)
h3 : (deriv^[k] fun x ↦ (x + (↑d + 1))⁻¹) = fun x ↦ (-1) ^ k * ↑k ! * (x + (↑d + 1)) ^ (-1 - ↑k)
⊢ (fun x ↦ (-1) ^ k * ↑k ! * (x - (↑d + 1)) ^ (-1 - ↑k)) z + deriv^[k] (fun z ↦ (z + (↑d + 1))⁻¹) z =
    (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ -1 < ψ

Tactic:
by
  rw [neg_lt, ← inv_goldenRatio]
  exact inv_lt_one_of_one_lt₀ one_lt_goldenRatio

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ f x✝¹ ≤ f (x₀ + ↑i)

Tactic:
apply hf <;> grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

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

Tactic:
← Finset.sum_Ico_add,

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

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
i : ℕ
hi : ↑i + 1 ≤ ↑a
this : IntervalIntegrable f volume (x₀ + ↑i) (x₀ + (↑i + 1))
x✝¹ : ℝ
x✝ : x✝¹ ∈ Icc (x₀ + ↑i) (x₀ + (↑i + 1))
⊢ f (x₀ + (↑i + 1)) ≤ f x✝¹

Tactic:
apply hf <;> grind

Goal state after:
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:
← Finset.sum_Ico_add,

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

Goal state before:
pp: case b0
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)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ f ↑a ≤ f x

Tactic:
apply hf <;> grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h₁
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)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ f ↑i ≤ f x

Tactic:
apply hf <;> grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case b0
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)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ f ↑b ≤ f ↑i

Tactic:
apply hf <;> grind

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case h₁
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)
i : ℕ
x : ℝ
hx : ↑i ≤ x ∧ x < ↑i + 1
hi : ↑a ≤ ↑i ∧ ↑i + 1 ≤ ↑b
⊢ f x ≤ f ↑i

Tactic:
apply hf <;> grind

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
⊢ IsIso (colimit.post F (coyoneda.obj (op (yoneda.obj X))))

Tactic:
suffices colimit.post F (coyoneda.obj (op (yoneda.obj X))) =
      (colimitObjIsoColimitCompEvaluation _ _).inv ≫ ((yonedaYonedaColimit F).app (op X)).inv from
    this ▸ inferInstance

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
⊢ colimit.post F (coyoneda.obj (op (yoneda.obj X))) =
    (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (yoneda.op.obj (op X))).inv ≫
      ((yonedaYonedaColimit F).app (op X)).inv