awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
a_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
a_int : (interior a).Nonempty
r : ℝ
ar : a ⊆ closedBall x r
μr :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
refine_1 : ∀ (h' : min r ε = r ∧ r ≤ ε), (min r ε, x, a).2.2 ⊆ closedBall (min r ε, x, a).2.1 (min r ε, x, a).1
⊢ (min r ε, x, a).2.2 ⊆ closedBall (min r ε, x, a).2.1 (min r ε, x, a).1
have refine_1₁ : ∀ (h' : min r ε = ε ∧ ε < r), (min r ε, x, a).2.2 ⊆ closedBall (min r ε, x, a).2.1 (min r ε, x, a).1
Tactic: rcases min_cases r ε with (h' | h')
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
a_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
a_int : (interior a).Nonempty
r : ℝ
ar : a ⊆ closedBall x r
μr :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h' : min r ε = r ∧ r ≤ ε
⊢ (min r ε, x, a).2.2 ⊆ closedBall (min r ε, x, a).2.1 (min r ε, x, a).1
have refine_1 : (r, x, a).2.2 ⊆ closedBall (r, x, a).2.1 (r, x, a).1
Tactic: rwa [h'.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
a_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
a_int : (interior a).Nonempty
r : ℝ
ar : a ⊆ closedBall x r
μr :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
h' : min r ε = ε ∧ ε < r
⊢ (min r ε, x, a).2.2 ⊆ closedBall (min r ε, x, a).2.1 (min r ε, x, a).1
have refine_1 : (ε, x, a).2.2 ⊆ closedBall (ε, x, a).2.1 (ε, x, a).1
Tactic: rwa [h'.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
a_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
a_int : (interior a).Nonempty
r : ℝ
ar : a ⊆ closedBall x r
μr :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (closedBall (min r ε, x, a).2.1 (3 * (min r ε, x, a).1)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (min r ε, x, a).2.2 : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall (min r ε, x, a).2.1 (3 * (min r ε, x, a).1)) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) : ℝ≥0∞)
Tactic: apply le_trans ?_ μr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
x : α
xs : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ f x
h'a : a ⊆ closedBall x ε
a_closed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
a_int : (interior a).Nonempty
r : ℝ
ar : a ⊆ closedBall x r
μr :
  (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
    HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall (min r ε, x, a).2.1 (3 * (min r ε, x, a).1)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) : ℝ≥0∞)
have h₁ : (min r ε, x, a).1 ≤ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
Tactic: have A : ∀ x ∈ s, ∀ ε : ℝ, ε > 0 → ∃ p, p ∈ t ∧ p.1 ≤ ε ∧ p.2.1 = x := by
      intro x xs ε εpos
      rcases ffine x xs ε εpos with ⟨a, ha, h'a⟩
      rcases fsubset x xs ha with ⟨a_closed, a_int, ⟨r, ar, μr⟩⟩
      refine ⟨⟨min r ε, x, a⟩, ⟨?_, ?_, a_int, a_closed, ha, xs⟩, min_le_right _ _, rfl⟩
      · rcases min_cases r ε with (h' | h') <;> rwa [h'.1]
      · apply le_trans ?_ μr
        gcongr
        apply min_le_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have rcases : ∀ (t' : Set (ℝ × α × Set α)) (t't : t' ⊆ t),
  t'.Countable →
    ∀ (t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2)
      (μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)),
      ∃ (t : Set (α × Set α)),
        (∀ p ∈ t, p.1 ∈ s) ∧
          (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
            (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases exists_disjoint_covering_ae μ s t C (fun p => p.1) (fun p => p.2.1) (fun p => p.2.2)
        (fun p hp => hp.1) (fun p hp => hp.2.1) (fun p hp => hp.2.2.1) (fun p hp => hp.2.2.2.1) A
      with ⟨t', t't, _, t'_disj, μt'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : ∀ (p : α × Set α), Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p → p.1 ∈ s
Tactic: refine ⟨(fun p : ℝ × α × Set α => p.2) '' t', ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : ∀ (p : α × Set α), Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p → p.1 ∈ s
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_2 : PairwiseDisjoint (α := Set α) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') fun (p : α × Set α) ↦ p.2
Tactic: refine ⟨(fun p : ℝ × α × Set α => p.2) '' t', ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : ∀ (p : α × Set α), Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p → p.1 ∈ s
refine_2 : PairwiseDisjoint (α := Set α) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') fun (p : α × Set α) ↦ p.2
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_3 : ∀ (p : α × Set α), Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p → p.2 ∈ f p.1
Tactic: refine ⟨(fun p : ℝ × α × Set α => p.2) '' t', ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Vitali (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
C : ℝ≥0
h :
  ∀ (x : α),
    ∃ᶠ (r : ℝ) in 𝓝[>] 0,
      (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
        HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (closedBall x r) : ℝ≥0∞)
s : Set α
f : α → Set (Set α)
fsubset :
  ∀ x ∈ s,
    f x ⊆
      {a : Set α |
        IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a ∧
          (interior a).Nonempty ∧
            ∃ (r : ℝ),
              a ⊆ closedBall x r ∧
                (μ : (a : Set α) → ℝ≥0∞) (closedBall x (3 * r)) ≤
                  HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) a : ℝ≥0∞)}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
t : Set (ℝ × α × Set α) :=
  {p : ℝ × α × Set α |
    p.2.2 ⊆ closedBall p.2.1 p.1 ∧
      (μ : (a : Set α) → ℝ≥0∞) (closedBall p.2.1 (3 * p.1)) ≤
          HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) p.2.2 : ℝ≥0∞) ∧
        (interior p.2.2).Nonempty ∧
          IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
A : ∀ x ∈ s, ∀ ε > 0, ∃ p ∈ t, p.1 ≤ ε ∧ p.2.1 = x
t' : Set (ℝ × α × Set α)
t't : t' ⊆ t
left : t'.Countable
t'_disj : t'.PairwiseDisjoint (α := Set α) fun (p : ℝ × α × Set α) ↦ p.2.2
μt' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ a ∈ t', a.2.2) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : ∀ (p : α × Set α), Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p → p.1 ∈ s
refine_2 : PairwiseDisjoint (α := Set α) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') fun (p : α × Set α) ↦ p.2
refine_3 :
  ∀ (p : α × Set α), Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p → p.2 ∈ f p.1
⊢ ∃ (t : Set (α × Set α)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set α) fun (p : α × Set α) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ ⋃ p ∈ t, p.2) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_4 : Eq (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞)
      (s \
        ⋃ (p : α × Set α),
          ⋃ (_ : Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p), p.2) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: refine ⟨(fun p : ℝ × α × Set α => p.2) '' t', ?_, ?_, ?_, ?_⟩