awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
refine_1 :
  Eq (α := MeasurableSpace (((i : γ) → α) × ((i : γ) → β))) Prod.instMeasurableSpace
    (generateFrom
      (image2 (fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2)
        (Set.pi (α := fun (i : γ) ↦ α) univ ''
          Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s})
        (Set.pi (α := fun (i : γ) ↦ β) univ ''
          Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s})))
refine_2 :
  ∀ (s : Set (((i : γ) → α) × ((i : γ) → β))),
    Membership.mem (γ := Set (Set (((i : γ) → α) × ((i : γ) → β))))
        (image2 (fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2)
          (Set.pi (α := fun (i : γ) ↦ α) univ ''
            Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s})
          (Set.pi (α := fun (i : γ) ↦ β) univ ''
            Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s}))
        s →
      Eq (α := ℝ≥0∞)
        (((Measure.pi (α := fun (i : γ) ↦ α) μ).prod (Measure.pi (α := fun (i : γ) ↦ β) ν) :
              (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        ((Measure.map (α := γ → α × β)
                (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ) : (a : γ → α × β) → (γ → α) × (γ → β))
                (Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i)) :
              (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
            s :
          ℝ≥0∞)
⊢ Eq (α := Measure ((γ → α) × (γ → β)))
    (Measure.map (α := γ → α × β)
      (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ) : (a : γ → α × β) → (γ → α) × (γ → β))
      (Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i)))
    (Measure.prod (Measure.pi (α := fun (i : γ) ↦ α) fun (i : γ) ↦ μ i)
      (Measure.pi (α := fun (a : γ) ↦ β) fun (i : γ) ↦ ν i))

Tactic:
refine (FiniteSpanningSetsIn.ext ?_ (isPiSystem_pi.prod isPiSystem_pi)
      ((FiniteSpanningSetsIn.pi fun i ↦ (μ i).toFiniteSpanningSetsIn).prod
      (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn))) ?_).symm

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.pi, IsPiSystem.prod, MeasureTheory.Measure.toFiniteSpanningSetsIn, isPiSystem_pi, Eq.symm, MeasureTheory.Measure.FiniteSpanningSetsIn.prod, MeasureTheory.Measure.FiniteSpanningSetsIn.ext
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
⊢ Eq (α := MeasurableSpace (((i : γ) → α) × ((i : γ) → β))) Prod.instMeasurableSpace
    (generateFrom
      (image2 (fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2)
        (Set.pi (α := fun (i : γ) ↦ α) univ ''
          Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s})
        (Set.pi (α := fun (i : γ) ↦ β) univ ''
          Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s})))

Tactic:
(generateFrom_eq_prod generateFrom_pi generateFrom_pi ?_ ?_).symm

Premises used: generateFrom_eq_prod, generateFrom_pi, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
refine_1 :
  IsCountablySpanning (α := (i : γ) → α)
    (Set.pi (α := fun (i : γ) ↦ α) univ ''
      Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s})
refine_1₁ :
  IsCountablySpanning (α := (i : γ) → β)
    (Set.pi (α := fun (i : γ) ↦ β) univ ''
      Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s})
⊢ Eq (α := MeasurableSpace (((i : γ) → α) × ((i : γ) → β))) Prod.instMeasurableSpace
    (generateFrom
      (image2 (fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2)
        (Set.pi (α := fun (i : γ) ↦ α) univ ''
          Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s})
        (Set.pi (α := fun (i : γ) ↦ β) univ ''
          Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s})))

Tactic:
refine (generateFrom_eq_prod generateFrom_pi generateFrom_pi ?_ ?_).symm

Premises used: generateFrom_eq_prod, generateFrom_pi, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
⊢ IsCountablySpanning (α := (i : γ) → α)
    (Set.pi (α := fun (i : γ) ↦ α) univ ''
      Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s})

Tactic:
(FiniteSpanningSetsIn.pi (fun i ↦ (μ i).toFiniteSpanningSetsIn)).isCountablySpanning

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.pi, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
⊢ IsCountablySpanning (α := (i : γ) → α)
    (Set.pi (α := fun (i : γ) ↦ α) univ ''
      Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s})

Tactic:
exact (FiniteSpanningSetsIn.pi (fun i ↦ (μ i).toFiniteSpanningSetsIn)).isCountablySpanning

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.pi, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
⊢ IsCountablySpanning (α := (i : γ) → β)
    (Set.pi (α := fun (i : γ) ↦ β) univ ''
      Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s})

