-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L
inst_6 : IsZLattice ℝ L
ι : Type u_3
inst_7 : Fintype ι
b : Basis.{u_3, 0, u_2} ι ℤ ↥L
s : Set E
hs : NullMeasurableSet s (volume : Measure E)
let let₁ let₂ let₃ :
  ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume L (volume : Measure E)))
let₄ :
  let e : Fin (finrank ℝ E) ≃ ι := Fintype.equivOfCardEq ⋯;
  let f : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (ι → ℝ) E :=
    (ContinuousLinearEquiv.symm (EuclideanSpace.equiv ι ℝ)).trans
      (ContinuousLinearEquiv.symm
        (↑(OrthonormalBasis.repr (OrthonormalBasis.reindex (stdOrthonormalBasis ℝ E) e)) : E ≃L[ℝ] EuclideanSpace ℝ ι));
  ∀
    (hf :
      MeasurePreserving.{u_3, u_2} (α := ι → ℝ) (β := E) (⇑f : (a : ι → ℝ) → E) (volume : Measure (ι → ℝ))
        (volume : Measure E)),
    ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
        ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s) =
      HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) s : ENNReal)
        (ENNReal.ofReal (covolume L (volume : Measure E)))
let₅ :
  let e : Fin (finrank ℝ E) ≃ ι := Fintype.equivOfCardEq ⋯;
  let f : ContinuousLinearEquiv.{0, 0, u_3, u_2} (RingHom.id ℝ) (ι → ℝ) E :=
    (ContinuousLinearEquiv.symm (EuclideanSpace.equiv ι ℝ)).trans
      (ContinuousLinearEquiv.symm
        (↑(OrthonormalBasis.repr (OrthonormalBasis.reindex (stdOrthonormalBasis ℝ E) e)) : E ≃L[ℝ] EuclideanSpace ℝ ι));
  ∀
    (hf :
      MeasurePreserving.{u_3, u_2} (α := ι → ℝ) (β := E) (⇑f : (a : ι → ℝ) → E) (volume : Measure (ι → ℝ))
        (volume : Measure E)),
    Eq (α := ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
          ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s) :
        ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
          (Function.comp (β := ι → ℝ)
              (⇑(Basis.map (Basis.ofZLatticeBasis ℝ L b) (↑f.symm : E ≃ₗ[ℝ] ι → ℝ)).equivFun : (a : ι → ℝ) → ι → ℝ)
              (⇑f.symm : (a : E) → ι → ℝ) ''
            s) :
        ENNReal)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal)
      ((⇑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (a : E) → ι → ℝ) '' s) =
    HDiv.hDiv (α := ENNReal) (((volume : Measure E) : (a : Set E) → ENNReal) s : ENNReal)
      (ENNReal.ofReal (covolume L (volume : Measure E)))

Tactic:
classical
  let e : Fin (finrank ℝ E) ≃ ι :=
    Fintype.equivOfCardEq (by rw [Fintype.card_fin, finrank_eq_card_basis (b.ofZLatticeBasis ℝ)])
  let f := (EuclideanSpace.equiv ι ℝ).symm.trans
    ((stdOrthonormalBasis ℝ E).reindex e).repr.toContinuousLinearEquiv.symm
  have hf : MeasurePreserving f :=
    ((stdOrthonormalBasis ℝ E).reindex e).measurePreserving_repr_symm.comp
      (PiLp.volume_preserving_toLp ι)
  rw [← hf.measure_preimage hs, ← (covolume_comap L volume volume hf),
    ← volume_image_eq_volume_div_covolume (ZLattice.comap ℝ L f.toLinearMap)
    (b.ofZLatticeComap ℝ L f.toLinearEquiv), Basis.ofZLatticeBasis_comap,
    ← f.image_symm_eq_preimage, ← Set.image_comp]
  simp

Premises used: Set.image_comp, Module.Basis.ofZLatticeBasis_comap