awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
ι : Type u_2
inst_8 : Fintype ι
inst_9 : DecidableEq ι
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ HMul.hMul (α := ℝ) (|(b₀.det : (a : ι → E) → ℝ) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E)| : ℝ)
      (μ.real (parallelepiped.{u_2, u_1} (ι := ι) (⇑b₀ : (a : ι) → E))) =
    HMul.hMul (α := ℝ)
      (|(b₀.det : (a : ι → E) → ℝ)
            (Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))| :
        ℝ)
      (μ.real (parallelepiped.{u_2, u_1} (ι := ι) (⇑b₀ : (a : ι) → E)))
have e_a : Eq (α := ι → E) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E)
  (Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
L : Submodule ℤ E
inst_5 : DiscreteTopology.{u_1} ↥L
inst_6 : IsZLattice ℝ L
μ : Measure E
inst_7 : μ.IsAddHaarMeasure
ι : Type u_2
inst_8 : Fintype ι
inst_9 : DecidableEq ι
b : Basis.{u_2, 0, u_1} ι ℤ ↥L
b₀ : Basis ι ℝ E
⊢ Eq (α := ι → E) (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → E)
    (Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))
have e_a : ∀ (x : ι),
  Eq.{u_1 + 1} (α := E) ((Basis.ofZLatticeBasis ℝ L b : (a : ι) → E) x : E)
    (Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst_2 : DiscreteTopology.{u_2} ↥L
inst_3 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L
b : Basis ι ℤ ↥L
⊢ covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    |Matrix.det.{0, u_2} (n := ι)
        ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
          (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L)))|
have rw : Eq (α := ℝ)
  |Matrix.det.{0, u_2} (n := ι)
      ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (⇑(Basis.ofZLatticeBasis ℝ L b : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ))|
  |Matrix.det.{0, u_2} (n := ι)
      ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L)))|
Tactic: rw [covolume_eq_measure_fundamentalDomain L volume (isAddFundamentalDomain b volume),
    volume_real_fundamentalDomain]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst_2 : DiscreteTopology.{u_2} ↥L
inst_3 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L
b : Basis ι ℤ ↥L
⊢ Eq (α := ℝ)
    |Matrix.det.{0, u_2} (n := ι)
        ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
          (⇑(Basis.ofZLatticeBasis ℝ L b : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ))|
    |Matrix.det.{0, u_2} (n := ι)
        ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
          (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L)))|
have e_a : Eq (α := ι → ι → ℝ) (⇑(Basis.ofZLatticeBasis ℝ L b : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ)
  (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Covolume (goal)
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst_2 : DiscreteTopology.{u_2} ↥L
inst_3 : IsZLattice.{0, u_2} ℝ (E := ι → ℝ) L
b : Basis ι ℤ ↥L
⊢ Eq (α := ι → ι → ℝ) (⇑(Basis.ofZLatticeBasis ℝ L b : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ)
    (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))
have e_a : ∀ (x : ι),
  Eq (α := ι → ℝ) (((Basis.ofZLatticeBasis ℝ L b : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ) x : ι → ℝ)
    (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L) x : ι → ℝ)
Tactic: ext1
-- 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
⊢ Eq (α := ι → ι → ℝ) (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))
    (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → ι → ℝ)
have h : ∀ (x x_1 : ι),
  Eq (α := ℝ) (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L) x x_1)
    ((Basis.ofZLatticeBasis ℝ L b : (a : ι) → ι → ℝ) x x_1)
Tactic: ext
-- 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
⊢ covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    |(↑(((LinearEquiv.det : ((ι → ℝ) ≃ₗ[ℝ] ι → ℝ) →* ℝˣ) : (a : (ι → ℝ) ≃ₗ[ℝ] ι → ℝ) → ℝˣ)
              (Basis.equivFun (Basis.ofZLatticeBasis ℝ L b))) :
          ℝ)|⁻¹
have rw : Eq (α := ℝ)
  (|((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
          ((↑(Basis.equiv (Basis.ofZLatticeBasis ℝ L b) (Pi.basisFun ℝ ι) (Equiv.refl ι)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
            (ι → ℝ) →ₗ[ℝ] ι → ℝ))⁻¹| :
    ℝ)
  (|((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
          ((↑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (ι → ℝ) →ₗ[ℝ] ι → ℝ))⁻¹| :
    ℝ)
Tactic: rw [covolume_eq_det L b, ← Pi.basisFun_det_apply, show (((↑) : L → _) ∘ ⇑b) =
    (b.ofZLatticeBasis ℝ) by ext; simp, ← Basis.det_inv, ← abs_inv, Units.val_inv_eq_inv_val,
    IsUnit.unit_spec, ← Basis.det_basis, LinearEquiv.coe_det]
-- 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₂
⊢ covolume.{u_2} (E := ι → ℝ) L₁ (volume : Measure (ι → ℝ)) /
      covolume.{u_2} (E := ι → ℝ) L₂ (volume : Measure (ι → ℝ)) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)
have rw : 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: rw [AddSubgroup.relIndex_eq_natAbs_det L₁.toAddSubgroup L₂.toAddSubgroup h b₁ b₂,
    Nat.cast_natAbs, Int.cast_abs]
-- 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₂
⊢ 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) :
                ι → ℝ)
              ⋯) :
        ℝ)|
