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

Goal state before:
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‖ₑ
w : ℂ
⊢ w ∈ Metric.eball 0 ‖z‖ₑ →
    ((z ^ (a + 1))⁻¹ • fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹) w = (fun x ↦ 1 / (z - x) ^ (a + 1)) w

Tactic:
hw

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‖ₑ
w : ℂ
hw : w ∈ Metric.eball 0 ‖z‖ₑ
⊢ ((z ^ (a + 1))⁻¹ • fun x ↦ ((1 - (z⁻¹ • ⇑1) x) ^ (a + 1))⁻¹) w = (fun x ↦ 1 / (z - x) ^ (a + 1)) w
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case e'_9
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x ↦ x.1 ^ x.2) ∘ fun x ↦ (id x, p))
    ((((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ p * x ^ (p - 1) =
    (((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0)

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: case e'_10
a b : ℂ
n✝ : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℂ (fun n ↦ a * ↑n + b) n✝) fun x ↦ 1) =
    (((b - a) • FormalMultilinearSeries.ofScalars ℂ 1 + a • FormalMultilinearSeries.ofScalars ℂ fun n ↦ ↑n + 1) n✝)
      fun x ↦ 1

Tactic:
simp

Goal state after:
case e'_10
a b : ℂ
n✝ : ℕ
⊢ a * ↑n✝ + b = b - a + a * (↑n✝ + 1)
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (fun x ↦ x ^ r) 0
y : ℝ := deriv (fun x ↦ x ^ r) 0
x : ℝ
hx : 0 < x
⊢ x ^ 1 * x ^ (r - 1) = x * x ^ (r - 1)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
ihn : ∀ {p : ℝ}, ↑n ≤ p → ContDiff ℝ ↑n fun x ↦ x ^ p
p : ℝ
h : ↑(n + 1) ≤ p
⊢ 1 ≤ ↑(n + 1)

Tactic:
simp

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

Goal state before:
pp: case refine_2.convert_11
w x : ℂ
hw : w ≠ x
⊢ 0 < ‖w - x‖ₑ

Tactic:
· simpa [sub_eq_zero]

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‖ₑ

Tactic:
simp

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

Goal state before:
pp: case zero
r x : ℝ
⊢ (deriv^[0] fun x ↦ x ^ r) = fun x ↦ Polynomial.eval r (descPochhammer ℝ 0) * x ^ (r - ↑0)

Tactic:
simp

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

Goal state before:
pp: case e'_10
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
n : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun n ↦ Ring.choose (a + ↑n - 1) n) n) fun x ↦ 1) =
    Complex.reCLM
      ((FormalMultilinearSeries.restrictScalars ℝ
          (FormalMultilinearSeries.ofScalars ℂ fun n ↦ Ring.choose (↑a + ↑n - 1) n) n)
        (⇑Complex.ofRealCLM ∘ fun x ↦ 1))

Tactic:
simp

Goal state after:
case e'_10
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
n : ℕ
⊢ Ring.choose (a + ↑n - 1) n = (Ring.choose (↑a + ↑n - 1) n).re
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‖ₑ

Tactic:
simp

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

Goal state before:
pp: f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    ((g x * f x ^ (g x - 1)) • ContinuousLinearMap.toSpanSingleton ℝ f' +
        (f x ^ g x * Real.log (f x)) • ContinuousLinearMap.toSpanSingleton ℝ g')
      1

Tactic:
simp

Goal state after:
f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    g x * f x ^ (g x - 1) * f' + f x ^ g x * Real.log (f x) * g'
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

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

Tactic:
by
  rcases eq_or_ne p 0 with rfl | hp
  case inl =>
    simp [zero_sub, Real.rpow_neg_one, Real.rpow_zero, deriv_const', Asymptotics.isBigO_zero]
  case inr =>
    exact (isTheta_deriv_rpow_const_atTop hp).1

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

Goal state before:
pp: case e'_10
a b : ℝ
n✝ : ℕ
⊢ ((FormalMultilinearSeries.ofScalars ℝ (fun x ↦ a * ↑x + b) n✝) fun x ↦ 1) =
    (((b - a) • FormalMultilinearSeries.ofScalars ℝ 1 + a • FormalMultilinearSeries.ofScalars ℝ fun n ↦ ↑n + 1) n✝)
      fun x ↦ 1

Tactic:
simp

Goal state after:
case e'_10
a b : ℝ
n✝ : ℕ
⊢ a * ↑n✝ + b = b - a + a * (↑n✝ + 1)
Module: Mathlib.Topology.MetricSpace.MetricSeparated

Goal state before:
pp: case empty
X : Type u_1
inst✝ : PseudoEMetricSpace X
ι : Type u_3
I : Set ι
s : ι → Set X
t : Set X
⊢ AreSeparated (⋃ i ∈ ∅, s i) t ↔ ∀ i ∈ ∅, AreSeparated (s i) t

Tactic:
simp

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
ε δ : ℝ≥0
s t N N₁ N₂ : Set X
x : X
⊢ ∀ (a : X), (a, a) ∈ {(x, y) | edist x y ≤ ↑ε}

Tactic:
simp

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

Goal state before:
pp: 𝕜 : 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
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ ω = ∞ → ω = ω

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
s : Set X
x : X
hA : ediam s ≤ ↑ε
hx : x ∈ s
x✝ : X
h_mem : x✝ ∈ s
⊢ x ∈ {x}

Tactic:
simp

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

Goal state before:
pp: case bot
⊢ ⊥.exp = ∞ ↔ ⊥ = ⊤

Tactic:
simp

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

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (↑a✝).exp = ∞ ↔ ↑a✝ = ⊤

Tactic:
simp

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

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

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case h
⊢ log 0 = ⊥

Tactic:
simp

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

Goal state before:
pp: case h
⊢ ∞.log = ⊤

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: ⊢ 1 = exp 0

Tactic:
simp

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

Goal state before:
pp: case convert_2
b : ℝ≥0∞
hb : 1 < b
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊥

Tactic:
simp

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

Goal state before:
pp: case convert_3
b : ℝ≥0∞
hb : 1 < b
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊤

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: case convert_2
b : ℝ≥0∞
hb : b < 1
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊥

Tactic:
simp

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

Goal state before:
pp: case convert_3
b : ℝ≥0∞
hb : b < 1
⊢ ⊤ ≠ 0 ∨ b.log ≠ ⊤

Tactic:
simp

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

Goal state before:
pp: case convert_2
b : ℝ≥0∞
hb : 1 < b
⊢ ⊥ ≠ 0 ∨ b.log ≠ ⊥

Tactic:
simp

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

Goal state before:
pp: case convert_3
b : ℝ≥0∞
hb : 1 < b
⊢ ⊥ ≠ 0 ∨ b.log ≠ ⊤

Tactic:
simp

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

Goal state before:
pp: case convert_2
b : ℝ≥0∞
hb : b < 1
⊢ ⊥ ≠ 0 ∨ b.log ≠ ⊥

Tactic:
simp

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

Goal state before:
pp: case convert_3
b : ℝ≥0∞
hb : b < 1
⊢ ⊥ ≠ 0 ∨ b.log ≠ ⊤

Tactic:
simp

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

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

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ 0 ≠ ⊥

Tactic:
· exact Or.inr EReal.zero_ne_bot

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊤ ∨ 0 ≠ ⊥

Tactic:
· exact Or.inr EReal.zero_ne_bot

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: case zero
α : 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
⊢ SuperpolynomialDecay l k (k ^ 0 * f) ↔ SuperpolynomialDecay l k f

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ linearGrowthInf (⨅ x ∈ Set.univ, u x) = ⨅ i, linearGrowthInf (u i)

Tactic:
linearGrowthInf_biInf u Set.finite_univ,

Goal state after:
ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ ⨅ x ∈ Set.univ, linearGrowthInf (u x) = ⨅ i, linearGrowthInf (u i)
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
x : α
⊢ (fun a ↦ k a ^ z)⁻¹ x = k x ^ (-z)

Tactic:
simp

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

Goal state before:
pp: case inl
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun x ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : t ∈ v.setsAt x
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
exact ⟨t, ⟨tf, h't⟩, ht.trans (closedBall_subset_closedBall (min_le_left _ _))⟩

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: case inr
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun x ↦ b * v x) ≤ expGrowthSup v

Tactic:
apply (expGrowthSup_mul_le _ _).trans_eq

Goal state after:
case inr
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun x ↦ b) + expGrowthSup v = expGrowthSup v

u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun x ↦ b) ≠ ⊥ ∨ expGrowthSup v ≠ ⊤

