awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
h₂ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
h : 0 = M * 0
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝 0)

Tactic:
convert! hr.const_mul M

Premises used: Filter.Tendsto.const_mul
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
h₂ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
⊢ 0 = M * 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
h₂ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝 0)

Tactic:
replace hr : Tendsto (fun i => M * r i) atTop (𝓝 0) := by convert! hr.const_mul M; simp
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i
h₁ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
h₂ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
hr : Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝 0)
⊢ ∀ᶠ (i : ℕ) in atTop, p i → 0 < M * r i

Tactic:
replace hr' : ∀ᶠ i in atTop, p i → 0 < M * r i := hr'.mono fun i hi hip ↦ mul_pos hM (hi hip)
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
h₁ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
h₂ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
hr : Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < M * r i
h₃ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (M * r i) (s i)) atTop p)
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ thickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)

Tactic:
h₃.symm.trans (h₂.trans h₁)

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
h₁ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)
h₂ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ cthickening (r i) (s i)) atTop p)
hr : Tendsto (β := ℝ) (fun (i : ℕ) ↦ M * r i) atTop (𝓝 0)
hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < M * r i
h₃ :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ cthickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (M * r i) (s i)) atTop p)
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ thickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)

Tactic:
exact h₃.symm.trans (h₂.trans h₁)

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun (i : ℕ) ↦ p i ∧ 0 < r i
u : ℕ → Set α
hu : ∀ (i : ℕ), u i ≠ ∅ → 0 < r i
i : ℕ
hi : u i ≠ ⊥
⊢ p i ↔ q i

Tactic:
simp [q, hu i hi]
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun (i : ℕ) ↦ p i ∧ 0 < r i
⊢ ∀ {u : ℕ → Set α} (hu : ∀ (i : ℕ), u i ≠ ∅ → 0 < r i), blimsup u atTop p = blimsup u atTop q

Tactic:
have hq {u : ℕ → Set α} (hu : ∀ i, u i ≠ ∅ → 0 < r i) :
      blimsup u atTop p = blimsup u atTop q :=
    blimsup_congr' <| Eventually.of_forall fun i hi ↦ by simp [q, hu i hi]
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun (i : ℕ) ↦ p i ∧ 0 < r i
hq : ∀ {u : ℕ → Set α} (hu : ∀ (i : ℕ), u i ≠ ∅ → 0 < r i), blimsup u atTop p = blimsup u atTop q
rw :
  (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ thickening (M * r i) (s i)) atTop q)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop q)
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ thickening (M * r i) (s i)) atTop p)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop p)

Tactic:
rw [hq fun i hi ↦ (thickening_nonempty_iff.1 <| nonempty_iff_ne_empty.2 hi).1,
    hq fun i hi ↦ (mul_pos_iff_of_pos_left hM).1 <|
      (thickening_nonempty_iff.1 <| nonempty_iff_ne_empty.2 hi).1]

Premises used: Iff.mpr, mul_pos_iff_of_pos_left, And.left, Iff.mp, Set.nonempty_iff_ne_empty, Metric.thickening_nonempty_iff
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun (i : ℕ) ↦ p i ∧ 0 < r i
hq : ∀ {u : ℕ → Set α} (hu : ∀ (i : ℕ), u i ≠ ∅ → 0 < r i), blimsup u atTop p = blimsup u atTop q
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ thickening (M * r i) (s i)) atTop q)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop q)

Tactic:
blimsup_thickening_mul_ae_eq_aux μ q s hM r hr (Eventually.of_forall fun i hi => hi.2)

Premises used: blimsup_thickening_mul_ae_eq_aux, Filter.Eventually.of_forall, And.right
-- Module: Mathlib.MeasureTheory.Covering.LiminfLimsup
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
M : ℝ
hM : 0 < M
r : ℕ → ℝ
hr : Tendsto r atTop (𝓝 0)
q : ℕ → Prop := fun (i : ℕ) ↦ p i ∧ 0 < r i
hq : ∀ {u : ℕ → Set α} (hu : ∀ (i : ℕ), u i ≠ ∅ → 0 < r i), blimsup u atTop p = blimsup u atTop q
⊢ (ae μ).EventuallyEq (β := Prop) (blimsup (fun (i : ℕ) ↦ thickening (M * r i) (s i)) atTop q)
    (blimsup (fun (i : ℕ) ↦ thickening (r i) (s i)) atTop q)

