mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ¬μ ⟂ₘ ν
f : ℕ → Set α
hf₁ : ∀ (n : ℕ), MeasurableSet (f n)
hf₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → ((1 / (↑n + 1)) • ν) (t ∩ f n) ≤ μ (t ∩ f n)
hf₃ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ (f n)ᶜ) ≤ ((1 / (↑n + 1)) • ν) (t ∩ (f n)ᶜ)
A : Set α := ⋂ n, (f n)ᶜ
hAmeas : MeasurableSet A
hA₂ : ∀ (n : ℕ) (t : Set α), MeasurableSet t → μ (t ∩ A) ≤ ((1 / (↑n + 1)) • ν) (t ∩ A)
μA νA : ℝ≥0
hA₃ : ∀ (n : ℕ), ↑μA ≤ ↑(1 / (↑n + 1)) * ↑νA
hb : 0 < νA
this : ∀ (b : ℝ≥0), 0 < b → μA ≤ b
⊢ μA = 0

Tactic:
by_contra h
        have h' := this (μA / 2) (half_pos (zero_lt_iff.2 h))
        rw [← @Classical.not_not (μA ≤ μA / 2)] at h'
        exact h' (not_le.2 (NNReal.half_lt_self h))

Goal state after:
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 μ
S : Set α
K : ℝ
x : α
⊢ Tendsto (fun a ↦ μ (S ∩ a) / μ a) ((vitaliFamily μ K).filterAt x) (𝓝 1) →
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j ↦ μ (S ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)

Tactic:
hx

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : IsUnifLocDoublingMeasure μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
inst✝ : IsLocallyFiniteMeasure μ
S : Set α
K : ℝ
x : α
hx : Tendsto (fun a ↦ μ (S ∩ a) / μ a) ((vitaliFamily μ K).filterAt x) (𝓝 1)
⊢ ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
        Tendsto (fun j ↦ μ (S ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
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 μ
E : Type u_2
inst✝ : NormedAddCommGroup E
f : α → E
hf : LocallyIntegrable f μ
K : ℝ
x : α
⊢ Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) ((vitaliFamily μ K).filterAt x) (𝓝 0) →
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j ↦ ⨍ (y : α) in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 0)

Tactic:
hx

Goal state after:
α : Type u_1
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : IsUnifLocDoublingMeasure μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
E : Type u_2
inst✝ : NormedAddCommGroup E
f : α → E
hf : LocallyIntegrable f μ
K : ℝ
x : α
hx : Tendsto (fun a ↦ ⨍ (y : α) in a, ‖f y - f x‖ ∂μ) ((vitaliFamily μ K).filterAt x) (𝓝 0)
⊢ ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
        Tendsto (fun j ↦ ⨍ (y : α) in closedBall (w j) (δ j), ‖f y - f x‖ ∂μ) l (𝓝 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 μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
K : ℝ
x : α
⊢ Tendsto (fun a ↦ ⨍ (y : α) in a, f y ∂μ) ((vitaliFamily μ K).filterAt x) (𝓝 (f x)) →
    ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
      Tendsto δ l (𝓝[>] 0) →
        (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
          Tendsto (fun j ↦ ⨍ (y : α) in closedBall (w j) (δ j), f y ∂μ) l (𝓝 (f x))

Tactic:
hx

Goal state after:
α : Type u_1
inst✝⁸ : PseudoMetricSpace α
inst✝⁷ : MeasurableSpace α
μ : Measure α
inst✝⁶ : IsUnifLocDoublingMeasure μ
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : BorelSpace α
inst✝³ : IsLocallyFiniteMeasure μ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : LocallyIntegrable f μ
K : ℝ
x : α
hx : Tendsto (fun a ↦ ⨍ (y : α) in a, f y ∂μ) ((vitaliFamily μ K).filterAt x) (𝓝 (f x))
⊢ ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) →
        Tendsto (fun j ↦ ⨍ (y : α) in closedBall (w j) (δ j), f y ∂μ) l (𝓝 (f x))
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))
x : α
⊢ x ∈ s → f x = g x

