-- 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 : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk :
  partialTraj (X := X) κ a k =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a k).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a k)
x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))
i : ↥(Iic (k + 1))
pos :
  ∀ (h : (↑i : ℕ) ≤ k) (h_1 : (↑i : ℕ) ≤ a),
    x.1.1 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) ⋯) =
      ((prodAssoc :
              (a_1 :
                  (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) ×
                    ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
                ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
            x).1
        (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) ⋯)
neg :
  ∀ (h : (↑i : ℕ) ≤ k) (h_1 : ¬(↑i : ℕ) ≤ a),
    x.1.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a k) (↑i : ℕ) ⋯) =
      ((prodAssoc :
                (a_1 :
                    (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) ×
                      ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
                  ((i : ↥(Iic a)) → X (↑i : ℕ)) ×
                    ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
              x).2.1
        (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a k) (↑i : ℕ) ⋯)
⊢ Eq.{u_1 + 1} (α := X (↑i : ℕ))
    (if h : (↑i : ℕ) ≤ k then
      if h_1 : (↑i : ℕ) ≤ a then x.1.1 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) ⋯)
      else x.1.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a k) (↑i : ℕ) ⋯)
    else x.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc k (k + 1)) (↑i : ℕ) ⋯))
    (if h : (↑i : ℕ) ≤ a then
      ((prodAssoc :
              (a_1 :
                  (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) ×
                    ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
                ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
            x).1
        (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) ⋯)
    else
      if h_1 : (↑i : ℕ) ≤ k then
        ((prodAssoc :
                  (a_1 :
                      (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) ×
                        ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
                    ((i : ↥(Iic a)) → X (↑i : ℕ)) ×
                      ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
                x).2.1
          (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a k) (↑i : ℕ) ⋯)
      else
        ((prodAssoc :
                  (a_1 :
                      (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) ×
                        ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
                    ((i : ↥(Iic a)) → X (↑i : ℕ)) ×
                      ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
                x).2.2
          (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc k (k + 1)) (↑i : ℕ) ⋯))
have pos₁ : ∀ (h : ¬(↑i : ℕ) ≤ k) (h_1 : (↑i : ℕ) ≤ a),
  x.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc k (k + 1)) (↑i : ℕ) sorry) =
    ((prodAssoc :
            (a_1 :
                (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) ×
                  ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
              ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
          x).1
      (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) sorry)
Tactic: split_ifs