u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun x ↦ b) ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
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 (Set ι)
UT : U ⊆ T
hU : IsChain (fun x1 x2 ↦ x1 ⊆ x2) U
⊢ (∀ t' ∈ U, t' ⊆ t) ∧
    (⋃₀ U).PairwiseDisjoint B ∧
      ∀ a ∈ t,
        ∀ (b : ι), ∀ x ∈ U, b ∈ x → (B a ∩ B b).Nonempty → ∃ c, (∃ t ∈ U, c ∈ t) ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c

Tactic:
refine
      ⟨fun u hu => (UT hu).1, (pairwiseDisjoint_sUnion hU.directedOn).2 fun u hu => (UT hu).2.1,
        fun a hat b u uU hbu hab => ?_⟩

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 (Set ι)
UT : U ⊆ T
hU : IsChain (fun x1 x2 ↦ x1 ⊆ x2) U
a : ι
hat : a ∈ t
b : ι
u : Set ι
uU : u ∈ U
hbu : b ∈ u
hab : (B a ∩ B b).Nonempty
⊢ ∃ c, (∃ t ∈ U, c ∈ t) ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ (u + v) n ≤ 2 * max (u n) (v n)

Tactic:
Pi.add_apply u v n,

Goal state after:
case a
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ u n + v n ≤ 2 * max (u n) (v n)
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x : ι → α
r : ι → ℝ
R τ : ℝ
hτ : 3 < τ
hr : ∀ a ∈ ∅, r a ≤ R
⊢ ∀ a ∈ ∅, ∃ b ∈ ∅, closedBall (x a) (r a) ⊆ closedBall (x b) (τ * r b)

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x : ι → α
r : ι → ℝ
R τ : ℝ
hτ : 3 < τ
hr : ∀ a ∈ ∅, r a ≤ R
⊢ ∀ a ∈ ∅, ∃ b ∈ ∅, ball (x a) (r a) ⊆ ball (x b) (τ * r b)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p
s_lt_top : μ s < ∞
A : ∫⁻ (x : α) in s, g x ∂μ + ↑ε * μ s ≤ ∫⁻ (x : α) in s, g x ∂μ + 0
⊢ μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0

