mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.ODE.PicardLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : ↑(Icc tmin tmax)
x₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ ↑r
α β : FunSpace t₀ x₀ r L
n : ℕ
hn :
  ∀ (t : ↑(Icc tmin tmax)),
    dist (((next hf hx)^[n] α).toFun t) (((next hf hx)^[n] β).toFun t) ≤ (↑K * |↑t - ↑t₀|) ^ n / ↑n ! * dist α β
t : ↑(Icc tmin tmax)
⊢ ∫ (τ : ℝ) in uIoc ↑t₀ ↑t, ↑K ^ (n + 1) * |τ - ↑t₀| ^ n / ↑n ! * dist α β ≤
    (↑K * |↑t - ↑t₀|) ^ (n + 1) / ↑(n + 1)! * dist α β

Tactic:
apply le_of_abs_le
        -- critical: `integral_pow_abs_sub_uIoc`
        rw [← intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.integral_mul_const,
          intervalIntegral.integral_div, intervalIntegral.integral_const_mul, abs_mul, abs_div,
          abs_mul, intervalIntegral.abs_intervalIntegral_eq, integral_pow_abs_sub_uIoc, abs_div,
          abs_pow, abs_pow, abs_dist, NNReal.abs_eq, abs_abs, mul_div, div_div, ← abs_mul,
          ← Nat.cast_succ, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.abs_cast, ← mul_pow]

Goal state after:
Module: Mathlib.Analysis.Polynomial.Basic

Goal state before:
pp: case neg.inl
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree < Q.degree
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q

pp: case neg.inr
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree = Q.degree
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q

Tactic:
· exact isBigO_of_div_tendsto_nhds hPQ 0 (div_tendsto_atTop_zero_of_degree_lt P Q h)

Goal state after:
case neg.inr
𝕜 : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree = Q.degree
⊢ (fun x ↦ eval x P) =O[atTop] fun x ↦ eval x Q
Module: Mathlib.RingTheory.Polynomial.GaussNorm

Goal state before:
pp: R : Type u_1
F : Type u_2
inst✝³ : Semiring R
inst✝² : FunLike F R ℝ
v : F
c : ℝ
inst✝¹ : ZeroHomClass F R ℝ
inst✝ : NonnegHomClass F R ℝ
p : R[X]
hc : 0 ≤ c
h_nonempty : {i | gaussNorm v c p = v (p.coeff i) * c ^ i}.Nonempty
j : ℕ
hj_lt : ∀ m ≤ j, ¬gaussNorm v c p = v (p.coeff m) * c ^ m
⊢ v (p.coeff j) * c ^ j < gaussNorm v c p

Tactic:
exact lt_of_le_of_ne (le_gaussNorm v _ hc j) fun a ↦ hj_lt j (Nat.le_refl j) a.symm

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : (coeff n) f ≠ 0
⊢ 0 < v ((coeff n) f) * ∏ i ∈ n.support, c i ^ n i

Tactic:
apply mul_pos _ (by exact Finset.prod_pos fun i a ↦ (fun i ↦ pow_pos (hc i) (n i)) i)

Goal state after:
R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
f : MvPowerSeries σ R
inst✝ : Semiring R
vZero : v 0 = 0
vNonneg : ∀ (a : R), v a ≥ 0
h_eq_zero : ∀ (x : R), v x = 0 → x = 0
hc : ∀ (i : σ), 0 < c i
hbd : HasGaussNorm v c f
hf : f ≠ 0
n : σ →₀ ℕ
hn : (coeff n) f ≠ 0
⊢ 0 < v ((coeff n) f)
Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm

Goal state before:
pp: R : Type u_1
σ : Type u_2
v : R → ℝ
c : σ → ℝ
inst✝ : Semiring R
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : IsNonarchimedean v
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), 0 ≤ ∏ i ∈ t.support, c i ^ t i
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t) (f + g)) * ∏ i ∈ t.support, c i ^ t i ≤
      max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i)
t : σ →₀ ℕ
⊢ max (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i) (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) ≤
    max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
by
      simp only [le_sup_iff]
      rcases max_choice (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i)
        (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) with h | h
      · left
        simpa [h] using! le_gaussNorm v c f hbfd t
      · right
        simpa [h] using! le_gaussNorm v c g hbgd t

Goal state after:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
h : p.degree = 1
⊢ (C (p.coeff 1) * X + C (p.coeff 0)).mahlerMeasure =
    max ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 1‖ ‖(C (p.coeff 1) * X + C (p.coeff 0)).coeff 0‖

Tactic:
simp [mahlerMeasure_C_mul_X_add_C (show p.coeff 1 ≠ 0 by exact coeff_ne_zero_of_eq_degree h)]

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

