-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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 : ι) → ι → ℝ)|
let₆ 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) :
                  ι → ℝ)
                ⋯) :
          ℝ)| :
      ℝ)
⊢ covolume.{u_2} (E := ι → ℝ) L₁ (volume : Measure (ι → ℝ)) /
      covolume.{u_2} (E := ι → ℝ) L₂ (volume : Measure (ι → ℝ)) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)

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)

Premises used: Int.cast_abs, Module.Basis.ofZLatticeBasis_apply, Units.val_inv_eq_inv_val, abs_inv, abs_mul, Matrix.map_apply, Nat.cast_natAbs, Int.cast_det, Module.Basis.toMatrix_apply, Module.Basis.det_inv, mul_comm, IsUnit.unit_spec, Module.Basis.det_apply, Pi.basisFun_det_apply