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}
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∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (s \
          ⋃ (p : α × Set α),
            ⋃ (_ : Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p), p.2) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have h₁ : Eq.{u_1 + 1} (α := Set α)
  (⋃ (p : α × Set α), ⋃ (_ : Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p), p.2)
  (⋃ a ∈ t', a.2.2)
Tactic: convert! μt' using 3
-- 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∞)
⊢ Eq.{u_1 + 1} (α := Set α)
    (⋃ (p : α × Set α), ⋃ (_ : Membership.mem (γ := Set (α × Set α)) ((fun (p : ℝ × α × Set α) ↦ p.2) '' t') p), p.2)
    (⋃ a ∈ t', a.2.2)
have h₁ : Eq.{u_1 + 1} (α := Set α) (⋃ y ∈ t', y.2.2) (⋃ a ∈ t', a.2.2)
Tactic: rw [biUnion_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst_1 : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal)
      ((ρ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal)
      ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal) =
    ∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X))
have rw : HAdd.hAdd (α := ENNReal) (β := ENNReal) (0 : ENNReal)
    ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal) =
  ∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
    (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X))
Tactic: rw [hρ h.measure_diff_biUnion, zero_add,
        measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst_1 : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
rw :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) (0 : ENNReal)
      ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal) =
    ∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X))
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal)
      ((ρ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal)
      ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal) =
    ∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X))
have rw₁ : Eq (α := ENNReal)
  ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal)
  (∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X)) :
    ENNReal)
Tactic: rw [hρ h.measure_diff_biUnion, zero_add,
        measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst_1 : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
rw :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) (0 : ENNReal)
      ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal) =
    ∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X))
rw₁ :
  Eq (α := ENNReal)
    ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal)
    (∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
        (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X)) :
      ENNReal)
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal)
      ((ρ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal)
      ((ρ : (a : Set X) → ENNReal) (⋃ p ∈ h.index (f := f) (s := s), h.covering (f := f) (s := s) p) : ENNReal) =
    ∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
      (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X))
have rw₂ : Eq (α := ENNReal)
  (∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
    (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X)))
  (∑' (p : (↑(h.index (f := f) (s := s)) : Type u_1)),
    (ρ : (a : Set X) → ENNReal) (h.covering (f := f) (s := s) (↑p : X × Set X)))
