awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [union_comm, inter_comm, measure_union_add_inter₀ t hs, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₃ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [union_comm, inter_comm, measure_union_add_inter₀ t hs, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [← measure_union_add_inter₀ s ht, hd, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
rw :
  (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_union_add_inter₀ s ht, hd, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
rw :
  (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₁ :
  (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
Tactic: rw [← measure_union_add_inter₀ s ht, hd, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : (μ : (a : Set α) → ℝ≥0∞) (t ∪ s) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [union_comm, measure_union₀ hs (AEDisjoint.symm hd), add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
rw :
  (μ : (a : Set α) → ℝ≥0∞) (t ∪ s) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [union_comm, measure_union₀ hs (AEDisjoint.symm hd), add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
rw :
  (μ : (a : Set α) → ℝ≥0∞) (t ∪ s) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [union_comm, measure_union₀ hs (AEDisjoint.symm hd), add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) univ
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ sᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [← measure_union₀' hs aedisjoint_compl_right, union_compl_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ sᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) univ
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [← measure_union₀' hs aedisjoint_compl_right, union_compl_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable β
μ : Measure (α × β)
x : α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    (∑' (y : β), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
  ((μ : (a : Set (α × β)) → ℝ≥0∞) (⋃ (i : β), {(x, i)}) : ℝ≥0∞)
Tactic: rw [← measure_iUnion (by simp [Pairwise]) fun _ ↦ .singleton _, iUnion_singleton_eq_range,
    preimage_fst_singleton_eq_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable β
μ : Measure (α × β)
x : α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    ((μ : (a : Set (α × β)) → ℝ≥0∞) (⋃ (i : β), {(x, i)}) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    (∑' (y : β), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
  ((μ : (a : Set (α × β)) → ℝ≥0∞) (range (Prod.mk x)) : ℝ≥0∞)
Tactic: rw [← measure_iUnion (by simp [Pairwise]) fun _ ↦ .singleton _, iUnion_singleton_eq_range,
    preimage_fst_singleton_eq_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable β
μ : Measure (α × β)
x : α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    ((μ : (a : Set (α × β)) → ℝ≥0∞) (⋃ (i : β), {(x, i)}) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    ((μ : (a : Set (α × β)) → ℝ≥0∞) (range (Prod.mk x)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    (∑' (y : β), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (range fun (x_1 : β) ↦ (x, x_1)) : ℝ≥0∞)
  ((μ : (a : Set (α × β)) → ℝ≥0∞) (range (Prod.mk x)) : ℝ≥0∞)
Tactic: rw [← measure_iUnion (by simp [Pairwise]) fun _ ↦ .singleton _, iUnion_singleton_eq_range,
    preimage_fst_singleton_eq_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable α
μ : Measure (α × β)
y : β
⊢ Eq (α := Set (α × β)) (Prod.snd ⁻¹' {y}) (⋃ (x : α), {(x, y)})
have h : ∀ (y_1 : α × β),
  Membership.mem (γ := Set (α × β)) (Prod.snd ⁻¹' {y}) y_1 ↔ Membership.mem (γ := Set (α × β)) (⋃ (x : α), {(x, y)}) y_1
Tactic: ext y
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (hypothesis)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable α
μ : Measure (α × β)
y : β
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' {y}) : ℝ≥0∞)
    (∑' (x : α), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
have this : Eq (α := Set (α × β)) (Prod.snd ⁻¹' {y}) (⋃ (x : α), {(x, y)})
Tactic: have : Prod.snd ⁻¹' {y} = ⋃ x : α, {(x, y)} := by ext y; simp [Prod.ext_iff, eq_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable α
μ : Measure (α × β)
y : β
this : Eq (α := Set (α × β)) (Prod.snd ⁻¹' {y}) (⋃ (x : α), {(x, y)})
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' {y}) : ℝ≥0∞)
    (∑' (x : α), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
have hn : Pairwise.{u_2} (α := α) (Function.onFun (β := Set (α × β)) Disjoint fun (x : α) ↦ {(x, y)})
Tactic: rw [this, measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable α
μ : Measure (α × β)
y : β
this : Eq (α := Set (α × β)) (Prod.snd ⁻¹' {y}) (⋃ (x : α), {(x, y)})
hn : Pairwise.{u_2} (α := α) (Function.onFun (β := Set (α × β)) Disjoint fun (x : α) ↦ {(x, y)})
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' {y}) : ℝ≥0∞)
    (∑' (x : α), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
have h : ∀ (i : α), MeasurableSet (α := α × β) {(i, y)}
Tactic: rw [this, measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Fintype β
μ : Measure (α × β)
x : α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    (∑ y : β, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑' (y : β), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)}) (∑ y : β, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
Tactic: rw [measure_preimage_fst_singleton_eq_tsum μ x, tsum_fintype]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Fintype β
μ : Measure (α × β)
x : α
rw :
  Eq (α := ℝ≥0∞) (∑' (y : β), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
    (∑ y : β, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.fst ⁻¹' {x}) : ℝ≥0∞)
    (∑ y : β, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (∑ b : β, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, b)}) (∑ y : β, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
Tactic: rw [measure_preimage_fst_singleton_eq_tsum μ x, tsum_fintype]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Fintype α
μ : Measure (α × β)
y : β
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' {y}) : ℝ≥0∞)
    (∑ x : α, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑' (x : α), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)}) (∑ x : α, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
Tactic: rw [measure_preimage_snd_singleton_eq_tsum μ y, tsum_fintype]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Fintype α
μ : Measure (α × β)
y : β
rw :
  Eq (α := ℝ≥0∞) (∑' (x : α), (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
    (∑ x : α, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (Prod.snd ⁻¹' {y}) : ℝ≥0∞)
    (∑ x : α, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)} : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (∑ b : α, (μ : (a : Set (α × β)) → ℝ≥0∞) {(b, y)}) (∑ x : α, (μ : (a : Set (α × β)) → ℝ≥0∞) {(x, y)})
Tactic: rw [measure_preimage_snd_singleton_eq_tsum μ y, tsum_fintype]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ_1 : Measure α
s t : Set α
x : MeasurableSpace α
μ : Measure α
⊢ μ.trim ≤ μ.toOuterMeasure
have nth_rewrite : μ.trim ≤ μ.trim
Tactic: nth_rewrite 2 [← μ.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen[inst] U
⊢ U =ᶠ[ae μ] ∅ ↔ U = ∅
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ U = ∅
Tactic: rw [ae_eq_empty, hU.measure_zero_iff_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
U : Set X
hU : IsOpen[inst] U
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ U = ∅
⊢ U =ᶠ[ae μ] ∅ ↔ U = ∅
have rw₁ : U = ∅ ↔ U = ∅
Tactic: rw [ae_eq_empty, hU.measure_zero_iff_eq_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst] F
h : F = univ
⊢ F =ᶠ[ae μ] univ
have rw : univ =ᶠ[ae μ] univ
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst] F
⊢ F =ᶠ[ae μ] univ ↔ F = univ
have refine : ∀ (h : F =ᶠ[ae μ] univ), F = univ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst] F
h : F =ᶠ[ae μ] univ
⊢ F = univ
have rwa : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Fᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), F = univ
Tactic: rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst] F
h : F =ᶠ[ae μ] univ
rwa : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Fᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), F = univ
⊢ F = univ
have rwa₁ : ∀ (h : Fᶜ = ∅), F = univ
Tactic: rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst] F
h : F =ᶠ[ae μ] univ
rwa : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Fᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), F = univ
rwa₁ : ∀ (h : Fᶜ = ∅), F = univ
⊢ F = univ
have rwa₂ : ∀ (h : F = univ), F = univ
Tactic: rwa [ae_eq_univ, hF.isOpen_compl.measure_eq_zero_iff μ, compl_empty_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
inst_2 : OpensMeasurableSpace X
inst_3 : IsFiniteMeasure μ
hF : IsClosed[inst] F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ↔ F = univ
have rw : F =ᶠ[ae μ] univ ↔ F = univ
Tactic: rw [← ae_eq_univ_iff_measure_eq hF.measurableSet.nullMeasurableSet, hF.ae_eq_univ_iff_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
inst_2 : OpensMeasurableSpace X
inst_3 : IsFiniteMeasure μ
hF : IsClosed[inst] F
rw : F =ᶠ[ae μ] univ ↔ F = univ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ↔ F = univ
have rw₁ : F = univ ↔ F = univ
Tactic: rw [← ae_eq_univ_iff_measure_eq hF.measurableSet.nullMeasurableSet, hF.ae_eq_univ_iff_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
inst_2 : OpensMeasurableSpace X
inst_3 : IsProbabilityMeasure μ
hF : IsClosed[inst] F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) (1 : ℝ≥0∞) ↔ F = univ
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ↔ F = univ
Tactic: rw [← measure_univ (μ := μ), hF.measure_eq_univ_iff_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
F : Set X
inst_2 : OpensMeasurableSpace X
inst_3 : IsProbabilityMeasure μ
hF : IsClosed[inst] F
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) ↔ F = univ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) F : ℝ≥0∞) (1 : ℝ≥0∞) ↔ F = univ
have rw₁ : F = univ ↔ F = univ
Tactic: rw [← measure_univ (μ := μ), hF.measure_eq_univ_iff_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst_1 : μ.IsOpenPosMeasure
p : X → Prop
hp : ∀ᵐ (x : X) ∂μ, p x
⊢ Dense.{u_1} (X := X) {x : X | p x}
have rw : Eq.{u_1 + 1} (α := Set X) (interior {x : X | p x}ᶜ) ∅
Tactic: rw [dense_iff_closure_eq, closure_eq_compl_interior_compl, compl_univ_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
h : f =ᶠ[ae (μ.restrict U)] g
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
⊢ EqOn f g U
have h₁ : ∀ᵐ (x : X) ∂μ, x ∈ U → f x = g x
Tactic: replace h := ae_imp_of_ae_restrict h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : ∀ᵐ (x : X) ∂μ, x ∈ U → f x = g x
⊢ EqOn f g U
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [ae_iff, Classical.not_imp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsOpen[inst] (U ∩ {a : X | f a ≠ g a})
have refine : ∀ (a : X) (ha : a ∈ U ∩ {a : X | f a ≠ g a}), {a : X | f a ≠ g a} ∈ 𝓝 a
Tactic: refine isOpen_iff_mem_nhds.mpr fun a ha => inter_mem (hU.mem_nhds ha.1) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
a : X
ha : a ∈ U ∩ {a : X | f a ≠ g a}
⊢ {a : X | f a ≠ g a} ∈ 𝓝 a
have ha₁ : a ∈ U
Tactic: rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.OpenPos (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
m : MeasurableSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space Y
μ : Measure X
inst_3 : μ.IsOpenPosMeasure
U : Set X
f g : X → Y
hU : IsOpen[inst] U
hf : ContinuousOn f U
hg : ContinuousOn g U
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) {a : X | a ∈ U ∧ ¬f a = g a} : ℝ≥0∞) (0 : ℝ≥0∞)
a : X
ha : a ∈ U ∩ {a : X | f a ≠ g a}
ha₁ : a ∈ U
⊢ {a : X | f a ≠ g a} ∈ 𝓝 a
have ha' : (f a, g a) ∈ (diagonal Y)ᶜ
Tactic: rcases ha with ⟨ha : a ∈ U, ha' : (f a, g a) ∈ (diagonal Y)ᶜ⟩
Cleared hypotheses: ha