-- Mathlib/Probability/Independence/Conditional.lean
lemma condIndepSets_iff (s1 s2 : Set (Set Ω)) (hs1 : ∀ s ∈ s1, MeasurableSet s)
    (hs2 : ∀ s ∈ s2, MeasurableSet s) (μ : Measure Ω) [IsFiniteMeasure μ] :
    CondIndepSets m' hm' s1 s2 μ ↔ ∀ (t1 t2 : Set Ω) (_ : t1 ∈ s1) (_ : t2 ∈ s2),
      (μ⟦t1 ∩ t2 | m'⟧) =ᵐ[μ] (μ⟦t1 | m'⟧) * (μ⟦t2 | m'⟧)

Proof state:
case h
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs2_eq : ∀ s ∈ s2, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω => (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᶠ[ae μ] μ[(s ∩ t).indicator fun ω => 1|m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h✝ : μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = (μ[s.indicator fun ω => 1|m']) ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = (μ[t.indicator fun ω => 1|m']) ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = (μ[(s ∩ t).indicator fun ω => 1|m']) ω
h : (μ[(s ∩ t).indicator fun ω => 1|m']) ω = (μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']) ω
h_ne_top : ((condExpKernel μ m') ω) (s ∩ t) ≠ ⊤
⊢ ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t

Tactic:
rw [← ENNReal.ofReal_toReal h_ne_top, hst_eq, h, Pi.mul_apply, ← hs_eq, ← ht_eq,
  ← ENNReal.toReal_mul, ENNReal.ofReal_toReal]

Result:
case h
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs2_eq : ∀ s ∈ s2, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω => (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᶠ[ae μ] μ[(s ∩ t).indicator fun ω => 1|m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h✝ : μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = (μ[s.indicator fun ω => 1|m']) ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = (μ[t.indicator fun ω => 1|m']) ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = (μ[(s ∩ t).indicator fun ω => 1|m']) ω
h : (μ[(s ∩ t).indicator fun ω => 1|m']) ω = (μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']) ω
h_ne_top : ((condExpKernel μ m') ω) (s ∩ t) ≠ ⊤
⊢ ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t ≠ ⊤

Proof state:
case refine_2
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs2_eq : ∀ s ∈ s2, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω => (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᶠ[ae μ] μ[(s ∩ t).indicator fun ω => 1|m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h : μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']
⊢ ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t

Tactic:
refine ((stronglyMeasurable_condExpKernel ((hs1 s hs).inter (hs2 t ht))).ae_eq_trim_iff hm'
  ((measurable_condExpKernel (hs1 s hs)).mul
    (measurable_condExpKernel (hs2 t ht))).stronglyMeasurable).mpr ?_

Result:
case refine_2
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs2_eq : ∀ s ∈ s2, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω => (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᶠ[ae μ] μ[(s ∩ t).indicator fun ω => 1|m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h : μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']
⊢ (fun ω => ((condExpKernel μ m') ω) (s ∩ t)) =ᶠ[ae μ] fun a => ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t

Proof state:
case refine_1
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs2_eq : ∀ s ∈ s2, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω => (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᶠ[ae μ] μ[(s ∩ t).indicator fun ω => 1|m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
h' :
  (fun x => ((condExpKernel μ m') x) (s ∩ t)) =ᶠ[ae μ] fun x => ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
⊢ μ[(s ∩ t).indicator fun ω => 1|m'] =ᶠ[ae μ] μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']

Tactic:
filter_upwards [hs1_eq s hs, hs2_eq t ht, hs12_eq s hs t ht, h'] with ω hs_eq ht_eq hst_eq h'

Result:
case h
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s1 s2 : Set (Set Ω)
hs1 : ∀ s ∈ s1, MeasurableSet s
hs2 : ∀ s ∈ s2, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hs1_eq : ∀ s ∈ s1, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs2_eq : ∀ s ∈ s2, (fun ω => (((condExpKernel μ m') ω) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω => (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᶠ[ae μ] μ[(s ∩ t).indicator fun ω => 1|m']
s t : Set Ω
hs : s ∈ s1
ht : t ∈ s2
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
h'✝ :
  (fun x => ((condExpKernel μ m') x) (s ∩ t)) =ᶠ[ae μ] fun x => ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = (μ[s.indicator fun ω => 1|m']) ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = (μ[t.indicator fun ω => 1|m']) ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = (μ[(s ∩ t).indicator fun ω => 1|m']) ω
h' : ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t
⊢ (μ[(s ∩ t).indicator fun ω => 1|m']) ω = (μ[s.indicator fun ω => 1|m'] * μ[t.indicator fun ω => 1|m']) ω