mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x ↦ -f x) atTop (𝓝 (-0))
⊢ -ofSeq f < ↑r✝

Tactic:
rw [neg_zero] at hg

Goal state after:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x ↦ -f x) atTop (𝓝 0)
⊢ -ofSeq f < ↑r✝
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r : ℝ
f : ℕ → ℝ
hx : Germ.Tendsto (ofSeq f) atTop
⊢ ↑r < ofSeq f

Tactic:
tendsto_ofSeq

Goal state after:
r : ℝ
f : ℕ → ℝ
hx : Tendsto f (↑(hyperfilter ℕ)) atTop
⊢ ↑r < ofSeq f
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: r : ℝ
f : ℕ → ℝ
hx : Germ.Tendsto (ofSeq f) atBot
⊢ ofSeq f < ↑r

Tactic:
tendsto_ofSeq

Goal state after:
r : ℝ
f : ℕ → ℝ
hx : Tendsto f (↑(hyperfilter ℕ)) atBot
⊢ ofSeq f < ↑r
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
h : x < 0 ∧ ArchimedeanClass.mk x < 0
⊢ Germ.Tendsto x atBot

Tactic:
by
    rcases ofSeq_surjective x with ⟨f, rfl⟩
    rw [tendsto_ofSeq, tendsto_atBot]
    exact fun r ↦ ofSeq_le_ofSeq.1 <|
      (lt_of_mk_lt_mk_of_nonpos (h.2.trans_le <| archimedeanClassMk_coe_nonneg r) h.1.le).le

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

Goal state before:
pp: case mpr
q : ℚ
hq : 0 ≤ q
⊢ (∃ r, q = r * r) → ∃ y, ↑y = √↑q

Tactic:
rintro ⟨q', rfl⟩
    exact ⟨|q'|, mod_cast (sqrt_mul_self_eq_abs q').symm⟩

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

Goal state before:
pp: q : ℚ
x : ℝ
h : Irrational x
⊢ Irrational (x - ↑q)

Tactic:
simpa only [sub_eq_add_neg, cast_neg] using h.add_ratCast (-q)

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ x.InfiniteNeg → ¬y.InfinitePos → (x + y).InfiniteNeg

Tactic:
by
  rw [← infinitePos_neg, ← infinitePos_neg, ← @infiniteNeg_neg y, neg_add]
  exact infinitePos_add_not_infiniteNeg

Goal state after:
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) ≤ ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1)

Tactic:
convert! integral_sin_pow_succ_le (2 * k + 1)

Goal state after:
case e'_3
k : ℕ
⊢ (2 * ↑k + 1) / (2 * ↑k + 2) * ∫ (x : ℝ) in 0..π, sin x ^ (2 * k) = ∫ (x : ℝ) in 0..π, sin x ^ (2 * k + 1 + 1)
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p ↦ qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x ↦ log (↑q - 1) + log (1 - x) - log x) p = -1 / (p * (1 - p))

Tactic:
deriv_fun_sub ?_ (differentiableAt_log xne0)

Goal state after:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p ↦ qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ deriv (fun x ↦ log (↑q - 1) + log (1 - x)) p - deriv log p = -1 / (p * (1 - p))

q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p ↦ qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (fun x ↦ log (↑q - 1) + log (1 - x)) p
Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy

Goal state before:
pp: q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - 1 / ↑q))
this : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
⊢ p < 1

Tactic:
have p_lt_1_minus_qinv : p < 1 - (q : ℝ)⁻¹ := by
        simp_all only [inv_pos, interior_Icc, mem_Ioo, one_div]

Goal state after:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - 1 / ↑q)
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - 1 / ↑q)
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - 1 / ↑q))
this : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
p_lt_1_minus_qinv : p < 1 - (↑q)⁻¹
⊢ p < 1
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
⊢ cfc (fun x ↦ a + b * x) z ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z

Tactic:
refine cfc_rpow fun r hr => ?_

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
r : ℝ
hr : r ∈ spectrum ℝ z
⊢ 0 < a + b * r
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:

