awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free.{0, u_1} ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
h : Set.range f ≤ f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)
⊢ Set.range f = f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)

Tactic:
refine le_antisymm ?_ (Set.image_subset_range _ _)

Premises used: Set.image_subset_range, le_antisymm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free.{0, u_1} ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
x : E
x' : ↥L :=
  (b.repr.symm : (a : Free.ChooseBasisIndex ℤ ↥L →₀ ℤ) → ↥L)
    ((Equiv.symm Finsupp.equivFunOnFinite : (a : Free.ChooseBasisIndex ℤ ↥L → ℤ) → Free.ChooseBasisIndex ℤ ↥L →₀ ℤ)
      fun (i : Free.ChooseBasisIndex ℤ ↥L) ↦
      Int.floor (α := ℝ)
        ((((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : (a : E) → Free.ChooseBasisIndex ℤ ↥L →₀ ℝ) x :
                Free.ChooseBasisIndex ℤ ↥L →₀ ℝ) :
              (a : Free.ChooseBasisIndex ℤ ↥L) → ℝ)
            i :
          ℝ))
⊢ f x ∈ f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)

Tactic:
⟨x + (- x'), ?_, hf' _ _ (- x').2⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, And.intro, Exists.intro, Set.image, Subtype.val, Neg.neg, Subtype.property
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free.{0, u_1} ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
x : E
x' : ↥L :=
  (b.repr.symm : (a : Free.ChooseBasisIndex ℤ ↥L →₀ ℤ) → ↥L)
    ((Equiv.symm Finsupp.equivFunOnFinite : (a : Free.ChooseBasisIndex ℤ ↥L → ℤ) → Free.ChooseBasisIndex ℤ ↥L →₀ ℤ)
      fun (i : Free.ChooseBasisIndex ℤ ↥L) ↦
      Int.floor (α := ℝ)
        ((((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : (a : E) → Free.ChooseBasisIndex ℤ ↥L →₀ ℝ) x :
                Free.ChooseBasisIndex ℤ ↥L →₀ ℝ) :
              (a : Free.ChooseBasisIndex ℤ ↥L) → ℝ)
            i :
          ℝ))
h : x + -(↑x' : E) ∈ (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)
⊢ f x ∈ f '' (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)

Tactic:
refine ⟨x + (- x'), ?_, hf' _ _ (- x').2⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : TopologicalSpace F
L : Submodule ℤ E
inst_4 : DiscreteTopology.{u_1} ↥L
inst_5 : IsZLattice ℝ L
f : E → F
hf : Continuous f
hf' : ∀ (z w : E), w ∈ L → f (z + w) = f z
this : Free.{0, u_1} ℤ ↥L
b : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
x : E
x' : ↥L :=
  (b.repr.symm : (a : Free.ChooseBasisIndex ℤ ↥L →₀ ℤ) → ↥L)
    ((Equiv.symm Finsupp.equivFunOnFinite : (a : Free.ChooseBasisIndex ℤ ↥L → ℤ) → Free.ChooseBasisIndex ℤ ↥L →₀ ℤ)
      fun (i : Free.ChooseBasisIndex ℤ ↥L) ↦
      Int.floor (α := ℝ)
        ((((Basis.repr (Basis.ofZLatticeBasis ℝ L b) : (a : E) → Free.ChooseBasisIndex ℤ ↥L →₀ ℝ) x :
                Free.ChooseBasisIndex ℤ ↥L →₀ ℝ) :
              (a : Free.ChooseBasisIndex ℤ ↥L) → ℝ)
            i :
          ℝ))
⊢ x + -(↑x' : E) ∈ (↑(Basis.parallelepiped (Basis.ofZLatticeBasis ℝ L b)) : Set E)

Tactic:
simp [parallelepiped_basis_eq, x', Int.floor_le, Int.lt_floor_add_one, le_of_lt, add_comm (1 : ℝ)]

Premises used: le_of_lt, Int.lt_floor_add_one, add_comm, parallelepiped_basis_eq, Int.floor_le, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
⊢ MeasurableVAdd (↥L) E

Tactic:
have : MeasurableVAdd L E := (inferInstance : MeasurableVAdd L.toAddSubgroup E)
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
this : MeasurableVAdd (↥L) E
⊢ VAddInvariantMeasure (↥L) E μ

Tactic:
have : VAddInvariantMeasure L E μ := (inferInstance : VAddInvariantMeasure L.toAddSubgroup E μ)
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
this_1 : MeasurableVAdd (↥L) E
this : VAddInvariantMeasure (↥L) E μ
⊢ covolume L μ = μ.real F

Tactic:
congr_arg ENNReal.toReal (h.covolume_eq_volume μ)

Premises used: MeasureTheory.Measure.real, congr_arg, ENNReal.toReal, MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume, ZLattice.covolume
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
F : Set E
h : IsAddFundamentalDomain (↥L) F μ
this_1 : MeasurableVAdd (↥L) E
this : VAddInvariantMeasure (↥L) E μ
⊢ covolume L μ = μ.real F

Tactic:
exact congr_arg ENNReal.toReal (h.covolume_eq_volume μ)

Premises used: congr_arg, ENNReal.toReal, MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
rw :
  Ne (α := ENNReal)
    ((μ : (a : Set E) → ENNReal)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L) (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) :
      ENNReal)
    (0 : ENNReal)
rw₁ :
  LT.lt (α := ENNReal)
    ((μ : (a : Set E) → ENNReal)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L) (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) :
      ENNReal)
    (⊤ : ENNReal)
⊢ covolume L μ ≠ 0

Tactic:
rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain (Free.chooseBasis ℤ L) μ),
    measureReal_ne_zero_iff (ne_of_lt _)]

Premises used: MeasureTheory.measureReal_ne_zero_iff, Membership.mem, Subtype, Int, ZLattice.covolume_eq_measure_fundamentalDomain, ZLattice.isAddFundamentalDomain, ne_of_lt, Module.Free.chooseBasis
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
⊢ Ne (α := ENNReal)
    ((μ : (a : Set E) → ENNReal)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L) (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) :
      ENNReal)
    (0 : ENNReal)

Tactic:
measure_fundamentalDomain_ne_zero _

Premises used: ZSpan.measure_fundamentalDomain_ne_zero
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
⊢ Ne (α := ENNReal)
    ((μ : (a : Set E) → ENNReal)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L) (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) :
      ENNReal)
    (0 : ENNReal)

Tactic:
exact measure_fundamentalDomain_ne_zero _

Premises used: ZSpan.measure_fundamentalDomain_ne_zero
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
⊢ LT.lt (α := ENNReal)
    ((μ : (a : Set E) → ENNReal)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L) (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) :
      ENNReal)
    (⊤ : ENNReal)

