awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : Set (α × β × γ)
hs_1 : MeasurableSet s_1
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₂
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s
t : Set β
ht : Membership.mem (γ := Set (Set β)) {t : Set β | MeasurableSet t} t
u : Set γ
hu : Membership.mem (γ := Set (Set γ)) {u : Set γ | MeasurableSet u} u
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set (α × β × γ)) → ℝ≥0∞)
      ((fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) s ((fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) t u)))
    ((ν : (a : Set (α × β × γ)) → ℝ≥0∞)
      ((fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) s ((fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) t u)))

Tactic:
h hs ht hu
-- 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_1 : Set (α × β × γ)
hs_1 : MeasurableSet s_1
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₂
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s
t : Set β
ht : Membership.mem (γ := Set (Set β)) {t : Set β | MeasurableSet t} t
u : Set γ
hu : Membership.mem (γ := Set (Set γ)) {u : Set γ | MeasurableSet u} u
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set (α × β × γ)) → ℝ≥0∞)
      ((fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) s ((fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) t u)))
    ((ν : (a : Set (α × β × γ)) → ℝ≥0∞)
      ((fun (x1 : Set α) (x2 : Set (β × γ)) ↦ x1 ×ˢ x2) s ((fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) t u)))

Tactic:
exact h hs ht hu
-- 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_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∞)
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
γ : 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∞)
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
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst : IsFiniteMeasure μ
h : μ = ν
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
rw rw₁ :
  Eq (α := ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
    ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
    ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥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 μ
rw :
  (∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            Eq (α := ℝ≥0∞)
              ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)
              ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)) ↔
    ∀ {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 α} {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∞)

Tactic:
rw [← MeasurableEquiv.prodAssoc.map_measurableEquiv_injective.eq_iff, ext_prod₃_iff]

Premises used: Function.Injective.eq_iff, MeasurableEquiv.prodAssoc, MeasureTheory.Measure.ext_prod₃_iff, MeasurableEquiv.map_measurableEquiv_injective
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν_1 : Measure ((α × β) × γ)
inst : IsFiniteMeasure μ
ν : Measure ((α × β) × γ)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Measurable (α := (α × β) × γ) (β := α × β × γ) (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν_1 : Measure ((α × β) × γ)
inst : IsFiniteMeasure μ
ν : Measure ((α × β) × γ)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
rw :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞)
        ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)

Tactic:
rw [map_apply (by fun_prop) (hs.prod (ht.prod hu))]

Premises used: MeasureTheory.Measure.map_apply, MeasurableSet.prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν_1 : Measure ((α × β) × γ)
inst : IsFiniteMeasure μ
ν : Measure ((α × β) × γ)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
h :
  ∀ (x : (α × β) × γ),
    Membership.mem (γ := Set ((α × β) × γ))
        ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u) x ↔
      x ∈ (s ×ˢ t) ×ˢ u
⊢ Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞)
        ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)

Tactic:
congr 1 with x
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν_1 : Measure ((α × β) × γ)
inst : IsFiniteMeasure μ
ν : Measure ((α × β) × γ)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
x : (α × β) × γ
⊢ Membership.mem (γ := Set ((α × β) × γ)) ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u)
      x ↔
    x ∈ (s ×ˢ t) ×ˢ u

Tactic:
simp [MeasurableEquiv.prodAssoc]

Premises used: MeasurableEquiv.prodAssoc
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst : IsFiniteMeasure μ
⊢ ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)

Tactic:
have h_eq (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ}
      (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u) :
      ν.map MeasurableEquiv.prodAssoc (s ×ˢ (t ×ˢ u)) = ν ((s ×ˢ t) ×ˢ u) := by
    rw [map_apply (by fun_prop) (hs.prod (ht.prod hu))]
    congr 1 with x
    simp [MeasurableEquiv.prodAssoc]
-- 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_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
⊢ (∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            Eq (α := ℝ≥0∞)
              ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)
              ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)) ↔
    ∀ {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∞)

Tactic:
⟨fun h s t u hs ht hu ↦ ?_, fun h s t u hs ht hu ↦ ?_⟩

Premises used: Iff.intro
-- 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_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
refine_1 :
  ∀
    (h :
      ∀ {s : Set α} {t : Set β} {u : Set γ},
        MeasurableSet s →
          MeasurableSet t →
            MeasurableSet u →
              Eq (α := ℝ≥0∞)
                ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞)
                    (s ×ˢ t ×ˢ u) :
                  ℝ≥0∞)
                ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
                    (s ×ˢ t ×ˢ u) :
                  ℝ≥0∞))
    (s : Set α) (t : Set β) (u : Set γ) (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
      ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
refine_2 :
  ∀
    (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 α) (t : Set β) (u : Set γ) (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
⊢ (∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s →
        MeasurableSet t →
          MeasurableSet u →
            Eq (α := ℝ≥0∞)
              ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)
              ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
                  (s ×ˢ t ×ˢ u) :
                ℝ≥0∞)) ↔
    ∀ {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∞)

Tactic:
refine ⟨fun h s t u hs ht hu ↦ ?_, fun h s t u hs ht hu ↦ ?_⟩
-- 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_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞)
            ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞)
                (s ×ˢ t ×ˢ u) :
              ℝ≥0∞)
            ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
                (s ×ˢ t ×ˢ u) :
              ℝ≥0∞)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)

Tactic:
specialize h hs ht hu
-- 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_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
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 α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)

Tactic:
specialize h hs ht hu
-- 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_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
h :
  Eq (α := ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
refine_1 :
  ∀
    (h :
      Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
        ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
            (s ×ˢ t ×ˢ u) :
          ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
      ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
refine_1₁ refine_1₂ refine_1₃ refine_1₄ :
  ∀
    (h :
      Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
        ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
      ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)

Tactic:
rwa [h_eq μ hs ht hu, h_eq ν hs ht hu] at 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_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ} (hs : MeasurableSet s) (ht : MeasurableSet t)
    (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
refine_2 :
  Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)

Tactic:
rwa [h_eq μ hs ht hu, h_eq ν hs ht hu]
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
h :
  ∀ (s : Set (β × α)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)) : (a : Set (β × α)) → ℝ≥0∞) s :
        ℝ≥0∞)
      ((sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) s :
        ℝ≥0∞)
⊢ Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))

Tactic:
ext s hs