-- 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:
case refine_2.refine_1
Ω : 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']
⊢ MeasurableSet (⋂ i ∈ s, f i)

Tactic:
exact .biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (hf i hi))

Result:
no goals

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']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
⊢ (∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ π i) →
        ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') a) (f i)) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ π i) →
        μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']

Tactic:
have h_inter_eq : ∀ (s : Finset ι) (f : ι → Set Ω) (_H : ∀ i, i ∈ s → f i ∈ π i),
    (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (⋂ i ∈ s, f i)))
      =ᵐ[μ] μ⟦⋂ i ∈ s, f i | m'⟧ := by
  refine fun s f H ↦ condExpKernel_ae_eq_condExp hm' ?_
  exact MeasurableSet.biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (H i hi))

Result:
Ω : 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 Ω},
      (∀ i ∈ s, f i ∈ π i) →
        ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') a) (f i)) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ π i) →
        μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|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, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω

Tactic:
simp_rw [← Finset.mem_coe]

Result:
Ω : 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, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|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 μ
⊢ iCondIndepSets m' hm' π μ ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ π i) →
        μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|m']

Tactic:
simp only [iCondIndepSets, Kernel.iIndepSets]

Result:
Ω : 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 μ
⊢ (∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ π i) →
        ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (⋂ i ∈ s, f i) = ∏ i ∈ s, ((condExpKernel μ m') a) (f i)) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ π i) →
        μ[(⋂ i ∈ s, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(f i).indicator fun ω => 1|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']
h_eq :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ MeasurableSet (⋂ i ∈ s, f i)

Tactic:
exact MeasurableSet.biInter (Finset.countable_toSet _) (fun i hi ↦ hπ i _ (H i hi))

Result:
no goals

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, (((condExpKernel μ m') ω) (f i)).toReal = (μ[(f i).indicator fun ω => 1|m']) ω

Tactic:
rw [ae_ball_iff (Finset.countable_toSet s)]

Result:
Ω : 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