Tactic:
(FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn)).isCountablySpanning

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.pi, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
⊢ IsCountablySpanning (α := (i : γ) → β)
    (Set.pi (α := fun (i : γ) ↦ β) univ ''
      Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s})

Tactic:
exact (FiniteSpanningSetsIn.pi (fun i ↦ (ν i).toFiniteSpanningSetsIn)).isCountablySpanning

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.pi, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
s : (i : γ) → Set α
left :
  Membership.mem (γ := Set ((i : γ) → Set α))
    (Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s}) s
t : (i : γ) → Set β
left_1 :
  Membership.mem (γ := Set ((i : γ) → Set β))
    (Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s}) t
refine_2 :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : γ) ↦ α) μ).prod (Measure.pi (α := fun (i : γ) ↦ β) ν) :
          (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
        ((fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2) (Set.pi (α := fun (i : γ) ↦ α) univ s)
          (Set.pi (α := fun (i : γ) ↦ β) univ t)) :
      ℝ≥0∞)
    ((Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i) : (a : Set (γ → α × β)) → ℝ≥0∞)
        (preimage (β := (γ → α) × (γ → β))
          (⇑(Equiv.arrowProdEquivProdArrow γ (fun (i : γ) ↦ α) fun (i : γ) ↦ β) : (a : γ → α × β) → (γ → α) × (γ → β))
          ((fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2) (Set.pi (α := fun (i : γ) ↦ α) univ s)
            (Set.pi (α := fun (i : γ) ↦ β) univ t))) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : γ) ↦ α) μ).prod (Measure.pi (α := fun (i : γ) ↦ β) ν) :
        (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
      ((fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2) (Set.pi (α := fun (i : γ) ↦ α) univ s)
        (Set.pi (α := fun (i : γ) ↦ β) univ t)))
    ((Measure.map (α := γ → α × β)
          (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ) : (a : γ → α × β) → (γ → α) × (γ → β))
          (Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i)) :
        (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
      ((fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2) (Set.pi (α := fun (i : γ) ↦ α) univ s)
        (Set.pi (α := fun (i : γ) ↦ β) univ t)))

Tactic:
rw [MeasurableEquiv.map_apply, MeasurableEquiv.arrowProdEquivProdArrow,
        MeasurableEquiv.coe_mk]

Premises used: MeasurableEquiv.arrowProdEquivProdArrow, MeasurableEquiv.map_apply, MeasurableEquiv.coe_mk
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
s : (i : γ) → Set α
left :
  Membership.mem (γ := Set ((i : γ) → Set α))
    (Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s}) s
t : (i : γ) → Set β
left_1 :
  Membership.mem (γ := Set ((i : γ) → Set β))
    (Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s}) t
h :
  ∀ (x : (i : γ) → α × β),
    Membership.mem (γ := Set ((i : γ) → α × β))
        ((⇑(Equiv.arrowProdEquivProdArrow γ (fun (i : γ) ↦ α) fun (i : γ) ↦ β) :
            (a : (i : γ) → α × β) → ((i : γ) → α) × ((i : γ) → β)) ⁻¹'
          Set.pi (α := fun (i : γ) ↦ α) univ s ×ˢ Set.pi (α := fun (i : γ) ↦ β) univ t)
        x ↔
      Membership.mem (γ := Set ((i : γ) → α × β)) (Set.pi (α := fun (i : γ) ↦ α × β) univ fun (i : γ) ↦ s i ×ˢ t i) x
⊢ Eq (α := Set ((i : γ) → α × β))
    ((⇑(Equiv.arrowProdEquivProdArrow γ (fun (i : γ) ↦ α) fun (i : γ) ↦ β) :
        (a : (i : γ) → α × β) → ((i : γ) → α) × ((i : γ) → β)) ⁻¹'
      Set.pi (α := fun (i : γ) ↦ α) univ s ×ˢ Set.pi (α := fun (i : γ) ↦ β) univ t)
    (Set.pi (α := fun (i : γ) ↦ α × β) univ fun (i : γ) ↦ s i ×ˢ t i)

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
s : (i : γ) → Set α
left :
  Membership.mem (γ := Set ((i : γ) → Set α))
    (Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s}) s
t : (i : γ) → Set β
left_1 :
  Membership.mem (γ := Set ((i : γ) → Set β))
    (Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s}) t
