awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β},
    MeasurableSet s →
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
s : Set (α × β)
hs : MeasurableSet s
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
h₁ :
  ∀ (t : Set (α × β))
    (ht :
      Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        t),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : ∀ (t : Set (α × β)) (htm : MeasurableSet t),
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) tᶜ : ℝ≥0∞)
Tactic: refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod (by simp)
    ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β},
    MeasurableSet s →
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
s : Set (α × β)
hs : MeasurableSet s
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
h₁ :
  ∀ (t : Set (α × β))
    (ht :
      Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        t),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞)
h₂ :
  ∀ (t : Set (α × β)) (htm : MeasurableSet t),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) tᶜ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : ∀ (f : ℕ → Set (α × β)),
  Pairwise (Disjoint on f) →
    ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)),
      (∀ (i : ℕ),
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (f i) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (f i) : ℝ≥0∞)) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
          ((ν : (a : Set (α × β)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
Tactic: refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod (by simp)
    ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h_1 :
  ∀ {s : Set α} {t : Set β},
    MeasurableSet s →
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
s : Set (α × β)
hs : MeasurableSet s
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
t : Set (α × β)
ht : MeasurableSet t
h : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have h₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((μ : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [measure_compl ht (measure_ne_top _ _), h, h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h_1 :
  ∀ {s : Set α} {t : Set β},
    MeasurableSet s →
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
s : Set (α × β)
hs : MeasurableSet s
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
t : Set (α × β)
ht : MeasurableSet t
h : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((μ : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have h₂ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [measure_compl ht (measure_ne_top _ _), h, h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β},
    MeasurableSet s →
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
s : Set (α × β)
hs : MeasurableSet s
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
f : ℕ → Set (α × β)
h_disj : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (f i) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((ν : (a : Set (α × β)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set (α × β)) → ℝ≥0∞) (f i)) (∑' (i : ℕ), (ν : (a : Set (α × β)) → ℝ≥0∞) (f i))
Tactic: simp_rw [measure_iUnion h_disj hf, h_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h : μ = ν
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
⊢ μ = ν
have h₁ : ∀ (s : Set (α × β × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
have simp_rw : Eq (α := ℝ≥0∞)
  ((μ : (a : Set (α × β × γ)) → ℝ≥0∞)
      (SProd.sprod (α := Set α) univ (SProd.sprod (α := Set β) (β := Set γ) univ univ)) :
    ℝ≥0∞)
  ((ν : (a : Set (α × β × γ)) → ℝ≥0∞)
      (SProd.sprod (α := Set α) univ (SProd.sprod (α := Set β) (β := Set γ) univ univ)) :
    ℝ≥0∞)
Tactic: simp_rw [← univ_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: have h_univ : μ univ = ν univ := by
    simp_rw [← univ_prod_univ]
    exact h .univ .univ .univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have this : IsFiniteMeasure ν
Tactic: have : IsFiniteMeasure ν := ⟨by simp [← h_univ]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) :=
  image2 (fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} C₂
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Prod.instMeasurableSpace = generateFrom C
Tactic: refine MeasurableSpace.induction_on_inter (s := C) ?_ ?_ (by simp) ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) :=
  image2 (fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} C₂
h₁ : Prod.instMeasurableSpace = generateFrom C
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : IsPiSystem C
Tactic: refine MeasurableSpace.induction_on_inter (s := C) ?_ ?_ (by simp) ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) :=
  image2 (fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} C₂
h₁ : Prod.instMeasurableSpace = generateFrom C
h₂ : IsPiSystem C
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₃ : ∀ (t : Set (α × β × γ)) (ht : t ∈ C),
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine MeasurableSpace.induction_on_inter (s := C) ?_ ?_ (by simp) ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) :=
  image2 (fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} C₂
h₁ : Prod.instMeasurableSpace = generateFrom C
h₂ : IsPiSystem C
h₃ :
  ∀ (t : Set (α × β × γ)) (ht : t ∈ C),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₄ : ∀ (t : Set (α × β × γ)) (htm : MeasurableSet t),
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) tᶜ : ℝ≥0∞)
Tactic: refine MeasurableSpace.induction_on_inter (s := C) ?_ ?_ (by simp) ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) :=
  image2 (fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} C₂
h₁ : Prod.instMeasurableSpace = generateFrom C
h₂ : IsPiSystem C
h₃ :
  ∀ (t : Set (α × β × γ)) (ht : t ∈ C),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
h₄ :
  ∀ (t : Set (α × β × γ)) (htm : MeasurableSet t),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) tᶜ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
have h₅ : ∀ (f : ℕ → Set (α × β × γ)),
  Pairwise (Disjoint on f) →
    ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)),
      (∀ (i : ℕ),
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (f i) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (f i) : ℝ≥0∞)) →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
          ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
Tactic: refine MeasurableSpace.induction_on_inter (s := C) ?_ ?_ (by simp) ?_ ?_ ?_ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) :=
  image2 (fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} C₂
⊢ Prod.instMeasurableSpace = generateFrom C
have h₁ : IsCountablySpanning C₂
Tactic: refine (generateFrom_eq_prod (C := { s : Set α | MeasurableSet s }) (D := C₂) (by simp)
      generateFrom_prod isCountablySpanning_measurableSet ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h_1 :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) :=
  image2 (fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} C₂
t : Set (α × β × γ)
ht : MeasurableSet t
h : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have h₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [measure_compl ht (measure_ne_top _ _), h, h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h_1 :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) :=
  image2 (fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} C₂
t : Set (α × β × γ)
ht : MeasurableSet t
h : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
h₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have h₂ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [measure_compl ht (measure_ne_top _ _), h, h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) :=
  image2 (fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} C₂
f : ℕ → Set (α × β × γ)
h_disj : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (f i) : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set (α × β × γ)) → ℝ≥0∞) (f i))
  (∑' (i : ℕ), (ν : (a : Set (α × β × γ)) → ℝ≥0∞) (f i))
Tactic: simp_rw [measure_iUnion h_disj hf, h_eq]