mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
p : ℂ[X]
hp : p = 0
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod

case neg
p : ℂ[X]
hp : ¬p = 0
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * (Multiset.map (fun a ↦ max 1 ‖a‖) p.roots).prod
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: p : ℂ[X]
⊢ p.mahlerMeasure ≤ p.sum fun x a ↦ ‖a‖

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
p : ℂ[X]
hp : p = 0
⊢ p.mahlerMeasure ≤ p.sum fun x a ↦ ‖a‖

case neg
p : ℂ[X]
hp : ¬p = 0
⊢ p.mahlerMeasure ≤ p.sum fun x a ↦ ‖a‖
Module: Mathlib.Analysis.Rat.NatSqrt.Real

Goal state before:
pp: x prec : ℕ
h : 0 < prec
this : x.ratSqrt prec ^ 2 ≤ ↑x
⊢ ↑(x.ratSqrt prec) ^ 2 ≤ ↑x

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Analysis.Rat.NatSqrt.Real

Goal state before:
pp: x prec : ℕ
h : 0 < prec
this : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2
⊢ ↑x < ↑((x.ratSqrt prec + 1 / ↑prec) ^ 2)

Tactic:
norm_cast

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

Goal state before:
pp: case inl
digits : ℕ → Fin 1
⊢ ofDigits digits ≤ 1

Tactic:
simp [ofDigits, ofDigitsTerm]

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

Goal state before:
pp: n : ℕ
p : ℂ[X]
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure

Tactic:
by_cases hp : p = 0

Goal state after:
case pos
n : ℕ
p : ℂ[X]
hp : p = 0
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure

case neg
n : ℕ
p : ℂ[X]
hp : ¬p = 0
⊢ ‖p.coeff n‖ ≤ ↑(p.natDegree.choose n) * p.mahlerMeasure
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
y : ℝ := ↑b ^ n * x
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊y⌋₊
⊢ ↑b * ↑⌊y⌋₊ + ↑↑(Fin.ofNat b ⌊↑b * y⌋₊) = ↑⌊↑b * y⌋₊

Tactic:
norm_cast

Goal state after:
case succ
x : ℝ
b : ℕ
inst✝ : NeZero b
hx : x ∈ Set.Ico 0 1
this : b ≠ 0
n : ℕ
y : ℝ := ↑b ^ n * x
ih : ↑b ^ n * ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i = ↑⌊y⌋₊
⊢ b * ⌊y⌋₊ + ↑(Fin.ofNat b ⌊↑b * y⌋₊) = ⌊↑b * y⌋₊
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ z ∈ x.toFinset, max 1 ↑‖z‖₊ ^ count z x ≤ ∏ z ∈ p.roots.toFinset, max 1 ↑‖z‖₊ ^ count z x

Tactic:
norm_cast

Goal state after:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ ∏ x_1 ∈ x.toFinset, max 1 ‖x_1‖₊ ^ count x_1 x ≤ ∏ x_1 ∈ p.roots.toFinset, max 1 ‖x_1‖₊ ^ count x_1 x
Module: Mathlib.Analysis.Real.OfDigits

Goal state before:
pp: x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ HasSum (ofDigitsTerm (x.digits b)) x

Tactic:
hasSum_iff_tendsto_nat_of_summable_norm (by exact summable_ofDigitsTerm.abs)

Goal state after:
x : ℝ
b : ℕ
inst✝ : NeZero b
hb : 1 < b
hx : x ∈ Set.Ico 0 1
⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (x.digits b) i) Filter.atTop (nhds x)
Module: Mathlib.Analysis.Polynomial.MahlerMeasure

Goal state before:
pp: case e_a
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
⊢ ∑ i ∈ S.toFinset, ↑(count i S) = ↑(p.natDegree.choose n)

Tactic:
norm_cast

Goal state after:
case e_a
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
this : ∀ x ∈ S.toFinset, ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots
⊢ ∑ x ∈ S.toFinset, count x S = p.natDegree.choose n
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
hni : ¬x.Infinite
⊢ x.IsSt (sSup {y | ↑y < x})

Tactic:
infinite_iff,

Goal state after:
x : ℝ*
hni : ¬ArchimedeanClass.mk x < 0
⊢ x.IsSt (sSup {y | ↑y < x})
Module: Mathlib.Analysis.Real.Pi.Leibniz

