-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_3
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
inst_3 : DecidableEq ι
i : ι
s : Set (α i)
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞) ((fun (f : (a : ι) → α a) ↦ f i) ⁻¹' s) : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := α) μ : (a : Set ((a : ι) → α a)) → ℝ≥0∞)
        (Set.pi (α := α) univ (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s)) :
      ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞)
    (∏ i_1 : ι,
        (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) :
      ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
h₃ :
  ∏ i_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) =
    HSMul.hSMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ)
      ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
h₄ :
  ∏ i_1 : ι, (μ i_1 : (a : Set (α i_1)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i_1) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
h₅ h₆ h₇ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      (∏ x ∈ Finset.erase Finset.univ i,
          (μ x : (a : Set (α x)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s x) :
        ℝ≥0∞)
      ((μ i : (a : Set (α i)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
h₈ :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ i,
      (μ x : (a : Set (α x)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s x))
    (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ)
h₉ h₁₀ :
  Eq (α := ℝ≥0∞)
    ((μ i : (a : Set (α i)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i) : ℝ≥0∞)
    ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
h₁₁ :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ i,
      (μ x : (a : Set (α x)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s x))
    (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ)
h₁₂ :
  Eq (α := ℝ≥0∞)
    ((μ i : (a : Set (α i)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s i) : ℝ≥0∞)
    ((μ i : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
h₁₃ h₁₄ :
  Eq (α := ℝ≥0∞)
    (∏ x ∈ Finset.erase Finset.univ i,
      (μ x : (a : Set (α x)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s x))
    (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ)
⊢ Eq (α := ℝ≥0∞) (((map (eval (β := α) i) (Measure.pi (α := α) μ) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (∏ j ∈ Finset.erase Finset.univ i, (μ j : (a : Set (α j)) → ℝ≥0∞) univ) (μ i) :
          (a : Set (α i)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁₅ : ∀ (j : ι) (hj : j ∈ Finset.erase Finset.univ i),
  Eq (α := ℝ≥0∞)
    ((μ j : (a : Set (α j)) → ℝ≥0∞) (update (β := fun (i : ι) ↦ Set (α i)) (fun (j : ι) ↦ univ) i s j) : ℝ≥0∞)
    ((μ j : (a : Set (α j)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: classical
  rw [Measure.map_apply (measurable_pi_apply i) hs, ← Set.univ_pi_update_univ, Measure.pi_pi,
    Measure.smul_apply, smul_eq_mul, ← Finset.prod_erase_mul _ _ (a := i) (by simp)]
  congrm ?_ * ?_
  swap; · simp
  refine Finset.prod_congr rfl fun j hj ↦ ?_
  simp [Function.update, Finset.ne_of_mem_erase hj]