mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ CauchySeq u

Tactic:
refine cauchySeq_of_le_geometric _ (↑f'symm.nnnorm * dist (f b) y) Icf' fun n ↦ ?_

Goal state after:
𝕜 : 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
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := fun x ↦ x + f'symm.toFun (y - f x)
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := fun n ↦ g^[n] b
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
D :
  ∀ (n : ℕ),
    dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
      dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
n : ℕ
⊢ dist (u n) (u (n + 1)) ≤ ↑f'symm.nnnorm * dist (f b) y * (↑c * ↑f'symm.nnnorm) ^ n
Module: Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
habc : ↑k = -a ∨ ↑k = -b ∨ ↑k = -c
hk : k < n
⊢ ofScalars 𝔸 (ordinaryHypergeometricCoefficient a b c) n = 0

Tactic:
ofScalars

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
n k : ℕ
habc : ↑k = -a ∨ ↑k = -b ∨ ↑k = -c
hk : k < n
⊢ ordinaryHypergeometricCoefficient a b c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸 = 0
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CharZero 𝕜
inst✝ : CompleteSpace E
z₀ : 𝕜
n : ℕ
f : 𝕜 → E
hf : AnalyticAt 𝕜 f z₀
IH : analyticOrderAt (deriv f) z₀ = ↑n ↔ (∀ k < n, iteratedDeriv (k + 1) f z₀ = 0) ∧ iteratedDeriv (n + 1) f z₀ ≠ 0
ho : analyticOrderAt f z₀ = ↑(n + 1)
h_zero : ∀ k < n, iteratedDeriv (k + 1) f z₀ = 0
h_nz : iteratedDeriv (n + 1) f z₀ ≠ 0
k : ℕ
hk : 0 < n + 1
⊢ iteratedDeriv 0 f z₀ = 0

Tactic:
rw [iteratedDeriv_zero, ← hf.analyticOrderAt_ne_zero, ho, Nat.cast_add_one]
             exact Nat.cast_add_one_ne_zero _

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

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
g : 𝕜 → 𝕜
z₀ : 𝕜
hf : AnalyticAt 𝕜 f (g z₀)
hg : AnalyticAt 𝕜 g z₀
hg_nc : EventuallyConst g (𝓝 z₀)
⊢ analyticOrderAt (f ∘ g) z₀ = analyticOrderAt f (g z₀) * analyticOrderAt (fun x ↦ g x - g z₀) z₀

Tactic:
have := hg_nc.comp f
    rw [eventuallyConst_iff_analyticOrderAt_sub_eq_top] at hg_nc this
    rw [hg_nc]
    by_cases hf' : f (g z₀) = 0
    · simpa [hf', show analyticOrderAt f (g z₀) ≠ 0 by grind [analyticOrderAt_ne_zero]]
    · rw [show analyticOrderAt f (g z₀) = 0 from ?_, zero_mul] <;>
      grind [hf.comp hg, AnalyticAt.analyticOrderAt_eq_zero]

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

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * (-1 * -1) - cexp (x * I) * (1 * I) * I) * 2⁻¹

Tactic:
neg_one_mul,

Goal state after:
case e'_9
x : ℂ
⊢ (cexp (x * I) + cexp (-x * I)) * 2⁻¹ = (cexp (-x * I) * - -1 - cexp (x * I) * (1 * I) * I) * 2⁻¹
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : AddCommMonoid R
inst✝¹ : Pow R ℕ
inst✝ : BinomialRing R
r : R
⊢ multichoose r 0 = r ^ 0

Tactic:
by
  rw [← nsmul_right_inj (Nat.factorial_ne_zero 0),
    factorial_nsmul_multichoose_eq_ascPochhammer, ascPochhammer_zero, smeval_one, Nat.factorial]

Goal state after:
Module: Mathlib.RingTheory.Binomial

Goal state before:
pp: R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ((r + 1) ^ 1 + (↑k).smeval (r + 1)) * (ascPochhammer ℕ k).smeval (r + 1) =
    k.succ • k.factorial • multichoose (r + 1) k + r ^ 1 * (ascPochhammer ℕ k).smeval (r ^ 1 + smeval 1 r)

Tactic:
factorial_nsmul_multichoose_eq_ascPochhammer

Goal state after:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
r : R
k : ℕ
⊢ ((r + 1) ^ 1 + (↑k).smeval (r + 1)) * (ascPochhammer ℕ k).smeval (r + 1) =
    k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r ^ 1 * (ascPochhammer ℕ k).smeval (r ^ 1 + smeval 1 r)