x : (i : γ) → α × β
⊢ Membership.mem (γ := Set ((i : γ) → α × β))
      ((⇑(Equiv.arrowProdEquivProdArrow γ (fun (i : γ) ↦ α) fun (i : γ) ↦ β) :
          (a : (i : γ) → α × β) → ((i : γ) → α) × ((i : γ) → β)) ⁻¹'
        Set.pi (α := fun (i : γ) ↦ α) univ s ×ˢ Set.pi (α := fun (i : γ) ↦ β) univ t)
      x ↔
    Membership.mem (γ := Set ((i : γ) → α × β)) (Set.pi (α := fun (i : γ) ↦ α × β) univ fun (i : γ) ↦ s i ×ˢ t i) x

Tactic:
simp [Set.mem_pi, forall_and]

Premises used: Set.mem_pi, forall_and
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
s : (i : γ) → Set α
left :
  Membership.mem (γ := Set ((i : γ) → Set α))
    (Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s}) s
t : (i : γ) → Set β
left_1 :
  Membership.mem (γ := Set ((i : γ) → Set β))
    (Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s}) t
refine_2 :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : γ) ↦ α) μ).prod (Measure.pi (α := fun (i : γ) ↦ β) ν) :
          (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
        ((fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2) (Set.pi (α := fun (i : γ) ↦ α) univ s)
          (Set.pi (α := fun (i : γ) ↦ β) univ t)) :
      ℝ≥0∞)
    ((Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i) : (a : Set (γ → α × β)) → ℝ≥0∞)
        (Set.pi (α := fun (i : γ) ↦ α × β) univ fun (i : γ) ↦ s i ×ˢ t i) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : γ) ↦ α) μ).prod (Measure.pi (α := fun (i : γ) ↦ β) ν) :
          (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
        ((fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2) (Set.pi (α := fun (i : γ) ↦ α) univ s)
          (Set.pi (α := fun (i : γ) ↦ β) univ t)) :
      ℝ≥0∞)
    ((Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i) : (a : Set (γ → α × β)) → ℝ≥0∞)
        (preimage (β := (γ → α) × (γ → β))
          (⇑(Equiv.arrowProdEquivProdArrow γ (fun (i : γ) ↦ α) fun (i : γ) ↦ β) : (a : γ → α × β) → (γ → α) × (γ → β))
          ((fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2) (Set.pi (α := fun (i : γ) ↦ α) univ s)
            (Set.pi (α := fun (i : γ) ↦ β) univ t))) :
      ℝ≥0∞)

Tactic:
rw [show Equiv.arrowProdEquivProdArrow γ _ _ ⁻¹' (univ.pi s ×ˢ univ.pi t) =
          (univ.pi fun i ↦ s i ×ˢ t i) by
          ext; simp [Set.mem_pi, forall_and]]
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst_3 : ∀ (i : γ), SigmaFinite (μ i)
inst_4 : ∀ (i : γ), SigmaFinite (ν i)
s : (i : γ) → Set α
left :
  Membership.mem (γ := Set ((i : γ) → Set α))
    (Set.pi (α := fun (i : γ) ↦ Set α) univ fun (i : γ) ↦ {s : Set α | MeasurableSet s}) s
t : (i : γ) → Set β
left_1 :
  Membership.mem (γ := Set ((i : γ) → Set β))
    (Set.pi (α := fun (i : γ) ↦ Set β) univ fun (i : γ) ↦ {s : Set β | MeasurableSet s}) t
refine_2 refine_2₁ :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : γ) ↦ α) μ).prod (Measure.pi (α := fun (i : γ) ↦ β) ν) :
          (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
        (Set.pi (α := fun (i : γ) ↦ α) univ s ×ˢ Set.pi (α := fun (i : γ) ↦ β) univ t) :
      ℝ≥0∞)
    ((Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i) : (a : Set (γ → α × β)) → ℝ≥0∞)
        (Set.pi (α := fun (i : γ) ↦ α × β) univ fun (i : γ) ↦ s i ×ˢ t i) :
      ℝ≥0∞)
refine_2₂ :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : γ) ↦ α) μ).prod (Measure.pi (α := fun (i : γ) ↦ β) ν) :
          (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
        (Set.pi (α := fun (i : γ) ↦ α) univ s ×ˢ Set.pi (α := fun (i : γ) ↦ β) univ t) :
      ℝ≥0∞)
    (∏ i : γ, ((μ i).prod (ν i) : (a : Set (α × β)) → ℝ≥0∞) (s i ×ˢ t i) : ℝ≥0∞)
