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 : ℝ
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
V : E
δ : ℝ
hδ : 0 ≤ δ
h : ∀ x ∈ uIoc a b, ‖f x - V‖ ≤ δ
hsub : uIcc a b ⊆ Ioi 0
hint_f : IntervalIntegrable (fun x ↦ x⁻¹ • f x) volume a b
hint_V : IntervalIntegrable (fun x ↦ x⁻¹ • V) volume a b
hint_inv : IntervalIntegrable (fun x ↦ x⁻¹ * δ) volume a b
x : ℝ
hx : x ∈ uIoc a b
⊢ ‖x⁻¹ • (f x - V)‖ ≤ x⁻¹ * δ

Tactic:
have hx_pos : 0 < x :=
              lt_of_lt_of_le (lt_min ha hb) (uIoc_subset_uIcc hx).1
            rw [norm_smul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hx_pos)]
            exact mul_le_mul_of_nonneg_left (h x hx) (inv_nonneg.2 hx_pos.le)

Goal state after:
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
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * (t⁻¹ - (t + x)⁻¹) = t ^ p * ((t + x - t) / (t * (t + x)))

Tactic:
simp only [inv_eq_one_div]

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * (1 / t - 1 / (t + x)) = t ^ p * ((t + x - t) / (t * (t + x)))
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 * x = p.rpowIntegrand₀₁ t 1 * x ^ p

Tactic:
simp only [rpowIntegrand₀₁_apply_mul hp ht hx, mul_assoc]

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
⊢ p.rpowIntegrand₀₁ t 1 * (x ^ (p - 1) * x) = p.rpowIntegrand₀₁ t 1 * x ^ p
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case pos
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≤ y
h : x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

pp: case neg
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≤ y
h : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y

Tactic:
case pos => simpa [h, rpowIntegrand₀₁] using rpowIntegrand₀₁_nonneg hp.1 ht hy

Goal state after:
case neg
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
x : ℝ
hx : x ∈ Ici 0
y : ℝ
hy : y ∈ Ici 0
hxy : x ≤ y
h : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x ≤ p.rpowIntegrand₀₁ t y
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case e_a
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ x / x = 1

Tactic:
exact (div_eq_one_iff_eq hx_zero).mpr rfl

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

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

Tactic:
div_self h1,

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
h2 : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ (1 - s).Gammaℝ⁻¹ = 1 / (1 - s).Gammaℝ
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: case left
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x ↦ cexp (a * ↑x ^ 2 + b * ↑x)) =o[atBot] fun x ↦ |x| ^ s

Tactic:
refine ((cexp_neg_quadratic_isLittleO_rpow_atTop ha (-b) s).comp_tendsto
      Filter.tendsto_neg_atBot_atTop).congr' (Eventually.of_forall fun x ↦ by simp) ?_

Goal state after:
case left
a : ℂ
ha : a.re < 0
b : ℂ
s : ℝ
⊢ (fun x ↦ x ^ s) ∘ Neg.neg =ᶠ[atBot] fun x ↦ |x| ^ s
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
⊢ 𝓕 f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)

Tactic:
hFf

Goal state after:
a : ℂ
ha : 0 < a.re
b : ℂ
f : ℝ → ℂ := fun x ↦ cexp (-↑π * a * ↑x ^ 2 + 2 * ↑π * b * ↑x)
hFf : 𝓕 f = fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)
h1 : 0 < (↑π * a).re
h2 : 0 < (↑π / a).re
f_bd : f =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
⊢ (fun x ↦ 1 / a ^ (1 / 2) * cexp (-↑π / a * (↑x + I * b) ^ 2)) =O[cocompact ℝ] fun x ↦ |x| ^ (-2)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
⊢ cfc (p.rpowIntegrand₀₁ t) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x

Tactic:
rpowIntegrand₀₁_eq_sub (by grind) ht

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
x : A
hx : x ∈ Ici 0
⊢ cfc (fun x ↦ t ^ (p - 1) - t ^ p * (t + x)⁻¹) x =
    (fun x ↦ (algebraMap ℝ A) (t ^ (p - 1)) - t ^ p • Ring.inverse ((algebraMap ℝ A) t + x)) x
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

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

Tactic:
rw [← logb_one]
  exact logb_lt_logb_iff hb h zero_lt_one

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

Goal state before:
pp: b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ -b ≠ -1 ∧ -b ≠ 0 ∧ -b ≠ 1

Tactic:
by simp [hb, neg_eq_iff_eq_neg]

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