Module: Mathlib.Analysis.Meromorphic.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
c : 𝕜
U : Set 𝕜
⊢ MeromorphicOn (f ∘ fun x ↦ x - c) U ↔ MeromorphicOn f (U - {c})

Tactic:
by
  simp_rw [sub_eq_add_neg, meromorphicOn_comp_add_const_iff_meromorphicOn, neg_singleton]

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

Goal state before:
pp: f : ℂ → ℂ
x : ℂ
hf : DifferentiableAt ℂ f x
c : ℂ
⊢ deriv (fun x ↦ c ^ f x) x = log c * deriv f x * c ^ f x

Tactic:
rw [← derivWithin_univ, derivWithin_const_cpow, derivWithin_univ]
  rwa [differentiableWithinAt_univ]

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

Goal state before:
pp: 𝕂 : Type v
inst✝² : RCLike 𝕂
𝔸 : Type u
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
k✝ : ℕ
| a ≠ ↑k✝

Tactic:
rw [ne_comm]

Goal state after:
𝕂 : Type v
inst✝² : RCLike 𝕂
𝔸 : Type u
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
a : 𝕂
ha : ∀ (k : ℕ), a ≠ ↑k
k✝ : ℕ
| ↑k✝ ≠ a
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y ↦ -(-↑y) ^ (r + 1) * cexp (↑π * I * r)) ((r + 1) * (-↑x) ^ r * cexp (↑π * I * r)) x

Tactic:
← ofReal_neg

Goal state after:
case inr
x : ℝ
hx✝ : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, ↑y ^ (r + 1) / (r + 1) = (-↑y) ^ (r + 1) * cexp (↑π * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun y ↦ -↑(-y) ^ (r + 1) * cexp (↑π * I * r)) ((r + 1) * ↑(-x) ^ r * cexp (↑π * I * r)) x
Module: Mathlib.Analysis.Analytic.RadiusLiminf

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
| ↑r ≤ (↑(‖p n‖₊ ^ (1 / ↑n)))⁻¹

Tactic:
ENNReal.le_inv_iff_mul_le,

Goal state after:
𝕜 : 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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
n : ℕ
hn : 0 < n
this : 0 < ↑n
| ↑r * ↑(‖p n‖₊ ^ (1 / ↑n)) ≤ 1
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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ (∑ σ_1, (p n) fun i ↦ (v ∘ ⇑σ) (σ_1 i)) = (iteratedFDerivWithin 𝕜 n f s x) v

Tactic:
hp.iteratedFDerivWithin_eq_sum h hs hx

Goal state after:
𝕜 : 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 : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ (∑ σ_1, (p n) fun i ↦ (v ∘ ⇑σ) (σ_1 i)) = ∑ σ, (p n) fun i ↦ v (σ i)
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (fun x ↦ (↑x * b.log).exp) Filter.atTop (𝓝 0)

Tactic:
refine EReal.tendsto_exp_nhds_bot_nhds_zero.comp ?_

Goal state after:
b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (fun x ↦ ↑x * b.log) Filter.atTop (𝓝 ⊥)
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (fun x ↦ (↑x * b.log).exp) Filter.atBot (𝓝 0)

Tactic:
refine EReal.tendsto_exp_nhds_bot_nhds_zero.comp ?_

Goal state after:
b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (fun x ↦ ↑x * b.log) Filter.atBot (𝓝 ⊥)
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
⊢ (linearGrowthInf fun x ↦ v x + b) ≤ linearGrowthInf v

Tactic:
rcases eq_bot_or_bot_lt b with rfl | b_bot

Goal state after:
case inl
u v : ℕ → EReal
hb : ⊥ ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥
⊢ (linearGrowthInf fun x ↦ v x + ⊥) ≤ linearGrowthInf v

case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthInf fun x ↦ v x + b) ≤ linearGrowthInf v
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
l : Filter α
k : α → β
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * 0 a) l (𝓝 0)

Tactic:
by simpa only [Pi.zero_apply, mul_zero] using tendsto_const_nhds

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
⊢ (linearGrowthSup fun x ↦ v x + b) ≤ linearGrowthSup v

Tactic:
rcases eq_bot_or_bot_lt b with rfl | b_bot

Goal state after:
case inl
u v : ℕ → EReal
hb : ⊥ ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥
⊢ (linearGrowthSup fun x ↦ v x + ⊥) ≤ linearGrowthSup v

case inr
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthSup fun x ↦ v x + b) ≤ linearGrowthSup v
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
n : ℕ
b_uvn : b * ↑(v n) ≤ u (v n)
n_0 : 0 < n
a_vn : a * ↑n ≤ ↑(v n)
⊢ a * b * ↑n ≤ (u ∘ v) n

