-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
ι : Type u_2
inst : Fintype ι
L₁ L₂ : Submodule ℤ (ι → ℝ)
inst_1 : DiscreteTopology.{u_2} ↥L₁
inst_2 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L₁
inst_3 : DiscreteTopology.{u_2} ↥L₂
inst_4 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L₂
h : L₁ ≤ L₂
let let₁ let₂ let₃ :
  covolume.{u_2} (E := ι → ℝ) L₁ (volume : Measure (ι → ℝ)) /
      covolume.{u_2} (E := ι → ℝ) L₂ (volume : Measure (ι → ℝ)) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
let₄ :
  let b₁ := IsZLattice.basis L₁;
  let b₂ := IsZLattice.basis L₂;
  covolume.{u_2} (E := ι → ℝ) L₁ (volume : Measure (ι → ℝ)) /
      covolume.{u_2} (E := ι → ℝ) L₂ (volume : Measure (ι → ℝ)) =
    |(↑((b₂.det :
              (a :
                  ι →
                    ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ))
                        L₂.toAddSubgroup)) →
                ℤ)
            fun (i : ι) ↦
            Subtype.mk (p := fun (x : ι → ℝ) ↦
              Membership.mem (γ := Submodule ℤ (ι → ℝ))
                ((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ)) L₂.toAddSubgroup :
                  Submodule ℤ (ι → ℝ))
                x)
              (↑((b₁ :
                      (a : ι) →
                        ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ))
                            L₁.toAddSubgroup))
                    i) :
                ι → ℝ)
              ⋯) :
        ℝ)|
let₅ :
  let b₁ := IsZLattice.basis L₁;
  let b₂ := IsZLattice.basis L₂;
  covolume.{u_2} (E := ι → ℝ) L₁ (volume : Measure (ι → ℝ)) /
      covolume.{u_2} (E := ι → ℝ) L₂ (volume : Measure (ι → ℝ)) =
    |((Basis.det (Basis.ofZLatticeBasis ℝ L₂ b₂) : (ι → ℝ) [⋀^ι]→ₗ[ℝ] ℝ) : (a : ι → ι → ℝ) → ℝ)
        (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁) : (a : ι) → ι → ℝ)|
⊢ covolume.{u_2} (E := ι → ℝ) L₁ (volume : Measure (ι → ℝ)) /
      covolume.{u_2} (E := ι → ℝ) L₂ (volume : Measure (ι → ℝ)) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
have let₆ : let b₁ := IsZLattice.basis L₁;
let b₂ := IsZLattice.basis L₂;
Eq (α := ℝ)
  (|((Basis.det (Basis.ofZLatticeBasis ℝ L₂ b₂) : (ι → ℝ) [⋀^ι]→ₗ[ℝ] ℝ) : (a : ι → ι → ℝ) → ℝ)
        (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁) : (a : ι) → ι → ℝ)| :
    ℝ)
  (|(↑((b₂.det :
              (a :
                  ι →
                    ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ))
                        L₂.toAddSubgroup)) →
                ℤ)
            fun (i : ι) ↦
            Subtype.mk (p := fun (x : ι → ℝ) ↦
              Membership.mem (γ := Submodule ℤ (ι → ℝ))
                ((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ)) L₂.toAddSubgroup :
                  Submodule ℤ (ι → ℝ))
                x)
              (↑((b₁ :
                      (a : ι) →
                        ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ))
                            L₁.toAddSubgroup))
                    i) :
                ι → ℝ)
              sorry) :
        ℝ)| :
    ℝ)
Tactic: classical
  let b₁ := IsZLattice.basis L₁
  let b₂ := IsZLattice.basis L₂
  rw [AddSubgroup.relIndex_eq_natAbs_det L₁.toAddSubgroup L₂.toAddSubgroup h b₁ b₂,
    Nat.cast_natAbs, Int.cast_abs]
  trans |(b₂.ofZLatticeBasis ℝ).det (b₁.ofZLatticeBasis ℝ)|
  · rw [← Basis.det_mul_det _ (Pi.basisFun ℝ ι) _, abs_mul, Pi.basisFun_det_apply,
      ← Basis.det_inv, Units.val_inv_eq_inv_val, IsUnit.unit_spec, Pi.basisFun_det_apply,
      covolume_eq_det _ b₁, covolume_eq_det _ b₂, mul_comm, abs_inv]
    congr 3 <;> ext <;> simp
  · rw [Basis.det_apply, Basis.det_apply, Int.cast_det]
    congr; ext i j
    rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.toMatrix_apply, Basis.ofZLatticeBasis_apply]
    exact (b₂.ofZLatticeBasis_repr_apply ℝ L₂ ⟨b₁ j, h (coe_mem _)⟩ i)