Tactic:
exact blimsup_thickening_mul_ae_eq_aux μ q s hM r hr (Eventually.of_forall fun i hi => hi.2)

Premises used: blimsup_thickening_mul_ae_eq_aux, Filter.Eventually.of_forall, And.right
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
rw : Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x
⊢ Icc x y ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x

Tactic:
rw [Icc_eq_closedBall]

Premises used: Real.Icc_eq_closedBall
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
linarith : (y - x) / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : (y - x) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (y - x) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : (y - x) / 2 ≤ 0 → x - y + (1 * y - 1 * x - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 < (y - x) / 2

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
refine : dist x ((x + y) / 2) ≤ 1 * ((y - x) / 2)
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x

Tactic:
refine closedBall_mem_vitaliFamily_of_dist_le_mul _ ?_ (by linarith)

Premises used: IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
rw : (x + y) / 2 - x ≤ 1 * ((y - x) / 2)
rw₁ : 0 ≤ (x + y) / 2 - x
⊢ dist x ((x + y) / 2) ≤ 1 * ((y - x) / 2)

Tactic:
rw [dist_comm, Real.dist_eq, abs_of_nonneg]

Premises used: dist_comm, Real.dist_eq, abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
linarith : 1 * ((y - x) / 2) < (x + y) / 2 - x → 2 / 2 = 1
linarith₁ linarith₂ : 1 * ((y - x) / 2) < (x + y) / 2 - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : 1 * ((y - x) / 2) < (x + y) / 2 - x → 2 / 2 = 1
linarith₄ : 1 * ((y - x) / 2) < (x + y) / 2 - x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 * ((y - x) / 2) < (x + y) / 2 - x → GT.gt (α := ℝ) 2 0
linarith₆ : 1 * ((y - x) / 2) < (x + y) / 2 - x → HMul.hMul (α := ℝ) 1 1 * (1 * y - 1 * x) - (1 * x + 1 * y - 2 * x) = 0
⊢ (x + y) / 2 - x ≤ 1 * ((y - x) / 2)

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
linarith : (x + y) / 2 - x < 0 → 2 / 2 = 1
linarith₁ : (x + y) / 2 - x < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (x + y) / 2 - x < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : (x + y) / 2 - x < 0 → x - y + (1 * x + 1 * y - 2 * x - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 ≤ (x + y) / 2 - x

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x : ℝ
⊢ Tendsto (fun (y : ℝ) ↦ Icc x y) (𝓝[>] x) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)

Tactic:
(VitaliFamily.tendsto_filterAt_iff _).2 ⟨?_, ?_⟩

Premises used: Iff.mpr, VitaliFamily.tendsto_filterAt_iff, And.intro
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x : ℝ
refine_1 : ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x
refine_2 : ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ⊆ Metric.closedBall x ε
⊢ Tendsto (fun (y : ℝ) ↦ Icc x y) (𝓝[>] x) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)

Tactic:
refine (VitaliFamily.tendsto_filterAt_iff _).2 ⟨?_, ?_⟩

Premises used: Iff.mpr, VitaliFamily.tendsto_filterAt_iff, And.intro
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hy : y ∈ Ioi x
⊢ Icc x y ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x

Tactic:
Icc_mem_vitaliFamily_at_right hy

Premises used: Real.Icc_mem_vitaliFamily_at_right
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x : ℝ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Ioi x →
          Membership.mem (γ := Set ℝ)
            {x_2 : ℝ | (fun (i : ℝ) ↦ Icc x i ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x) x_2} x_1}
      a
h₁ h₂ : ∀ (y : ℝ) (hy : y ∈ Ioi x), Icc x y ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x
⊢ ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy using Icc_mem_vitaliFamily_at_right hy

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x ε : ℝ
εpos : ε > 0
linarith : x + ε ≤ x → 0 - ε + (x + ε - x) = 0
⊢ x < x + ε

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x ε : ℝ
εpos : ε > 0
h : ∀ (y : ℝ) (hy : y ∈ Icc x (x + ε)), Icc x y ⊆ Metric.closedBall x ε
⊢ ∀ᶠ (i : ℝ) in 𝓝[>] x, Icc x i ⊆ Metric.closedBall x ε

