mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.Vitali

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      μ (closedBall p.2.1 (3 * p.1)) ≤ ↑C * μ p.2.2 ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
⊢ ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x

Tactic:
intro x

Goal state after:
α : Type u_1
ι : Type u_2
inst✝⁴ : PseudoMetricSpace α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : SecondCountableTopology α
μ : Measure α
inst✝ : IsLocallyFiniteMeasure μ
C : ℝ≥0
h : ∀ (x : α), ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑C * μ (closedBall x r)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ ↑C * μ a}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      μ (closedBall p.2.1 (3 * p.1)) ≤ ↑C * μ p.2.2 ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
⊢ x ∈ s → ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: α : 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}
⊢ v.FineSubfamilyOn f s

Tactic:
intro x

Goal state after:
α : 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}
x : α
⊢ x ∈ s → ∀ ε > 0, ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε
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 : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
⊢ ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall x r)

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
K : ℝ
R : ℝ := scalingScaleOf μ (max (4 * K + 3) 3)
Rpos : 0 < R
x : α
⊢ ∃ᶠ (r : ℝ) in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ ↑(scalingConstantOf μ (max (4 * K + 3) 3)) * μ (closedBall x r)
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case h₂
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
⊢ ∀ x ∈ s ∩ o, ∃ᶠ (a : Set α) in v.filterAt x, (↑ε • μ) a ≤ ρ a

Tactic:
intro x

Goal state after:
case h₂
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
ε : ℝ≥0
εpos : ε > 0
s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a}
o : Set α
left✝ : MeasurableSet o
ρo : ρ o = 0
μo : μ oᶜ = 0
x : α
⊢ x ∈ s ∩ o → ∃ᶠ (a : Set α) in v.filterAt x, (↑ε • μ) 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ρ : ρ ⟂ₘ μ
A : ∀ ε > 0, ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑ε * μ a
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
⊢ ∀ (a : α),
    (∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt a, ρ a < ↑(u n) * μ a) →
      (∀ᶠ (a : Set α) in v.filterAt a, 0 < μ a) → Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a) (𝓝 0)

Tactic:
intro x

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
u : ℕ → ℝ≥0
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
B : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a
x : α
⊢ (∀ (n : ℕ), ∀ᶠ (a : Set α) in v.filterAt x, ρ a < ↑(u n) * μ a) →
    (∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a) → Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 0)
Module: Mathlib.Order.Monotone.Extension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
⊢ EqOn f g s

Tactic:
intro x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
f : α → β
s : Set α
h : MonotoneOn f s
hu : BddAbove (f '' s)
a : β
ha : a ∈ lowerBounds (f '' s)
hu' : ∀ (x : α), BddAbove (f '' (Iic x ∩ s))
g : α → β := fun x ↦ if Disjoint (Iic x) s then a else sSup (f '' (Iic x ∩ s))
x : α
⊢ x ∈ s → f x = g x
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case hc
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
⊢ ∀ (x : α),
    (∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c) →
      (∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x) → ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a

Tactic:
intro x

Goal state after:
case hc
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
⊢ (∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c) →
    (∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x) → ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ↑c * μ a
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case hd
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
⊢ ∀ (x : α),
    (∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c) →
      (∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x) → ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ a ≤ ρ a

Tactic:
intro x

Goal state after:
case hd
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
c : ℝ≥0
hc : ↑c ∈ w
d : ℝ≥0
hd : ↑d ∈ w
hcd : ↑c < ↑d
x : α
⊢ (∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < ↑c) →
    (∃ᶠ (x : Set α) in v.filterAt x, ↑d < ρ x / μ x) → ∃ᶠ (a : Set α) in v.filterAt x, ↑d * μ 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ρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
⊢ ∀ (a : α),
    (∀ c ∈ w,
        ∀ d ∈ w,
          c < d → ¬((∃ᶠ (a : Set α) in v.filterAt a, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt a, d < ρ a / μ a)) →
      ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a) (𝓝 c)

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ∞ ∉ w
I : ∀ x ∈ w, x ≠ ∞
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
x : α
⊢ (∀ c ∈ w,
      ∀ d ∈ w,
        c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)) →
    ∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)
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ρ : ρ ≪ μ
⊢ ∀ (a : α),
    (∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a) (𝓝 c)) →
      Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatio ρ a))

Tactic:
intro x

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
⊢ (∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)) →
    Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case refine_3
α : 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
⊢ {x | v.limRatio ρ x < ↑p} ⊆ toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (u n)

Tactic:
intro x

Goal state after:
case refine_3
α : 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
x : α
⊢ x ∈ {x | v.limRatio ρ x < ↑p} → x ∈ toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (u n)
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case refine_4
α : 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
⊢ {x | ↑q < v.limRatio ρ x} ⊆ toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (w n)