Goal state before:
pp: θ : ℝ
⊢ I 0 θ * θ = 2 * sin θ

Tactic:
by
  rw [mul_comm, I]
  simp [mul_integral_comp_mul_right, two_mul]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
⊢ z ≠ (2 * ↑k + 1) * ↑π / 2

Tactic:
rw [ne_eq, Complex.ext_iff, not_and_or] at h₀ ⊢

Goal state after:
z : ℂ
h₀ : ¬z.re = (↑π / 2).re ∨ ¬z.im = (↑π / 2).im
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
k : ℤ
⊢ ¬z.re = ((2 * ↑k + 1) * ↑π / 2).re ∨ ¬z.im = ((2 * ↑k + 1) * ↑π / 2).im
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < x ^ 2 + y ^ 2
⊢ 2 * x * y + 2 * x * y < x ^ 2 + 2 * x * y + y ^ 2

Tactic:
add_right_comm

Goal state after:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 2 * x * y < x ^ 2 + y ^ 2
⊢ 2 * x * y + 2 * x * y < x ^ 2 + y ^ 2 + 2 * x * y
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
⊢ Tendsto (fun n ↦ dist (x.agmSequences y n).1 (x.agmSequences y n).2) atTop (𝓝 0)

Tactic:
apply squeeze_zero (fun _ ↦ dist_nonneg) dist_agmSequences_fst_snd

Goal state after:
x y : ℝ≥0
⊢ Tendsto (fun t ↦ dist x y / 2 ^ (t + 1)) atTop (𝓝 0)
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n : ℕ
key : Tendsto (fun n_1 ↦ (x.agmSequences y (n_1 + (n + 1))).2) atTop (𝓝 (x.agm y))
m : ℕ
⊢ ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[m + 1 + (n + 1)] (x, y)).2 =
    ((fun p ↦ (sqrt (p.1 * p.2), (p.1 + p.2) / 2))^[m + (n + 1) + 1] (x, y)).2

Tactic:
add_right_comm

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

Goal state before:
pp: θ : ℝ
n : ℕ
⊢ I (n + 2) θ * θ ^ 2 * θ ^ (2 * n + 3) =
    2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1))

Tactic:
rw [recursion]

Goal state after:
θ : ℝ
n : ℕ
⊢ (2 * (↑n + 2) * (2 * ↑n + 3) * I (n + 1) θ - 4 * (↑n + 2) * (↑n + 1) * I n θ) * θ ^ (2 * n + 3) =
    2 * (↑n + 2) * (2 * ↑n + 3) * (I (n + 1) θ * θ ^ (2 * (n + 1) + 1)) -
      4 * (↑n + 2) * (↑n + 1) * θ ^ 2 * (I n θ * θ ^ (2 * n + 1))
Module: Mathlib.Analysis.Real.Pi.Irrational

Goal state before:
pp: h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
this : 0 * ↑b < ↑a
⊢ 0 < ↑a

Tactic:
zero_mul

Goal state after:
h' : ¬Irrational (π / 2)
a : ℤ
b : ℕ
hb : 0 < b
h : π / 2 = ↑a / ↑b
this : 0 < ↑a
⊢ 0 < ↑a
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
⊢ p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1) → ∀ x ∈ s, dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε

Tactic:
hp₃

Goal state after:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
ε : ℝ
hε : 0 < ε
pbound : ℝ := ε / (sSup ((fun x ↦ ‖log x‖ ^ 2) '' s) + 1)
hxs : ∀ x ∈ s, x ≠ 0
sSup_nonneg : 0 ≤ sSup ((fun x ↦ ‖log x‖ ^ 2) '' s)
sSup_nonneg' : 0 ≤ sSup ((fun x ↦ ‖log x‖) '' s)
pbound_pos : 0 < pbound
h₁ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, 0 < p ∧ p < pbound
h₂ : ∀ᶠ (p : ℝ) in 𝓝[>] 0, p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
hcont : ContinuousOn (fun x ↦ ‖log x‖ ^ 2) s
hcont' : ContinuousOn (fun x ↦ ‖log x‖) s
p : ℝ
hp₁ : 0 < p
hp₂ : p < pbound
hp₃ : p ≤ 1 / (sSup ((fun x ↦ ‖log x‖) '' s) + 1)
⊢ ∀ x ∈ s, dist (log x) (p⁻¹ * (x ^ p - 1)) ≤ ε
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
⊢ |δ| * |log (b / a)| = δ * |log (b / a)|

Tactic:
rw [abs_of_nonneg hδ]

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

Goal state before:
pp: case h.refine_2
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)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ ContinuousOn (fun r ↦ r ^ (-1)) (spectrum ℝ z)

