-- 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:
Ω : 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:
refine ⟨fun h S ↦ h S (fun i _ ↦ rfl), fun h S f hf ↦ ?_⟩

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 μ
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
⊢ μ[(⋂ 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Ω
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
⊢ μ[(⋂ i ∈ S, f i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(f i).indicator fun ω => 1|m']

Tactic:
filter_upwards [h S] with a ha

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

Proof state:
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

Tactic:
simpa only [Set.mem_singleton_iff, forall_eq]

Result:
no goals

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 ∈ S, μ[(s i).indicator fun ω => 1|m']) a = (∏ i ∈ S, μ[(f i).indicator fun ω => 1|m']) a

Tactic:
simp_rw [Finset.prod_apply]

Result:
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
⊢ ∏ c ∈ S, (μ[(s c).indicator fun ω => 1|m']) a = ∏ c ∈ S, (μ[(f c).indicator fun ω => 1|m']) a

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
⊢ ∏ c ∈ S, (μ[(s c).indicator fun ω => 1|m']) a = ∏ c ∈ S, (μ[(f c).indicator fun ω => 1|m']) a

Tactic:
refine Finset.prod_congr rfl (fun i hi ↦ ?_)

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

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

Tactic:
refine Eq.trans ?_ (ha.trans ?_)

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

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 ∈ S, μ[(s i).indicator fun ω => 1|m']) a = (∏ i ∈ S, μ[(f i).indicator fun ω => 1|m']) a

Proof state:
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

Tactic:
rfl

Result:
no goals