-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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))) :
              ℝ)|⁻¹)
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)
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)
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)
rw₇ 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
        |(LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            ((↑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (ι → ℝ) →ₗ[ℝ] ι → ℝ)|)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) s : ENNReal)
⊢ ((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 (ι → ℝ))))

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]

Premises used: Iff.mpr, ZLattice.covolume_eq_det_inv, Units.ne_zero, LinearEquiv.image_eq_preimage_symm, LinearEquiv.symm_symm, abs_pos, ENNReal.ofReal_inv_of_pos, inv_inv, MeasureTheory.Measure.addHaar_preimage_linearEquiv, ENNReal.div_eq_inv_mul, LinearEquiv.coe_det