Goal state before:
pp: case right
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i / (2 * ↑i + 1)) atTop (𝓝 l)
m : 𝓝[<] 1 ≤ 𝓝 1
q : Tendsto (fun x ↦ x ^ 2) (𝓝[<] 1) (𝓝[<] 1)
abel : Tendsto (fun x ↦ ((fun x ↦ ∑' (n : ℕ), (-1) ^ n / (2 * ↑n + 1) * x ^ n) ∘ fun x ↦ x ^ 2) x * x) (𝓝[<] 1) (𝓝 l)
y : ℝ
hy1 : y - 1 < 1 ∧ 1 - y < 1
hy2 : y < 1
ny : ‖y‖ < 1
⊢ ∑' (x : ℕ), (-1) ^ x * y ^ (2 * x + 1) / (2 * ↑x + 1) = ∑' (b : ℕ), (-1) ^ b * y ^ (2 * b + 1) / ↑(2 * b + 1)

Tactic:
norm_cast

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

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
hl : y < x
⊢ sqrt (x * y) < (x + y) / 2

Tactic:
have key : 0 < (x - y) ^ 2 := sq_pos_iff.mpr (by rwa [← zero_lt_iff, tsub_pos_iff_lt])

Goal state after:
x y : ℝ≥0
h : x ≠ y
hl : y < x
key : 0 < (x - y) ^ 2
⊢ sqrt (x * y) < (x + y) / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: x : ℝ
| (↑x).arctan

Tactic:
← Real.tan_arctan x

Goal state after:
x : ℝ
| (↑(Real.tan (Real.arctan x))).arctan
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case h₀
x : ℝ
⊢ ↑(Real.arctan x) ≠ ↑π / 2

Tactic:
norm_cast

Goal state after:
case h₀
x : ℝ
⊢ ¬Real.arctan x = π / 2
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case h₁
x : ℝ
⊢ -(π / 2) < (↑(Real.arctan x)).re

Tactic:
norm_cast

Goal state after:
case h₁
x : ℝ
⊢ -(π / 2) < Real.arctan x
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case h₂
x : ℝ
⊢ (↑(Real.arctan x)).re ≤ π / 2

Tactic:
norm_cast

Goal state after:
case h₂
x : ℝ
⊢ Real.arctan x ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.CompareExp

Goal state before:
pp: l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z ↦ z ^ a₂ * cexp (↑b₂ * z)) =ᶠ[l] fun z ↦ z ^ a₂ * cexp (↑b₂ * z)

Tactic:
norm_cast

Goal state after:
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 : ℝ
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < 1 - (↑q)⁻¹
⊢ 0 < log (↑q - 1) + log (1 - p) - log p

Tactic:
simp only [sub_pos, gt_iff_lt]

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 : ℝ
this✝ : 2 ≤ ↑q
zero_le_qinv : 0 < (↑q)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < 1 - (↑q)⁻¹
⊢ log p < log (↑q - 1) + log (1 - p)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order

Goal state before:
pp: case tendsto
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsStrictlyPositive a
⊢ TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) Real.log (𝓝[>] 0) (spectrum ℝ a)

Tactic:
case tendsto =>
    let s := {a : A | IsStrictlyPositive a}
    let f (p : ℝ) (x : ℝ) := if p > 0 then p⁻¹ * (x ^ p - 1) else Real.log x
    have hmain := Real.tendstoLocallyUniformlyOn_rpow_sub_one_log
    rw [tendstoLocallyUniformlyOn_iff_forall_isCompact isOpen_Ioi] at hmain
    exact hmain (spectrum ℝ a) (by grind) (by grind)

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

Goal state before:

Tactic:
_ ≤ p * ‖log x‖ ^ 2 := Real.norm_inv_mul_rpow_sub_one_sub_log_le hp₁ (hs hx) hx'
    _ ≤ p * sSup ((fun x => ‖log x‖ ^ 2) '' s) := by
          gcongr
          refine le_csSup ?_ (by grind)
          grind [IsCompact.bddAbove, ← IsCompact.image_of_continuousOn]
    _ ≤ pbound * (sSup ((fun x => ‖log x‖ ^ 2) '' s) + 1) := by gcongr; grind
    _ = ε := by grind

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

Goal state before:
pp: case pos
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
ha' : a = 0
hb' : b = 1
⊢ 0 < r

Tactic:
#adaptation_note /-- Before nightly-2026-06-04, this was just `grind.
      `spectrum_pos` is not activating in `grind` despite the
      ```
      grind_pattern IsStrictlyPositive.spectrum_pos => x ∈ spectrum 𝕜 a, IsStrictlyPositive a
      ```
      rule, because `grind` will not fill in the `𝕜 := ℝ`. -/

Goal state after:
case pos
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
ha' : a = 0
hb' : b = 1
⊢ 0 < r
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
t : ℝ
ht : max 1 (N / min a b) ≤ t
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
ht_pos : 0 < t
⊢ min a b * t = min (a * t) (b * t)

Tactic:
rw [min_mul_of_nonneg _ _ ht_pos.le]

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

Goal state before:
pp: a : ℂ
ha : 0 < a.re
s : ℝ
⊢ (-a).re < 0

Tactic:
rwa [neg_re, neg_lt_zero]

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

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ 2 * (2 * ↑π) ^ (-s)
⊢ 2 * ↑π ≠ 0

Tactic:
exact_mod_cast Real.two_pi_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) = ↑√π
⊢ HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1