Tactic:
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)

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ ∫ (t : ℝ) in Ioi 1, 1 / 2 * t ^ (p - 2) ≤ ∫ (t : ℝ) in Ioi 1, p.rpowIntegrand₀₁ t 1

Tactic:
by
        refine setIntegral_mono_on ?_ ?_ measurableSet_Ioi ?_
        · refine Integrable.const_mul ?_ _
          push _ ∈ _ at hp
          exact integrableOn_Ioi_rpow_of_lt (by linarith) zero_lt_one
        · exact integrableOn_rpowIntegrand₀₁_Ioi_one hp zero_le_one
        · exact fun t ht => rpowIntegrand₀₁_one_ge_rpow_sub_two hp (le_of_lt ht)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun x ↦ |x| ^ s * rexp (-a * |x| ^ 2)) (cocompact ℝ) (𝓝 0)

Tactic:
rw [cocompact_eq_atBot_atTop, ← comap_abs_atTop]

Goal state after:
a : ℝ
ha : 0 < a
s : ℝ
⊢ Tendsto (fun x ↦ |x| ^ s * rexp (-a * |x| ^ 2)) (comap abs atTop) (𝓝 0)
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: case refine_1
⊢ ∀ (m : ℕ), ↑(1 / 2) ≠ -↑m

Tactic:
intro m
    rw [← ofReal_natCast, ← ofReal_neg, ne_eq, ofReal_inj]
    exact ((neg_nonpos.mpr m.cast_nonneg).trans_lt one_half_pos).ne'

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

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

Tactic:
← ofReal_log Real.pi_pos.le,

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

Goal state before:
pp: case h.right
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ logb b (-b ^ x) = x

Tactic:
rw [logb_neg_eq_logb, logb_rpow b_pos b_ne_one]

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

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

Tactic:
simp only [nthRoot]
    apply nthRoot.lt_pow_go_succ
    exact a.lt_succ_self.trans_le (Nat.le_self_pow hn _)

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

Goal state before:
pp: case h.inr
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
j : ℂ
hj : j ∈ b
m : ℕ
h' : j + ↑n = -↑m
⊢ ↑m < 0

Tactic:
suffices -j.re < n by
      have h : j = -m - n := by grind
      simpa [h] using this

Goal state after:
case h.inr
a b : Multiset ℂ
h : ∀ j ∈ a, ∀ (k : ℕ), j ≠ -↑k
n : ℕ
hn : (b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) + 1 ≤ n
j : ℂ
hj : j ∈ b
m : ℕ
h' : j + ↑n = -↑m
⊢ -j.re < ↑n
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

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

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

Goal state before:
pp: case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ HasStrictDerivAt arcsin (1 / √(1 - x ^ 2)) x ∧ ContDiffAt ℝ ω arcsin x

Tactic:
have : 1 - x ^ 2 < 0 := by nlinarith [h₂]
    rw [sqrt_eq_zero'.2 this.le, div_zero]
    have : arcsin =ᶠ[𝓝 x] fun _ => π / 2 := (lt_mem_nhds h₂).mono fun y hy => arcsin_of_one_le hy.le
    exact ⟨(hasStrictDerivAt_const x _).congr_of_eventuallyEq this.symm,
      contDiffAt_const.congr_of_eventuallyEq this⟩

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

Goal state before:
pp: case succ
L : PeriodPair
l₀ x : ℂ
i : ℕ
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x
          else (↑i + 1) * (L.sumInvPow x (i + 2) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 2))⁻¹ else 0)).coeff
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

Tactic:
split_ifs with hl₀

Goal state after:
case pos
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x else (↑i + 1) * (L.sumInvPow x (i + 2) - ((l₀ - x) ^ (i + 2))⁻¹)).coeff
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0

case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∉ L.lattice
⊢ (FormalMultilinearSeries.ofScalars ℂ fun i ↦
          if i = 0 then ℘[L - l₀] x else (↑i + 1) * (L.sumInvPow x (i + 2) - 0)).coeff
      (i + 1) =
    ∑' (l : ↥L.lattice),
      if ↑l = l₀ then 0 else (↑(i + 1) + 1) * (↑l - x) ^ (-↑(i + 1 + 2)) - Nat.casesOn (i + 1) (↑l ^ (-2)) 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:

Tactic:
_ = (log (2 * π) + log n) / 2 + n * (log n - 1) := by ring
    _ = log (√(2 * π * n) * (n / rexp 1) ^ n) := by
      rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp] <;>
      positivity
    _ ≤ _ := log_le_log (by positivity) (le_factorial_stirling n)

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 0
⊢ False

Tactic:
Set.mem_singleton_iff

Goal state after:
case inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 0
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 3
⊢ False

Tactic:
Set.mem_singleton_iff

