Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case pos
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 κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc 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))
h✝¹ : ↑i ≤ k
h✝ : ↑i ≤ a
⊢ x.1.1 ⟨↑i, ⋯⟩ = (prodAssoc x).1 ⟨↑i, ⋯⟩

pp: case neg
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 κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc 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))
h✝¹ : ↑i ≤ k
h✝ : ¬↑i ≤ a
⊢ x.1.2 ⟨↑i, ⋯⟩ = (prodAssoc x).2.1 ⟨↑i, ⋯⟩

pp: case pos
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 κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc 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))
h✝¹ : ¬↑i ≤ k
h✝ : ↑i ≤ a
⊢ x.2 ⟨↑i, ⋯⟩ = (prodAssoc x).1 ⟨↑i, ⋯⟩

pp: case neg
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 κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc 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))
h✝¹ : ¬↑i ≤ k
h✝ : ¬↑i ≤ a
⊢ x.2 ⟨↑i, ⋯⟩ = (prodAssoc x).2.2 ⟨↑i, ⋯⟩

Tactic:
<;>

Goal state after:
case pos
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 κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc 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))
h✝¹ : ↑i ≤ k
h✝ : ↑i ≤ a
⊢ x.1.1 ⟨↑i, ⋯⟩ = (prodAssoc x).1 ⟨↑i, ⋯⟩

case neg
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 κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc 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))
h✝¹ : ↑i ≤ k
h✝ : ¬↑i ≤ a
⊢ x.1.2 ⟨↑i, ⋯⟩ = (prodAssoc x).2.1 ⟨↑i, ⋯⟩

case pos
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 κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc 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))
h✝¹ : ¬↑i ≤ k
h✝ : ↑i ≤ a
⊢ x.2 ⟨↑i, ⋯⟩ = (prodAssoc x).1 ⟨↑i, ⋯⟩

case neg
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 κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc 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))
h✝¹ : ¬↑i ≤ k
h✝ : ¬↑i ≤ a
⊢ x.2 ⟨↑i, ⋯⟩ = (prodAssoc x).2.2 ⟨↑i, ⋯⟩