Tactic:
have aux2 : (√π : ℂ) ≠ 0 := by rw [ofReal_ne_zero]; positivity

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

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ StrictAntiOn (logb b) (Iio 0)

Tactic:
by
  rintro x (hx : x < 0) y (hy : y < 0) hxy
  rw [← logb_abs b y, ← logb_abs b x]
  refine logb_lt_logb hb (abs_pos.2 hy.ne) ?_
  rwa [abs_of_neg hy, abs_of_neg hx, neg_lt_neg_iff]

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

Goal state before:
pp: ⊢ AntitoneOn (fun x ↦ log x / x) (Ici (rexp 1))

Tactic:
by
  intro x hex y hey hxy
  have x_pos : 0 < x := (exp_pos 1).trans_le hex
  have y_pos : 0 < y := (exp_pos 1).trans_le hey
  have hlogx : 1 ≤ log x := by rwa [le_log_iff_exp_le x_pos]
  have hyx : 0 ≤ y / x - 1 := by rwa [le_sub_iff_add_le, le_div_iff₀ x_pos, zero_add, one_mul]
  rw [div_le_iff₀ y_pos, ← sub_le_sub_iff_right (log x)]
  calc
    log y - log x = log (y / x) := by rw [log_div y_pos.ne' x_pos.ne']
    _ ≤ y / x - 1 := log_le_sub_one_of_pos (div_pos y_pos x_pos)
    _ ≤ log x * (y / x - 1) := le_mul_of_one_le_left hyx hlogx
    _ = log x / x * y - log x := by ring

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

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
z : ℝ
hz : z ∈ Ici (rexp a⁻¹)
⊢ z ^ a ∈ {b | rexp 1 ≤ b}

Tactic:
mem_ofPred_eq

Goal state after:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
z : ℝ
hz : z ∈ Ici (rexp a⁻¹)
⊢ rexp 1 ≤ z ^ a
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 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
hnpos : 0 < ↑n
x : E
⊢ ε * (g x * g x) ≤ ε * (‖g‖ * ‖g‖)

Tactic:
apply mul_le_mul (le_refl ε) _ (mul_self_nonneg (g x)) (le_of_lt hε)

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
hnpos : 0 < ↑n
x : E
⊢ g x * g x ≤ ‖g‖ * ‖g‖
Module: Mathlib.Analysis.SpecialFunctions.Pochhammer

Goal state before:
pp: n : ℕ
⊢ ConvexOn ℝ (Set.Ici (↑n - 1)) fun x ↦ Polynomial.eval x (descPochhammer ℝ n)

Tactic:
rcases n.eq_zero_or_pos with h_eq | _
  · simp [h_eq, convexOn_const, convex_Ici]
  · apply MonotoneOn.convexOn_of_deriv (convex_Ici (n - 1 : ℝ))
      continuous_descPochhammer_eval.continuousOn
      differentiable_descPochhammer_eval.differentiableOn
    rw [interior_Ici]
    exact monotoneOn_deriv_descPochhammer_eval n

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