Tactic:
intro x

Goal state after:
case refine_4
α : 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
x : α
⊢ x ∈ {x | ↑q < v.limRatio ρ x} → x ∈ toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (w n)
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) ≠ ∞
⊢ (p • μ) (u m ∩ toMeasurable (ρ + μ) (w n)) = ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))

Tactic:
simp only [coe_nnreal_smul_apply,
          measure_toMeasurable_add_inter_right (measurableSet_toMeasurable _ _) I]

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) ≠ ∞
A :
  ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑q * μ (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m)) = ↑q * μ (w n ∩ toMeasurable (ρ + μ) (u m))

Tactic:
measure_toMeasurable_add_inter_right (measurableSet_toMeasurable _ _) J

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))
⊢ ↑q * μ (w n ∩ toMeasurable (ρ + μ) (u m)) = ↑q * μ (w n ∩ toMeasurable (ρ + μ) (u m))
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 ∈ toMeasurable (ρ + μ) (u m) ∩ w n, ∃ᶠ (a : Set α) in v.filterAt x, (q • μ) a ≤ ρ a

Tactic:
intro x

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 : α
⊢ x ∈ toMeasurable (ρ + μ) (u m) ∩ w n → ∃ᶠ (a : Set α) in v.filterAt x, (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ρ : ρ ≪ μ
⊢ ∀ (a : α),
    Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatio ρ a)) →
      v.limRatio ρ a = AEMeasurable.mk (v.limRatio ρ) ⋯ a →
        Tendsto (fun a ↦ ρ a / μ a) (v.filterAt a) (𝓝 (v.limRatioMeas hρ a))

Tactic:
intro x

Goal state after:
α : 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) (𝓝 (v.limRatio ρ x)) →
    v.limRatio ρ x = AEMeasurable.mk (v.limRatio ρ) ⋯ x →
      Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))
Module: Mathlib.Topology.EMetricSpace.BoundedVariation

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
hs : s.Nonempty
⊢ Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }

Tactic:
obtain ⟨x, hx⟩ := hs

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ Nonempty { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }
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 ∈ s ∩ t, ∃ᶠ (a : Set α) in v.filterAt x, (q • μ) a ≤ ρ a

Tactic:
intro x

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 : α
⊢ x ∈ s ∩ t → ∃ᶠ (a : Set α) in v.filterAt x, (q • μ) a ≤ ρ a
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
as : a ∈ s
bs : b ∈ s
cs : c ∈ s
bc : b ≤ c
⊢ (edist (f b) (f c)).toReal ≤ (eVariationOn f (s ∩ Icc b c)).toReal

Tactic:
apply ENNReal.toReal_mono (hf b c bs cs)

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
hf : LocallyBoundedVariationOn f s
a b c : α
as : a ∈ s
bs : b ∈ s
cs : c ∈ s
bc : b ≤ c
⊢ edist (f b) (f c) ≤ eVariationOn f (s ∩ Icc b c)
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ MonotoneOn (fun x ↦ (variationOnFromTo f s c x + f x) / 2) s

Tactic:
intro x

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
⊢ x ∈ s →
    ∀ ⦃b : α⦄,
      b ∈ s →
        x ≤ b → (fun x ↦ (variationOnFromTo f s c x + f x) / 2) x ≤ (fun x ↦ (variationOnFromTo f s c x + f x) / 2) b
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ MonotoneOn (fun x ↦ (variationOnFromTo f s c x - f x) / 2) s

Tactic:
intro x

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
⊢ x ∈ s →
    ∀ ⦃b : α⦄,
      b ∈ s →
        x ≤ b → (fun x ↦ (variationOnFromTo f s c x - f x) / 2) x ≤ (fun x ↦ (variationOnFromTo f s c x - f x) / 2) b
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: case inr.refine_4
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
⊢ ∀ x ∈ s,
    ∀ y ∈ s,
      (fun x ↦ (variationOnFromTo f s c x + f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x + f x) / 2) x +
          ((fun x ↦ (variationOnFromTo f s c x - f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x - f x) / 2) x) =
        variationOnFromTo f s x y

Tactic:
intro x

Goal state after:
case inr.refine_4
α : Type u_1
inst✝ : LinearOrder α
f : α → ℝ
s : Set α
h : LocallyBoundedVariationOn f s
c : α
cs : c ∈ s
x : α
⊢ x ∈ s →
    ∀ y ∈ s,
      (fun x ↦ (variationOnFromTo f s c x + f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x + f x) / 2) x +
          ((fun x ↦ (variationOnFromTo f s c x - f x) / 2) y - (fun x ↦ (variationOnFromTo f s c x - f x) / 2) x) =
        variationOnFromTo f s x y