-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ℕ))
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Iic a
inl :
  Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Iic b))
        (fun (i : ↥(Iic b)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx)) :
      ℝ≥0∞)
inl₁ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯) : ℕ))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯)) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx)) :
      ℝ≥0∞)
inl₂ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯) : ℕ))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯)) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (restrict₂ (π := fun (n : ℕ) ↦ Set (X n)) ⋯ s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx)) :
      ℝ≥0∞)
inl₃ inl₄ :
  Eq (α := ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯) : ℕ))) :
          (a : Set (X (↑⟨x, ⋯⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) x ⋯)) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ))) :
          (a : Set (X (↑⟨x, hx⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic b) (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) x hx) : ℕ) ⋯)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Iic b))
      (fun (i : ↥(Iic b)) ↦ ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i)) 1 x)
    (Function.extend (Subtype.val (p := fun (x : ℕ) ↦ x ∈ Iic a))
      (fun (i : ↥(Iic a)) ↦
        ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞)
          (frestrictLe₂ (π := fun (n : ℕ) ↦ Set (X n)) hab s i))
      1 x)

Tactic:
rw [Function.extend_val_apply hx, Function.extend_val_apply (Iic_subset_Iic.2 hab hx),
        frestrictLe₂, restrict₂]

Premises used: Iff.mpr, Finset.Iic_subset_Iic, Preorder.frestrictLe₂, Finset.restrict₂, Function.extend_val_apply