awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 γ
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∞)
have rw : Eq (α := ℝ≥0∞) ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
  ((ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥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 μ
⊢ μ = ν ↔
    ∀ {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 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∞)
Tactic: rw [← MeasurableEquiv.prodAssoc.map_measurableEquiv_injective.eq_iff, ext_prod₃_iff]
-- 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 γ
μ ν_1 : 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∞)
have rw : Eq (α := ℝ≥0∞)
  ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u) :
    ℝ≥0∞)
  ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
Tactic: rw [map_apply (by fun_prop) (hs.prod (ht.prod hu))]
-- 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 γ
μ ν_1 : Measure ((α × β) × γ)
inst : IsFiniteMeasure μ
ν : Measure ((α × β) × γ)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞)
        ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
have h : ∀ (x : (α × β) × γ),
  Membership.mem (γ := Set ((α × β) × γ)) ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u)
      x ↔
    x ∈ (s ×ˢ t) ×ˢ u
Tactic: congr 1 with x
-- 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 μ
⊢ (∀ {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∞)
have 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∞)
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]
-- 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_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∞)
have 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∞)
Tactic: refine ⟨fun h s t u hs ht hu ↦ ?_, fun h s t u hs ht hu ↦ ?_⟩
-- 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_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∞)
⊢ (∀ {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∞)
have 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∞)
Tactic: refine ⟨fun h s t u hs ht hu ↦ ?_, fun h s t u hs ht hu ↦ ?_⟩
-- 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_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∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
have 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∞)
Tactic: specialize h hs ht hu
Cleared hypotheses: h
-- 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_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∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
  ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
Tactic: specialize h hs ht hu
Cleared hypotheses: 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_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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
have 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∞)
Tactic: rwa [h_eq μ hs ht hu, h_eq ν hs ht hu] at h
Cleared hypotheses: 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_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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
    ((ν : (a : Set ((α × β) × γ)) → ℝ≥0∞) ((s ×ˢ t) ×ˢ u) : ℝ≥0∞)
have 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∞)
Tactic: rwa [h_eq μ hs ht hu, h_eq ν hs ht hu] at h
Cleared hypotheses: 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_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∞)
⊢ Eq (α := ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) μ : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ν : (a : Set (α × β × γ)) → ℝ≥0∞) (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
have refine_2 : Eq (α := ℝ≥0∞) ((μ : (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
⊢ 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)))
have 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∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
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∞)
have h : Eq (α := ℝ≥0∞)
  (∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)) : (a : Set (β × α)) → ℝ≥0∞) s)
  (∑' (i : ℕ × ℕ), (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) s)
Tactic: rw [sum_apply _ hs, sum_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
⊢ map Prod.swap (μ.prod ν) = ν.prod μ
have this : 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: have : 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))) := by
    ext s hs
    rw [sum_apply _ hs, sum_apply _ hs]
    exact ((Equiv.prodComm ℕ ℕ).tsum_eq _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
this :
  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)))
⊢ map Prod.swap (μ.prod ν) = ν.prod μ
have rw : Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
  (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2))
Tactic: rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, prod_sum, prod_sum,
    map_sum measurable_swap.aemeasurable, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
this :
  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)))
⊢ Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
    (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2))
have e_f : Eq (α := ℕ × ℕ → Measure (β × α)) (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
  fun (p : ℕ × ℕ) ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
this :
  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)))
⊢ Eq (α := ℕ × ℕ → Measure (β × α)) (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
    fun (p : ℕ × ℕ) ↦ (sfiniteSeq ν p.1).prod (sfiniteSeq μ p.2)
have e_f : ∀ (i : ℕ × ℕ), map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) = (sfiniteSeq ν i.1).prod (sfiniteSeq μ i.2)
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
this :
  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)))
i : ℕ × ℕ
⊢ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) = (sfiniteSeq ν i.1).prod (sfiniteSeq μ i.2)
have e_f : ∀ (s : Set β) (t : Set α),
  MeasurableSet s →
    MeasurableSet t →
      (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) (s ×ˢ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine (prod_eq ?_).symm