-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X (↑i : ι))
ms : ∀ (i : ↥J), MeasurableSet (s i)
simp_rw simp_rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI) (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        (restrict₂ (π := X) hJI ⁻¹' Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₃ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥I) ↦ X (↑i : ι)) Set.univ fun (j : ↥I) ↦
          if h : (↑j : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑j : ι) h) else Set.univ) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₄ :
  Eq (α := ℝ≥0∞)
    (∏ i : ↥I,
      ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
        (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i))
simp_rw₅ :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ I,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x)
    (∏ x ∈ J,
      Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
        (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
refine_1 :
  ∀ (x : ι) (hx : x ∈ I \ J),
    Eq (α := ℝ≥0∞)
      (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
        (fun (i : ↥I) ↦
          ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
            (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
        1 x)
      1
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (restrict₂ (π := X) hJI)
            ((fun (I : Finset ι) ↦
                (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) :
                  Measure ((i : ↥I) → X (↑i : ι))))
              I) :
          (a : Set ((i : ↥J) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (j : ↥J) ↦ X (↑j : ι)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥J, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i) : ℝ≥0∞)
have refine_2 : ∀ (x : ι) (hx : x ∈ J),
  Eq (α := ℝ≥0∞)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ J))
      (fun (i : ↥J) ↦ ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (s i)) 1 x)
    (Function.extend (Subtype.val (p := fun (x : ι) ↦ x ∈ I))
      (fun (i : ↥I) ↦
        ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
          (if h : (↑i : ι) ∈ J then s (Subtype.mk (p := fun (x : ι) ↦ x ∈ J) (↑i : ι) h) else Set.univ))
      1 x)
Tactic: classical
  simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI,
    Measure.pi_pi, prod_eq_prod_extend]
  refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm
  · rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
  · rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]