Tactic:
rw [comp_apply, mul_comm a b, mul_assoc b a]

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
n : ℕ
b_uvn : b * ↑(v n) ≤ u (v n)
n_0 : 0 < n
a_vn : a * ↑n ≤ ↑(v n)
⊢ b * (a * ↑n) ≤ u (v n)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * ↑(v n)
n : ℕ
uvn_b : u (v n) ≤ b * ↑(v n)
n_0 : 0 < n
vn_a : ↑(v n) ≤ a * ↑n
⊢ (u ∘ v) n ≤ a * b * ↑n

Tactic:
rw [comp_apply, mul_comm a b, mul_assoc b a]

Goal state after:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * ↑(v n)
n : ℕ
uvn_b : u (v n) ≤ b * ↑(v n)
n_0 : 0 < n
vn_a : ↑(v n) ≤ a * ↑n
⊢ u (v n) ≤ b * (a * ↑n)
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case pos
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : u = ⊥
⊢ linearGrowthInf (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthInf u

Tactic:
rw [u_0, Pi.bot_comp, linearGrowthInf_bot]; exact bot_le

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

Goal state before:
pp: case neg
α : 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
p q : β
H : ¬(p ∈ s ∧ q ∈ s ∧ p < q)
⊢ ∃ u v,
    MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → μ (u ∩ v) = 0)

Tactic:
refine
        ⟨univ, univ, MeasurableSet.univ, MeasurableSet.univ, subset_univ _, subset_univ _,
          fun ps qs pq => ?_⟩

Goal state after:
case neg
α : 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
p q : β
H : ¬(p ∈ s ∧ q ∈ s ∧ p < q)
ps : p ∈ s
qs : q ∈ s
pq : p < q
⊢ μ (univ ∩ univ) = 0
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg.inr.refine_2
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n
u_b : ∃ᶠ (x : ℕ) in atTop, (u x ≤ b * ↑x ∧ 0 < x) ∧ ∃ m, a⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a'⁻¹ * ↑x
M M' : ℕ
aM_M' : a * ↑M ≤ ↑M'
n : ℕ
n_M' : M' ≤ n
un_bn : u n ≤ b * ↑n
right✝ : 0 < n
k : ℕ
an_k : a⁻¹ * ↑n ≤ ↑k
k_an' : ↑k ≤ a'⁻¹ * ↑n
vk_ak' : ↑(v k) ≤ a' * ↑k
⊢ (u ∘ v) k ≤ a * b * ↑k

Tactic:
rw [comp_apply, mul_comm a b, mul_assoc b a]

Goal state after:
case neg.inr.refine_2
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n
u_b : ∃ᶠ (x : ℕ) in atTop, (u x ≤ b * ↑x ∧ 0 < x) ∧ ∃ m, a⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a'⁻¹ * ↑x
M M' : ℕ
aM_M' : a * ↑M ≤ ↑M'
n : ℕ
n_M' : M' ≤ n
un_bn : u n ≤ b * ↑n
right✝ : 0 < n
k : ℕ
an_k : a⁻¹ * ↑n ≤ ↑k
k_an' : ↑k ≤ a'⁻¹ * ↑n
vk_ak' : ↑(v k) ≤ a' * ↑k
⊢ u (v k) ≤ b * (a * ↑k)
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 1 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
⊢ expGrowthSup (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * expGrowthSup u

Tactic:
apply linearGrowthSup_comp_le (u := log ∘ u) (hu.mono fun n h ↦ ?_) hv₀ hv₁ hv₂

Goal state after:
u : ℕ → ℝ≥0∞
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 1 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
n : ℕ
h : 1 ≤ u n
⊢ 0 ≤ (log ∘ u) n
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg.refine_2
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)
b_u : ∃ᶠ (x : ℕ) in atTop, (b * ↑x ≤ u x ∧ 0 < x) ∧ ∃ m, a'⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a⁻¹ * ↑x
M M' : ℕ
aM_M' : a' * ↑M ≤ ↑M'
n : ℕ
n_M' : M' ≤ n
bn_un : b * ↑n ≤ u n
right✝ : 0 < n
k : ℕ
an_k' : a'⁻¹ * ↑n ≤ ↑k
k_an : ↑k ≤ a⁻¹ * ↑n
ak_vk' : a' * ↑k ≤ ↑(v k)
⊢ a * b * ↑k ≤ (u ∘ v) k

Tactic:
rw [comp_apply, mul_comm a b, mul_assoc b a]

Goal state after:
case neg.refine_2
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
v_0 : 0 < linearGrowthInf fun n ↦ ↑(v n)
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * ↑n ≤ ↑(v n)
b_u : ∃ᶠ (x : ℕ) in atTop, (b * ↑x ≤ u x ∧ 0 < x) ∧ ∃ m, a'⁻¹ * ↑x ≤ ↑m ∧ ↑m ≤ a⁻¹ * ↑x
M M' : ℕ
aM_M' : a' * ↑M ≤ ↑M'
n : ℕ
n_M' : M' ≤ n
bn_un : b * ↑n ≤ u n
right✝ : 0 < n
k : ℕ
an_k' : a'⁻¹ * ↑n ≤ ↑k
k_an : ↑k ≤ a⁻¹ * ↑n
ak_vk' : a' * ↑k ≤ ↑(v k)
⊢ b * (a * ↑k) ≤ u (v k)
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 ∂μ
A : ∀ (ε N : ℝ≥0) (p : ℕ), 0 < ε → μ ({x | g x + ↑ε ≤ f x ∧ g x ≤ ↑N} ∩ spanningSets μ p) = 0
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : ℕ → Set α := fun n ↦ {x | g x + ↑(u n) ≤ f x ∧ g x ≤ ↑↑n} ∩ spanningSets μ n
μs : ∀ (n : ℕ), μ (s n) = 0
B : {x | f x ≤ g x}ᶜ ⊆ ⋃ n, s n
⊢ ∑' (n : ℕ), μ (s n) = 0

Tactic:
by simp only [μs, tsum_zero]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ∞ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
⊢ f =ᵐ[μ] g

Tactic:
by
  have hf' : AEFinStronglyMeasurable f μ :=
    ENNReal.aefinStronglyMeasurable_of_aemeasurable hfi hf
  have hg' : AEFinStronglyMeasurable g μ :=
    ENNReal.aefinStronglyMeasurable_of_aemeasurable hgi hg
  let s := hf'.sigmaFiniteSet
  let t := hg'.sigmaFiniteSet
  suffices f =ᵐ[μ.restrict (s ∪ t)] g by
    refine ae_of_ae_restrict_of_ae_restrict_compl _ this ?_
    simp only [Set.compl_union]
    have h1 : f =ᵐ[μ.restrict sᶜ] 0 := hf'.ae_eq_zero_compl
    have h2 : g =ᵐ[μ.restrict tᶜ] 0 := hg'.ae_eq_zero_compl
    rw [ae_restrict_iff' (hf'.measurableSet.compl.inter hg'.measurableSet.compl)]
    rw [EventuallyEq, ae_restrict_iff' hf'.measurableSet.compl] at h1
    rw [EventuallyEq, ae_restrict_iff' hg'.measurableSet.compl] at h2
    filter_upwards [h1, h2] with x h1 h2 hx
    rw [h1 (Set.inter_subset_left hx), h2 (Set.inter_subset_right hx)]
  refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf.restrict hg.restrict
    fun u hu huμ ↦ ?_
  rw [Measure.restrict_restrict hu]
  rw [Measure.restrict_apply hu] at huμ
  exact hfg (hu.inter (hf'.measurableSet.union hg'.measurableSet)) huμ

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst✝ : IsProbabilityMeasure μ
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ 0 < μ {x | ∫⁻ (a : α), f a ∂μ ≤ f x}

Tactic:
by
  simpa only [laverage_eq_lintegral] using
    measure_laverage_le_pos (IsProbabilityMeasure.ne_zero μ) hint

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + (ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν))

Tactic:
conv_rhs => rw [add_assoc, add_comm (μ₂.singularPart ν), ← add_assoc, ← add_assoc]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst✝¹ : μ₁.HaveLebesgueDecomposition ν
inst✝ : μ₂.HaveLebesgueDecomposition ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ μ.withDensity ((r • ν).rnDeriv μ) = μ.withDensity (r • ν.rnDeriv μ)

Tactic:
simp_rw [ENNReal.smul_def]

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ μ.withDensity ((↑r • ν).rnDeriv μ) = μ.withDensity (↑r • ν.rnDeriv μ)
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)

Tactic:
simp_rw [ENNReal.smul_def]

Goal state after:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : IsFiniteMeasure ν
inst✝ : ν.HaveLebesgueDecomposition μ
r : ℝ≥0
hr : r ≠ 0
⊢ (↑r • μ).withDensity (ν.rnDeriv (↑r • μ)) = (↑r • μ).withDensity (↑r⁻¹ • ν.rnDeriv μ)