awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ AEMeasurable (β := Measure (Ω × β × β'))
    (⇑(Kernel.id ×ₖ
          (Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f ×ₖ
            Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g)) :
      (a : Ω) → Measure (Ω × β × β'))
    (μ.trim ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ AEMeasurable (β := Measure (γ × β × β')) (_m := mγ)
    (⇑(Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) : (a : γ) → Measure (γ × β × β')) (Measure.map k μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ Measurable k

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.Conditional
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)
rw₁ :
  Measurable (β := ℝ≥0∞) fun (a : γ) ↦
    (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) a :
          Measure (γ × β × β')) :
        (a : Set (γ × β × β')) → ℝ≥0∞)
      (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∞)

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]

Premises used: MeasureTheory.Measure.bind_apply, MeasurableSet.prod, MeasureTheory.lintegral_trim, MeasureTheory.lintegral_map
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ 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:
Kernel.measurable_coe _ ((hk_meas hs).prod (ht.prod hu))

Premises used: MeasurableSet.prod, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ 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:
exact Kernel.measurable_coe _ ((hk_meas hs).prod (ht.prod hu))

Premises used: MeasurableSet.prod, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ Measurable (β := ℝ≥0∞) fun (a : γ) ↦
    (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) a :
          Measure (γ × β × β')) :
        (a : Set (γ × β × β')) → ℝ≥0∞)
      (s ×ˢ t ×ˢ u)

Tactic:
Kernel.measurable_coe _ (hs.prod (ht.prod hu))

Premises used: MeasurableSet.prod, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Independence.Conditional
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
⊢ Measurable (β := ℝ≥0∞) fun (a : γ) ↦
    (((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ) : (a : γ) → Measure (γ × β × β')) a :
          Measure (γ × β × β')) :
        (a : Set (γ × β × β')) → ℝ≥0∞)
      (s ×ˢ t ×ˢ u)

Tactic:
exact Kernel.measurable_coe _ (hs.prod (ht.prod hu))

Premises used: MeasurableSet.prod, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Independence.Conditional
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) ∂μ

Tactic:
lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Independence.Conditional
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
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)
⊢ ∫⁻ (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:
refine lintegral_congr_ae ?_

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.Probability.Independence.Conditional
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 : Ω
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∞)
⊢ s.indicator 1 (k a) *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (((((condDistrib f k μ : Kernel γ β) : (a : γ) → Measure β) (k a) : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
        (((((condDistrib g k μ : Kernel γ β') : (a : γ) → Measure β') (k a) : Measure β') : (a : Set β') → ℝ≥0∞) u :
          ℝ≥0∞) =
    (k ⁻¹' s).indicator 1 a *
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
        (((((Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) f : Kernel Ω β) : (a : Ω) → Measure β) a :
                Measure β) :
              (a : Set β) → ℝ≥0∞)
            t :
          ℝ≥0∞)
        (((((Kernel.map (condExpKernel μ (MeasurableSpace.comap k mγ)) g : Kernel Ω β') : (a : Ω) → Measure β') a :
                Measure β') :
              (a : Set β') → ℝ≥0∞)
            u :
          ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.Probability.Independence.Conditional
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∞)

Tactic:
have h_right {s : Set γ} {t : Set β} {u : Set β'} (hs : MeasurableSet s) (ht : MeasurableSet t)
      (hu : MeasurableSet u) :
      ((Kernel.id ×ₖ (condDistrib f k μ ×ₖ condDistrib g k μ)) ∘ₘ μ.map k) (s ×ˢ t ×ˢ u) =
        ((Kernel.id ×ₖ
          ((condExpKernel μ (mγ.comap k)).map f ×ₖ (condExpKernel μ (mγ.comap k)).map g)) ∘ₘ
        μ.trim hk.comap_le) ((k ⁻¹' s) ×ˢ t ×ˢ u) := by
    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]
    rotate_left
    · exact Kernel.measurable_coe _ ((hk_meas hs).prod (ht.prod hu))
    · exact Kernel.measurable_coe _ (hs.prod (ht.prod hu))
    refine lintegral_congr_ae ?_
    filter_upwards [condDistrib_apply_ae_eq_condExpKernel_map hf hk ht,
      condDistrib_apply_ae_eq_condExpKernel_map hg hk hu] with a haX haT
    simp only [Kernel.prod_apply_prod, Kernel.id_apply, Measure.dirac_apply' _ hs]
    rw [@Measure.dirac_apply' _ (mγ.comap k) _ _ (hk_meas hs)]
    congr