refine_2₃ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((Measure.pi (α := fun (i : γ) ↦ α) μ : (a : Set ((i : γ) → α)) → ℝ≥0∞) (Set.pi (α := fun (i : γ) ↦ α) univ s) :
        ℝ≥0∞)
      ((Measure.pi (α := fun (i : γ) ↦ β) ν : (a : Set ((i : γ) → β)) → ℝ≥0∞) (Set.pi (α := fun (i : γ) ↦ β) univ t) :
        ℝ≥0∞) =
    ∏ x : γ,
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ x : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞)
        ((ν x : (a : Set β) → ℝ≥0∞) (t x) : ℝ≥0∞)
refine_2₄ :
  HMul.hMul (α := ℝ≥0∞) (∏ i : γ, (μ i : (a : Set α) → ℝ≥0∞) (s i)) (∏ i : γ, (ν i : (a : Set β) → ℝ≥0∞) (t i)) =
    ∏ x : γ,
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ x : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞)
        ((ν x : (a : Set β) → ℝ≥0∞) (t x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : γ) ↦ α) μ).prod (Measure.pi (α := fun (i : γ) ↦ β) ν) :
          (a : Set (((i : γ) → α) × ((i : γ) → β))) → ℝ≥0∞)
        ((fun (x1 : Set ((i : γ) → α)) (x2 : Set ((i : γ) → β)) ↦ x1 ×ˢ x2) (Set.pi (α := fun (i : γ) ↦ α) univ s)
          (Set.pi (α := fun (i : γ) ↦ β) univ t)) :
      ℝ≥0∞)
    ((Measure.pi (α := fun (a : γ) ↦ α × β) fun (i : γ) ↦ (μ i).prod (ν i) : (a : Set (γ → α × β)) → ℝ≥0∞)
        (Set.pi (α := fun (i : γ) ↦ α × β) univ fun (i : γ) ↦ s i ×ˢ t i) :
      ℝ≥0∞)

