mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Ring R
r s : R
h : Commute r s
k : ℕ
ih :
  (descPochhammer ℤ k).smeval (r + s) =
    ∑ ij ∈ antidiagonal k, ↑(k.choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)
⊢ (descPochhammer ℤ (k + 1)).smeval (r + s) =
    ∑ ij ∈ antidiagonal (k + 1),
      ↑((k + 1).choose ij.1) * ((descPochhammer ℤ ij.1).smeval r * (descPochhammer ℤ ij.2).smeval s)

Tactic:
rw [descPochhammer_succ_right, mul_comm, smeval_mul, sum_antidiagonal_choose_succ_mul
      fun i j => ((descPochhammer ℤ i).smeval r * (descPochhammer ℤ j).smeval s),
      ← sum_add_distrib, smeval_sub, smeval_X, smeval_natCast, pow_zero, pow_one, ih, mul_sum]
    refine sum_congr rfl ?_
    intro ij hij -- try to move `descPochhammer`s to right, gather multipliers.
    have hdx : (descPochhammer ℤ ij.1).smeval r * (X - (ij.2 : ℤ[X])).smeval s =
        (X - (ij.2 : ℤ[X])).smeval s * (descPochhammer ℤ ij.1).smeval r := by
      refine (commute_iff_eq ((descPochhammer ℤ ij.1).smeval r)
        ((X - (ij.2 : ℤ[X])).smeval s)).mp ?_
      exact smeval_commute ℤ (descPochhammer ℤ ij.1) (X - (ij.2 : ℤ[X])) h
    rw [descPochhammer_succ_right, mul_comm, smeval_mul, descPochhammer_succ_right, mul_comm,
      smeval_mul, ← mul_assoc ((descPochhammer ℤ ij.1).smeval r), hdx]
    simp only [mul_assoc _ ((descPochhammer ℤ ij.1).smeval r) _,
      ← mul_assoc _ _ (((descPochhammer ℤ ij.1).smeval r) * _)]
    have hl : (r + s - k • 1) * (k.choose ij.1) = (k.choose ij.1) * (X - (ij.2 : ℤ[X])).smeval s +
        ↑(k.choose ij.2) * (X - (ij.1 : ℤ[X])).smeval r := by
      simp only [smeval_sub, smeval_X, pow_one, smeval_natCast, pow_zero]
      rw [← Nat.choose_symm_of_eq_add (List.Nat.mem_antidiagonal.mp hij).symm,
        (List.Nat.mem_antidiagonal.mp hij).symm, ← mul_add, Nat.cast_comm, add_smul]
      abel_nf
    rw [hl, ← add_mul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticAt 𝕜 f z
p : A[X]
⊢ AnalyticAt 𝕜 (fun x ↦ (aeval (f x)) p) z

Tactic:
rw [← analyticWithinAt_univ] at hf ⊢
  exact hf.aeval_polynomial p

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_10
a : ℕ
z : ℂ
hz : z ≠ 0
this✝ :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
H : 1 / ‖z⁻¹ • 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹)
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0 ‖z‖ₑ
⊢ (FormalMultilinearSeries.ofScalars ℂ fun n ↦ (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) =
    (z ^ (a + 1))⁻¹ •
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)

pp: case convert_2
a : ℕ
z : ℂ
hz : z ≠ 0
this✝ :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
H : 1 / ‖z⁻¹ • 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹)
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0 ‖z‖ₑ
⊢ Set.EqOn ((z ^ (a + 1))⁻¹ • fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹) (fun x ↦ 1 / (z - x) ^ (a + 1))
    (Metric.eball 0 ‖z‖ₑ)

Tactic:
· ext n
    simp only [FormalMultilinearSeries.smul_apply, smul_apply,
      FormalMultilinearSeries.compContinuousLinearMap_apply]
    simp [add_assoc, pow_add _ _ (a + 1), mul_assoc]

Goal state after:
case convert_2
a : ℕ
z : ℂ
hz : z ≠ 0
this✝ :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)) ((z⁻¹ • 1) 0) 1
H : 1 / ‖z⁻¹ • 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹)
    ((FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑((a + n).choose a)).compContinuousLinearMap (z⁻¹ • 1)) 0 ‖z‖ₑ
⊢ Set.EqOn ((z ^ (a + 1))⁻¹ • fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹) (fun x ↦ 1 / (z - x) ^ (a + 1))
    (Metric.eball 0 ‖z‖ₑ)
