-- Mathlib/Probability/Independence/Kernel.lean
lemma iIndepFun.comp {β γ : ι → Type*} {mβ : ∀ i, MeasurableSpace (β i)}
    {mγ : ∀ i, MeasurableSpace (γ i)} {f : ∀ i, Ω → β i}
    (h : iIndepFun mβ f κ μ) (g : ∀ i, β i → γ i) (hg : ∀ i, Measurable (g i)) :
    iIndepFun mγ (fun i ↦ g i ∘ f i) κ μ

Proof state:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
this :
  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ t, f i ⁻¹' (fun i => g i ⁻¹' s i) i) = ∏ i ∈ t, (κ a) (f i ⁻¹' (fun i => g i ⁻¹' s i) i)
a : α
ha : (κ a) (⋂ i ∈ t, f i ⁻¹' (g i ⁻¹' s i)) = ∏ i ∈ t, (κ a) (f i ⁻¹' (g i ⁻¹' s i))
⊢ (κ a) (⋂ i ∈ t, g i ∘ f i ⁻¹' s i) = ∏ i ∈ t, (κ a) (g i ∘ f i ⁻¹' s i)

Tactic:
simp_rw [Set.preimage_comp]

Result:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
this :
  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ t, f i ⁻¹' (fun i => g i ⁻¹' s i) i) = ∏ i ∈ t, (κ a) (f i ⁻¹' (fun i => g i ⁻¹' s i) i)
a : α
ha : (κ a) (⋂ i ∈ t, f i ⁻¹' (g i ⁻¹' s i)) = ∏ i ∈ t, (κ a) (f i ⁻¹' (g i ⁻¹' s i))
⊢ (κ a) (⋂ i ∈ t, f i ⁻¹' (g i ⁻¹' s i)) = ∏ x ∈ t, (κ a) (f x ⁻¹' (g x ⁻¹' s x))

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h : iIndepFun mβ f κ μ
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
⊢ iIndepFun mγ (fun i => g i ∘ f i) κ μ

Tactic:
rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at h ⊢

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
⊢ ∀ (S : Finset ι) {sets : (i : ι) → Set (γ i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, g i ∘ f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (g i ∘ f i ⁻¹' sets i)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
this :
  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ t, f i ⁻¹' (fun i => g i ⁻¹' s i) i) = ∏ i ∈ t, (κ a) (f i ⁻¹' (fun i => g i ⁻¹' s i) i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ t, g i ∘ f i ⁻¹' s i) = ∏ i ∈ t, (κ a) (g i ∘ f i ⁻¹' s i)

Tactic:
filter_upwards [this] with a ha

Result:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
this :
  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ t, f i ⁻¹' (fun i => g i ⁻¹' s i) i) = ∏ i ∈ t, (κ a) (f i ⁻¹' (fun i => g i ⁻¹' s i) i)
a : α
ha : (κ a) (⋂ i ∈ t, f i ⁻¹' (g i ⁻¹' s i)) = ∏ i ∈ t, (κ a) (f i ⁻¹' (g i ⁻¹' s i))
⊢ (κ a) (⋂ i ∈ t, g i ∘ f i ⁻¹' s i) = ∏ i ∈ t, (κ a) (g i ∘ f i ⁻¹' s i)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ t, g i ∘ f i ⁻¹' s i) = ∏ i ∈ t, (κ a) (g i ∘ f i ⁻¹' s i)

Tactic:
have := h t (sets := fun i ↦ g i ⁻¹' (s i)) (fun i a ↦ hg i (hs i a))

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
this :
  ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ t, f i ⁻¹' (fun i => g i ⁻¹' s i) i) = ∏ i ∈ t, (κ a) (f i ⁻¹' (fun i => g i ⁻¹' s i) i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ t, g i ∘ f i ⁻¹' s i) = ∏ i ∈ t, (κ a) (g i ∘ f i ⁻¹' s i)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
⊢ ∀ (S : Finset ι) {sets : (i : ι) → Set (γ i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, g i ∘ f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (g i ∘ f i ⁻¹' sets i)

Tactic:
refine fun t s hs ↦ ?_

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : ι → Type u_8
γ : ι → Type u_9
mβ : (i : ι) → MeasurableSpace (β i)
mγ : (i : ι) → MeasurableSpace (γ i)
f : (i : ι) → Ω → β i
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) → ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i ⁻¹' sets i) = ∏ i ∈ S, (κ a) (f i ⁻¹' sets i)
g : (i : ι) → β i → γ i
hg : ∀ (i : ι), Measurable (g i)
t : Finset ι
s : (i : ι) → Set (γ i)
hs : ∀ i ∈ t, MeasurableSet (s i)
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ t, g i ∘ f i ⁻¹' s i) = ∏ i ∈ t, (κ a) (g i ∘ f i ⁻¹' s i)