awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [Measure.map_apply_of_aemeasurable hf hs, Measure.map_apply_of_aemeasurable hg ht]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
Tactic: rw [Measure.map_apply_of_aemeasurable hf hs, Measure.map_apply_of_aemeasurable hg ht]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (hypothesis)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) ↔
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))
have h₀ : ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
        ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
Tactic: have h₀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) :
      μ (f ⁻¹' s) * μ (g ⁻¹' t) = μ.map f s * μ.map g t ∧
      μ (f ⁻¹' s ∩ g ⁻¹' t) = μ.map (fun ω ↦ (f ω, g ω)) (s ×ˢ t) :=
    ⟨by rw [Measure.map_apply_of_aemeasurable hf hs, Measure.map_apply_of_aemeasurable hg ht],
      (Measure.map_apply_of_aemeasurable (hf.prodMk hg) (hs.prod ht)).symm⟩
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) ↔
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))
have mp : (∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) →
  Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.prod (Measure.map f μ) (Measure.map g μ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
mp :
  (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) →
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) ↔
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))
have mpr : Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.prod (Measure.map f μ) (Measure.map g μ)) →
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
⊢ (∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)) →
    Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
      (Measure.prod (Measure.map f μ) (Measure.map g μ))
have mp : ∀
  (h :
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s →
        MeasurableSet t →
          (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
              ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞))
  (s : Set β) (t : Set β') (hs : MeasurableSet s) (ht : MeasurableSet t),
  (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine fun h ↦ (Measure.prod_eq fun s t hs ht ↦ ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
have mp : (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
Tactic: rw [← (h₀ hs ht).1, ← (h₀ hs ht).2, h s t hs ht]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
mp :
  (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
⊢ (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
have mp₁ : (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
Tactic: rw [← (h₀ hs ht).1, ← (h₀ hs ht).2, h s t hs ht]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
h :
  ∀ (s : Set β) (t : Set β'),
    MeasurableSet s →
      MeasurableSet t →
        (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
mp :
  (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
mp₁ :
  (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
⊢ (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
have mp₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
Tactic: rw [← (h₀ hs ht).1, ← (h₀ hs ht).2, h s t hs ht]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
h :
  Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.prod (Measure.map f μ) (Measure.map g μ))
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
have mpr : (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
h :
  Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.prod (Measure.map f μ) (Measure.map g μ))
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
mpr :
  (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
have mpr₁ : (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.Basic (goal)
Goal:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : AEMeasurable f μ
hg : AEMeasurable g μ
σf : SigmaFinite (m0 := mβ) (Measure.map f μ)
σg : SigmaFinite (m0 := mβ') (Measure.map g μ)
h₀ :
  ∀ {s : Set β} {t : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
          (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞) ∧
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) : ℝ≥0∞)
        ((Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
h :
  Eq (α := Measure (β × β')) (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ)
    (Measure.prod (Measure.map f μ) (Measure.map g μ))
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
mpr :
  (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
mpr₁ :
  (Measure.map (fun (ω : Ω) ↦ (f ω, g ω)) μ : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s ∩ g ⁻¹' t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞)
have mpr₂ : (Measure.prod (Measure.map f μ) (Measure.map g μ) : (a : Set (β × β')) → ℝ≥0∞) (s ×ˢ t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((Measure.map g μ : Measure β') : (a : Set β') → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [(h₀ hs ht).1, (h₀ hs ht).2, h, Measure.prod_prod]