-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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₁ L₂ : Submodule ℤ E
inst_5 : DiscreteTopology.{u_2} ↥L₁
inst_6 : IsZLattice ℝ L₁
inst_7 : DiscreteTopology.{u_2} ↥L₂
inst_8 : IsZLattice ℝ L₂
h : L₁ ≤ L₂
f : (Fin (finrank ℝ E) → ℝ) ≃L[ℝ] E :=
  ContinuousLinearEquiv.trans (ContinuousLinearEquiv.symm (EuclideanSpace.equiv (Fin (finrank ℝ E)) ℝ))
    (ContinuousLinearEquiv.symm
      (↑(OrthonormalBasis.repr (stdOrthonormalBasis ℝ E)) : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))))
hf :
  MeasurePreserving (α := Fin (finrank ℝ E) → ℝ) (β := E) (⇑f : (a : Fin (finrank ℝ E) → ℝ) → E) volume
    (volume : Measure E)
rw :
  covolume (ZLattice.comap ℝ L₁ (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E)) volume /
      covolume L₂ (volume : Measure E) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
rw₁ :
  covolume (ZLattice.comap ℝ L₁ (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E)) volume /
      covolume (ZLattice.comap ℝ L₂ (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E))
        volume =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
rw₂ :
  Eq (α := ℝ)
    (↑((ZLattice.comap ℝ L₁
                (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E)).toAddSubgroup.relIndex
          (ZLattice.comap ℝ L₂
              (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E)).toAddSubgroup) :
      ℝ)
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
rw₃ :
  Eq (α := ℝ)
    (↑((AddSubgroup.comap (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E).toAddMonoidHom
              L₁.toAddSubgroup).relIndex
          (ZLattice.comap ℝ L₂
              (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E)).toAddSubgroup) :
      ℝ)
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
rw₄ :
  Eq (α := ℝ)
    (↑((AddSubgroup.comap (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E).toAddMonoidHom
              L₁.toAddSubgroup).relIndex
          (AddSubgroup.comap (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E).toAddMonoidHom
            L₂.toAddSubgroup)) :
      ℝ)
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
rw₅ :
  (AddSubgroup.comap (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E).toAddMonoidHom
          L₁.toAddSubgroup).relIndex
      (AddSubgroup.comap (↑(↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E) : (Fin (finrank ℝ E) → ℝ) →ₗ[ℝ] E).toAddMonoidHom
        L₂.toAddSubgroup) =
    L₁.toAddSubgroup.relIndex L₂.toAddSubgroup
⊢ covolume L₁ (volume : Measure E) / covolume L₂ (volume : Measure E) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
have rw₆ : AddSubgroup.relIndex (G := Fin (finrank ℝ E) → ℝ)
    (AddSubgroup.comap (↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E).toAddEquiv.toAddMonoidHom L₁.toAddSubgroup)
    (AddSubgroup.comap (↑f : (Fin (finrank ℝ E) → ℝ) ≃ₗ[ℝ] E).toAddEquiv.toAddMonoidHom L₂.toAddSubgroup) =
  L₁.toAddSubgroup.relIndex L₂.toAddSubgroup
Tactic: rw [← covolume_comap L₁ volume volume hf, ← covolume_comap L₂ volume volume hf,
    covolume_div_covolume_eq_relIndex _ _ (fun _ h' ↦ h h'), ZLattice.comap_toAddSubgroup,
    ZLattice.comap_toAddSubgroup, Nat.cast_inj, LinearEquiv.toAddMonoidHom_commutes,
    AddSubgroup.comap_equiv_eq_map_symm', AddSubgroup.comap_equiv_eq_map_symm',
    AddSubgroup.relIndex_map_map_of_injective _ _ f.symm.injective]