Goal state before:
pp: k n : ℕ
⊢ (Set.Ici (↑n - 1)).piecewise (fun x ↦ Polynomial.eval x (descPochhammer ℝ n)) 0 ↑k = ↑(k.descFactorial n)

Tactic:
rw [Set.piecewise, descPochhammer_eval_eq_descFactorial, ite_eq_left_iff, Set.mem_Ici, not_le,
    eq_comm, Pi.zero_apply, Nat.cast_eq_zero, Nat.descFactorial_eq_zero_iff_lt, ← @Nat.cast_lt ℝ]
  exact (sub_lt_self (n : ℝ) zero_lt_one).trans'

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ Polynomial.eval (↑n - 1) (descPochhammer ℝ n) = 0

Tactic:
simpa [← Nat.cast_pred hn] using descPochhammer_eval_coe_nat_of_lt (Nat.sub_one_lt_of_lt hn)

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

Goal state before:
pp: case e_a.e_a.e_a
E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
h_rpow : IntegrableOn (fun y ↦ y ^ (↑(Module.finrank ℝ E) - 1 - α)) (Ioo 0 r) volume
y : ℝ
hy : 0 < y
right✝ : y < r
⊢ ↑(Module.finrank ℝ E) - 1 = ↑(Module.finrank ℝ E - 1)

Tactic:
norm_cast

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

Goal state before:
pp: r : ℝ
hr : 0 < r
s : ℂ
hs : ‖s‖ < r
l : ℂ
h : 2 * r ≤ ‖l‖
this✝ : s ≠ l
this : 0 < ‖l‖
⊢ 10 * r / ‖l‖ ^ 3 = 10 * r * ‖l‖ ^ (-3)

Tactic:
norm_cast

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

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
⊢ regularizedHGFunCoeff a b n = 0 ↔ (∃ j ∈ a, ∃ k < n, j = -↑k) ∨ ∃ j ∈ b, ∃ m, j + ↑n = -↑m

Tactic:
unfold regularizedHGFunCoeff

Goal state after:
a b : Multiset ℂ
n : ℕ
⊢ (Multiset.map (fun x ↦ Polynomial.eval x (ascPochhammer ℂ n)) a).prod /
        (↑n ! * (Multiset.map (fun x ↦ Gamma (x + ↑n)) b).prod) =
      0 ↔
    (∃ j ∈ a, ∃ k < n, j = -↑k) ∨ ∃ j ∈ b, ∃ m, j + ↑n = -↑m
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ regularizedHGFunCoeff a b (n + 1) =
    (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n) * (i + ↑n)) a).prod /
      (↑n ! * (↑n + 1) * (Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b).prod)

Tactic:
unfold regularizedHGFunCoeff

Goal state after:
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ (Multiset.map (fun x ↦ Polynomial.eval x (ascPochhammer ℂ (n + 1))) a).prod /
      (↑(n + 1)! * (Multiset.map (fun x ↦ Gamma (x + ↑(n + 1))) b).prod) =
    (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n) * (i + ↑n)) a).prod /
      (↑n ! * (↑n + 1) * (Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b).prod)
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n) * (i + ↑n)) a).prod /
      (↑n ! * (↑n + 1) * (Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b).prod) =
    regularizedHGFunCoeff a b n *
      ((Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1)))

Tactic:
unfold regularizedHGFunCoeff

Goal state after:
a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n) * (i + ↑n)) a).prod /
      (↑n ! * (↑n + 1) * (Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b).prod) =
    (Multiset.map (fun x ↦ Polynomial.eval x (ascPochhammer ℂ n)) a).prod /
        (↑n ! * (Multiset.map (fun x ↦ Gamma (x + ↑n)) b).prod) *
      ((Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1)))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
hx : x ∈ L.lattice
H : ContinuousAt (fun z ↦ ℘[L - x] z + (1 / (z - x) ^ 2 - 1 / x ^ 2)) x
⊢ ContinuousAt (fun x ↦ x ^ (-2)) 0

Tactic:
simpa [Function.comp_def] using!
    (((H.sub ((L.differentiableOn_weierstrassPExcept x).differentiableAt
      (L.compl_lattice_sdiff_singleton_mem_nhds x)).continuousAt).add
      (continuous_const (y := 1 / x ^ 2)).continuousAt).comp_of_eq
      (continuous_const_add x).continuousAt (add_zero _) :)

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

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 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:
by_cases! hb : ∀ k ∈ b, k ≠ -n