Tactic:
_ = (a • conjSqrt x 1 + b • conjSqrt x z)⁻¹ʳ := by
        rw [conjSqrt_conjSqrt_ringInverse _ _ xpos, conjSqrt_one x xpos.nonneg]
      _ = (conjSqrt x (a • 1 + b • z))⁻¹ʳ := by simp
      _ = conjSqrt x⁻¹ʳ ((a • 1 + b • z) ^ (-1 : ℝ)) := by
        rw [ringInverse_conjSqrt _ _ xpos, ← inverse_eq_rpow_neg_one]
      _ ≤ conjSqrt x⁻¹ʳ (a • 1 + b • z ^ (-1 : ℝ)) := by
        gcongr
        rw [h₁, h₂]
        refine (cfc_le_iff _ _ _ ?_ ?_).mpr ?_
        · apply ContinuousOn.rpow_const (by fun_prop)
          intro r hr
          have := zpos.spectrum_pos hr
          have : 0 ≤ b * r := by positivity
          cases lt_or_eq_of_le ha <;> grind
        · refine ContinuousOn.const_add (ContinuousOn.const_mul ?_ _) _
          exact ContinuousOn.rpow_const (by fun_prop) (by
            #adaptation_note /-- Before nightly-2026-06-04, this was just `grind. -/
            intro x h
            have := IsStrictlyPositive.spectrum_pos (𝕜 := ℝ) zpos h
            grind)
        · intro r hr
          suffices (a • 1 + b • r) ^ (-1 : ℤ) ≤ a • 1 ^ (-1 : ℤ) + b • r ^ (-1 : ℤ) by
            simp_rw [← Real.rpow_intCast] at this
            simpa using this
          have : ConvexOn ℝ (Set.Ioi 0) (fun z : ℝ => z ^ (-1 : ℤ)) := convexOn_zpow (-1)
          grind [ConvexOn, IsStrictlyPositive.spectrum_pos]
      _ = conjSqrt x⁻¹ʳ (a • 1 + b • z⁻¹ʳ) := by rw [← inverse_eq_rpow_neg_one]
      _ = a • inverse x + b • conjSqrt x⁻¹ʳ z⁻¹ʳ := by
        simp [conjSqrt_one x⁻¹ʳ (by grind)]
      _ = _ := by
        rw [← ringInverse_conjSqrt _ _ xpos, conjSqrt_conjSqrt_ringInverse _ _ xpos]

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
⊢ p.rpowIntegrand₀₁ (x * t) x * x = p.rpowIntegrand₀₁ t 1 * x ^ p

Tactic:
simp only [rpowIntegrand₀₁_apply_mul hp ht hx, mul_assoc]
  congr
  simpa using Eq.symm <| Real.rpow_add' hx (by aesop : (p - 1) + 1 ≠ 0)

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 1 / 2 * t ^ (p - 2) = t ^ (p - 1) * (1 / 2 * 1 / t)

Tactic:
by
            have : p - 2 = p - 1 - 1 := by ring
            rw [this, Real.rpow_sub (by linarith), Real.rpow_one]
            ring

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

Goal state before:
pp: ⊢ eulerMascheroniSeq' 6 < 2 / 3

Tactic:
have h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6 := by
    rw [eulerMascheroniSeq']
    norm_num

Goal state after:
h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ eulerMascheroniSeq' 6 < 2 / 3
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case inr
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
heqOn : EqOn (fun t ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun t ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)
⊢ ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1

Tactic:
simp only [Function.comp, setIntegral_congr_fun measurableSet_Ioi heqOn,
    ← smul_eq_mul (b := x ^ p), integral_smul_const]

Goal state after:
case inr
p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
heqOn : EqOn (fun t ↦ p.rpowIntegrand₀₁ (x * t) x * x) (fun t ↦ p.rpowIntegrand₀₁ t 1 * x ^ p) (Ioi 0)
⊢ (∫ (x : ℝ) in Ioi 0, p.rpowIntegrand₀₁ x 1 ∂volume) • x ^ p = x ^ p * ∫ (x : ℝ) in Ioi 0, p.rpowIntegrand₀₁ x 1
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : a < 0
b s : ℝ
⊢ Tendsto (fun x ↦ -x - (a * x ^ 2 + b * x)) atTop atTop

Tactic:
have : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1)) := by
    ext1 x; ring_nf

Goal state after:
a : ℝ
ha : a < 0
b s : ℝ
this : (fun x ↦ -x - (a * x ^ 2 + b * x)) = fun x ↦ x * (-a * x - (b + 1))
⊢ Tendsto (fun x ↦ -x - (a * x ^ 2 + b * x)) atTop atTop
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
⊢ -log b r⁻¹ = clog b r

Tactic:
rw [log_inv, neg_neg]

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

Goal state before:
pp: case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ 0 < a

Tactic:
exact lt_of_lt_of_le zero_lt_one ha

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

Goal state before:
pp: case zero
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
⊢ ∀ x ∈ Ico x₀ (r ^ (0 + 1) * x₀), P x