Tactic:
filter_upwards [Icc_mem_nhdsGT <| show x < x + ε by linarith] with y hy

Premises used: Icc_mem_nhdsGT
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
h : Icc x y ⊆ Icc (x - ε) (x + ε)
⊢ Icc x y ⊆ Metric.closedBall x ε

Tactic:
rw [closedBall_eq_Icc]

Premises used: Real.closedBall_eq_Icc
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
linarith : x < x - ε → 0 - ε + (x - (x - ε)) = 0
⊢ x - ε ≤ x

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Icc (x - ε) (x + ε)

Tactic:
exact Icc_subset_Icc (by linarith) hy.2

Premises used: And.right, Set.Icc_subset_Icc
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
rw : Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) y
⊢ Icc x y ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) y

Tactic:
rw [Icc_eq_closedBall]

Premises used: Real.Icc_eq_closedBall
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
refine : dist y ((x + y) / 2) ≤ 1 * ((y - x) / 2)
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) y

Tactic:
refine closedBall_mem_vitaliFamily_of_dist_le_mul _ ?_ (by linarith)

Premises used: IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
rw : y - (x + y) / 2 ≤ 1 * ((y - x) / 2)
rw₁ : 0 ≤ y - (x + y) / 2
⊢ dist y ((x + y) / 2) ≤ 1 * ((y - x) / 2)

Tactic:
rw [Real.dist_eq, abs_of_nonneg]

Premises used: Real.dist_eq, abs_of_nonneg
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
linarith : 1 * ((y - x) / 2) < y - (x + y) / 2 → 2 / 2 = 1
linarith₁ linarith₂ : 1 * ((y - x) / 2) < y - (x + y) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : 1 * ((y - x) / 2) < y - (x + y) / 2 → 2 / 2 = 1
linarith₄ : 1 * ((y - x) / 2) < y - (x + y) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 * ((y - x) / 2) < y - (x + y) / 2 → GT.gt (α := ℝ) 2 0
linarith₆ :
  1 * ((y - x) / 2) < y - (x + y) / 2 → HMul.hMul (α := ℝ) 1 1 * (1 * y - 1 * x) - (2 * y - (1 * x + 1 * y)) = 0
⊢ y - (x + y) / 2 ≤ 1 * ((y - x) / 2)

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hxy : x < y
linarith : y - (x + y) / 2 < 0 → 2 / 2 = 1
linarith₁ : y - (x + y) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : y - (x + y) / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : y - (x + y) / 2 < 0 → x - y + (2 * y - (1 * x + 1 * y) - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 ≤ y - (x + y) / 2

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x : ℝ
⊢ Tendsto (fun (y : ℝ) ↦ Icc y x) (𝓝[<] x) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)

Tactic:
(VitaliFamily.tendsto_filterAt_iff _).2 ⟨?_, ?_⟩

Premises used: Iff.mpr, VitaliFamily.tendsto_filterAt_iff, And.intro
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x : ℝ
refine_1 : ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x
refine_2 : ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε
⊢ Tendsto (fun (y : ℝ) ↦ Icc y x) (𝓝[<] x) (VitaliFamily.filterAt (μ := volume) (vitaliFamily volume 1) x)

Tactic:
refine (VitaliFamily.tendsto_filterAt_iff _).2 ⟨?_, ?_⟩

Premises used: Iff.mpr, VitaliFamily.tendsto_filterAt_iff, And.intro
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x y : ℝ
hy : y ∈ Iio x
⊢ Icc y x ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x

Tactic:
Icc_mem_vitaliFamily_at_left hy

Premises used: Real.Icc_mem_vitaliFamily_at_left
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x : ℝ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Iio x →
          Membership.mem (γ := Set ℝ)
            {x_2 : ℝ | (fun (i : ℝ) ↦ Icc i x ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x) x_2} x_1}
      a
h₁ h₂ : ∀ (y : ℝ) (hy : y ∈ Iio x), Icc y x ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x
⊢ ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ∈ VitaliFamily.setsAt (μ := volume) (vitaliFamily volume 1) x

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy using Icc_mem_vitaliFamily_at_left hy

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x ε : ℝ
εpos : ε > 0
linarith : x ≤ x - ε → 0 - ε + (x - (x - ε)) = 0
⊢ x - ε < x

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x ε : ℝ
εpos : ε > 0
h : ∀ (y : ℝ) (hy : y ∈ Icc (x - ε) x), Icc y x ⊆ Metric.closedBall x ε
⊢ ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε

Tactic:
filter_upwards [Icc_mem_nhdsLT <| show x - ε < x by linarith] with y hy

Premises used: Icc_mem_nhdsLT
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc (x - ε) x
h : Icc y x ⊆ Icc (x - ε) (x + ε)
⊢ Icc y x ⊆ Metric.closedBall x ε

Tactic:
rw [closedBall_eq_Icc]

Premises used: Real.closedBall_eq_Icc
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc (x - ε) x
linarith : x + ε < x → 0 - ε + (x + ε - x) = 0
⊢ x ≤ x + ε

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Covering.OneDim
Goal:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Icc (x - ε) (x + ε)

Tactic:
exact Icc_subset_Icc hy.1 (by linarith)

Premises used: And.left, Set.Icc_subset_Icc
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
⊢ ∃ (m : Set ι), Maximal (fun (x : Set ι) ↦ x ∈ T) m

Tactic:
zorn_subset _ fun U UT hU => ?_

Premises used: zorn_subset
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
refine : ∀ (U : Set (Set ι)) (UT : U ⊆ T) (hU : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) U), ∃ ub ∈ T, ∀ s ∈ U, s ⊆ ub
⊢ ∃ (m : Set ι), Maximal (fun (x : Set ι) ↦ x ∈ T) m

Tactic:
refine zorn_subset _ fun U UT hU => ?_

Premises used: zorn_subset
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) U
⊢ ∃ ub ∈ T, ∀ s ∈ U, s ⊆ ub

Tactic:
⟨⋃₀ U, ?_, fun s hs => subset_sUnion_of_mem hs⟩

Premises used: Set.sUnion, And.intro, Exists.intro, Set.subset_sUnion_of_mem
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) U
refine : ⋃₀ U ∈ T
⊢ ∃ ub ∈ T, ∀ s ∈ U, s ⊆ ub

Tactic:
refine ⟨⋃₀ U, ?_, fun s hs => subset_sUnion_of_mem hs⟩
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) U
simp :
  (∀ t' ∈ U, t' ⊆ t) ∧
    (⋃₀ U).PairwiseDisjoint B ∧
      ∀ a ∈ t,
        ∀ (b : ι),
          ∀ x ∈ U, b ∈ x → (B a ∩ B b).Nonempty → ∃ (c : ι), (∃ t ∈ U, c ∈ t) ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c
⊢ ⋃₀ U ∈ T

Tactic:
simp only [T, Set.sUnion_subset_iff, and_imp, forall_exists_index, mem_sUnion,
      Set.mem_setOf_eq]

Premises used: and_imp, forall_exists_index, Set.mem_setOf_eq, Set.sUnion_subset_iff, Set.mem_sUnion
-- Module: Mathlib.MeasureTheory.Covering.Vitali
Goal:
α : Type u_1
ι : Type u_2
B : ι → Set α
t : Set ι
δ : ι → ℝ
τ : ℝ
hτ : 1 < τ
δnonneg : ∀ a ∈ t, 0 ≤ δ a
R : ℝ
δle : ∀ a ∈ t, δ a ≤ R
hne : ∀ a ∈ t, (B a).Nonempty
T : Set (Set ι) :=
  {u : Set ι |
    u ⊆ t ∧
      u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∀ b ∈ u, (B a ∩ B b).Nonempty → ∃ c ∈ u, (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c}
U : Set (Set ι)
UT : U ⊆ T
hU : IsChain (fun (x1 x2 : Set ι) ↦ x1 ⊆ x2) U
⊢ (∀ t' ∈ U, t' ⊆ t) ∧
    (⋃₀ U).PairwiseDisjoint B ∧
      ∀ a ∈ t,
        ∀ (b : ι),
          ∀ x ∈ U, b ∈ x → (B a ∩ B b).Nonempty → ∃ (c : ι), (∃ t ∈ U, c ∈ t) ∧ (B a ∩ B c).Nonempty ∧ δ a ≤ τ * δ c

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

Premises used: Iff.mpr, IsChain.directedOn, Set.pairwiseDisjoint_sUnion, And.right, And.left, And.intro