Goal state after:
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))

case neg
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))
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: n : ℕ
a b : Multiset ℂ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
norm_cast

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

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * ‖l‖ ^ 3 ≤ 2 * (2 * ‖↑l - s‖) ^ 3

Tactic:
norm_cast

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * ‖l‖ ^ 3 ≤ 2 * (2 * ‖↑l - s‖) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 2 * ‖l‖ ^ 3 ≤ 16 * ‖↑l - s‖ ^ 3

Tactic:
refine LE.le.trans_eq (b := 2 * (2 * ‖l - s‖) ^ 3) ?_ (by ring)
    norm_cast
    gcongr
    refine le_trans ?_ (mul_le_mul le_rfl (norm_sub_norm_le _ _) (by linarith) (by linarith))
    norm_cast at *
    linarith

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

Goal state before:
pp: 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
⊢ ↑(b.toFinset.sup fun x ↦ ⌈-x.re⌉₊) < ↑n

Tactic:
norm_cast

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

Goal state before:
pp: a : Multiset ℂ
⊢ ∀ i ∈ a, Tendsto (fun n ↦ i / ↑n + 1) atTop (𝓝 ((fun x ↦ 1) i))

Tactic:
intro i

Goal state after:
a : Multiset ℂ
i : ℂ
⊢ i ∈ a → Tendsto (fun n ↦ i / ↑n + 1) atTop (𝓝 ((fun x ↦ 1) i))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
⊢ ℘[L] (z + ↑l) = ℘[L] z

Tactic:
have := L.weierstrassPExcept_add_coe_aux (z + l) (add_mem hz l.2) l hl (x := z) (by simp)

Goal state after:
case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this :
  (fun x ↦ ℘[L - z + ↑l] (x + ↑l)) z = (fun x ↦ ℘[L - z + ↑l - ↑l] x + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)) z
⊢ ℘[L] (z + ↑l) = ℘[L] z
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case hf
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun l ↦ if ↑l = ↑l₀ then 0 else -2 / (z - ↑l) ^ 3

pp: case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0

Tactic:
· exact ⟨_, L.hasSum_derivWeierstrassPExcept _ _⟩

Goal state after:
case hg
L : PeriodPair
l₀ : ↥L.lattice
z : ℂ
⊢ Summable fun i ↦ if ↑i = ↑l₀ then -2 / (z - ↑l₀) ^ 3 else 0
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ DifferentiableOn ℂ ℘'[L] (↑L.lattice)ᶜ

Tactic:
← L.derivWeierstrassPExcept_of_notMem _ L.ω₁_div_two_notMem_lattice

Goal state after:
L : PeriodPair
⊢ DifferentiableOn ℂ ℘'[L - L.ω₁ / 2] (↑L.lattice)ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
this : HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))
j : ℕ
⊢ 3 ≤ 2 * (↑j + 1) + 1

Tactic:
norm_cast

Goal state after:
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
this : HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))
j : ℕ
⊢ 3 ≤ 2 * (j + 1) + 1
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬↑l = l₀
⊢ (↑i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - 0) = (↑(i + 1) + 1) * ((↑l - x) ^ (↑i + 1 + 2))⁻¹ - 0

Tactic:
norm_cast

Goal state after:
case neg
L : PeriodPair
l₀ x : ℂ
i : ℕ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
e : ¬↑l = l₀
⊢ ↑(i + 2) * (((↑l - x) ^ (i + 3))⁻¹ - 0) = ↑(i + 1 + 1) * ((↑l - x) ^ (i + 1 + 2))⁻¹ - 0
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Tactic:
← Filter.tendsto_add_atTop_iff_nat 1

Goal state after:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun n ↦ stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun n ↦ stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Tactic:
exact tendsto_atTop_ciInf stirlingSeq'_antitone ⟨x, hx'⟩

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

Goal state before:
pp: n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
⊢ ↑↑n * (↑i * π / ↑n) = ↑i * π

Tactic:
norm_cast

Goal state after:
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
⊢ ↑n * (↑i * π / ↑n) = ↑i * π