Goal state after:
case inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 3
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 2
⊢ False

Tactic:
Set.mem_singleton_iff

Goal state after:
case inr.inr.inl
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 1 / 2
⊢ False
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case inr.inr.inr
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r ∈ {2 / 3}
⊢ False

Tactic:
Set.mem_singleton_iff

Goal state after:
case inr.inr.inr
r : ℚ
hr : 3 < (Int.fract r).den
hnz : ¬Irrational (cos (↑r * π))
hr' : Int.fract r = 2 / 3
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ (∑' (l : ↥L.lattice) (i : ℕ),
      if ↑l = l₀ then 0 else ((↑i + 1) * (↑l - x) ^ (-↑(i + 2)) - Nat.casesOn i (↑l ^ (-2)) 0) * (z - x) ^ i) =
    ∑' (l : ↥L.lattice) (i : ℕ), L.weierstrassPExceptSummand l₀ x i l * (z - x) ^ i

Tactic:
simp only [weierstrassPExceptSummand, ite_mul, zero_mul]

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

Goal state before:
pp: c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ z.im ≤ √((c * z.re + d) ^ 2 + (↑c * z).im ^ 2)

Tactic:
rw [Real.le_sqrt' hz, im_ofReal_mul, mul_pow]

Goal state after:
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ z.im ^ 2 ≤ (c * z.re + d) ^ 2 + c ^ 2 * z.im ^ 2
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:
simp [hs, hscard]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : IsRCLikeNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
f : ι → 𝕜 → F
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
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
⊢ ∀ y ∈ s, Summable fun n ↦ iteratedDerivWithin m (fun z ↦ f n z) s y

Tactic:
intro r hr
      by_cases hm2 : m = 0
      · simp [hm2, hsum r hr]
      · exact ((h m (by lia) (by lia)).summable hr).congr (fun _ ↦ by simp)

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

Goal state before:
pp: k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ iteratedDeriv k (fun z ↦ cotTerm z d) z =
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z

Tactic:
← Pi.add_def,

Goal state after:
k d : ℕ
z : ℂ
hz : z ∈ ℂ_ℤ
⊢ iteratedDeriv k ((fun z ↦ 1 / (z - (↑d + 1))) + fun z ↦ 1 / (z + (↑d + 1))) z =
    (fun z ↦ (-1) ^ k * ↑k ! * ((z + (↑d + 1)) ^ (-1 - ↑k) + (z - (↑d + 1)) ^ (-1 - ↑k))) z
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case inr
n k : ℕ
h✝ : MinFacHelper n k
this : 2 < n.minFac
h : n > 0
⊢ 1 < n

Tactic:
rcases (succ_le_of_lt h).eq_or_lt with rfl | h

Goal state after:
case inr.inl
k : ℕ
h✝ : MinFacHelper (succ 0) k
this : 2 < (succ 0).minFac
h : succ 0 > 0
⊢ 1 < succ 0

case inr.inr
n k : ℕ
h✝¹ : MinFacHelper n k
this : 2 < n.minFac
h✝ : n > 0
h : succ 0 < n
⊢ 1 < n
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case refine_2.inl
n k' : ℕ
e : n.minFac + 2 = k'
h : MinFacHelper n n.minFac
np : n.minFac ≠ n.minFac
⊢ n.minFac + 2 ≤ n.minFac

Tactic:
exact (np rfl).elim

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
⊢ ∃ u, Summable u ∧ ∀ (n : ℕ), ∀ k_1 ∈ K, ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ k_1‖ ≤ u n

Tactic:
lift K to Set ℍ using hK

Goal state after:
k : ℕ
hk : 1 ≤ k
K : Set ℍ
hKc : IsCompact (UpperHalfPlane.coe '' K)
⊢ ∃ u,
    Summable u ∧ ∀ (n : ℕ), ∀ k_1 ∈ UpperHalfPlane.coe '' K, ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ k_1‖ ≤ u n
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case hbc
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 : ∀ ⦃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
⊢ |u (c n) / ↑(c n) - l| ≤ ε

Tactic:
simpa using hn

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x = ∑ i ∈ Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x

Tactic:
by
    convert! (sum_integral_adjacent_intervals hf.intervalIntegrable_subset).symm
    simp

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

Goal state before:
pp: case hbc
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
⊢ |u (c n) / ↑(c n) - l| ≤ ε

Tactic:
simpa using hn

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
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
L : Tendsto (fun ε ↦ d + ε * (1 + l)) (𝓝[>] 0) (𝓝 d)
⊢ ∃ ε, d + ε * (1 + l) < l ∧ 0 < ε

Tactic:
exact (((tendsto_order.1 L).2 l hd).and self_mem_nhdsWithin).exists

Goal state after: