mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv

Goal state before:
pp: case inr
c : ℂ
hc : c ≠ 0
⊢ (deriv fun x ↦ ↑x ^ c) =O[atTop] fun x ↦ x ^ (c.re - 1)

Tactic:
exact (isTheta_deriv_ofReal_cpow_const_atTop hc).1

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

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

Tactic:
simp_rw [exp_coe]
      exact ENNReal.ofReal_lt_ofReal_iff'.mpr ⟨Real.exp_strictMono (mod_cast h), Real.exp_pos _⟩

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

Goal state before:
pp: x : ℝ≥0∞
n : ℕ
⊢ (x ^ n).log = ↑n * x.log

Tactic:
← rpow_natCast,

Goal state after:
x : ℝ≥0∞
n : ℕ
⊢ (x ^ ↑n).log = ↑n * x.log
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ (v.enlarge δ δpos).filterAt = v.filterAt

Tactic:
ext1 x

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
⊢ (v.enlarge δ δpos).filterAt x = v.filterAt x
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 : ↑n / a ≤ ↑k
k_an' : a' * ↑k ≤ ↑n
vk_ak' : ↑(v k) ≤ a' * ↑k
⊢ u (v k) ≤ b * (a * ↑k)

Tactic:
div_le_iff_le_mul a_0 a_top

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 : ↑n ≤ a * ↑k
k_an' : a' * ↑k ≤ ↑n
vk_ak' : ↑(v k) ≤ a' * ↑k
⊢ u (v k) ≤ b * (a * ↑k)
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]
    rw [← EReal.div_eq_inv_mul, le_div_iff_mul_le a_0' (ne_top_of_lt a_a'), mul_comm] at k_an'
    rw [← EReal.div_eq_inv_mul, div_le_iff_le_mul a_0 a_top] at an_k
    have vk_n := Nat.cast_le.1 (vk_ak'.trans k_an')
    exact (h vk_n).trans <| un_bn.trans <| by gcongr

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

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

Tactic:
laverage_eq

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

Goal state before:
pp: case inl
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
⊢ μ.real univ • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ

Tactic:
rw [hμ, integral_zero_measure, average_zero_measure, smul_zero]

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 : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : μ s ≠ ∞
htμ : μ t ≠ ∞
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < μ.real s
ht₀ : 0 < μ.real t
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

Tactic:
exact mem_openSegment_iff_div.mpr
    ⟨μ.real s, μ.real t, hs₀, ht₀, (average_union hd ht hsμ htμ hfs hft).symm⟩

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
x✝ : μ s < ∞
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]

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

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
x✝ : μ s < ∞
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ

Tactic:
rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]

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

Goal state before:
pp: case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ ∃ b ∈ (fun μ ↦ μ.restrict s) '' {d | μ ≤ d + ν}, b ≤ ν'

Tactic:
refine ⟨ν'.restrict s, ?_, restrict_le_self⟩

Goal state after:
case a
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_meas_s : MeasurableSet s
h_nonempty : {d | μ ≤ d + ν}.Nonempty
ν' : Measure α
h_ν'_in : μ.restrict s ≤ ν' + ν.restrict s
⊢ ν'.restrict s ∈ (fun μ ↦ μ.restrict s) '' {d | μ ≤ d + ν}
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case e_f
α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
f : α → Set (Set α) := fun x ↦ {a | μ a = 0}
h : v.FineSubfamilyOn f s
⊢ (fun x ↦ μ (h.covering ↑x)) = fun x ↦ 0

Tactic:
ext1 x

Goal state after:
case e_f
α : Type u_1
inst✝¹ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝ : SecondCountableTopology α
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}
hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}
f : α → Set (Set α) := fun x ↦ {a | μ a = 0}
h : v.FineSubfamilyOn f s
x : ↑h.index
⊢ μ (h.covering ↑x) = 0
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 0)

Tactic:
have A : ∀ ε > (0 : ℝ≥0), ∀ᵐ x ∂μ, ∀ᶠ a in v.filterAt x, ρ a < ε * μ a := by
    intro ε εpos
    set s := {x | ¬∀ᶠ a in v.filterAt x, ρ a < ε * μ a} with hs
    change μ s = 0
    obtain ⟨o, _, ρo, μo⟩ : ∃ o : Set α, MeasurableSet o ∧ ρ o = 0 ∧ μ oᶜ = 0 := hρ
    apply le_antisymm _ bot_le
    calc
      μ s ≤ μ (s ∩ o ∪ oᶜ) := by
        conv_lhs => rw [← inter_union_compl s o]
        gcongr
        apply inter_subset_right
      _ ≤ μ (s ∩ o) + μ oᶜ := measure_union_le _ _
      _ = μ (s ∩ o) := by rw [μo, add_zero]
      _ = (ε : ℝ≥0∞)⁻¹ * (ε • μ) (s ∩ o) := by
        simp only [coe_nnreal_smul_apply, ← mul_assoc, mul_comm _ (ε : ℝ≥0∞)]
        rw [ENNReal.mul_inv_cancel (ENNReal.coe_pos.2 εpos).ne' ENNReal.coe_ne_top, one_mul]
      _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ (s ∩ o) := by
        gcongr _ * ?_
        refine v.measure_le_of_frequently_le ρ smul_absolutelyContinuous _ ?_
        intro x hx
        rw [hs] at hx
        simp only [mem_inter_iff, not_lt, not_eventually, mem_ofPred_eq] at hx
        exact hx.1
      _ ≤ (ε : ℝ≥0∞)⁻¹ * ρ o := by gcongr; apply inter_subset_right
      _ = 0 := by rw [ρo, mul_zero]

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 0)
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
j : ι
⊢ x ∈ closedBall (w j) (K * δ j) → j ∈ δ ⁻¹' Ioi 0 → closedBall (w j) (δ j) ∈ (vitaliFamily μ K).setsAt x

Tactic:
hj

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
δlim : Tendsto δ l (𝓝[>] 0)
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
j : ι
hj : x ∈ closedBall (w j) (K * δ j)
⊢ j ∈ δ ⁻¹' Ioi 0 → closedBall (w j) (δ j) ∈ (vitaliFamily μ K).setsAt x
Module: Mathlib.MeasureTheory.Covering.DensityTheorem

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
x : α
ι : Type u_2
l : Filter ι
w : ι → α
δ : ι → ℝ
xmem : ∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)
ε : ℝ
hε : ε > 0
h : l.NeBot
δpos : ∀ᶠ (i : ι) in l, δ i ∈ Ioi 0
δlim : Tendsto δ l (𝓝 0)
hK : 0 < K + 1
j : ι
hj₀ : 0 < δ j
y : α
hjε : (K + 1) * δ j < ε
hx : dist x (w j) ≤ K * δ j
hy : dist y (w j) ≤ δ j
⊢ dist y x ≤ ε

Tactic:
linarith [dist_triangle_right y x (w j)]

Goal state after:
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
h'x : f.measure.rnDeriv volume x < ⊤
h''x : ¬leftLim (↑f) x ≠ ↑f x
y : ℝ
hxy : x < y
⊢ 0 ≤ (↑f y - ↑f x) / (y - x)

Tactic:
exact div_nonneg (sub_nonneg.2 (f.mono hxy.le)) (sub_pos.2 hxy).le

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h✝ : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : ℕ → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun f ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun n ↦ ∫⁻ (x : α), (⨆ k, ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ n, ⨆ k, ⨆ (_ : k ≤ n), f k) x ∂ν))
n : ℕ
x✝ : α
⊢ (⨆ k, ⨆ (_ : k ≤ n), f k) x✝ = ⨆ k, ⨆ (_ : k ≤ n), f k x✝

Tactic:
simp only [iSup_apply]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
m n : ℕ
I : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
⊢ ρ (u m ∩ toMeasurable (ρ + μ) (w n)) ≤ (p • μ) (u m ∩ toMeasurable (ρ + μ) (w n))

Tactic:
refine v.measure_le_of_frequently_le (p • μ) hρ _ fun x hx => ?_

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
m n : ℕ
I : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
⊢ ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ (p • μ) a
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
m n : ℕ
I✝ : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p
a : Set α
ha : ρ a / μ a < ↑p
⊢ ρ a ≤ (p • μ) a

Tactic:
rw [coe_nnreal_smul_apply]

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
m n : ℕ
I✝ : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p
a : Set α
ha : ρ a / μ a < ↑p
⊢ ρ a ≤ ↑p * μ a
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
m n : ℕ
I✝ : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
A :
  ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
I : ∀ᶠ (b : Set α) in v.filterAt x, ↑q < ρ b / μ b
a : Set α
ha : ↑q < ρ a / μ a
⊢ (q • μ) a ≤ ρ a

Tactic:
rw [coe_nnreal_smul_apply]

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n ↦ s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n ↦ s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n
m n : ℕ
I✝ : (ρ + μ) (u m) ≠ ∞
J : (ρ + μ) (w n) ≠ ∞
A :
  ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
I : ∀ᶠ (b : Set α) in v.filterAt x, ↑q < ρ b / μ b
a : Set α
ha : ↑q < ρ a / μ a
⊢ ↑q * μ a ≤ ρ a
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
⊢ ρ (s ∩ t) ≤ (p • μ) (s ∩ t)

Tactic:
refine v.measure_le_of_frequently_le (p • μ) hρ _ fun x hx => ?_

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
x : α
hx : x ∈ s ∩ t
⊢ ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ (p • μ) a
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p
a : Set α
ha : ρ a / μ a < ↑p
⊢ ρ a ≤ (p • μ) a

Tactic:
rw [coe_nnreal_smul_apply]

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p : ℝ≥0
s : Set α
h : s ⊆ {x | v.limRatioMeas hρ x < ↑p}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (b : Set α) in v.filterAt x, ρ b / μ b < ↑p
a : Set α
ha : ρ a / μ a < ↑p
⊢ ρ a ≤ ↑p * μ a
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in v.filterAt x, ↑q < ρ a / μ a
a : Set α
ha : ↑q < ρ a / μ a
⊢ (q • μ) a ≤ ρ a

Tactic:
rw [coe_nnreal_smul_apply]

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
q : ℝ≥0
s : Set α
h : s ⊆ {x | ↑q < v.limRatioMeas hρ x}
t : Set α := {x | Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))}
A : μ tᶜ = 0
x : α
hx : x ∈ s ∩ t
I : ∀ᶠ (a : Set α) in v.filterAt x, ↑q < ρ a / μ a
a : Set α
ha : ↑q < ρ a / μ a
⊢ ↑q * μ a ≤ ρ a
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : i + 1 < N
⊢ w i ≤ w (i + 1)

pp: case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : i + 1 = N
⊢ w i ≤ w (i + 1)

pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : N < i + 1
⊢ w i ≤ w (i + 1)

Tactic:
· grind [Monotone]

Goal state after:
case inr.inl
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : i + 1 = N
⊢ w i ≤ w (i + 1)

case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : N < i + 1
⊢ w i ≤ w (i + 1)
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
x : α
hx : x ∈ s
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
n : ℕ
h : x < u n
exists_N : ∃ N ≤ n, x < u N
N : ℕ := Nat.find exists_N
hN : N ≤ n ∧ x < u N
w : ℕ → α := fun i ↦ if i < N then u i else if i = N then x else u (i - 1)
i : ℕ
hi : N < i + 1
⊢ w i ≤ w (i + 1)

Tactic:
· grind [Monotone]

Goal state after: