-- Mathlib/Probability/Independence/Conditional.lean
lemma iCondIndepSets_iff (π : ι → Set (Set Ω)) (hπ : ∀ i s (_hs : s ∈ π i), MeasurableSet s)
    (μ : Measure Ω) [IsFiniteMeasure μ] :
    iCondIndepSets m' hm' π μ ↔ ∀ (s : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s → f i ∈ π i),
      μ⟦⋂ i ∈ s, f i | m'⟧ =ᵐ[μ] ∏ i ∈ s, (μ⟦f i | m'⟧)

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω => (((condExpKernel μ m') ω) (f i)).toReal) =ᶠ[ae μ] μ[(f i).indicator fun ω => 1|m']
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ ∀ i ∈ ↑s, ∀ᵐ (x : Ω) ∂μ, (((condExpKernel μ m') x) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) x

Tactic:
exact h_eq' s f H

Result:
no goals

Proof state:
case refine_2.refine_3
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω => (((condExpKernel μ m') ω) (f i)).toReal) =ᶠ[ae μ] μ[(f i).indicator fun ω => 1|m']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
h_inter_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω => (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᶠ[ae μ] μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h : μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']
⊢ (fun ω => ((condExpKernel μ m') ω) (⋂ i ∈ s, f i)) =ᶠ[ae μ] fun a => ∏ i ∈ s, ((condExpKernel μ m') a) (f i)

Tactic:
filter_upwards [h_eq s f hf, h_inter_eq s f hf, h] with ω h_eq h_inter_eq h

Result:
case h
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω => (((condExpKernel μ m') ω) (f i)).toReal) =ᶠ[ae μ] μ[(f i).indicator fun ω => 1|m']
h_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
h_inter_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω => (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᶠ[ae μ] μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h✝ : μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']
ω : Ω
h_eq : ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
h_inter_eq : (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal = (μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m']) ω
h : (μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m']) ω = (∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']) ω
⊢ ((condExpKernel μ m') ω) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') ω) (f i)

Proof state:
case h
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω => (((condExpKernel μ m') ω) (f i)).toReal) =ᶠ[ae μ] μ[(f i).indicator fun ω => 1|m']
h_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
h_inter_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω => (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᶠ[ae μ] μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') a) (f i)
h'✝ : (fun x => ((condExpKernel μ m') x) (⋂ i ∈ s, f i)) =ᶠ[ae μ] fun x => ∏ i ∈ s, ((condExpKernel μ m') x) (f i)
ω : Ω
h_eq : ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
h_inter_eq : (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal = (μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m']) ω
h' : ((condExpKernel μ m') ω) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') ω) (f i)
⊢ (μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m']) ω = (∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']) ω

Tactic:
rw [← h_inter_eq, h', ENNReal.toReal_prod, Finset.prod_apply]

Result:
case h
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω => (((condExpKernel μ m') ω) (f i)).toReal) =ᶠ[ae μ] μ[(f i).indicator fun ω => 1|m']
h_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
h_inter_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω => (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᶠ[ae μ] μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m']
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, f i ∈ π i
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') a) (f i)
h'✝ : (fun x => ((condExpKernel μ m') x) (⋂ i ∈ s, f i)) =ᶠ[ae μ] fun x => ∏ i ∈ s, ((condExpKernel μ m') x) (f i)
ω : Ω
h_eq : ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
h_inter_eq : (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal = (μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m']) ω
h' : ((condExpKernel μ m') ω) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') ω) (f i)
⊢ ∏ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = ∏ c ∈ s, (μ[(f c).indicator fun ω => 1|m']) ω