awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
⊢ IsFiniteMeasure ν

Tactic:
have : IsFiniteMeasure ν := ⟨by simp [← h_univ]⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) ∅) ((ν : (a : Set (α × β)) → ℝ≥0∞) ∅)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod (by simp)
    ?_ ?_ ?_ s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
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_1 : Set (α × β)
hs_1 : MeasurableSet s_1
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s
t : Set β
ht : Membership.mem (γ := Set (Set β)) {t : Set β | MeasurableSet t} t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t))
    ((ν : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t))

Tactic:
h hs ht
-- Module: Mathlib.MeasureTheory.Measure.Prod
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_1 : Set (α × β)
hs_1 : MeasurableSet s_1
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s
t : Set β
ht : Membership.mem (γ := Set (Set β)) {t : Set β | MeasurableSet t} t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t))
    ((ν : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t))

Tactic:
exact h hs ht
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
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∞)

Tactic:
simp_rw [measure_compl ht (measure_ne_top _ _), h, h_univ]

Premises used: MeasureTheory.measure_compl, MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
h₁ :
  Eq (α := ℝ≥0∞) (∑' (i : ℕ), (μ : (a : Set (α × β)) → ℝ≥0∞) (f i)) (∑' (i : ℕ), (ν : (a : Set (α × β)) → ℝ≥0∞) (f i))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    ((ν : (a : Set (α × β)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
simp_rw [measure_iUnion h_disj hf, h_eq]

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
rw rw₁ :
  Eq (α := ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
h₁ :
  ∀ (s : Set (α × β × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp_rw [← univ_prod_univ]

Premises used: Set.univ_prod_univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
        (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:
h .univ .univ .univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
        (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:
exact h .univ .univ .univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)

Tactic:
have h_univ : μ univ = ν univ := by
    simp_rw [← univ_prod_univ]
    exact h .univ .univ .univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [← h_univ]
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
⊢ IsFiniteMeasure ν

Tactic:
have : IsFiniteMeasure ν := ⟨by simp [← h_univ]⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞) ∅) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) ∅)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine MeasurableSpace.induction_on_inter (s := C) ?_ ?_ (by simp) ?_ ?_ ?_ s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
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₂
⊢ generateFrom {s : Set α | MeasurableSet s} = mα

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Prod
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₁ : IsCountablySpanning C₂
⊢ Prod.instMeasurableSpace = generateFrom C

Tactic:
refine (generateFrom_eq_prod (C := { s : Set α | MeasurableSet s }) (D := C₂) (by simp)
      generateFrom_prod isCountablySpanning_measurableSet ?_).symm

Premises used: isCountablySpanning_measurableSet, generateFrom_prod, generateFrom_eq_prod, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Prod
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₂
⊢ IsCountablySpanning C₂

Tactic:
isCountablySpanning_measurableSet.prod isCountablySpanning_measurableSet

Premises used: isCountablySpanning_measurableSet, IsCountablySpanning.prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
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₂
⊢ IsCountablySpanning C₂

Tactic:
exact isCountablySpanning_measurableSet.prod isCountablySpanning_measurableSet

Premises used: isCountablySpanning_measurableSet, IsCountablySpanning.prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
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₂
⊢ IsPiSystem C

Tactic:
MeasurableSpace.isPiSystem_measurableSet.prod isPiSystem_prod

Premises used: isPiSystem_prod, MeasurableSpace.isPiSystem_measurableSet, IsPiSystem.prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
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₂
⊢ IsPiSystem C

Tactic:
exact MeasurableSpace.isPiSystem_measurableSet.prod isPiSystem_prod

Premises used: isPiSystem_prod, MeasurableSpace.isPiSystem_measurableSet, IsPiSystem.prod