Tactic:
hx

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 : α
hx : x ∈ s
⊢ f x = g x
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : StieltjesFunction ℝ
x : ℝ
⊢ Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x)) →
    f.measure.rnDeriv volume x < ⊤ → ¬leftLim (↑f) x ≠ ↑f x → HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x

Tactic:
hx

Goal state after:
f : StieltjesFunction ℝ
x : ℝ
hx : Tendsto (fun a ↦ f.measure a / volume a) ((vitaliFamily volume 1).filterAt x) (𝓝 (f.measure.rnDeriv volume x))
⊢ f.measure.rnDeriv volume x < ⊤ → ¬leftLim (↑f) x ≠ ↑f x → HasDerivAt (↑f) (f.measure.rnDeriv volume x).toReal x
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)
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)

Tactic:
hx

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 : α
hx :
  ∀ 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ρ : ρ ≪ μ
x : α
⊢ (∃ c, Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 c)) →
    Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x))

Tactic:
hx

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : ∃ 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 : α
⊢ x ∈ {x | v.limRatio ρ x < ↑p} → x ∈ toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (u n)

Tactic:
hx

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 : α
hx : 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 : α
⊢ x ∈ {x | ↑q < v.limRatio ρ x} → x ∈ toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (w n)

Tactic:
hx

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 : α
hx : x ∈ {x | ↑q < v.limRatio ρ x}
⊢ x ∈ toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (w n)
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
hf : Monotone f
x : ℝ
⊢ HasDerivAt (↑hf.stieltjesFunction) (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x →
    ¬¬ContinuousAt f x → HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x

Tactic:
hx

Goal state after:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx : HasDerivAt (↑hf.stieltjesFunction) (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
⊢ ¬¬ContinuousAt f x → HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
Module: Mathlib.MeasureTheory.Covering.Differentiation

Goal state before:
pp: case refine_5
α : 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
⊢ μ ((toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (u n)) ∩ (toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (w n))) = 0

Tactic:
suffices H : ∀ m n : ℕ, μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0 by
    have A :
      (toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (u n)) ∩
          (toMeasurable μ sᶜ ∪ ⋃ n, toMeasurable (ρ + μ) (w n)) ⊆
        toMeasurable μ sᶜ ∪
          ⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n) := by
      simp only [inter_union_distrib_left, union_inter_distrib_right, true_and,
        subset_union_left, union_subset_iff, inter_self]
      refine ⟨?_, ?_, ?_⟩
      · exact inter_subset_right.trans subset_union_left
      · exact inter_subset_left.trans subset_union_left
      · simp_rw [iUnion_inter, inter_iUnion]; exact subset_union_right
    refine le_antisymm ((measure_mono A).trans ?_) bot_le
    calc
      μ (toMeasurable μ sᶜ ∪
        ⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
          μ (toMeasurable μ sᶜ) +
            μ (⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
        measure_union_le _ _
      _ = μ (⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) := by
        have : μ sᶜ = 0 := v.ae_tendsto_div hρ; rw [measure_toMeasurable, this, zero_add]
      _ ≤ ∑' (m) (n), μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
        ((measure_iUnion_le _).trans (ENNReal.tsum_le_tsum fun m => measure_iUnion_le _))
      _ = 0 := by simp only [H, tsum_zero]

Goal state after:
case refine_5
α : 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 : ℕ), μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 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ρ : ρ ≪ μ
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

Tactic:
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) ≠ ∞
A :
  ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
⊢ ∃ᶠ (a : Set α) in v.filterAt x, (q • μ) a ≤ ρ a
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
hf : Monotone f
x : ℝ
⊢ HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x → DifferentiableAt ℝ f x

Tactic:
hx

Goal state after:
f : ℝ → ℝ
hf : Monotone f
x : ℝ
hx : HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv volume x).toReal x
⊢ DifferentiableAt ℝ f x
Module: Mathlib.Analysis.Calculus.Monotone

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
⊢ DifferentiableAt ℝ g x → x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x

Tactic:
hx

