awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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})))
have refine_1 : IsCountablySpanning (α := (i : γ) → α)
  (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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})
⊢ 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})))
have refine_1₁ : IsCountablySpanning (α := (i : γ) → β)
  (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ 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)))
have 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∞)
Tactic: rw [MeasurableEquiv.map_apply, MeasurableEquiv.arrowProdEquivProdArrow,
        MeasurableEquiv.coe_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ 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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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
⊢ 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∞)
have 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∞)
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]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: simp_rw [pi_pi, prod_prod, pi_pi, Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: simp_rw [pi_pi, prod_prod, pi_pi, Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: simp_rw [pi_pi, prod_prod, pi_pi, Finset.prod_mul_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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) μ
have 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∞)
Tactic: refine (pi_eq fun s _ => ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
s : (i : ι ⊕ ι') → Set (X i)
h : ∀ (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∞)
have simp_rw : Eq (α := ℝ≥0∞)
  ((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 (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))) → ℝ≥0∞)
      ((⇑(MeasurableEquiv.symm (MeasurableEquiv.sumPiEquivProdPi X)) :
          (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i) ⁻¹'
        Set.pi (α := X) univ s) :
    ℝ≥0∞)
  (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: simp_rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_sumPiEquivProdPi_symm,
      Equiv.sumPiEquivProdPi_symm_preimage_univ_pi, Measure.prod_prod, Measure.pi_pi,
      Fintype.prod_sum_type]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
s : (i : ι ⊕ ι') → Set (X i)
h : ∀ (i : ι ⊕ ι'), MeasurableSet (s i)
simp_rw :
  Eq (α := ℝ≥0∞)
    ((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 (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))) → ℝ≥0∞)
        ((⇑(MeasurableEquiv.symm (MeasurableEquiv.sumPiEquivProdPi X)) :
            (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i) ⁻¹'
          Set.pi (α := X) univ s) :
      ℝ≥0∞)
    (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ 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∞)
have simp_rw₁ : Eq (α := ℝ≥0∞)
  ((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 (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))) → ℝ≥0∞)
      ((⇑(Equiv.sumPiEquivProdPi X).symm :
          (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i) ⁻¹'
        Set.pi (α := X) univ s) :
    ℝ≥0∞)
  (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: simp_rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_sumPiEquivProdPi_symm,
      Equiv.sumPiEquivProdPi_symm_preimage_univ_pi, Measure.prod_prod, Measure.pi_pi,
      Fintype.prod_sum_type]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
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)
s : (i : ι ⊕ ι') → Set (X i)
h : ∀ (i : ι ⊕ ι'), MeasurableSet (s i)
simp_rw :
  Eq (α := ℝ≥0∞)
    ((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 (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))) → ℝ≥0∞)
        ((⇑(MeasurableEquiv.symm (MeasurableEquiv.sumPiEquivProdPi X)) :
            (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i) ⁻¹'
          Set.pi (α := X) univ s) :
      ℝ≥0∞)
    (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞)
    ((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 (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))) → ℝ≥0∞)
        ((⇑(Equiv.sumPiEquivProdPi X).symm :
            (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i) ⁻¹'
          Set.pi (α := X) univ s) :
      ℝ≥0∞)
    (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ 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∞)
have simp_rw₂ : Eq (α := ℝ≥0∞)
  ((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 (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))) → ℝ≥0∞)
      (SProd.sprod (α := Set ((i : ι) → X (Sum.inl i))) (β := Set ((i : ι') → X (Sum.inr i)))
        (Set.pi (α := fun (i : ι) ↦ X (Sum.inl i)) univ fun (i : ι) ↦ s (Sum.inl i))
        (Set.pi (α := fun (i : ι') ↦ X (Sum.inr i)) univ fun (i : ι') ↦ s (Sum.inr i))) :
    ℝ≥0∞)
  (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
Tactic: simp_rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_sumPiEquivProdPi_symm,
      Equiv.sumPiEquivProdPi_symm_preimage_univ_pi, Measure.prod_prod, Measure.pi_pi,
      Fintype.prod_sum_type]