Module: Mathlib.Analysis.Analytic.IteratedFDeriv

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
y : E
hy : y ∈ Metric.eball 0 r
⊢ n ∈ Finset.range (n + 1)

pp: case h₀
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
y : E
hy : y ∈ Metric.eball 0 r
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ n → ((q b) fun x ↦ y) = 0

Tactic:
· simp

Goal state after:
case h₀
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
h's : s ⊆ Metric.eball x r
I : insert x s ∩ Metric.eball x r = s
fcont : ContDiffOn 𝕜 (↑n) f s
g : E → F := fun z ↦ (p n) fun x_1 ↦ z - x
gcont : ContDiff 𝕜 ω g
q : FormalMultilinearSeries 𝕜 E F := fun k ↦ if h : n = k then h ▸ p n else 0
y : E
hy : y ∈ Metric.eball 0 r
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ n → ((q b) fun x ↦ y) = 0
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case refine_1
w x : ℂ
hw : w ≠ x
⊢ HasFPowerSeriesOnBall (fun z ↦ 1 / (z - w) ^ 2)
    (FormalMultilinearSeries.ofScalars ℂ fun i ↦ (↑i + 1) * (w - x) ^ (-↑(i + 2))) x ‖w - x‖ₑ

Tactic:
simpa only [sub_sub_sub_cancel_right, zero_add, sub_sq_comm w, zpow_neg, zpow_natCast, mul_comm]
      using (one_div_sub_sq_hasFPowerSeriesOnBall_zero
        (z := w - x) (by simp [sub_eq_zero, hw])).comp_sub x

Goal state after:
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_12
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ

pp: case convert_2
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ (1 + x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ (1 + x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
· simp

Goal state after:
case convert_2
a : ℝ
H : binomialSeries ℂ a = FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ ↑a)
this : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ ↑a) (binomialSeries ℂ a) (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ (1 + x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ (1 + x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))
Module: Mathlib.Analysis.Analytic.Binomial

Goal state before:
pp: case e'_12
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ

pp: case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))

Tactic:
· simp

Goal state after:
case convert_2
a : ℝ
this :
  HasFPowerSeriesOnBall (fun x ↦ 1 / (1 - x) ^ ↑a)
    (FormalMultilinearSeries.restrictScalars ℝ
      (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n))
    (Complex.ofRealCLM 0) 1
⊢ Set.EqOn (⇑Complex.reCLM ∘ (fun x ↦ 1 / (1 - x) ^ ↑a) ∘ ⇑Complex.ofRealCLM) (fun x ↦ 1 / (1 - x) ^ a)
    (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
s : Set X
ε K₁ : ℝ≥0
f : X → Y
hs : IsSeparated (↑ε) s
hf : AntilipschitzWith K₁ f
hK₁ : 0 < K₁
x : X
hx : x ∈ s
y : X
hy : y ∈ s
hne : f x ≠ f y
⊢ x ≠ y

Tactic:
by grind

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

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 0
⊢ (deriv fun x ↦ x ^ p) =O[atTop] fun x ↦ x ^ (p - 1)

Tactic:
case inr =>
    exact (isTheta_deriv_rpow_const_atTop hp).1

Goal state after:
Module: Mathlib.Topology.MetricSpace.Cover

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
f : X → Y
s N : Set X
ε K₂ : ℝ≥0
hs : IsCover ε s N
hf : LipschitzWith K₂ f
x : X
hx : x ∈ s
x₀ : X
hx₀ : x₀ ∈ N
hcover : edist x x₀ ≤ ↑ε
⊢ f x₀ = f x₀

Tactic:
by grind

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

Goal state before:
pp: case bot
y : EReal
h : ⊥ < y
⊢ ⊥.exp < y.exp

Tactic:
exp_bot,

Goal state after:
case bot
y : EReal
h : ⊥ < y
⊢ 0 < y.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe.top
a✝ : ℝ
h : ↑a✝ < ⊤
⊢ (↑a✝).exp < ⊤.exp

Tactic:
· simp

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

Goal state before:
pp: case bot
⊢ (-⊥).exp = ⊥.exp⁻¹

pp: case coe
a✝ : ℝ
⊢ (-↑a✝).exp = (↑a✝).exp⁻¹

pp: case top
⊢ (-⊤).exp = ⊤.exp⁻¹

Tactic:
· simp

Goal state after:
case coe
a✝ : ℝ
⊢ (-↑a✝).exp = (↑a✝).exp⁻¹

case top
⊢ (-⊤).exp = ⊤.exp⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top
⊢ (-⊤).exp = ⊤.exp⁻¹

Tactic:
· simp

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

Goal state before:
pp: case bot
y : EReal
⊢ (⊥ + y).exp = ⊥.exp * y.exp

pp: case coe
y : EReal
a✝ : ℝ
⊢ (↑a✝ + y).exp = (↑a✝).exp * y.exp

pp: case top
y : EReal
⊢ (⊤ + y).exp = ⊤.exp * y.exp

Tactic:
· simp

Goal state after:
case coe
y : EReal
a✝ : ℝ
⊢ (↑a✝ + y).exp = (↑a✝).exp * y.exp

case top
y : EReal
⊢ (⊤ + y).exp = ⊤.exp * y.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).exp = (↑a✝).exp * ⊥.exp

pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).exp = (↑a✝¹).exp * (↑a✝).exp

pp: case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).exp = (↑a✝).exp * ⊤.exp

Tactic:
· simp

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).exp = (↑a✝¹).exp * (↑a✝).exp

case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).exp = (↑a✝).exp * ⊤.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inl
y : ℝ≥0∞
⊢ (0 * y).log = log 0 + y.log

pp: case inr.inl
y : ℝ≥0∞
⊢ (∞ * y).log = ∞.log + y.log

pp: case inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * y).log = x.log + y.log

Tactic:
· simp

Goal state after:
case inr.inl
y : ℝ≥0∞
⊢ (∞ * y).log = ∞.log + y.log

case inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * y).log = x.log + y.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top.bot
⊢ (⊤ + ⊥).exp = ⊤.exp * ⊥.exp

pp: case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).exp = ⊤.exp * (↑a✝).exp

pp: case top.top
⊢ (⊤ + ⊤).exp = ⊤.exp * ⊤.exp

Tactic:
· simp

Goal state after:
case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).exp = ⊤.exp * (↑a✝).exp

case top.top
⊢ (⊤ + ⊤).exp = ⊤.exp * ⊤.exp
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: case top.top
⊢ (⊤ + ⊤).exp = ⊤.exp * ⊤.exp

Tactic:
· simp

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

Goal state before:
pp: case bot
⊢ ⊥.exp.log = ⊥

pp: case coe
a✝ : ℝ
⊢ (↑a✝).exp.log = ↑a✝

pp: case top
⊢ ⊤.exp.log = ⊤

Tactic:
· simp

Goal state after:
case coe
a✝ : ℝ
⊢ (↑a✝).exp.log = ↑a✝

case top
⊢ ⊤.exp.log = ⊤
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: case top
⊢ ⊤.exp.log = ⊤

Tactic:
· simp

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

Goal state before:
pp: case inr.inl.inr.inl
⊢ (∞ * ∞).log = ⊤ + ∞.log

pp: case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (∞ * y).log = ⊤ + y.log

Tactic:
· simp

Goal state after:
case inr.inl.inr.inr
y : ℝ≥0∞
y_real : 0 < y.toReal
⊢ (∞ * y).log = ⊤ + y.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * 0).log = ↑(Real.log x.toReal) + log 0

pp: case inr.inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * ∞).log = ↑(Real.log x.toReal) + ∞.log

pp: case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ (x * y).log = ↑(Real.log x.toReal) + y.log

Tactic:
· simp

Goal state after:
case inr.inr.inr.inl
x : ℝ≥0∞
x_real : 0 < x.toReal
⊢ (x * ∞).log = ↑(Real.log x.toReal) + ∞.log

case inr.inr.inr.inr
x y : ℝ≥0∞
x_real : 0 < x.toReal
y_real : 0 < y.toReal
⊢ (x * y).log = ↑(Real.log x.toReal) + y.log
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: case inr.inl
x : ℝ≥0∞
⊢ (x ^ 0).log = ↑0 * x.log

pp: case inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
⊢ (x ^ y).log = ↑y * x.log

Tactic:
· simp

Goal state after:
case inr.inr
x : ℝ≥0∞
y : ℝ
y_pos : 0 < y
⊢ (x ^ y).log = ↑y * x.log
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn =>
    simpa [pow_succ, ← mul_comm k, mul_assoc,
      superpolynomialDecay_param_mul_iff (k ^ n * f) hk] using hn

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
f'_meas : Measurable f'
t : Set α := ⋃ p, ⋃ q, u' ↑p ∩ v ↑p ↑q
⊢ ∑' (p : ↑s) (q : ↑(s ∩ Ioi ↑p)), μ (u ↑p ↑q ∩ v ↑p ↑q) = ∑' (p : ↑s) (x : ↑(s ∩ Ioi ↑p)), 0

