-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
ι : Type u_2
inst : Fintype ι
L : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_2} ↥L
inst_2 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
rw :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(LinearEquiv.symm (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b))) : (a : ι → ℝ) → ι → ℝ) ⁻¹' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
rw₁ :
  HMul.hMul (β := ENNReal)
      (ENNReal.ofReal
        |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            (↑(LinearEquiv.symm (LinearEquiv.symm (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)))) :
              (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
rw₂ :
  HMul.hMul (β := ENNReal)
      (ENNReal.ofReal
        |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            (↑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
rw₃ :
  HMul.hMul (β := ENNReal)
      (ENNReal.ofReal
        |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            (↑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal
        |(↑(((LinearEquiv.det : ((ι → ℝ) ≃ₗ[ℝ] ι → ℝ) →* ℝˣ) : (a : (ι → ℝ) ≃ₗ[ℝ] ι → ℝ) → ℝˣ)
                  (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b))) :
              ℝ)|⁻¹)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : ι → ℝ) → ι → ℝ) '' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ))))
have rw₄ : HMul.hMul (β := ENNReal)
    (ENNReal.ofReal
      |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
          (↑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal) =
  HMul.hMul (β := ENNReal)
    (ENNReal.ofReal
        |(↑(((LinearEquiv.det : ((ι → ℝ) ≃ₗ[ℝ] ι → ℝ) →* ℝˣ) : (a : (ι → ℝ) ≃ₗ[ℝ] ι → ℝ) → ℝˣ)
                  (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b))) :
              ℝ)|⁻¹)⁻¹
    (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
Tactic: rw [LinearEquiv.image_eq_preimage_symm, Measure.addHaar_preimage_linearEquiv,
    LinearEquiv.symm_symm, covolume_eq_det_inv L b, ENNReal.div_eq_inv_mul,
    ENNReal.ofReal_inv_of_pos (abs_pos.2 (LinearEquiv.det _).ne_zero), inv_inv, LinearEquiv.coe_det]