awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
⊢ Eq (α := Matrix ι ι ℝ)
    (Basis.toMatrix (M := ι → ℝ) (Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ))
      (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁) : (a : ι) → ι → ℝ))
    (Matrix.map
      (b₂.toMatrix 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) :
            ι → ℝ)
          ⋯)
      fun (x : ℤ) ↦ (↑x : ℝ))
have e_a : ∀ (i j : ι),
  Basis.toMatrix (M := ι → ℝ) (Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ))
      (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁) : (a : ι) → ι → ℝ) i j =
    Matrix.map
      (b₂.toMatrix 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)
      (fun (x : ℤ) ↦ (↑x : ℝ)) i j
Tactic: ext i j
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
i j : ι
⊢ Basis.toMatrix (M := ι → ℝ) (Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ))
      (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁) : (a : ι) → ι → ℝ) i j =
    Matrix.map
      (b₂.toMatrix 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) :
            ι → ℝ)
          ⋯)
      (fun (x : ℤ) ↦ (↑x : ℝ)) i j
have e_a : Eq (α := ℝ)
  (((((Basis.repr (Basis.ofZLatticeBasis ℝ L₂ b₂) : (ι → ℝ) ≃ₗ[ℝ] ι →₀ ℝ) : (a : ι → ℝ) → ι →₀ ℝ)
            (↑((b₁ : (a : ι) → ↥L₁) j) : ι → ℝ) :
          ι →₀ ℝ) :
        (a : ι) → ℝ)
      i :
    ℝ)
  ((↑((((b₂.repr :
                  (a :
                      ↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℝ)) → Submodule ℤ (ι → ℝ))
                          L₂.toAddSubgroup)) →
                    ι →₀ ℤ)
                (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))
                        j) :
                    ι → ℝ)
                  sorry) :
              ι →₀ ℤ) :
            (a : ι) → ℤ)
          i) :
      ℝ) :
    ℝ)
Tactic: rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.toMatrix_apply, Basis.ofZLatticeBasis_apply]
-- 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) : ℝ)
⊢ 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₂;
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) :
              ι → ℝ)
            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)
-- 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) :
                ι → ℝ)
              ⋯) :
        ℝ)|
⊢ 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₂;
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 : ι) → ι → ℝ)|
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)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (hypothesis)
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))))
⊢ covolume L₁ (volume : Measure E) / covolume L₂ (volume : Measure E) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
have hf : MeasurePreserving (α := Fin (finrank ℝ E) → ℝ) (β := E) (⇑f : (a : Fin (finrank ℝ E) → ℝ) → E) volume
  (volume : Measure E)
Tactic: have hf : MeasurePreserving f := (stdOrthonormalBasis ℝ E).measurePreserving_repr_symm.comp
    (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm
-- 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)
⊢ covolume L₁ (volume : Measure E) / covolume L₂ (volume : Measure E) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
have 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) : ℝ)
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]
-- 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) : ℝ)
⊢ covolume L₁ (volume : Measure E) / covolume L₂ (volume : Measure E) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
have 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) : ℝ)
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]
-- 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) : ℝ)
⊢ covolume L₁ (volume : Measure E) / covolume L₂ (volume : Measure E) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
have 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) : ℝ)
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]
-- 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) : ℝ)
⊢ covolume L₁ (volume : Measure E) / covolume L₂ (volume : Measure E) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
have 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) : ℝ)
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]
-- 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) : ℝ)
⊢ covolume L₁ (volume : Measure E) / covolume L₂ (volume : Measure E) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
have 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) : ℝ)
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
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 (ι → ℝ)
⊢ ((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 (ι → ℝ))))
have 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 (ι → ℝ))))
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]