Tactic:
Bornology.IsBounded.measure_lt_top (fundamentalDomain_isBounded _)

Premises used: Bornology.IsBounded.measure_lt_top, ZSpan.fundamentalDomain_isBounded
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
⊢ LT.lt (α := ENNReal)
    ((μ : (a : Set E) → ENNReal)
        (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L) (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L))) :
      ENNReal)
    (⊤ : ENNReal)

Tactic:
exact Bornology.IsBounded.measure_lt_top (fundamentalDomain_isBounded _)

Premises used: Bornology.IsBounded.measure_lt_top, ZSpan.fundamentalDomain_isBounded
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
⊢ 0 < covolume L μ

Tactic:
lt_of_le_of_ne ENNReal.toReal_nonneg (covolume_ne_zero L μ).symm

Premises used: ENNReal.toReal_nonneg, Ne.symm, ZLattice.covolume_ne_zero, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
F : Type u_2
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℝ F
inst_10 : FiniteDimensional ℝ F
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
ν : Measure F
inst_13 : ν.IsAddHaarMeasure
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e : (a : F) → E) ν μ
rw :
  ν.real
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L)
        (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
          (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)))) =
    ν.real
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L)
        (Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F)))
⊢ covolume (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E)) ν = covolume L μ

Tactic:
rw [covolume_eq_measure_fundamentalDomain _ _ (isAddFundamentalDomain (Free.chooseBasis ℤ L) μ),
    covolume_eq_measure_fundamentalDomain _ _ ((isAddFundamentalDomain
    ((Free.chooseBasis ℤ L).ofZLatticeComap ℝ L e.toLinearEquiv) ν)), ← he.measureReal_preimage
    (fundamentalDomain_measurableSet _).nullMeasurableSet, ← e.image_symm_eq_preimage,
    ← e.symm.coe_toLinearEquiv, map_fundamentalDomain]

Premises used: MeasureTheory.MeasurePreserving.measureReal_preimage, ZSpan.fundamentalDomain_measurableSet, ContinuousLinearEquiv.symm, Real, ContinuousLinearEquiv.toLinearEquiv, MeasurableSet.nullMeasurableSet, Membership.mem, Subtype, Int, ContinuousLinearEquiv.coe_toLinearEquiv, ZLattice.covolume_eq_measure_fundamentalDomain, ContinuousLinearEquiv.image_symm_eq_preimage, Module.Basis.ofZLatticeComap, ZLattice.isAddFundamentalDomain, ZSpan.map_fundamentalDomain, Module.Free.chooseBasis
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
F : Type u_2
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℝ F
inst_10 : FiniteDimensional ℝ F
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
ν : Measure F
inst_13 : ν.IsAddHaarMeasure
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e : (a : F) → E) ν μ
h :
  Eq (α := Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ ↥L) ℝ F)
    (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
      (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)))
    (Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F))