Goal state after:
f : ℝ → ℝ
s : Set ℝ
hf : MonotoneOn f s
a b : ℝ
as : a ∈ s
bs : b ∈ s
a✝ : a < b
g : ℝ → ℝ
hg : Monotone g
gf : EqOn f g (s ∩ Icc a b)
x : ℝ
hx : DifferentiableAt ℝ g x
⊢ x ∈ s ∩ Ioo a b → DifferentiableWithinAt ℝ f s x
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) (𝓝 (v.limRatio ρ x)) →
    v.limRatio ρ x = AEMeasurable.mk (v.limRatio ρ) ⋯ x →
      Tendsto (fun a ↦ ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatioMeas hρ x))

Tactic:
hx

Goal state after:
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
x : α
hx : 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.VariationOnFromTo

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : variationOnFromTo f s a b = 0
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
    LocallyBoundedVariationOn f s →
      ∀ {a b : α}, a ∈ s → b ∈ s → variationOnFromTo f s a b = 0 → a ≤ b → edist (f a) (f b) = 0
h' : ¬a ≤ b
⊢ edist (f a) (f b) = 0

Tactic:
edist_comm

Goal state after:
case inr
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
h : variationOnFromTo f s a b = 0
this :
  ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
    LocallyBoundedVariationOn f s →
      ∀ {a b : α}, a ∈ s → b ∈ s → variationOnFromTo f s a b = 0 → a ≤ b → edist (f a) (f b) = 0
h' : ¬a ≤ b
⊢ edist (f b) (f a) = 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ρ : ρ ≪ μ
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

Tactic:
hx

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
ba : b ≤ a
⊢ variationOnFromTo f s a b = 0 ↔ ∀ ⦃x : α⦄, x ∈ s ∩ Icc b a → ∀ ⦃y : α⦄, y ∈ s ∩ Icc b a → edist (f x) (f y) = 0

Tactic:
rw [variationOnFromTo.eq_of_ge _ _ ba, neg_eq_zero, ENNReal.toReal_eq_zero_iff,
    or_iff_left (hf b a hb ha), eVariationOn.eq_zero_iff]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
⊢ AntitoneOn (fun a ↦ variationOnFromTo f s a b) s

Tactic:
rintro a as c cs ac

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : α → E
s : Set α
hf : LocallyBoundedVariationOn f s
b : α
bs : b ∈ s
a : α
as : a ∈ s
c : α
cs : c ∈ s
ac : a ≤ c
⊢ (fun a ↦ variationOnFromTo f s a b) c ≤ (fun a ↦ variationOnFromTo f s a b) a
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
H :
  Tendsto (fun x ↦ variationOnFromTo f s a b - variationOnFromTo f s x b) (𝓝[s ∩ Iio b] b)
    (𝓝 (variationOnFromTo f s a b - dist (f b) l))
x : α
⊢ x ∈ s ∩ Iio b → variationOnFromTo f s a b - variationOnFromTo f s x b = variationOnFromTo f s a x

Tactic:
hx

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
H :
  Tendsto (fun x ↦ variationOnFromTo f s a b - variationOnFromTo f s x b) (𝓝[s ∩ Iio b] b)
    (𝓝 (variationOnFromTo f s a b - dist (f b) l))
x : α
hx : x ∈ s ∩ Iio b
⊢ variationOnFromTo f s a b - variationOnFromTo f s x b = variationOnFromTo f s a x
Module: Mathlib.Topology.EMetricSpace.VariationOnFromTo

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
H : Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc x b)).toReal) (𝓝[s ∩ Iio b] b) (𝓝 (dist (f b) l))
x : α
⊢ x ∈ s ∩ Iio b → (eVariationOn f (s ∩ Icc x b)).toReal = variationOnFromTo f s x b

Tactic:
hx

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
s : Set α
E : Type u_3
inst✝² : PseudoMetricSpace E
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → E
l : E
a b : α
ha : a ∈ s
hb : b ∈ s
hf : LocallyBoundedVariationOn f s
h'f : Tendsto f (𝓝[s ∩ Iio b] b) (𝓝 l)
H : Tendsto (fun x ↦ (eVariationOn f (s ∩ Icc x b)).toReal) (𝓝[s ∩ Iio b] b) (𝓝 (dist (f b) l))
x : α
hx : x ∈ s ∩ Iio b
⊢ (eVariationOn f (s ∩ Icc x b)).toReal = variationOnFromTo f s x b