-- Lean 4 proof step from Mathlib.Analysis.BoxIntegral.UnitPartition (goal)
Goal:
ι : Type u_1
n : ℕ
inst : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst_1 : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ≤ (↑B : Set (ι → ℝ))
this :
  Fintype
    (↑(s ∩
          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))) :
      Type u_1)
x : ι → ℝ
hx_1 :
  x ∈
    (s ∩
        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))).toFinset
hx :
  x ∈
    s ∩
      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
refine_4 :
  F x / HPow.hPow (α := ℝ) (↑n : ℝ) (card ι) =
    ENNReal.toReal
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
          (↑((fun (x : ι → ℝ)
                    (x_1 :
                      x ∈
                        (s ∩
                            HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                              (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) :
                                Set (ι → ℝ))).toFinset) ↦
                  box n (index n x))
                x hx_1) :
            Set (ι → ℝ))) *
      F
        ((prepartition n B).tag
          ((fun (x : ι → ℝ)
                (x_1 :
                  x ∈
                    (s ∩
                        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) :
                            Set (ι → ℝ))).toFinset) ↦
              box n (index n x))
            x hx_1))
⊢ F x / HPow.hPow (α := ℝ) (↑n : ℝ) (card ι) =
    Measure.real.{u_1} (α := ι → ℝ) (m := MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ)) (volume : Measure (ι → ℝ))
        (↑((fun (x : ι → ℝ)
                  (x_1 :
                    x ∈
                      (s ∩
                          HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                            (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) :
                              Set (ι → ℝ))).toFinset) ↦
                box n (index n x))
              x hx_1) :
          Set (ι → ℝ)) *
      F
        ((prepartition n B).tag
          ((fun (x : ι → ℝ)
                (x_1 :
                  x ∈
                    (s ∩
                        HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                          (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) :
                            Set (ι → ℝ))).toFinset) ↦
              box n (index n x))
            x hx_1))
have refine_4₁ : F x / HPow.hPow (α := ℝ) (↑n : ℝ) (card ι) =
  (1 / HPow.hPow (α := ENNReal) (↑n : ENNReal) (card ι)).toReal *
    F
      ((prepartition n B).tag
        ((fun (x : ι → ℝ)
              (x_1 :
                x ∈
                  (s ∩
                      HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                        (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) :
                          Set (ι → ℝ))).toFinset) ↦
            box n (index n x))
          x hx_1))
Tactic: rw [measureReal_def, volume_box,
      prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)),
      tag_index_eq_self_of_mem_smul_span n hx.2, ENNReal.toReal_div,
      ENNReal.toReal_one, ENNReal.toReal_pow, ENNReal.toReal_natCast, mul_comm_div, one_mul]