awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
s : Set β
⊢ Membership.mem (γ := Filter β) (Filter.map (⇑f : (a : α) → β) (ae μ)) s ↔
    s ∈ ae (F := Measure β) (map (⇑f : (a : α) → β) μ)
have h : (⇑f : (a : α) → β) ⁻¹' s ∈ ae μ ↔ s ∈ ae (F := Measure β) (map (⇑f : (a : α) → β) μ)
Tactic: simp_rw [mem_map, mem_ae_iff, ← preimage_compl, f.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
s : Set β
h : (⇑f : (a : α) → β) ⁻¹' s ∈ ae μ ↔ s ∈ ae (F := Measure β) (map (⇑f : (a : α) → β) μ)
⊢ Membership.mem (γ := Filter β) (Filter.map (⇑f : (a : α) → β) (ae μ)) s ↔
    s ∈ ae (F := Measure β) (map (⇑f : (a : α) → β) μ)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) (((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [mem_map, mem_ae_iff, ← preimage_compl, f.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Map (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
s : Set β
h : (⇑f : (a : α) → β) ⁻¹' s ∈ ae μ ↔ s ∈ ae (F := Measure β) (map (⇑f : (a : α) → β) μ)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Filter β) (Filter.map (⇑f : (a : α) → β) (ae μ)) s ↔
    s ∈ ae (F := Measure β) (map (⇑f : (a : α) → β) μ)
have h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f : (a : α) → β) ⁻¹' sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) (((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [mem_map, mem_ae_iff, ← preimage_compl, f.map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
have contrapose! : ∀ (hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
ht : MeasurableSet t
⊢ 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∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
  HAdd.hAdd (β := ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [← measure_inter_add_diff (s ∪ t) ht, Set.union_inter_cancel_right, union_diff_right, ←
    measure_inter_add_diff s ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ 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 ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ 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.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet 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∞)
⊢ 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 ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ 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.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet 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.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet 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.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)
have haveI : ∀ (this : Encodable (↑s : Type u_2)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)
Tactic: haveI := hs.toEncodable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : β → Set α
hs : s.Countable
hd : s.Pairwise (AEDisjoint μ on f)
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
this : Encodable (↑s : Type u_2)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
    (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : (↑s : Type u_2)), f (↑x : β)) : ℝ≥0∞)
  (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f (↑p : β)) : ℝ≥0∞)
Tactic: rw [biUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise (AEDisjoint μ)
h : ∀ s ∈ S, NullMeasurableSet s μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ S) : ℝ≥0∞)
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ S, i) : ℝ≥0∞)
  (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
Tactic: rw [sUnion_eq_biUnion, measure_biUnion₀ hs hd h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise (AEDisjoint μ)
h : ∀ s ∈ S, NullMeasurableSet s μ
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ S, i) : ℝ≥0∞)
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ S) : ℝ≥0∞)
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (∑' (p : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑p : Set α))
  (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α))