Tactic:
have B : (∫⁻ x in s, g x ∂μ) ≠ ∞ :=
      (setLIntegral_lt_top_of_le_nnreal s_lt_top.ne ⟨N, fun _ h ↦ h.1.2⟩).ne

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p
s_lt_top : μ s < ∞
A : ∫⁻ (x : α) in s, g x ∂μ + ↑ε * μ s ≤ ∫⁻ (x : α) in s, g x ∂μ + 0
B : ∫⁻ (x : α) in s, g x ∂μ ≠ ∞
⊢ μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
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

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

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

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure α
f g : α → E
h : f =ᵐ[μ] g
⊢ ⨍ (x : α), f x ∂μ = ⨍ (x : α), g x ∂μ

Tactic:
simp only [average_eq, integral_congr_ae h]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
⊢ ∫ (x : α), ⨍ (a : α), f a ∂μ ∂μ = ∫ (x : α), f x ∂μ

Tactic:
simp

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

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Average

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.restrict s)
hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞
⊢ (⨍⁻ (x : α) in s, f x ∂μ).toReal = ⨍ (x : α) in s, (f x).toReal ∂μ

Tactic:
simpa [laverage_eq] using toReal_laverage hf hf'

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

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ ≤ sInf {d | μ ≤ d + 0}

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Sub

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
⊢ μ ∅ - ν ∅ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ μ = (μ, 0).1 + ν.withDensity (μ, 0).2

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ = (0, 1).1 + μ.withDensity (0, 1).2

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : r = 0
⊢ μ = (μ, 0).1 + (r • ν).withDensity (μ, 0).2

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = ↑r⁻¹ • μ.rnDeriv ν
⊢ μ = (μ.singularPart ν, (↑r)⁻¹ • μ.rnDeriv ν).1 + ((↑r)⁻¹ * ↑r) • ν.withDensity (μ.rnDeriv ν)

Tactic:
ENNReal.inv_mul_cancel,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = ↑r⁻¹ • μ.rnDeriv ν
⊢ μ = (μ.singularPart ν, (↑r)⁻¹ • μ.rnDeriv ν).1 + 1 • ν.withDensity (μ.rnDeriv ν)

case neg.h0
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = ↑r⁻¹ • μ.rnDeriv ν
⊢ ↑r ≠ 0

case neg.ht
α : Type u_1
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = ↑r⁻¹ • μ.rnDeriv ν
⊢ ↑r ≠ ∞