-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hp :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) →
      X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯) : ℕ))
    ((fun (x : (n : ↥(Iic (a + 1))) → X (↑n : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      _root_.IicProdIoc (X := X) a (a + 1))
    ((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
      Prod.snd)
rw :
  (map (mβ := MeasurableSpace.pi (X := fun (i : ↥(Iic (a + 1))) ↦ X (↑i : ℕ)))
      (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a (a + 1)))
      fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) =
    κ a
rw₁ :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
        _root_.IicProdIoc (X := X) a (a + 1)) =
    κ a
rw₂ :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      ((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
        Prod.snd) =
    κ a
rw₃ :
  map (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) (mβ :=
      MeasurableSpace.pi (X := fun (i : ↥(Ioc a (a + 1))) ↦ X (↑i : ℕ)))
      (map (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
        Prod.snd)
      (⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) =
    κ a
rw₄ :
  map (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) (mβ :=
      MeasurableSpace.pi (X := fun (i : ↥(Ioc a (a + 1))) ↦ X (↑i : ℕ)))
      (snd
        (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))))
      (⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) =
    κ a
rw₅ :
  map (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) (mβ :=
      MeasurableSpace.pi (X := fun (i : ↥(Ioc a (a + 1))) ↦ X (↑i : ℕ)))
      ((κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      (⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) =
    κ a
rw₆ :
  (κ a).map
      (Function.comp (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
        (⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1))
        (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) =
    κ a
⊢ (map (partialTraj (X := X) κ a (a + 1)) fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) =
    κ a
have rw₇ : (κ a).map id = κ a
Tactic: rw [partialTraj_succ_self, ← map_comp_right _ (by fun_prop) (by fun_prop), hp,
    map_comp_right _ (by fun_prop) (by fun_prop), ← snd_eq, snd_prod,
    ← map_comp_right _ (by fun_prop) (by fun_prop), symm_comp_self, map_id]