awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞)
    ((Measure.bind (mα := mγ) (Measure.map k μ)
            (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
          (a : Set (γ × β × β')) → ℝ≥0∞)
        (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    (((⇑(Kernel.id ×ₖ
                  (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                    Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g)) :
              (a : Ω) → Measure (Ω × β × β')) ∘ₘ
            μ.trim ⋯ :
          (a : Set (Ω × β × β')) → ℝ≥0∞)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) :
      ℝ≥0∞)
have rw : ∫⁻ (a : Ω),
    (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) (k a) :
          Measure (γ × β × β')) :
        (a : Set (γ × β × β')) → ℝ≥0∞)
      (s ×ˢ t ×ˢ u) ∂μ =
  ∫⁻ (a : Ω),
    (((Kernel.id ×ₖ
                (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                  Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g) :
              (a : Ω) → Measure (Ω × β × β'))
            a :
          Measure (Ω × β × β')) :
        (a : Set (Ω × β × β')) → ℝ≥0∞)
      ((k ⁻¹' s) ×ˢ t ×ˢ u) ∂μ
Tactic: rw [Measure.bind_apply ((hk_meas hs).prod (ht.prod hu)) (by fun_prop),
      Measure.bind_apply (hs.prod (ht.prod hu)) (by fun_prop), lintegral_map ?_ (by fun_prop),
      lintegral_trim]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
rw :
  ∫⁻ (a : Ω),
      (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) (k a) :
            Measure (γ × β × β')) :
          (a : Set (γ × β × β')) → ℝ≥0∞)
        (s ×ˢ t ×ˢ u) ∂μ =
    ∫⁻ (a : Ω),
      (((Kernel.id ×ₖ
                  (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                    Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g) :
                (a : Ω) → Measure (Ω × β × β'))
              a :
            Measure (Ω × β × β')) :
          (a : Set (Ω × β × β')) → ℝ≥0∞)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) ∂μ
⊢ Eq (α := ℝ≥0∞)
    ((Measure.bind (mα := mγ) (Measure.map k μ)
            (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
          (a : Set (γ × β × β')) → ℝ≥0∞)
        (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    (((⇑(Kernel.id ×ₖ
                  (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                    Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g)) :
              (a : Ω) → Measure (Ω × β × β')) ∘ₘ
            μ.trim ⋯ :
          (a : Set (Ω × β × β')) → ℝ≥0∞)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) :
      ℝ≥0∞)
have hf₁ : Measurable (β := ℝ≥0∞) fun (a : Ω) ↦
  (((Kernel.id ×ₖ
              (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g) :
            (a : Ω) → Measure (Ω × β × β'))
          a :
        Measure (Ω × β × β')) :
      (a : Set (Ω × β × β')) → ℝ≥0∞)
    ((k ⁻¹' s) ×ˢ t ×ˢ u)
Tactic: rw [Measure.bind_apply ((hk_meas hs).prod (ht.prod hu)) (by fun_prop),
      Measure.bind_apply (hs.prod (ht.prod hu)) (by fun_prop), lintegral_map ?_ (by fun_prop),
      lintegral_trim]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
rw :
  ∫⁻ (a : Ω),
      (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) (k a) :
            Measure (γ × β × β')) :
          (a : Set (γ × β × β')) → ℝ≥0∞)
        (s ×ˢ t ×ˢ u) ∂μ =
    ∫⁻ (a : Ω),
      (((Kernel.id ×ₖ
                  (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                    Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g) :
                (a : Ω) → Measure (Ω × β × β'))
              a :
            Measure (Ω × β × β')) :
          (a : Set (Ω × β × β')) → ℝ≥0∞)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) ∂μ
hf₁ :
  Measurable (β := ℝ≥0∞) fun (a : Ω) ↦
    (((Kernel.id ×ₖ
                (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                  Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g) :
              (a : Ω) → Measure (Ω × β × β'))
            a :
          Measure (Ω × β × β')) :
        (a : Set (Ω × β × β')) → ℝ≥0∞)
      ((k ⁻¹' s) ×ˢ t ×ˢ u)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.bind (mα := mγ) (Measure.map k μ)
            (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
          (a : Set (γ × β × β')) → ℝ≥0∞)
        (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    (((⇑(Kernel.id ×ₖ
                  (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                    Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g)) :
              (a : Ω) → Measure (Ω × β × β')) ∘ₘ
            μ.trim ⋯ :
          (a : Set (Ω × β × β')) → ℝ≥0∞)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) :
      ℝ≥0∞)
have rw₁ : Measurable (β := ℝ≥0∞) fun (a : γ) ↦
  (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) a : Measure (γ × β × β')) :
      (a : Set (γ × β × β')) → ℝ≥0∞)
    (s ×ˢ t ×ˢ u)
Tactic: rw [Measure.bind_apply ((hk_meas hs).prod (ht.prod hu)) (by fun_prop),
      Measure.bind_apply (hs.prod (ht.prod hu)) (by fun_prop), lintegral_map ?_ (by fun_prop),
      lintegral_trim]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ ∫⁻ (a : Ω),
      (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) (k a) :
            Measure (γ × β × β')) :
          (a : Set (γ × β × β')) → ℝ≥0∞)
        (s ×ˢ t ×ˢ u) ∂μ =
    ∫⁻ (a : Ω),
      (((Kernel.id ×ₖ
                  (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                    Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g) :
                (a : Ω) → Measure (Ω × β × β'))
              a :
            Measure (Ω × β × β')) :
          (a : Set (Ω × β × β')) → ℝ≥0∞)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) ∂μ
have refine : (ae μ).EventuallyEq (β := ℝ≥0∞)
  (fun (a : Ω) ↦
    (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) (k a) :
          Measure (γ × β × β')) :
        (a : Set (γ × β × β')) → ℝ≥0∞)
      (s ×ˢ t ×ˢ u))
  fun (a : Ω) ↦
  (((Kernel.id ×ₖ
              (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g) :
            (a : Ω) → Measure (Ω × β × β'))
          a :
        Measure (Ω × β × β')) :
      (a : Set (Ω × β × β')) → ℝ≥0∞)
    ((k ⁻¹' s) ×ˢ t ×ˢ u)
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Ω) ↦
      (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) (k a) :
            Measure (γ × β × β')) :
          (a : Set (γ × β × β')) → ℝ≥0∞)
        (s ×ˢ t ×ˢ u))
    fun (a : Ω) ↦
    (((Kernel.id ×ₖ
                (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                  Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g) :
              (a : Ω) → Measure (Ω × β × β'))
            a :
          Measure (Ω × β × β')) :
        (a : Set (Ω × β × β')) → ℝ≥0∞)
      ((k ⁻¹' s) ×ˢ t ×ˢ u)
have h : ∀ (a : Ω)
  (haX :
    Eq (α := ℝ≥0∞)
      (((((condDistrib f k μ : Kernel γ β) : (a : γ) → Measure β) (k a) : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
      (((((Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f : Kernel Ω β) : (a : Ω) → Measure β) a :
              Measure β) :
            (a : Set β) → ℝ≥0∞)
          t :
        ℝ≥0∞))
  (haT :
    Eq (α := ℝ≥0∞)
      (((((condDistrib g k μ : Kernel γ β') : (a : γ) → Measure β') (k a) : Measure β') : (a : Set β') → ℝ≥0∞) u : ℝ≥0∞)
      (((((Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g : Kernel Ω β') : (a : Ω) → Measure β') a :
              Measure β') :
            (a : Set β') → ℝ≥0∞)
          u :
        ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    ((((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) (k a) :
            Measure (γ × β × β')) :
          (a : Set (γ × β × β')) → ℝ≥0∞)
        (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
    ((((Kernel.id ×ₖ
                  (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                    Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g) :
                (a : Ω) → Measure (Ω × β × β'))
              a :
            Measure (Ω × β × β')) :
          (a : Set (Ω × β × β')) → ℝ≥0∞)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) :
      ℝ≥0∞)
Tactic: filter_upwards [condDistrib_apply_ae_eq_condExpKernel_map hf hk ht,
      condDistrib_apply_ae_eq_condExpKernel_map hg hk hu] with a haX haT
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
h_right :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.bind (mα := mγ) (Measure.map k μ)
              (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
            (a : Set (γ × β × β')) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      (((⇑(Kernel.id ×ₖ
                    (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                      Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g)) :
                (a : Ω) → Measure (Ω × β × β')) ∘ₘ
              μ.trim ⋯ :
            (a : Set (Ω × β × β')) → ℝ≥0∞)
          ((k ⁻¹' s) ×ˢ t ×ˢ u) :
        ℝ≥0∞)
h :
  ∀ {s : Set Ω} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞)
            ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            (((⇑(Kernel.id ×ₖ
                          (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                            Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
                      (a : Ω) → Measure (Ω × β × β')) ∘ₘ
                    μ.trim ⋯ :
                  (a : Set (Ω × β × β')) → ℝ≥0∞)
                (s ×ˢ t ×ˢ u) :
              ℝ≥0∞)
s : Set γ
t : Set β
u : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
    ((Measure.bind (mα := mγ) (Measure.map k μ)
            (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
          (a : Set (γ × β × β')) → ℝ≥0∞)
        (s ×ˢ t ×ˢ u) :
      ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
  ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
Tactic: convert! h (hk_meas hs) ht hu
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
hk_meas : ∀ {s : Set γ} (hs : MeasurableSet s), MeasurableSet (k ⁻¹' s)
h_left :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
      ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
h_right :
  ∀ {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞)
      ((Measure.bind (mα := mγ) (Measure.map k μ)
              (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
            (a : Set (γ × β × β')) → ℝ≥0∞)
          (s ×ˢ t ×ˢ u) :
        ℝ≥0∞)
      (((⇑(Kernel.id ×ₖ
                    (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
                      Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g)) :
                (a : Ω) → Measure (Ω × β × β')) ∘ₘ
              μ.trim ⋯ :
            (a : Set (Ω × β × β')) → ℝ≥0∞)
          ((k ⁻¹' s) ×ˢ t ×ˢ u) :
        ℝ≥0∞)
h :
  ∀ {s : Set γ} {t : Set β} {u : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          Eq (α := ℝ≥0∞)
            ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
            ((Measure.bind (mα := mγ) (Measure.map k μ)
                    (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) :
                  (a : Set (γ × β × β')) → ℝ≥0∞)
                (s ×ˢ t ×ˢ u) :
              ℝ≥0∞)
t : Set β
u : Set β'
s : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
    (((⇑(Kernel.id ×ₖ
                  (Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) f ×ₖ
                    Kernel.map (condExpKernel μ (MeasurableSpace.comap k inferInstance)) g)) :
              (a : Ω) → Measure (Ω × β × β')) ∘ₘ
            μ.trim ⋯ :
          (a : Set (Ω × β × β')) → ℝ≥0∞)
        ((k ⁻¹' s) ×ˢ t ×ˢ u) :
      ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞)
  ((Measure.map (fun (ω : Ω) ↦ (ω, f ω, g ω)) μ : (a : Set (Ω × β × β')) → ℝ≥0∞) ((k ⁻¹' s) ×ˢ t ×ˢ u) : ℝ≥0∞)
  ((Measure.map (fun (ω : Ω) ↦ (k ω, f ω, g ω)) μ : (a : Set (γ × β × β')) → ℝ≥0∞) (s ×ˢ t ×ˢ u) : ℝ≥0∞)
Tactic: convert! h hs ht hu
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
⊢ g ⟂ᵢ[k, hk; μ] f ↔
    (ae (F := Measure (γ × β')) (Measure.map (fun (ω : Ω) ↦ (k ω, g ω)) μ)).EventuallyEq (β := Measure β)
      (⇑(condDistrib f (fun (ω : Ω) ↦ (k ω, g ω)) μ) : (a : γ × β') → Measure β)
      (⇑(Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure β)
have rw : Eq (α := Measure (γ × β' × β)) (Measure.map (fun (ω : Ω) ↦ (k ω, g ω, f ω)) μ)
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) : (a : γ) → Measure (γ × β' × β))) ↔
  Eq (α := Measure ((γ × β') × β)) (Measure.map (fun (x : Ω) ↦ ((k x, g x), f x)) μ)
    (Measure.bind (α := γ × β') (mα := Prod.instMeasurableSpace) (Measure.map (fun (ω : Ω) ↦ (k ω, g ω)) μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
Tactic: rw [condDistrib_ae_eq_iff_measure_eq_compProd (μ := μ) _ hf.aemeasurable,
    condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib hg hf hk,
    Measure.compProd_eq_comp_prod]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
⊢ Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (mα := Prod.instMeasurableSpace) (Measure.map k μ ⊗ₘ condDistrib g k μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) : (a : γ × β') → Measure ((γ × β') × β)))
have rw : Eq (α := Measure ((γ × β') × β))
  (Measure.bind (mα := mγ) (Measure.map k μ)
    (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
  (Measure.bind (mα := mγ) (Measure.map k μ)
    (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ) ∘ₖ (Kernel.id ×ₖ condDistrib g k μ)) :
      (a : γ) → Measure ((γ × β') × β)))
Tactic: rw [Measure.compProd_eq_comp_prod, Measure.comp_assoc]
-- Lean 4 proof step from Mathlib.Probability.Independence.Conditional (goal)
Goal:
Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
inst_4 : StandardBorelSpace β'
inst_5 : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.symm MeasurableEquiv.prodAssoc
⊢ Eq (α := Measure ((γ × β') × β))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) : (a : γ) → Measure ((γ × β') × β)))
    (Measure.bind (mα := mγ) (Measure.map k μ)
      (⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ) ∘ₖ (Kernel.id ×ₖ condDistrib g k μ)) :
        (a : γ) → Measure ((γ × β') × β)))
have e_f : Eq (α := Kernel γ ((γ × β') × β)) (Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ)
  (Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ) ∘ₖ (Kernel.id ×ₖ condDistrib g k μ))
Tactic: congr 2