Tactic:
simp_rw [pi_pi, prod_prod, pi_pi, Finset.prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, MeasureTheory.Measure.prod_prod, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α : Type u_4
β : Type u_5
γ : Type u_6
inst : MeasureSpace α
inst_1 : MeasureSpace β
inst_2 : Fintype γ
inst_3 : SigmaFinite.{u_4} (α := α) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_4 : SigmaFinite.{u_5} (α := β) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ MeasurePreserving (α := γ → α × β) (β := (γ → α) × (γ → β))
    (⇑(MeasurableEquiv.arrowProdEquivProdArrow α β γ) : (a : γ → α × β) → (γ → α) × (γ → β))
    (volume : Measure (γ → α × β)) (volume : Measure ((γ → α) × (γ → β)))

Tactic:
measurePreserving_arrowProdEquivProdArrow α β γ (fun _ ↦ volume) (fun _ ↦ volume)

Premises used: MeasureTheory.measurePreserving_arrowProdEquivProdArrow, MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
inst : Fintype ι
inst_1 : Fintype ι'
X : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (X i)
μ : (i : ι ⊕ ι') → Measure (X i)
inst_2 : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
⊢ Measure.map (α := ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.sumPiEquivProdPi X)) :
        (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i)
      (Measure.prod (Measure.pi (α := fun (i : ι) ↦ X (Sum.inl i)) fun (i : ι) ↦ μ (Sum.inl i))
        (Measure.pi (α := fun (i' : ι') ↦ X (Sum.inr i')) fun (i : ι') ↦ μ (Sum.inr i))) =
    Measure.pi (α := X) μ

Tactic:
(pi_eq fun s _ => ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
inst : Fintype ι
inst_1 : Fintype ι'
X : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (X i)
μ : (i : ι ⊕ ι') → Measure (X i)
inst_2 : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
refine :
  ∀ (s : (i : ι ⊕ ι') → Set (X i)),
    (∀ (i : ι ⊕ ι'), MeasurableSet (s i)) →
      Eq (α := ℝ≥0∞)
        ((Measure.map (α := ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))
                (⇑(MeasurableEquiv.symm (MeasurableEquiv.sumPiEquivProdPi X)) :
                  (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i)
                (Measure.prod (Measure.pi (α := fun (i : ι) ↦ X (Sum.inl i)) fun (i : ι) ↦ μ (Sum.inl i))
                  (Measure.pi (α := fun (i' : ι') ↦ X (Sum.inr i')) fun (i : ι') ↦ μ (Sum.inr i))) :
              (a : Set ((i : ι ⊕ ι') → X i)) → ℝ≥0∞)
            (Set.pi (α := X) univ s) :
          ℝ≥0∞)
        (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Measure.map (α := ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.sumPiEquivProdPi X)) :
        (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i)
      (Measure.prod (Measure.pi (α := fun (i : ι) ↦ X (Sum.inl i)) fun (i : ι) ↦ μ (Sum.inl i))
        (Measure.pi (α := fun (i' : ι') ↦ X (Sum.inr i')) fun (i : ι') ↦ μ (Sum.inr i))) =
    Measure.pi (α := X) μ

Tactic:
refine (pi_eq fun s _ => ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
inst : Fintype ι
inst_1 : Fintype ι'
X : ι ⊕ ι' → Type u_4
inst_2 : (i : ι ⊕ ι') → MeasureSpace (X i)
inst_3 : ∀ (i : ι ⊕ ι'), SigmaFinite.{u_4} (α := X i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
measurePreserving_sumPiEquivProdPi_symm (fun _ ↦ volume)

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.measurePreserving_sumPiEquivProdPi_symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
inst : Fintype ι
inst_1 : Fintype ι'
X : ι ⊕ ι' → Type u_4
_m : (i : ι ⊕ ι') → MeasurableSpace (X i)
μ : (i : ι ⊕ ι') → Measure (X i)
inst_2 : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
⊢ MeasurePreserving (β := ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))
    (⇑(MeasurableEquiv.sumPiEquivProdPi X) :
      (a : (i : ι ⊕ ι') → X i) → ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))
    (Measure.pi (α := X) μ)
    (Measure.prod (Measure.pi (α := fun (i : ι) ↦ X (Sum.inl i)) fun (i : ι) ↦ μ (Sum.inl i))
      (Measure.pi (α := fun (i' : ι') ↦ X (Sum.inr i')) fun (i : ι') ↦ μ (Sum.inr i)))

Tactic:
measurePreserving_sumPiEquivProdPi_symm μ |>.symm

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.measurePreserving_sumPiEquivProdPi_symm
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
ι' : Type u_2
inst : Fintype ι
inst_1 : Fintype ι'
X : ι ⊕ ι' → Type u_4
inst_2 : (i : ι ⊕ ι') → MeasureSpace (X i)
inst_3 : ∀ (i : ι ⊕ ι'), SigmaFinite.{u_4} (α := X i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ MeasurePreserving (α := (i : ι ⊕ ι') → X i) (β := ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))
    (⇑(MeasurableEquiv.sumPiEquivProdPi X) :
      (a : (i : ι ⊕ ι') → X i) → ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))
    volume volume

Tactic:
measurePreserving_sumPiEquivProdPi (fun _ ↦ volume)

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.measurePreserving_sumPiEquivProdPi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
n : ℕ
α : Fin (n + 1) → Type u
m : (i : Fin (n + 1)) → MeasurableSpace (α i)
μ : (i : Fin (n + 1)) → Measure (α i)
inst : ∀ (i : Fin (n + 1)), SigmaFinite (μ i)
i : Fin (n + 1)
e : α i × ((j : Fin n) → α (i.succAbove j)) ≃ᵐ ((j : Fin (n + 1)) → α j) :=
  MeasurableEquiv.symm (MeasurableEquiv.piFinSuccAbove α i)
⊢ MeasurePreserving (β := α i × ((j : Fin n) → α (i.succAbove j)))
    (⇑(MeasurableEquiv.piFinSuccAbove α i) : (a : (j : Fin (n + 1)) → α j) → α i × ((j : Fin n) → α (i.succAbove j)))
    (Measure.pi (α := α) μ)
    ((μ i).prod (Measure.pi (α := fun (j : Fin n) ↦ α (i.succAbove j)) fun (j : Fin n) ↦ μ (i.succAbove j)))

Tactic:
MeasurePreserving.symm e ?_

Premises used: Fin.succAboveCases, MeasureTheory.MeasurePreserving.symm, Fin.insertNth, dite, Fin.insertNthEquiv, Equiv.symm