Tactic: rw [hρ h.measure_diff_biUnion, zero_add,
        measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
ε : ℝ
εpos : ε > 0
⊢ ∃ s ∈ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, s ⊆ closedBall x ε
have rcases : ∀ (s : Set X) (hs : s ∈ v.setsAt x) (h's : s ⊆ closedBall x ε),
  ∃ s ∈ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, s ⊆ closedBall x ε
Tactic: rcases v.nontrivial x ε εpos with ⟨s, hs, h's⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε
have obtain : ∀ (t : Set X) (tf : t ∈ f x) (ht : t ⊆ closedBall x (min ε δ)), ∃ t ∈ g x, t ⊆ closedBall x ε
Tactic: obtain ⟨t, tf, ht⟩ : ∃ t ∈ f x, t ⊆ closedBall x (min ε δ) :=
        ffine x hx (min ε δ) (lt_min εpos δpos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε
have inl : ∀ (h't : t ∈ v.setsAt x), ∃ t ∈ g x, t ⊆ closedBall x ε
Tactic: rcases fset x hx tf with (h't | h't)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
inl : ∀ (h't : t ∈ v.setsAt x), ∃ t ∈ g x, t ⊆ closedBall x ε
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε
have inr : ∀
  (h't :
    Membership.mem (γ := Set (Set X)) {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ} t),
  ∃ t ∈ g x, t ⊆ closedBall x ε
Tactic: rcases fset x hx tf with (h't | h't)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
x : X
hx : x ∈ s
ε : ℝ
εpos : ε > 0
t : Set X
tf : t ∈ f x
ht : t ⊆ closedBall x (min ε δ)
h't : Membership.mem (γ := Set (Set X)) {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ} t
⊢ ∃ t ∈ g x, t ⊆ closedBall x ε
have inr : t ⊆ closedBall x δ
Tactic: refine False.elim (h't.2.2 ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (hypothesis)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
⊢ ∃ (t : Set (X × Set X)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧
          Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)
have this : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ g x, t ⊆ closedBall x ε
Tactic: have : ∀ x ∈ s, ∀ ε : ℝ, ε > 0 → ∃ t ∈ g x, t ⊆ closedBall x ε := by
      intro x hx ε εpos
      obtain ⟨t, tf, ht⟩ : ∃ t ∈ f x, t ⊆ closedBall x (min ε δ) :=
        ffine x hx (min ε δ) (lt_min εpos δpos)
      rcases fset x hx tf with (h't | h't)
      · exact ⟨t, ⟨tf, h't⟩, ht.trans (closedBall_subset_closedBall (min_le_left _ _))⟩
      · refine False.elim (h't.2.2 ?_)
        exact ht.trans (closedBall_subset_closedBall (min_le_right _ _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s : Set X | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun (x : X) ↦ f x ∩ v.setsAt x
this : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ g x, t ⊆ closedBall x ε
⊢ ∃ (t : Set (X × Set X)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧
          Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)
have rcases : ∀ (t : Set (X × Set X)) (ts : ∀ p ∈ t, p.1 ∈ s) (tdisj : t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2)
  (tg : ∀ p ∈ t, p.2 ∈ g p.1)
  (μt : Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)),
  ∃ (t : Set (X × Set X)),
    (∀ p ∈ t, p.1 ∈ s) ∧
      (t.PairwiseDisjoint (α := Set X) fun (p : X × Set X) ↦ p.2) ∧
        (∀ p ∈ t, p.2 ∈ f p.1) ∧
          Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) (s \ ⋃ p ∈ t, p.2) : ENNReal) (0 : ENNReal)
Tactic: rcases v.covering s g (fun x _ => inter_subset_right) this with ⟨t, ts, tdisj, tg, μt⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
⊢ ∀ᶠ (t : Set X) in v.filterAt x, MeasurableSet t
have h : ∀ (a : Set X),
  Membership.mem (γ := Set (Set X))
    {x_1 : Set X |
      Membership.mem (γ := Set (Set X)) {x_2 : Set X | (fun (t : Set X) ↦ t ∈ v.setsAt x) x_2} x_1 →
        Membership.mem (γ := Set (Set X)) {x : Set X | (fun (t : Set X) ↦ MeasurableSet t) x} x_1}
    a
Tactic: filter_upwards [v.eventually_filterAt_mem_setsAt x] with _ ha using v.measurableSet _ _ ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
h :
  ∀ (a : Set X),
    Membership.mem (γ := Set (Set X))
      {x_1 : Set X |
        Membership.mem (γ := Set (Set X)) {x_2 : Set X | (fun (t : Set X) ↦ t ∈ v.setsAt x) x_2} x_1 →
          Membership.mem (γ := Set (Set X)) {x : Set X | (fun (t : Set X) ↦ MeasurableSet t) x} x_1}
      a
⊢ ∀ᶠ (t : Set X) in v.filterAt x, MeasurableSet t
have h₁ : ∀ a ∈ v.setsAt x, MeasurableSet a
Tactic: filter_upwards [v.eventually_filterAt_mem_setsAt x] with _ ha using v.measurableSet _ _ ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ (v.enlarge δ δpos).filterAt = v.filterAt
have h : ∀ (x : X), (v.enlarge δ δpos).filterAt x = v.filterAt x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
⊢ (v.enlarge δ δpos).filterAt x = v.filterAt x
have h : {t : Set X | MeasurableSet t → (interior t).Nonempty → ¬t ⊆ closedBall x δ → t ∈ v.setsAt x} ∈ (𝓝 x).smallSets
Tactic: suffices {t | MeasurableSet t → (interior t).Nonempty → ¬t ⊆ closedBall x δ →
      t ∈ v.setsAt x} ∈ (𝓝 x).smallSets by
    simpa [VitaliFamily.filterAt, VitaliFamily.enlarge, ← sup_principal, inf_sup_left,
      mem_inf_principal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
⊢ {t : Set X | MeasurableSet t → (interior t).Nonempty → ¬t ⊆ closedBall x δ → t ∈ v.setsAt x} ∈ (𝓝 x).smallSets
have h : ∀ a ⊆ closedBall x δ, MeasurableSet a → (interior a).Nonempty → ¬a ⊆ closedBall x δ → a ∈ v.setsAt x
Tactic: filter_upwards [eventually_smallSets_subset.mpr (closedBall_mem_nhds _ δpos)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.VitaliFamily (goal)
Goal:
X : Type u_1
inst : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
⊢ v.FineSubfamilyOn f s ↔ ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
have refine : ∀ (x : X) (hx : x ∈ s), (∀ ε > 0, ∃ t ∈ v.setsAt x ∩ f x, t ⊆ closedBall x ε) ↔ ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
Tactic: refine forall₂_congr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
⊢ StronglyMeasurable.{u_1, u_2} (α := α) (β := β)
    (if h : ∃ (b : β), f = mk (const α b) ⋯ then const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) ⋯) h)
    else AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯)
have pos : ∀ (h : ∃ (b : β), f = mk (const α b) sorry),
  StronglyMeasurable (const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) sorry) h))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
pos :
  ∀ (h : ∃ (b : β), f = mk (const α b) ⋯),
    StronglyMeasurable (const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) ⋯) h))
⊢ StronglyMeasurable.{u_1, u_2} (α := α) (β := β)
    (if h : ∃ (b : β), f = mk (const α b) ⋯ then const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) ⋯) h)
    else AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯)
have neg : ∀ (h : ¬∃ (b : β), f = mk (const α b) sorry), StronglyMeasurable (AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) sorry)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
⊢ mk
      (if h : ∃ (b : β), f = mk (const α b) ⋯ then
        const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) ⋯) h)
      else AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯)
      ⋯ =
    f
have pos : ∀ (h : ∃ (b : β), f = mk (const α b) sorry),
  mk (const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) sorry) h)) sorry = f
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
pos :
  ∀ (h : ∃ (b : β), f = mk (const α b) ⋯),
    mk (const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) ⋯) h)) ⋯ = f
⊢ mk
      (if h : ∃ (b : β), f = mk (const α b) ⋯ then
        const α (Classical.choose (p := fun (x : β) ↦ f = mk (const α x) ⋯) h)
      else AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯)
      ⋯ =
    f
have neg : ∀ (h : ¬∃ (b : β), f = mk (const α b) sorry), mk (AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) sorry) sorry = f
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ (b : β), f = mk (const α b) ⋯
| f
have rw : Quotient.mk'' (Quotient.out f)
Tactic: rw [← Quotient.out_eq' f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ (b : β), f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯) ⋯ = f
have neg : mk (AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) sorry) sorry = Quotient.mk'' (Quotient.out f)
Tactic: conv_rhs => rw [← Quotient.out_eq' f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α →ₘ[μ] β
h : ¬∃ (b : β), f = mk (const α b) ⋯
⊢ mk (AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) ⋯) ⋯ = Quotient.mk'' (Quotient.out f)
have neg : AEStronglyMeasurable.mk (↑(Quotient.out f) : α → β) sorry =ᶠ[ae μ] (↑(Quotient.out f) : α → β)
Tactic: rw [← mk, mk_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f g : α →ₘ[μ] β
h : (↑f : α → β) =ᶠ[ae μ] (↑g : α → β)
⊢ f = g
have rwa : mk (↑f : α → β) sorry = g
Tactic: rwa [← f.mk_coeFn, ← g.mk_coeFn, mk_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f g : α →ₘ[μ] β
h : (↑f : α → β) =ᶠ[ae μ] (↑g : α → β)
rwa : mk (↑f : α → β) ⋯ = g
⊢ f = g
have rwa₁ : mk (↑f : α → β) sorry = mk (↑g : α → β) sorry
Tactic: rwa [← f.mk_coeFn, ← g.mk_coeFn, mk_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ (↑(mk f hf) : α → β) =ᶠ[ae μ] f
have rw : mk (↑(mk f hf) : α → β) sorry = mk f hf
Tactic: rw [← mk_eq_mk (hf := AEEqFun.aestronglyMeasurable ..) (hg := hf), mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f : α → β
hf : AEStronglyMeasurable f μ
rw : mk (↑(mk f hf) : α → β) ⋯ = mk f hf
⊢ (↑(mk f hf) : α → β) =ᶠ[ae μ] f
have rw₁ : mk f hf = mk f hf
Tactic: rw [← mk_eq_mk (hf := AEEqFun.aestronglyMeasurable ..) (hg := hf), mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
⊢ g.compQuasiMeasurePreserving f hf = mk ((↑g : β → γ) ∘ f) ⋯
have rw : g.compQuasiMeasurePreserving f hf = (mk (↑g : β → γ) sorry).compQuasiMeasurePreserving f hf
Tactic: rw [← compQuasiMeasurePreserving_mk g.aestronglyMeasurable hf, mk_coeFn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqFun (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace γ
inst_2 : MeasurableSpace β
ν : Measure β
f : α → β
g : β →ₘ[ν] γ
hf : QuasiMeasurePreserving f μ ν
rw : g.compQuasiMeasurePreserving f hf = (mk (↑g : β → γ) ⋯).compQuasiMeasurePreserving f hf
⊢ g.compQuasiMeasurePreserving f hf = mk ((↑g : β → γ) ∘ f) ⋯
have rw₁ : g.compQuasiMeasurePreserving f hf = g.compQuasiMeasurePreserving f hf
Tactic: rw [← compQuasiMeasurePreserving_mk g.aestronglyMeasurable hf, mk_coeFn]