⊢ ν.real
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L)
        (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
          (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)))) =
    ν.real
      (fundamentalDomain (ι := Free.ChooseBasisIndex ℤ ↥L)
        (Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F)))

Tactic:
congr!
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
F : Type u_2
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℝ F
inst_10 : FiniteDimensional ℝ F
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
ν : Measure F
inst_13 : ν.IsAddHaarMeasure
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e : (a : F) → E) ν μ
h :
  ∀ (i : Free.ChooseBasisIndex ℤ ↥L),
    Eq.{u_2 + 1} (α := F)
      ((Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
              (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)) :
            (a : Free.ChooseBasisIndex ℤ ↥L) → F)
          i :
        F)
      ((Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F) :
            (a : Free.ChooseBasisIndex ℤ ↥L) → F)
          i :
        F)
⊢ Eq (α := Basis.{u_1, 0, u_2} (Free.ChooseBasisIndex ℤ ↥L) ℝ F)
    (Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
      (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)))
    (Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
F : Type u_2
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace ℝ F
inst_10 : FiniteDimensional ℝ F
inst_11 : MeasurableSpace F
inst_12 : BorelSpace F
ν : Measure F
inst_13 : ν.IsAddHaarMeasure
e : F ≃L[ℝ] E
he : MeasurePreserving (⇑e : (a : F) → E) ν μ
i : Free.ChooseBasisIndex ℤ ↥L
⊢ Eq.{u_2 + 1} (α := F)
    ((Basis.ofZLatticeBasis ℝ (ZLattice.comap ℝ L (↑(↑e : F ≃ₗ[ℝ] E) : F →ₗ[ℝ] E))
            (Basis.ofZLatticeComap ℝ L (↑e : F ≃ₗ[ℝ] E) (Free.chooseBasis ℤ ↥L)) :
          (a : Free.ChooseBasisIndex ℤ ↥L) → F)
        i :
      F)
    ((Basis.map (Basis.ofZLatticeBasis ℝ L (Free.chooseBasis ℤ ↥L)) (↑e.symm : E ≃ₗ[ℝ] F) :
          (a : Free.ChooseBasisIndex ℤ ↥L) → F)
        i :
      F)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
rw :
  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)))
⊢ covolume L μ =
    HMul.hMul (α := ℝ)
      (|(b₀.det : (a : ι → E) → ℝ)
            (Function.comp (β := ↥L) (Subtype.val (p := fun (x : E) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))| :
        ℝ)
      (μ.real (fundamentalDomain b₀))

Tactic:
rw [covolume_eq_measure_fundamentalDomain L μ (isAddFundamentalDomain b μ),
    measureReal_fundamentalDomain _ _ b₀,
    measureReal_congr (fundamentalDomain_ae_parallelepiped b₀ μ)]

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

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

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
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:
b.ofZLatticeBasis_apply ℝ L _

Premises used: Real, Module.Basis.ofZLatticeBasis_apply
-- Module: Mathlib.Algebra.Module.ZLattice.Covolume
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
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:
exact b.ofZLatticeBasis_apply ℝ L _

Premises used: Real, Module.Basis.ofZLatticeBasis_apply
-- 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
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)))|
⊢ 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)))|

Tactic:
rw [covolume_eq_measure_fundamentalDomain L volume (isAddFundamentalDomain b volume),
    volume_real_fundamentalDomain]

Premises used: ZSpan.volume_real_fundamentalDomain, ZLattice.covolume_eq_measure_fundamentalDomain, MeasureTheory.MeasureSpace.volume, ZLattice.isAddFundamentalDomain
-- 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
e_a :
  Eq (α := ι → ι → ℝ) (⇑(Basis.ofZLatticeBasis ℝ L b : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ)
    (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥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)))|

Tactic:
congr
-- 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
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 : ι → ℝ)
⊢ Eq (α := ι → ι → ℝ) (⇑(Basis.ofZLatticeBasis ℝ L b : Basis ι ℝ (ι → ℝ)) : (a : ι) → ι → ℝ)
    (Function.comp (β := ↥L) (Subtype.val (p := fun (x : ι → ℝ) ↦ x ∈ L)) (⇑b : (a : ι) → ↥L))

Tactic:
ext1
-- 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:
b.ofZLatticeBasis_apply ℝ L _

Premises used: Real, Module.Basis.ofZLatticeBasis_apply