have trans : 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: trans |(b₂.ofZLatticeBasis ℝ).det (b₁.ofZLatticeBasis ℝ)|
-- 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₂
trans :
  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 (ι → ℝ)) =
    |(↑((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) :
                ι → ℝ)
              ⋯) :
        ℝ)|
have trans₁ : 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: trans |(b₂.ofZLatticeBasis ℝ).det (b₁.ofZLatticeBasis ℝ)|
-- 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₂
⊢ 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 : ι) → ι → ℝ)|
have rw : HDiv.hDiv (α := ℝ)
    |Matrix.det.{0, u_2} (n := ι)
        ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
          (Function.comp (β := ↥L₁) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₁)) (⇑b₁ : (a : ι) → ↥L₁)))|
    |Matrix.det.{0, u_2} (n := ι)
        ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
          (Function.comp (β := ↥L₂) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₂)) (⇑b₂ : (a : ι) → ↥L₂)))| =
  HMul.hMul (α := ℝ)
    |Matrix.det.{0, u_2} (n := ι)
        ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
          (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ))|
    |Matrix.det.{0, u_2} (n := ι)
          ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
            (⇑(Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ))|⁻¹
Tactic: 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]
-- 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₂
⊢ HDiv.hDiv (α := ℝ)
      |Matrix.det.{0, u_2} (n := ι)
          ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
            (Function.comp (β := ↥L₁) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₁)) (⇑b₁ : (a : ι) → ↥L₁)))|
      |Matrix.det.{0, u_2} (n := ι)
          ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
            (Function.comp (β := ↥L₂) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₂)) (⇑b₂ : (a : ι) → ↥L₂)))| =
    HMul.hMul (α := ℝ)
      |Matrix.det.{0, u_2} (n := ι)
          ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
            (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ))|
      |Matrix.det.{0, u_2} (n := ι)
            ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
              (⇑(Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ))|⁻¹
have e_a : Eq (α := Matrix ι ι ℝ)
  ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
      (Function.comp (β := ↥L₁) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₁)) (⇑b₁ : (a : ι) → ↥L₁)) :
    Matrix ι ι ℝ)
  ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
      (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ) :
    Matrix ι ι ℝ)
Tactic: congr 3
-- 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₂
e_a :
  Eq (α := Matrix ι ι ℝ)
    ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (Function.comp (β := ↥L₁) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₁)) (⇑b₁ : (a : ι) → ↥L₁)) :
      Matrix ι ι ℝ)
    ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ) :
      Matrix ι ι ℝ)
⊢ HDiv.hDiv (α := ℝ)
      |Matrix.det.{0, u_2} (n := ι)
          ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
            (Function.comp (β := ↥L₁) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₁)) (⇑b₁ : (a : ι) → ↥L₁)))|
      |Matrix.det.{0, u_2} (n := ι)
          ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
            (Function.comp (β := ↥L₂) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₂)) (⇑b₂ : (a : ι) → ↥L₂)))| =
    HMul.hMul (α := ℝ)
      |Matrix.det.{0, u_2} (n := ι)
          ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
            (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ))|
      |Matrix.det.{0, u_2} (n := ι)
            ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
              (⇑(Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ))|⁻¹
have e_a₁ : Eq (α := Matrix ι ι ℝ)
  ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
      (Function.comp (β := ↥L₂) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₂)) (⇑b₂ : (a : ι) → ↥L₂)) :
    Matrix ι ι ℝ)
  ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
      (⇑(Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ) :
    Matrix ι ι ℝ)
Tactic: congr 3
-- 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 ι ι ℝ)
    ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (Function.comp (β := ↥L₁) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₁)) (⇑b₁ : (a : ι) → ↥L₁)) :
      Matrix ι ι ℝ)
    ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ) :
      Matrix ι ι ℝ)
have e_a : ∀ (i j : ι),
  Eq (α := ℝ)
    ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (Function.comp (β := ↥L₁) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₁)) (⇑b₁ : (a : ι) → ↥L₁)) i j :
      ℝ)
    ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ) i j :
      ℝ)
Tactic: ext
-- 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 ι ι ℝ)
    ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (Function.comp (β := ↥L₂) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₂)) (⇑b₂ : (a : ι) → ↥L₂)) :
      Matrix ι ι ℝ)
    ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (⇑(Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ) :
      Matrix ι ι ℝ)
have e_a : ∀ (i j : ι),
  Eq (α := ℝ)
    ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (Function.comp (β := ↥L₂) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L₂)) (⇑b₂ : (a : ι) → ↥L₂)) i j :
      ℝ)
    ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ)
        (⇑(Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ) i j :
      ℝ)
Tactic: ext
-- 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 (α := ℝ)
    (|((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) :
                  ι → ℝ)
                ⋯) :
          ℝ)| :
      ℝ)
have rw : |Matrix.det.{0, u_2} (n := ι)
      (Basis.toMatrix (M := ι → ℝ) (Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ))
        (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁) : (a : ι) → ι → ℝ))| =
  |Matrix.det
      (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 : ℝ))|
Tactic: rw [Basis.det_apply, Basis.det_apply, Int.cast_det]
-- 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₂
⊢ |Matrix.det.{0, u_2} (n := ι)
        (Basis.toMatrix (M := ι → ℝ) (Basis.ofZLatticeBasis ℝ L₂ b₂ : Basis ι ℝ (ι → ℝ))
          (⇑(Basis.ofZLatticeBasis ℝ L₁ b₁) : (a : ι) → ι → ℝ))| =
    |Matrix.det
        (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 : 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) :
          ι → ℝ)
        sorry)
    fun (x : ℤ) ↦ (↑x : ℝ))
Tactic: congr