Tactic:
simpa using base

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
⊢ μ.toSphere univ < ∞

Tactic:
toSphere_apply_univ'

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ ↑(dim E) * μ (ball 0 1 \ {0}) < ∞
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)
aux : AEMeasurable (fun x ↦ p) μ
⊢ AEMeasurable (fun ω ↦ ENNReal.ofReal (f ω ^ p / p)) μ

Tactic:
exact measurable_id.ennreal_ofReal.comp_aemeasurable <| (f_mble.pow aux).div_const p

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

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
⊢ regularizedHGFunSeries a b n = 0 ↔ regularizedHGFunCoeff a b n = 0

Tactic:
apply FormalMultilinearSeries.ofScalars_eq_zero

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
⊢ Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)

Tactic:
have := (tendsto_one_div_atTop_nhds_zero_nat (𝕜 := ℂ)).pow (b.card + 1 - a.card)

Goal state after:
a b : Multiset ℂ
h : a.card ≤ b.card
ha : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
this : Tendsto (fun x ↦ (1 / ↑x) ^ (b.card + 1 - a.card)) atTop (𝓝 (0 ^ (b.card + 1 - a.card)))
⊢ Tendsto (fun n ↦ ↑n ^ (↑a.card - ↑b.card - 1)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: x : ℝ
⊢ x.sigmoid * rexp (-x) = (-x).sigmoid

Tactic:
by
  rw [sigmoid_neg, sigmoid_def]
  field

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

Goal state before:
pp: x : ℝ
h : x ≠ -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x

Tactic:
rcases eq_or_ne x 1 with (rfl | h')

Goal state after:
case inl
h : 1 ≠ -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - 1 ^ 2)) (Ici 1) 1

case inr
x : ℝ
h : x ≠ -1
h' : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
i : ℕ
hi : i ∈ Finset.Iic n
⊢ 1 * ((-1) ^ i * c i) = eval (node n i) (T ℝ ↑n) * c i

Tactic:
by
      rw [eval_T_real_node hi, one_mul]

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

Goal state before:
pp: L : PeriodPair
l₀ x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice \ {l₀})ᶜ
z : ℂ
hz : ‖z‖ < ↑r
this :
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z‖ < ‖↑l - x‖) →
    HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * z ^ i) (℘[L - l₀] (x + z))
l : ↥L.lattice
hl : ↑l ≠ l₀
⊢ ↑r < ‖↑l - x‖

Tactic:
simpa [-Metric.mem_closedBall, mem_closedBall_iff_norm] using
        Set.subset_compl_comm.mp hr ⟨l.2, hl⟩

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
h₁ : P.degree < ↑(Finset.range (n + 1)).card
⊢ ∑ i ≤ n,
      eval (node n i) P *
        (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)) =
    ↑k.factorial *
      ∑ i ∈ Finset.range (n + 1),
        (eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
          ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
            ∏ a ∈ t, (x - node n a)

Tactic:
rw [Finset.mul_sum]

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
h₁ : P.degree < ↑(Finset.range (n + 1)).card
⊢ ∑ i ≤ n,
      eval (node n i) P *
        (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)) =
    ∑ i ∈ Finset.range (n + 1),
      ↑k.factorial *
        ((eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
          ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
            ∏ a ∈ t, (x - node n a))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l : ℂ
⊢ deriv ℘'[L - l] l = 6 * L.sumInvPow l 4

Tactic:
simpa using! L.iteratedDeriv_derivWeierstrassPExcept_self l (n := 1)

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

Goal state before:
pp: z : ℂ
c k : ℤ
hk : 2 ≤ k
⊢ Summable fun d ↦ ((↑c * z + ↑d) ^ k)⁻¹

Tactic:
by
  apply summable_inv_of_isBigO_rpow_inv (a := k) (by norm_cast)
  lift k to ℕ using by lia
  grind [(linear_inv_isBigO_right c z).abs_right.pow k,
    zpow_natCast, Int.cast_natCast, Real.rpow_natCast, ← inv_pow]

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

Goal state before:
pp: L : PeriodPair
⊢ AnalyticAt ℂ (L.relation * id ^ 6) 0

Tactic:
by
  refine .congr ?_ L.relation_mul_id_pow_six_eventuallyEq.symm
  fun_prop

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

Goal state before:
pp: k : ℕ
d : ℤ
⊢ ContDiffOn ℂ (↑k) (fun z ↦ 1 / (z + ↑d)) ℂ_ℤ

Tactic:
by
  simpa using ContDiffOn.fun_inv (by fun_prop) (fun x hx ↦ integerComplement_add_ne_zero hx d)

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

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

Tactic:
simp only [one_div, one_mul, one_pow, mul_one, Int.reduceNeg, iteratedDeriv_eq_iterate] at *

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)
⊢ 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))
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.range (b - a), f ↑(a + x)