Goal state before:
pp: case succ
P : ℝ → Prop
x₀ r : ℝ
hr : 1 < r
hx₀ : 0 < x₀
base : ∀ x ∈ Ico x₀ (r * x₀), P x
step : ∀ n ≥ 1, (∀ z ∈ Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z
n : ℕ
ih : ∀ x ∈ Ico x₀ (r ^ (n + 1) * x₀), P x
⊢ ∀ x ∈ Ico x₀ (r ^ (n + 1 + 1) * x₀), P x

Tactic:
| succ n ih =>

Goal state after:
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 →ᵇ ℝ
u : ℕ → ℝ
⊢ Tendsto u atTop (𝓝[>] 0) → Tendsto ((fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ u) atTop (𝓝 (∫ (x : E), g x ∂P))

Tactic:
hu

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
g : E →ᵇ ℝ
u : ℕ → ℝ
hu : Tendsto u atTop (𝓝[>] 0)
⊢ Tendsto ((fun ε ↦ ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) ∘ u) atTop (𝓝 (∫ (x : E), g x ∂P))
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: case succ
n : ℕ
ih : MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) (Set.Ioi (↑n - 1))
⊢ MonotoneOn (deriv fun x ↦ Polynomial.eval x (descPochhammer ℝ (n + 1))) (Set.Ioi (↑(n + 1) - 1))

Tactic:
| succ n ih =>

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) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ

Tactic:
congr with ω
    rw [← ENNReal.ofReal_mul p_pos.le, mul_div_cancel₀ (f ω ^ p) p_pos.ne.symm]

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

Goal state before:
pp: n✝ : ℕ
hn✝ : n✝ ≠ 0
a n : ℕ
hn : n + 2 ≠ 0
⊢ a < (a + 1) ^ (n + 2)

Tactic:
exact a.lt_succ_self.trans_le (Nat.le_self_pow hn _)

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

Goal state before:
pp: case inr
n a b : ℕ
hn : n ≠ 0
hlt : n.nthRoot b < a
⊢ a ≤ n.nthRoot b ↔ a ^ n ≤ b

Tactic:
| inr hlt =>

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
⊢ (↑(dim E) * μ.real (ball 0 1)) •
      ∫ (x : ↑(Ioi 0)), (↑x ^ (dim E - 1)).toNNReal • f ↑x ∂Measure.comap Subtype.val volume =
    dim E • μ.real (ball 0 1) • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

pp: case f_meas
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
⊢ Measurable fun r ↦ (↑r ^ (dim E - 1)).toNNReal

Tactic:
← nsmul_eq_mul,

Goal state after:
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
⊢ (dim E • μ.real (ball 0 1)) • ∫ (x : ↑(Ioi 0)), (↑x ^ (dim E - 1)).toNNReal • f ↑x ∂Measure.comap Subtype.val volume =
    dim E • μ.real (ball 0 1) • ∫ (y : ℝ) in Ioi 0, y ^ (dim E - 1) • f y

case f_meas
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
⊢ Measurable fun r ↦ (↑r ^ (dim E - 1)).toNNReal
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘'[L] (z + ↑l) = ℘'[L] z

Tactic:
simp only [derivWeierstrassP]
  rw [← (Equiv.addRight l).tsum_eq]
  simp only [← tsum_neg, ← div_neg, Equiv.coe_addRight, Submodule.coe_add, add_sub_add_right_eq_sub]

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

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

Tactic:
exact summable_of_hasFiniteSupport ((Set.finite_singleton ⟨l₀, hl₀⟩).subset (by simp))

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1) = (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - log (rexp 1))

pp: case hx
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

pp: case hy
n : ℕ
hn : n ≠ 0
⊢ rexp 1 ≠ 0

pp: case hx
n : ℕ
hn : n ≠ 0
⊢ 2 * π ≠ 0

pp: case hy
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

pp: n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * ↑n

pp: case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

pp: case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0

Tactic:
log_exp

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1) = (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1)

case hx
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ rexp 1 ≠ 0

case hx
n : ℕ
hn : n ≠ 0
⊢ 2 * π ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * ↑n

case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
this :
  (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (-1) ^ k - 1
⊢ ∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I) =
    Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1)

Tactic:
have hf {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0) : s = a / b * t := by
      linear_combination (norm := field) h * a / b

Goal state after:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬2 * ↑n ∣ k
this :
  (∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I)) * (Complex.exp (↑k / (2 * ↑n) * ↑π * I))⁻¹ *
      (Complex.exp (↑k / ↑n * ↑π * I) - 1) =
    (-1) ^ k - 1
