awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
x : ι
⊢ Eq (α := ι → ℝ) (((Basis.ofZLatticeBasis ℝ L b : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ) x : ι → ℝ)
    (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L) x : ι → ℝ)

Tactic:
exact b.ofZLatticeBasis_apply ℝ L _

Premises used: Real, Module.Basis.ofZLatticeBasis_apply
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
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)
⊢ Eq (α := ι → ι → ℝ) (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))
    (⇑(Basis.ofZLatticeBasis ℝ L b) : (a : ι) → ι → ℝ)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
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:
simp
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
rw :
  Eq (α := ℝ)
    (|((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            ((↑(Basis.equiv (Basis.ofZLatticeBasis ℝ L b) (Pi.basisFun ℝ ι) (Equiv.refl ι)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
              (ι → ℝ) →ₗ[ℝ] ι → ℝ))⁻¹| :
      ℝ)
    (|((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            ((↑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (ι → ℝ) →ₗ[ℝ] ι → ℝ))⁻¹| :
      ℝ)
⊢ covolume.{u_2} (E := ι → ℝ) L (volume : Measure (ι → ℝ)) =
    |(↑(((LinearEquiv.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]

Premises used: Units.val_inv_eq_inv_val, abs_inv, Module.Basis.det_basis, Module.Basis.det_inv, IsUnit.unit_spec, Pi.basisFun_det_apply, LinearEquiv.coe_det, ZLattice.covolume_eq_det
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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 (α := ℝ)
    (|((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            ((↑(Basis.equiv (Basis.ofZLatticeBasis ℝ L b) (Pi.basisFun ℝ ι) (Equiv.refl ι)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) :
              (ι → ℝ) →ₗ[ℝ] ι → ℝ))⁻¹| :
      ℝ)
    (|((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ)
            ((↑(Basis.equivFun (Basis.ofZLatticeBasis ℝ L b)) : (ι → ℝ) →ₗ[ℝ] ι → ℝ) : (ι → ℝ) →ₗ[ℝ] ι → ℝ))⁻¹| :
      ℝ)

Tactic:
rfl
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
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) :
                ι → ℝ)
              ⋯) :
        ℝ)|
⊢ covolume.{u_2} (E := ι → ℝ) L₁ (volume : Measure (ι → ℝ)) /
      covolume.{u_2} (E := ι → ℝ) L₂ (volume : Measure (ι → ℝ)) =
    (↑(L₁.toAddSubgroup.relIndex L₂.toAddSubgroup) : ℝ)

Tactic:
rw [AddSubgroup.relIndex_eq_natAbs_det L₁.toAddSubgroup L₂.toAddSubgroup h b₁ b₂,
    Nat.cast_natAbs, Int.cast_abs]

Premises used: Int.cast_abs, Nat.cast_natAbs, Submodule.toAddSubgroup, AddSubgroup.relIndex_eq_natAbs_det
-- 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₂
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 : ι) → ι → ℝ)|
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) :
                  ι → ℝ)
                ⋯) :
          ℝ)| :
      ℝ)
⊢ 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) :
                ι → ℝ)
              ⋯) :
        ℝ)|

Tactic:
trans |(b₂.ofZLatticeBasis ℝ).det (b₁.ofZLatticeBasis ℝ)|

Premises used: Real, Module.Basis.ofZLatticeBasis, Module.Basis.det, DFunLike.coe
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
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 : ι) → ι → ℝ))|⁻¹
⊢ 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:
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]

Premises used: Real, Units.val_inv_eq_inv_val, abs_inv, abs_mul, Module.Basis.det_inv, mul_comm, Module.Basis.det_mul_det, Pi.basisFun, IsUnit.unit_spec, Pi.basisFun_det_apply, ZLattice.covolume_eq_det
-- 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₂
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 ι ι ℝ)
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 : ι) → ι → ℝ))|⁻¹

Tactic:
congr 3
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
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 :
        ℝ)
⊢ 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:
ext
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
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 :
        ℝ)
⊢ 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:
ext
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
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:
simp
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
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:
simp
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
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) :
                ι → ℝ)
              ⋯)
          fun (x : ℤ) ↦ (↑x : ℝ))|
⊢ 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) :
                  ι → ℝ)
                ⋯) :
          ℝ)| :
      ℝ)

Tactic:
rw [Basis.det_apply, Basis.det_apply, Int.cast_det]

Premises used: Int.cast_det, Module.Basis.det_apply
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
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) :
            ι → ℝ)
          ⋯)
      fun (x : ℤ) ↦ (↑x : ℝ))
⊢ |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 : ℝ))|

Tactic:
congr
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
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) :
              ι → ℝ)
            ⋯)
        (fun (x : ℤ) ↦ (↑x : ℝ)) i j
⊢ 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 : ℝ))

Tactic:
ext i j
-- 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₂
b₁ : Basis ι ℤ ↥L₁ := IsZLattice.basis L₁
b₂ : Basis ι ℤ ↥L₂ := IsZLattice.basis L₂
i j : ι
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) :
                      ι → ℝ)
                    ⋯) :
                ι →₀ ℤ) :
              (a : ι) → ℤ)
            i) :
        ℝ) :
      ℝ)
⊢ 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

Tactic:
rw [Matrix.map_apply, Basis.toMatrix_apply, Basis.toMatrix_apply, Basis.ofZLatticeBasis_apply]

Premises used: Module.Basis.ofZLatticeBasis_apply, Matrix.map_apply, Module.Basis.toMatrix_apply