Tactic:
by grind

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
x : ℝ
xA : x ∈ δ '' A
⊢ x ≤ R

Tactic:
rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩

Goal state after:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
a' : ι
ha' : a' ∈ A
xA : δ a' ∈ δ '' A
⊢ δ a' ≤ R
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: α : Type u_1
u : α → ℕ → ℝ≥0∞
s : Set α
hs : s.Finite
⊢ expGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, expGrowthSup (u x)

Tactic:
have := map_finset_sup expGrowthSupBotHom hs.toFinset u
  simpa only [expGrowthSupBotHom, SupBotHom.coe_mk, SupHom.coe_mk, Finset.sup_eq_iSup,
    hs.mem_toFinset, comp_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
x : ℝ
xA : x ∈ δ '' A
hx : m / τ < x
⊢ ∃ a' ∈ A, m / τ ≤ δ a'

Tactic:
rcases (mem_image _ _ _).1 xA with ⟨a', ha', rfl⟩

Goal state after:
case inr
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
u : Set ι
hu : Maximal (fun x ↦ x ∈ T) u
a : ι
hat : a ∈ t
hcon : ∀ b ∈ u, (B a ∩ B b).Nonempty → τ * δ b < δ a
a_disj : ∀ c ∈ u, Disjoint (B a) (B c)
A : Set ι := {a' | a' ∈ t ∧ ∀ c ∈ u, Disjoint (B a') (B c)}
Anonempty : A.Nonempty
m : ℝ := sSup (δ '' A)
bddA : BddAbove (δ '' A)
this : 0 ≤ m
mpos : 0 < m
I : m / τ < m
a' : ι
ha' : a' ∈ A
xA : δ a' ∈ δ '' A
hx : m / τ < δ a'
⊢ ∃ a' ∈ A, m / τ ≤ δ a'
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂0 ≠ ∞
⊢ ⨍⁻ (x : α), f x ∂0 < ∞

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hμ : μ ≠ 0
⊢ ⨍⁻ (x : α), f x ∂μ < ∞

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hμ : μ ≠ 0
⊢ ⨍⁻ (x : α), f x ∂μ < ∞
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
inst✝ : IsFiniteMeasure 0
⊢ (⨍⁻ (a : α), f a ∂0) * 0 univ = ∫⁻ (x : α), f x ∂0

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
⊢ (⨍⁻ (a : α), f a ∂μ) * μ univ = ∫⁻ (x : α), f x ∂μ

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
⊢ (⨍⁻ (a : α), f a ∂μ) * μ univ = ∫⁻ (x : α), f x ∂μ
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ
hf : Integrable f 0
hf₀ : 0 ≤ᵐ[0] f
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂0) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂0) / 0 univ

pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᵐ[μ] f
hμ : μ ≠ 0
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ univ

Tactic:
· simp

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᵐ[μ] f
hμ : μ ≠ 0
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) = (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) / μ univ
Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∫⁻ (x : α) in ∅, f x ∂μ = ∫⁻ (x : α) in ∅, g x ∂μ

pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ (t : Set α),
    MeasurableSet t →
      ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ → ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ

pp: case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ (f_1 : ℕ → Set α),
    Pairwise (Function.onFun Disjoint f_1) →
      (∀ (i : ℕ), MeasurableSet (f_1 i)) →
        (∀ (i : ℕ), ∫⁻ (x : α) in f_1 i, f x ∂μ = ∫⁻ (x : α) in f_1 i, g x ∂μ) →
          ∫⁻ (x : α) in ⋃ i, f_1 i, f x ∂μ = ∫⁻ (x : α) in ⋃ i, f_1 i, g x ∂μ

Tactic:
· simp

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ (t : Set α),
    MeasurableSet t →
      ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ → ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ

case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ (f_1 : ℕ → Set α),
    Pairwise (Function.onFun Disjoint f_1) →
      (∀ (i : ℕ), MeasurableSet (f_1 i)) →
        (∀ (i : ℕ), ∫⁻ (x : α) in f_1 i, f x ∂μ = ∫⁻ (x : α) in f_1 i, g x ∂μ) →
          ∫⁻ (x : α) in ⋃ i, f_1 i, f x ∂μ = ∫⁻ (x : α) in ⋃ i, f_1 i, g x ∂μ