-- Mathlib/Probability/Kernel/Condexp.lean
lemma compProd_trim_condExpKernel (hm : m ≤ mΩ) :
    (μ.trim hm) ⊗ₘ condExpKernel μ m
      = @Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω ↦ (id ω, id ω)) μ

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun ω => (id ω, id ω)) μ

Tactic:
rcases isEmpty_or_nonempty Ω with h | h

Result:
case inl
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : IsEmpty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun ω => (id ω, id ω)) μ

case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun ω => (id ω, id ω)) μ

Proof state:
case inr.e_κ
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h✝ : Nonempty Ω
this : m ⊓ mΩ = m
h : Measure.map id μ ⊗ₘ condDistrib id id μ = Measure.map (fun a => (id a, id a)) μ
⊢ (condDistrib id id μ).comap id ⋯ = condDistrib id id μ

Tactic:
ext a s hs

Result:
case inr.e_κ.h.h
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h✝ : Nonempty Ω
this : m ⊓ mΩ = m
h : Measure.map id μ ⊗ₘ condDistrib id id μ = Measure.map (fun a => (id a, id a)) μ
a : Ω
s : Set Ω
hs : MeasurableSet s
⊢ (((condDistrib id id μ).comap id ⋯) a) s = ((condDistrib id id μ) a) s

Proof state:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun ω => (id ω, id ω)) μ

Tactic:
rw [condExpKernel_eq]

Result:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
⊢ μ.trim hm ⊗ₘ (condDistrib id id μ).comap id ⋯ = Measure.map (fun ω => (id ω, id ω)) μ

Proof state:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
⊢ μ.trim hm ⊗ₘ (condDistrib id id μ).comap id ⋯ = Measure.map (fun ω => (id ω, id ω)) μ

Tactic:
have : m ⊓ mΩ = m := inf_of_le_left hm

Result:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
this : m ⊓ mΩ = m
⊢ μ.trim hm ⊗ₘ (condDistrib id id μ).comap id ⋯ = Measure.map (fun ω => (id ω, id ω)) μ

Proof state:
case inr.e_κ.h.h
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h✝ : Nonempty Ω
this : m ⊓ mΩ = m
h : Measure.map id μ ⊗ₘ condDistrib id id μ = Measure.map (fun a => (id a, id a)) μ
a : Ω
s : Set Ω
hs : MeasurableSet s
⊢ (((condDistrib id id μ).comap id ⋯) a) s = ((condDistrib id id μ) a) s

Tactic:
simp only [Kernel.coe_comap, Function.comp_apply, id_eq]

Result:
case inr.e_κ.h.h
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h✝ : Nonempty Ω
this : m ⊓ mΩ = m
h : Measure.map id μ ⊗ₘ condDistrib id id μ = Measure.map (fun a => (id a, id a)) μ
a : Ω
s : Set Ω
hs : MeasurableSet s
⊢ ((condDistrib id id μ) a) s = ((condDistrib id id μ) a) s

Proof state:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h✝ : Nonempty Ω
this : m ⊓ mΩ = m
h : Measure.map id μ ⊗ₘ condDistrib id id μ = Measure.map (fun a => (id a, id a)) μ
⊢ μ.trim hm ⊗ₘ (condDistrib id id μ).comap id ⋯ = Measure.map (fun ω => (id ω, id ω)) μ

Tactic:
rw [← h, trim_eq_map hm]

Result:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h✝ : Nonempty Ω
this : m ⊓ mΩ = m
h : Measure.map id μ ⊗ₘ condDistrib id id μ = Measure.map (fun a => (id a, id a)) μ
⊢ Measure.map id μ ⊗ₘ (condDistrib id id μ).comap id ⋯ = Measure.map id μ ⊗ₘ condDistrib id id μ

Proof state:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
this : m ⊓ mΩ = m
⊢ μ.trim hm ⊗ₘ (condDistrib id id μ).comap id ⋯ = Measure.map (fun ω => (id ω, id ω)) μ

Tactic:
have h := compProd_map_condDistrib (mβ := m) (μ := μ) (X := id) measurable_id.aemeasurable

Result:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h✝ : Nonempty Ω
this : m ⊓ mΩ = m
h : Measure.map id μ ⊗ₘ condDistrib id id μ = Measure.map (fun a => (id a, id a)) μ
⊢ μ.trim hm ⊗ₘ (condDistrib id id μ).comap id ⋯ = Measure.map (fun ω => (id ω, id ω)) μ

Proof state:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h✝ : Nonempty Ω
this : m ⊓ mΩ = m
h : Measure.map id μ ⊗ₘ condDistrib id id μ = Measure.map (fun a => (id a, id a)) μ
⊢ Measure.map id μ ⊗ₘ (condDistrib id id μ).comap id ⋯ = Measure.map id μ ⊗ₘ condDistrib id id μ

Tactic:
congr 1

Result:
case inr.e_κ
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h✝ : Nonempty Ω
this : m ⊓ mΩ = m
h : Measure.map id μ ⊗ₘ condDistrib id id μ = Measure.map (fun a => (id a, id a)) μ
⊢ (condDistrib id id μ).comap id ⋯ = condDistrib id id μ

Proof state:
case inr.e_κ.h.h
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h✝ : Nonempty Ω
this : m ⊓ mΩ = m
h : Measure.map id μ ⊗ₘ condDistrib id id μ = Measure.map (fun a => (id a, id a)) μ
a : Ω
s : Set Ω
hs : MeasurableSet s
⊢ ((condDistrib id id μ) a) s = ((condDistrib id id μ) a) s

Tactic:
congr

Result:
no goals

Proof state:
case inl
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : IsEmpty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun ω => (id ω, id ω)) μ

Tactic:
simp [Measure.eq_zero_of_isEmpty μ]

Result:
no goals