Tactic: rw [sUnion_eq_biUnion, measure_biUnion₀ hs hd h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise Disjoint
h : ∀ s ∈ S, MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ S) : ℝ≥0∞)
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ S, i) : ℝ≥0∞)
  (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
Tactic: rw [sUnion_eq_biUnion, measure_biUnion hs hd h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hs : S.Countable
hd : S.Pairwise Disjoint
h : ∀ s ∈ S, MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ S, i) : ℝ≥0∞)
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ S) : ℝ≥0∞)
    (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (∑' (p : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑p : Set α))
  (∑' (s : (↑S : Type u_1)), (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α))
Tactic: rw [sUnion_eq_biUnion, measure_biUnion hs hd h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞) (∑ p ∈ s, (μ : (a : Set α) → ℝ≥0∞) (f p) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, f b) : ℝ≥0∞)
  (∑' (b : ↥s), (μ : (a : Set α) → ℝ≥0∞) (f (↑b : ι)) : ℝ≥0∞)
Tactic: rw [← Finset.sum_attach, Finset.attach_eq_univ, ← tsum_fintype (L := .unconditional s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_8
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)
have rw : ∀ (i : Finset ι),
  LE.le (α := ℝ≥0∞) (∑ a ∈ i, (μ : (a : Set α) → ℝ≥0∞) (As a) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)
Tactic: rw [ENNReal.tsum_eq_iSup_sum, iSup_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_8
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
⊢ LE.le (α := ℝ≥0∞) (∑ a ∈ s, (μ : (a : Set α) → ℝ≥0∞) (As a) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)
have simp : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, As b) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)
Tactic: simp only [← measure_biUnion_finset₀ (fun _i _hi _j _hj hij => As_disj hij) fun i _ => As_mble i]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_8
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ b ∈ s, As b) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞)
have h : ∀ (i : ι), ⋃ (_ : i ∈ s), As i ⊆ As i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
hs : s.Countable
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ Eq (α := ℝ≥0∞) (∑' (b : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {(↑b : β)}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑' (b : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {(↑b : β)}) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ s, f ⁻¹' {y}) : ℝ≥0∞)
Tactic: rw [← Set.biUnion_preimage_singleton, measure_biUnion hs (pairwiseDisjoint_fiber f s) hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
hs : s.Countable
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
rw :
  Eq (α := ℝ≥0∞) (∑' (b : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {(↑b : β)}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ s, f ⁻¹' {y}) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (b : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {(↑b : β)}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (∑' (b : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {(↑b : β)}))
  (∑' (p : (↑s : Type u_2)), (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {(↑p : β)}))
Tactic: rw [← Set.biUnion_preimage_singleton, measure_biUnion hs (pairwiseDisjoint_fiber f s) hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : α → β
hs : s.Countable
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {x}) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ s, f ⁻¹' {y}) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {x}) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← biUnion_preimage_singleton, measure_biUnion_null_iff hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Set β
f : α → β
hs : s.Countable
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ y ∈ s, f ⁻¹' {y}) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {x}) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {x}) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : (∀ i ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {i}) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ∀ x ∈ s, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {x}) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← biUnion_preimage_singleton, measure_biUnion_null_iff hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst : MeasurableSingletonClass α
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
have trans : Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) {x}) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' {x}))
Tactic: trans ∑ x ∈ s, μ (id ⁻¹' {x})
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst : MeasurableSingletonClass α
trans : Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) {x}) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' {x}))
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) {x} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
have trans₁ : Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' {x}) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
Tactic: trans ∑ x ∈ s, μ (id ⁻¹' {x})
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst : MeasurableSingletonClass α
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' {x}) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' (↑s : Set α)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
Tactic: rw [sum_measure_preimage_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Finset α
inst : MeasurableSingletonClass α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' (↑s : Set α)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (id ⁻¹' {x}) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
have hf : ∀ y ∈ s, MeasurableSet (α := α) (id ⁻¹' {y})
Tactic: rw [sum_measure_preimage_singleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t \ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
Tactic: rw [← measure_union₀' hs disjoint_sdiff_right.aedisjoint, union_diff_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t \ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
Tactic: rw [← measure_union₀' hs disjoint_sdiff_right.aedisjoint, union_diff_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
hm : NullMeasurableSet t μ
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
  (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)
Tactic: rw [add_comm, measure_add_diff hm, union_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
hm : NullMeasurableSet t μ
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
Tactic: rw [add_comm, measure_add_diff hm, union_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t s : Set α
hm : NullMeasurableSet t μ
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∪ t)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
Tactic: rw [add_comm, measure_add_diff hm, union_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : NullMeasurableSet s₂ μ
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s₁ \ s₂) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
have rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
Tactic: rw [measure_diff' _ h₂ h_fin, union_eq_self_of_subset_right h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : NullMeasurableSet s₂ μ
h_fin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s₁ \ s₂) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
have rw₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
Tactic: rw [measure_diff' _ h₂ h_fin, union_eq_self_of_subset_right h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∩ s₂) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s₁ \ s₂) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ \ s₂) : ℝ≥0∞)
have bc : s₁ ∩ s₂ ⊆ s₂
Tactic: gcongr