hf : ∀ {s a b t : ℂ}, s * a⁻¹ * b = t → a ≠ 0 → b ≠ 0 → s = a / b * t
⊢ ∑ i ∈ range n, Complex.exp (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π) * I) =
    Complex.exp (↑k / (2 * ↑n) * ↑π * I) / (Complex.exp (↑k / ↑n * ↑π * I) - 1) * ((-1) ^ k - 1)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ↑((Equiv.prodCongrLeft fun x ↦
            { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
          (Prod.map some id p)).2 =
    l₀
⊢ ‖0 *
        (z - x) ^
          ((Equiv.prodCongrLeft fun x ↦
                { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
              (Prod.map some id p)).1‖ ≤
    (↑p.1 + 2) * κ ^ (-↑p.1) * (‖↑p.2 - x‖ ^ (-3) * ‖z - x‖)

Tactic:
simp only [zero_mul, norm_zero, zpow_neg, zpow_natCast, Int.reduceNeg]

Goal state after:
case pos
L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
κ : ℝ
hκ : 1 < κ
hκ' : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ * κ < ‖↑l - x‖
e : ℕ × ↥L.lattice ≃ ↥L.lattice ⊕ ℕ × ↥L.lattice :=
  (Equiv.prodCongrLeft fun x ↦ (Denumerable.eqv (Option ℕ)).symm).trans optionProdEquiv
H₁ : Summable fun i ↦ (↑i + 2) * κ ^ (-↑i)
H₂ : Summable fun l ↦ ‖↑l - x‖ ^ (-3) * ‖z - x‖
p : ℕ × ↥L.lattice
hp :
  ↑((Equiv.prodCongrLeft fun x ↦
            { toFun := Encodable.encode, invFun := Denumerable.ofNat (Option ℕ), left_inv := ⋯, right_inv := ⋯ })
          (Prod.map some id p)).2 =
    l₀
⊢ 0 ≤ (↑p.1 + 2) * (κ ^ p.1)⁻¹ * ((‖↑p.2 - x‖ ^ 3)⁻¹ * ‖z - x‖)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case pos
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h✝ : P = 0
⊢ P.leadingCoeff ≤ 2 ^ (n - 1)

pp: case neg
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h✝ : ¬P = 0
⊢ P.leadingCoeff ≤ 2 ^ (n - 1)

Tactic:
case pos hP => simp [hP]

Goal state after:
case neg
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h✝ : ¬P = 0
⊢ P.leadingCoeff ≤ 2 ^ (n - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
⊢ 0 ≤ ↑n * (arccos x / π)

Tactic:
positivity [arccos_nonneg x]

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

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * a ^ n * u₀ + a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k

Tactic:
add_comm n,

Goal state after:
case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ a * a ^ n * u₀ + a * (b * ∑ k ∈ Finset.range n, a ^ k) + b = a ^ (1 + n) * u₀ + b * ∑ k ∈ Finset.range (1 + n), a ^ k
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
⊢ (Rat.divInt (2 * ↑k + 1) (2 * ↑n)).den = 2 * n / (2 * n).gcd (2 * k + 1)

Tactic:
rw [Rat.den_divInt]; norm_cast; simp [hn]

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

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
⊢ b / (1 - a) < arithGeom a b u₀ n

Tactic:
by
  induction n with
  | zero => exact h0
  | succ n hn =>
    calc b / (1 - a)
    _ = a * (b / (1 - a)) + b := by grind
    _ < a * arithGeom a b u₀ n + b := by gcongr

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

Goal state before:
pp: m n : ℕ
⊢ fib (-↑m + -↑n) - fib (-↑m + -↑(n + 1)) =
    fib (-↑m - 1) * fib (-↑n) + fib (-↑m) * fib (-↑n + 1) - fib (-↑m - 1) * fib (-↑n - 1) - fib (-↑m) * fib (-↑n)

Tactic:
by
        conv_lhs => rw [fib_neg_natCast_add_neg_natCast, fib_neg_natCast_add_neg_natCast]
        grind

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

Goal state before:
pp: ⊢ Irrational φ

Tactic:
by
  have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
  have := this.ratCast_add 1
  convert! this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
  simp
  ring

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

Goal state before:
pp: case succ
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * ↑(Nat.fib (n + 1 + 1)) + ↑(Nat.fib (n + 1)) = φ ^ (n + 1 + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
⊢ φ.Faithful

Tactic:
← isSeparator_iff_faithful_preadditiveCoyonedaObj

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := preadditiveCoyonedaObj G
⊢ IsSeparator 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
ε : ℝ
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:
simp_rw [div_eq_inv_mul]

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 < (↑n)⁻¹ * u n
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case eq
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j j✝ j'✝ : C
hj₁ : cofilteredClosure f j✝
hj₂ : cofilteredClosure f j'✝
g g' : j✝ ⟶ j'✝
ih : ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := j✝, property := hj₁ }.obj
ih' : ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := j'✝, property := hj₂ }.obj
⊢ ∃ a, CofilteredClosureSmall.abstractCofilteredClosureRealization f a = { obj := eq g g', property := ⋯ }.obj

Tactic:
rcases ih with ⟨⟨n, x⟩, rfl⟩
    rcases ih' with ⟨⟨m, y⟩, rfl⟩
    refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
    · simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      refine CofilteredClosureSmall.InductiveStep.eq ?_ ?_ x y g g'
      all_goals apply Nat.lt_succ_of_le
      exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
    · simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
      rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0
⊢ g ≫ f = 0 ≫ f

Tactic:
exact hc.pushout_hom_ext (by simpa using hf)

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
⊢ Mono (I.ι.f 0)

Tactic:
exact mono_of_isLimit_fork I.isLimitKernelFork

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝² : P.IsSerreClass
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ kernel.ι (f₁ - f₂) ≫ f₁ = kernel.ι (f₁ - f₂) ≫ f₂

Tactic:
· simpa only [Preadditive.comp_sub, sub_eq_zero] using kernel.condition (f₁ - f₂)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
⊢ (L.objObjPreimageIso W).hom ≫ z = 0

Tactic:
hφ,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : C
f : X ⟶ Y
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
⊢ φ.map L ⋯ = 0