-- Mathlib/Probability/Independence/Basic.lean
lemma iIndepFun.cond [Finite ι] (hY : ∀ i, Measurable (Y i))
    (hindep : iIndepFun (fun _ ↦ mα.prod mβ) (fun i ω ↦ (X i ω, Y i ω)) μ)
    (hy : ∀ i, μ (Y i ⁻¹' t i) ≠ 0) (ht : ∀ i, MeasurableSet (t i)) :
    iIndepFun (fun _ ↦ mα) X μ[|⋂ i, Y i ⁻¹' t i]

Proof state:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun x => mα.prod mβ) (fun i ω => (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ iIndepFun (fun x => mα) X μ[|⋂ i, Y i ⁻¹' t i]

Tactic:
rw [iIndepFun_iff]

Result:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun x => mα.prod mβ) (fun i ω => (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ (s : Finset ι) {f' : ι → Set Ω},
    (∀ i ∈ s, MeasurableSet (f' i)) → μ[⋂ i ∈ s, f' i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f' i | ⋂ i, Y i ⁻¹' t i]

Proof state:
case h.e'_3.a
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun x => mα.prod mβ) (fun i ω => (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
i : ι
hi : i ∈ s
⊢ μ[f i | ⋂ i, Y i ⁻¹' t i] = μ[f i | Y i ⁻¹' t i]

Tactic:
simpa using cond_iInter hY hindep (fun j hj ↦ hf _ <| Finset.mem_singleton.1 hj ▸ hi)
  (fun i _ ↦ hy _) ht

Result:
no goals

Proof state:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun x => mα.prod mβ) (fun i ω => (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
⊢ μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | ⋂ i, Y i ⁻¹' t i]

Tactic:
convert cond_iInter hY hindep hf (fun i _ ↦ hy _) ht using 2 with i hi

Result:
case h.e'_3.a
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun x => mα.prod mβ) (fun i ω => (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
i : ι
hi : i ∈ s
⊢ μ[f i | ⋂ i, Y i ⁻¹' t i] = μ[f i | Y i ⁻¹' t i]

Proof state:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun x => mα.prod mβ) (fun i ω => (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ (s : Finset ι) {f' : ι → Set Ω},
    (∀ i ∈ s, MeasurableSet (f' i)) → μ[⋂ i ∈ s, f' i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f' i | ⋂ i, Y i ⁻¹' t i]

Tactic:
intro s f hf

Result:
ι : Type u_6
Ω : Type u_7
α : Type u_8
β : Type u_9
mΩ : MeasurableSpace Ω
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure Ω
X : ι → Ω → α
Y : ι → Ω → β
t : ι → Set β
inst✝ : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (fun x => mα.prod mβ) (fun i ω => (X i ω, Y i ω)) μ
hy : ∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0
ht : ∀ (i : ι), MeasurableSet (t i)
s : Finset ι
f : ι → Set Ω
hf : ∀ i ∈ s, MeasurableSet (f i)
⊢ μ[⋂ i ∈ s, f i | ⋂ i, Y i ⁻¹' t i] = ∏ i ∈ s, μ[f i | ⋂ i, Y i ⁻¹' t i]