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

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

Tactic:
exact Set.iInter₂_congr hf

Result:
no goals

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

Tactic:
apply congr_arg₂

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

case h.refine_1.e_f.hy
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h : ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']
S : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ S, f i = s i
a : Ω
ha : (μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m']) a = (∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']) a
⊢ (fun ω => 1) = fun ω => 1

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

Tactic:
rw [hf i hi]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepSets m' hm' (fun i => {s i}) μ ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']

Tactic:
rw [iCondIndepSets_iff]

Result:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i ∈ {s i}) →
        μ[(⋂ i ∈ s_1, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s_1, μ[(f i).indicator fun ω => 1|m']) ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']

case hπ
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), ∀ s_1 ∈ {s i}, MeasurableSet s_1

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

Tactic:
congr

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

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i ∈ {s i}) →
        μ[(⋂ i ∈ s_1, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s_1, μ[(f i).indicator fun ω => 1|m']) ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']

Tactic:
simp only [Set.mem_singleton_iff]

Result:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
s : ι → Set Ω
hπ : ∀ (i : ι), MeasurableSet (s i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s_1 : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s_1, f i = s i) →
        μ[(⋂ i ∈ s_1, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s_1, μ[(f i).indicator fun ω => 1|m']) ↔
    ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']