-- Mathlib/Probability/Process/Adapted.lean
theorem comp {t : ι → Ω → ι} [TopologicalSpace ι] [BorelSpace ι] [MetrizableSpace ι]
    (h : ProgMeasurable f u) (ht : ProgMeasurable f t) (ht_le : ∀ i ω, t i ω ≤ i) :
    ProgMeasurable f fun i ω => u (t i ω) ω

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
⊢ ProgMeasurable f fun i ω => u (t i ω) ω

Tactic:
intro i

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
⊢ StronglyMeasurable fun p => (fun i ω => u (t i ω) ω) (↑p.1) p.2

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p => u (t (↑p.1) p.2) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ StronglyMeasurable fun p => (fun i ω => u (t i ω) ω) (↑p.1) p.2

Tactic:
rw [this]

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p => u (t (↑p.1) p.2) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ StronglyMeasurable ((fun p => u (↑p.1) p.2) ∘ fun p => (⟨t (↑p.1) p.2, ⋯⟩, p.2))

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p => u (t (↑p.1) p.2) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ StronglyMeasurable ((fun p => u (↑p.1) p.2) ∘ fun p => (⟨t (↑p.1) p.2, ⋯⟩, p.2))

Tactic:
exact (h i).comp_measurable ((ht i).measurable.subtype_mk.prod_mk measurable_snd)

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
⊢ StronglyMeasurable fun p => (fun i ω => u (t i ω) ω) (↑p.1) p.2

Tactic:
have : (fun p : ↥(Set.Iic i) × Ω => u (t (p.fst : ι) p.snd) p.snd) =
  (fun p : ↥(Set.Iic i) × Ω => u (p.fst : ι) p.snd) ∘ fun p : ↥(Set.Iic i) × Ω =>
    (⟨t (p.fst : ι) p.snd, Set.mem_Iic.mpr ((ht_le _ _).trans p.fst.prop)⟩, p.snd) := rfl

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder ι
u : ι → Ω → β
f : Filtration ι m
inst✝³ : MeasurableSpace ι
t : ι → Ω → ι
inst✝² : TopologicalSpace ι
inst✝¹ : BorelSpace ι
inst✝ : MetrizableSpace ι
h : ProgMeasurable f u
ht : ProgMeasurable f t
ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i
i : ι
this : (fun p => u (t (↑p.1) p.2) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨t (↑p.1) p.2, ⋯⟩, p.2)
⊢ StronglyMeasurable fun p => (fun i ω => u (t i ω) ω) (↑p.1) p.2