Tactic:
suffices ∫ x in a..a + ↑(b - a), f x ≤ ∑ x ∈ .range (b - a), f (a + x) by simp_all

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.range (b - a), f (↑a + ↑x)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ ↑(c n) * l - u (c n) ≤ ε * ↑(c n)

Tactic:
calc
        (c n : ℝ) * l - u (c n) = -(u (c n) / c n - l) * c n := by field
        _ ≤ ε * c n := by
          gcongr
          refine le_trans (neg_le_abs _) ?_
          simpa using hn

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
⊢ ∫ (x : ℝ) in Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)

Tactic:
have integrable := anti.integrableOn_Ioi_of_summable_comp_add summable nonneg

Goal state after:
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
lim : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f ↑(i + N)) atTop (nhds (∑' (i : ℕ), f ↑(i + N)))
this : Tendsto (fun x ↦ ↑x + ↑N) atTop atTop
integrable : IntegrableOn f (Ioi ↑N) volume
⊢ ∫ (x : ℝ) in Ioi ↑N, f x ≤ ∑' (n : ℕ), f ↑(n + N)
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
a✝ : (preadditiveYoneda.obj J).PreservesEpimorphisms
⊢ (yoneda.obj J).PreservesEpimorphisms

Tactic:
exact (inferInstance : (preadditiveYoneda.obj J ⋙ forget _).PreservesEpimorphisms)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
⊢ HomologicalComplex.quasiIso C (ComplexShape.up ℤ) R.ι'

Tactic:
by rw [HomologicalComplex.mem_quasiIso_iff]; infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
⊢ pseudoApply f abar = pseudoApply f abar' → abar = abar'

Tactic:
induction abar, abar' using Quotient.inductionOn₂ with | _ a a'
   =>  _ 

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
⊢ pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧ → ⟦a⟧ = ⟦a'⟧
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
⊢ HomologicalComplex.quasiIso C (ComplexShape.up ℤ) R.π'

Tactic:
by rw [HomologicalComplex.mem_quasiIso_iff]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderQuotients
⊢ (MorphismProperty.ofObjectProperty P P).cokernels ≤ P

Tactic:
by
    intro _ ⟨_, k, hk, hf⟩
    let := Cofork.IsColimit.epi hk
    exact P.prop_of_epi k.π hf.2

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
⊢ [Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0].TFAE

Tactic:
by
  have := Localization.essSurj L P.isoModSerre
  tfae_have 1 → 2 := fun _ ↦ by
    have hf : L.map (kernel.ι f) = 0 := by
      rw [← cancel_mono (L.map f), zero_comp, ← L.map_comp,
        kernel.condition, L.map_zero]
    simpa [hf] using! map_comp_eq_zero_iff_of_epi_mono L P (𝟙 _) (kernel.ι f)
  tfae_have 2 → 3 := fun hf ↦ by
    intro Z z hz
    rw [← L.map_comp] at hz
    rw [map_eq_zero_iff L P, ← exists_comp_monoModSerre_eq_zero_iff P] at hz ⊢
    obtain ⟨W, s, hs, eq⟩ := hz
    exact ⟨W, f ≫ s, MorphismProperty.comp_mem _ _ _ hf hs, by simpa using! eq⟩
  tfae_have 3 → 1 := fun hf ↦ by
    rw [Preadditive.mono_iff_cancel_zero]
    intro W z hz
    obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.isoModSerre
      ((L.objObjPreimageIso W).hom ≫ z)
    rw [← cancel_epi (L.objObjPreimageIso W).hom, comp_zero, hφ,
      ← cancel_epi (L.map φ.s), comp_zero,
      MorphismProperty.RightFraction.map_s_comp_map]
    apply hf φ.f
    have : L.map φ.s ≫ (L.objObjPreimageIso W).hom ≫ z = L.map φ.f := by cat_disch
    rw [← this, Category.assoc, Category.assoc, hz, comp_zero, comp_zero]
  tfae_finish

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ inl ((φ g)⁻¹ n) = inr g⁻¹ * inl n * inr g

Tactic:
rw [← map_inv, inl_aut, inv_inv]

Goal state after: