awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
h :
  Set.MapsTo (⇑b.equivFun : (a : E) → ι → ℝ) (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ Function.Injective
    (Set.MapsTo.restrict (⇑b.equivFun : (a : E) → ι → ℝ)
      (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) h)

Tactic:
Subtype.map_injective _ (Basis.equivFun b).injective

Premises used: Subtype.map_injective, LinearEquiv.injective, Set.MapsTo.restrict, Module.Basis.equivFun
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
h :
  Set.MapsTo (⇑b.equivFun : (a : E) → ι → ℝ) (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ Function.Injective
    (Set.MapsTo.restrict (⇑b.equivFun : (a : E) → ι → ℝ)
      (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) h)

Tactic:
refine Subtype.map_injective _ (Basis.equivFun b).injective

Premises used: Subtype.map_injective, LinearEquiv.injective, Module.Basis.equivFun
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
⊢ DiscreteTopology.{u_1}
    ↥(toAddSubgroup (module_M := AddCommGroup.toIntModule E)
        (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))

Tactic:
inferInstanceAs <| DiscreteTopology (span ℤ (Set.range b))

Premises used: _private.0.ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite._proof_1
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : ProperSpace E
inst_3 : Finite ι
s : Set E
hs : IsBounded s
⊢ DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))

Tactic:
have : DiscreteTopology (span ℤ (Set.range b)) := inferInstance
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : ProperSpace E
inst_3 : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
⊢ (s ∩ (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)).Finite

Tactic:
Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete hs ?_

Premises used: DiscreteTopology.isDiscrete, Metric.finite_isBounded_inter_isClosed
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : ProperSpace E
inst_3 : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
refine : IsClosed (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
⊢ (s ∩ (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)).Finite

Tactic:
refine Metric.finite_isBounded_inter_isClosed DiscreteTopology.isDiscrete hs ?_

Premises used: DiscreteTopology.isDiscrete, Metric.finite_isBounded_inter_isClosed
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : ProperSpace E
inst_3 : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
⊢ IsClosed
    (↑(toAddSubgroup (module_M := AddCommGroup.toIntModule E)
          (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) :
      Set E)

Tactic:
AddSubgroup.isClosed_of_discrete

Premises used: AddSubgroup.isClosed_of_discrete
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : ProperSpace E
inst_3 : Finite ι
s : Set E
hs : IsBounded s
this : DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
⊢ IsClosed
    (↑(toAddSubgroup (module_M := AddCommGroup.toIntModule E)
          (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) :
      Set E)

Tactic:
exact AddSubgroup.isClosed_of_discrete

Premises used: AddSubgroup.isClosed_of_discrete
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
intro : ∀ (val : Fintype ι), MeasurableSet (fundamentalDomain b)
⊢ MeasurableSet (fundamentalDomain b)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
⊢ FiniteDimensional ℝ E

Tactic:
haveI : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
intro : MeasurableSet.{u_1} (α := E) ((⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D)
rw : fundamentalDomain b = (⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D
⊢ MeasurableSet (fundamentalDomain b)

Tactic:
rw [(_ : fundamentalDomain b = b.equivFun.toLinearMap ⁻¹' D)]
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
⊢ MeasurableSet.{u_1} (α := E) ((⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D)

Tactic:
measurableSet_preimage (LinearMap.continuous_of_finiteDimensional _).measurable ?_

Premises used: LinearMap.continuous_of_finiteDimensional, Continuous.measurable, measurableSet_preimage
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
intro : MeasurableSet D
⊢ MeasurableSet.{u_1} (α := E) ((⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D)

Tactic:
refine measurableSet_preimage (LinearMap.continuous_of_finiteDimensional _).measurable ?_

Premises used: LinearMap.continuous_of_finiteDimensional, Continuous.measurable, measurableSet_preimage
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
⊢ MeasurableSet D

Tactic:
MeasurableSet.pi Set.countable_univ fun _ _ => measurableSet_Ico

Premises used: measurableSet_Ico, Set.countable_univ, MeasurableSet.pi
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
⊢ MeasurableSet D

Tactic:
exact MeasurableSet.pi Set.countable_univ fun _ _ => measurableSet_Ico

Premises used: measurableSet_Ico, Set.countable_univ, MeasurableSet.pi
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
h :
  ∀ (x : E),
    x ∈ fundamentalDomain b ↔ Membership.mem (γ := Set E) ((⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D) x
⊢ fundamentalDomain b = (⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D

Tactic:
ext
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : MeasurableSpace E
inst_3 : OpensMeasurableSpace E
inst_4 : Finite ι
val : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.pi (α := fun (a : ι) ↦ ℝ) Set.univ fun (x : ι) ↦ Set.Ico 0 1
x : E
⊢ x ∈ fundamentalDomain b ↔ Membership.mem (γ := Set E) ((⇑(↑b.equivFun : E →ₗ[ℝ] ι → ℝ) : (a : E) → ι → ℝ) ⁻¹' D) x

Tactic:
simp only [D, fundamentalDomain, Set.mem_Ico, Set.mem_setOf_eq, LinearEquiv.coe_coe,
      Set.mem_preimage, Basis.equivFun_apply, Set.mem_pi, Set.mem_univ, forall_true_left]

Premises used: forall_true_left, Set.mem_Ico, Set.mem_pi, Set.mem_setOf_eq, Module.Basis.equivFun_apply, Set.mem_univ, ZSpan.fundamentalDomain, Set.mem_preimage, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
intro :
  ∀ (val : Fintype ι),
    IsAddFundamentalDomain (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (fundamentalDomain b) μ
⊢ IsAddFundamentalDomain (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (fundamentalDomain b) μ

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
val : Fintype ι
⊢ IsAddFundamentalDomain (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (fundamentalDomain b) μ

Tactic:
IsAddFundamentalDomain.mk' (nullMeasurableSet (fundamentalDomain_measurableSet b))
    fun x => exist_unique_vadd_mem_fundamentalDomain b x

Premises used: ZSpan.fundamentalDomain_measurableSet, Set.Mem, MeasurableSet.nullMeasurableSet, ZSpan.exist_unique_vadd_mem_fundamentalDomain, MeasureTheory.IsAddFundamentalDomain.mk'
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
val : Fintype ι
⊢ IsAddFundamentalDomain (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (fundamentalDomain b) μ

Tactic:
exact IsAddFundamentalDomain.mk' (nullMeasurableSet (fundamentalDomain_measurableSet b))
    fun x => exist_unique_vadd_mem_fundamentalDomain b x

Premises used: ZSpan.fundamentalDomain_measurableSet, MeasurableSet.nullMeasurableSet, ZSpan.exist_unique_vadd_mem_fundamentalDomain, MeasureTheory.IsAddFundamentalDomain.mk'
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
⊢ IsAddFundamentalDomain
    (↥(toAddSubgroup (module_M := AddCommGroup.toIntModule E)
        (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))))
    (fundamentalDomain b) μ

Tactic:
ZSpan.isAddFundamentalDomain b μ

Premises used: Set.Mem, ZSpan.isAddFundamentalDomain, Submodule.span
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
⊢ Ne (α := ENNReal) ((μ : (a : Set E) → ENNReal) (fundamentalDomain b) : ENNReal) (0 : ENNReal)

Tactic:
(ZSpan.isAddFundamentalDomain b μ).measure_ne_zero (NeZero.ne μ)

Premises used: ZSpan.isAddFundamentalDomain, MeasureTheory.IsAddFundamentalDomain.measure_ne_zero, NeZero.ne
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
convert! : VAddInvariantMeasure (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) E μ
⊢ Ne (α := ENNReal) ((μ : (a : Set E) → ENNReal) (fundamentalDomain b) : ENNReal) (0 : ENNReal)

Tactic:
convert! (ZSpan.isAddFundamentalDomain b μ).measure_ne_zero (NeZero.ne μ)
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
⊢ VAddInvariantMeasure (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) E μ

Tactic:
inferInstanceAs <| VAddInvariantMeasure (span ℤ (Set.range b)).toAddSubgroup E μ

Premises used: _private.0.ZSpan.measure_fundamentalDomain_ne_zero._proof_1
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
⊢ VAddInvariantMeasure (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) E μ

Tactic:
exact inferInstanceAs <| VAddInvariantMeasure (span ℤ (Set.range b)).toAddSubgroup E μ
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : DecidableEq ι
inst_4 : MeasurableSpace E
μ : Measure E
inst_5 : BorelSpace E
inst_6 : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
⊢ FiniteDimensional ℝ E

Tactic:
have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : DecidableEq ι
inst_4 : MeasurableSpace E
μ : Measure E
inst_5 : BorelSpace E
inst_6 : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ (μ : (a : Set E) → ENNReal) ((⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) ⁻¹' fundamentalDomain b₀) =
    HMul.hMul (β := ENNReal)
      (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑(b.equiv b₀ (Equiv.refl ι)).symm : E →ₗ[ℝ] E)|)
      ((μ : (a : Set E) → ENNReal) (fundamentalDomain b₀) : ENNReal)

Tactic:
μ.addHaar_preimage_linearEquiv (b.equiv b₀ (Equiv.refl ι)) (fundamentalDomain b₀)

Premises used: Module.Basis.equiv, ZSpan.fundamentalDomain, MeasureTheory.Measure.addHaar_preimage_linearEquiv, Equiv.refl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : DecidableEq ι
inst_4 : MeasurableSpace E
μ : Measure E
inst_5 : BorelSpace E
inst_6 : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
h : fundamentalDomain b = (⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) ⁻¹' fundamentalDomain b₀
h₁ :
  Eq (α := ℝ) ((b₀.det : (a : ι → E) → ℝ) (⇑b : (a : ι) → E) : ℝ)
    ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑(b.equiv b₀ (Equiv.refl ι)).symm : E →ₗ[ℝ] E) : ℝ)
⊢ (μ : (a : Set E) → ENNReal) (fundamentalDomain b) =
    HMul.hMul (β := ENNReal) (ENNReal.ofReal |(b₀.det : (a : ι → E) → ℝ) (⇑b : (a : ι) → E)|)
      ((μ : (a : Set E) → ENNReal) (fundamentalDomain b₀) : ENNReal)

Tactic:
convert! μ.addHaar_preimage_linearEquiv (b.equiv b₀ (Equiv.refl ι)) (fundamentalDomain b₀)

Premises used: Module.Basis.equiv, ZSpan.fundamentalDomain, MeasureTheory.Measure.addHaar_preimage_linearEquiv, Equiv.refl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : DecidableEq ι
inst_4 : MeasurableSpace E
μ : Measure E
inst_5 : BorelSpace E
inst_6 : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
h : (⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) '' fundamentalDomain b = fundamentalDomain b₀
h₁ : fundamentalDomain (b.map (b.equiv b₀ (Equiv.refl ι))) = fundamentalDomain b₀
h₂ : fundamentalDomain (b₀.reindex (Equiv.refl ι).symm) = fundamentalDomain b₀
h₃ : fundamentalDomain (b₀.reindex (Equiv.refl ι)) = fundamentalDomain b₀
h₄ h₅ : fundamentalDomain b₀ = fundamentalDomain b₀
⊢ fundamentalDomain b = (⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) ⁻¹' fundamentalDomain b₀

Tactic:
rw [Set.eq_preimage_iff_image_eq (LinearEquiv.bijective _), map_fundamentalDomain,
      Basis.map_equiv, Equiv.refl_symm, Basis.reindex_refl]

Premises used: LinearEquiv.bijective, Module.Basis.reindex_refl, Module.Basis.map_equiv, Set.eq_preimage_iff_image_eq, Equiv.refl_symm, ZSpan.map_fundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : DecidableEq ι
inst_4 : MeasurableSpace E
μ : Measure E
inst_5 : BorelSpace E
inst_6 : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ Eq (α := ℝ) ((b₀.det : (a : ι → E) → ℝ) (⇑b : (a : ι) → E) : ℝ)
    ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑(b.equiv b₀ (Equiv.refl ι)).symm : E →ₗ[ℝ] E) : ℝ)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : DecidableEq ι
inst_4 : MeasurableSpace E
μ : Measure E
inst_5 : BorelSpace E
inst_6 : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
⊢ μ.real (fundamentalDomain b) =
    HMul.hMul (α := ℝ) (|(b₀.det : (a : ι → E) → ℝ) (⇑b : (a : ι) → E)| : ℝ) (μ.real (fundamentalDomain b₀))

Tactic:
simp [measureReal_def, measure_fundamentalDomain b μ b₀]

Premises used: ZSpan.measure_fundamentalDomain, MeasureTheory.measureReal_def
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
rw :
  ENNReal.ofReal |(Basis.det (Pi.basisFun ℝ ι) : (a : ι → ι → ℝ) → ℝ) (⇑b : (a : ι) → ι → ℝ)| =
    ENNReal.ofReal
      |Matrix.det.{0, u_2} (n := ι)
          (Matrix.transpose ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ) (⇑b : (a : ι) → ι → ℝ)))|
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (fundamentalDomain (ι := ι) (K := ℝ) b) =
    ENNReal.ofReal |Matrix.det.{0, u_2} (n := ι) ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ) (⇑b : (a : ι) → ι → ℝ))|

Tactic:
rw [measure_fundamentalDomain b volume (b₀ := Pi.basisFun ℝ ι), fundamentalDomain_pi_basisFun,
    volume_pi, Measure.pi_pi, Real.volume_Ico, sub_zero, ENNReal.ofReal_one, Finset.prod_const_one,
    mul_one, ← Matrix.det_transpose]

Premises used: MeasureTheory.volume_pi, Real, Matrix.det_transpose, sub_zero, ZSpan.measure_fundamentalDomain, Real.volume_Ico, ENNReal.ofReal_one, Finset.prod_const_one, MeasureTheory.MeasureSpace.volume, ZSpan.fundamentalDomain_pi_basisFun, Pi.basisFun, mul_one, MeasureTheory.Measure.pi_pi
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ ENNReal.ofReal |(Basis.det (Pi.basisFun ℝ ι) : (a : ι → ι → ℝ) → ℝ) (⇑b : (a : ι) → ι → ℝ)| =
    ENNReal.ofReal
      |Matrix.det.{0, u_2} (n := ι)
          (Matrix.transpose ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ) (⇑b : (a : ι) → ι → ℝ)))|

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ Measure.real.{u_2} (α := ι → ℝ) (m := MeasureSpace.toMeasurableSpace) volume (fundamentalDomain (ι := ι) (K := ℝ) b) =
    |Matrix.det.{0, u_2} (n := ι) ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ) (⇑b : (a : ι) → ι → ℝ))|

Tactic:
simp [measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
⊢ FiniteDimensional ℝ E

Tactic:
have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
rw :
  Eq (α := ENNReal)
    ((μ : (a : Set E) → ENNReal) (parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b) :
      ENNReal)
    (0 : ENNReal)
⊢ fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)

Tactic:
rw [← measure_symmDiff_eq_zero_iff, symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)]

Premises used: ZSpan.fundamentalDomain_subset_parallelepiped, symmDiff_of_le, MeasureTheory.measure_symmDiff_eq_zero_iff
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
inst_3 : MeasurableSpace E
μ : Measure E
inst_4 : BorelSpace E
inst_5 : μ.IsAddHaarMeasure
this_1 : FiniteDimensional ℝ E
this :
  parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b ⊆
    ⋃ (i : ι),
      (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
            AffineSubspace ℝ E) :
        Set E)
⊢ Eq (α := ENNReal)
    ((μ : (a : Set E) → ENNReal) (parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b) :
      ENNReal)
    (0 : ENNReal)

Tactic:
measure_mono_null this
      (measure_iUnion_null_iff.mpr fun i ↦ Measure.addHaar_affineSubspace μ _ ?_)

Premises used: Iff.mpr, Real, Set.univ, AffineSubspace.mk', MeasureTheory.measure_iUnion_null_iff, MeasureTheory.measure_mono_null, SDiff.sdiff, MeasureTheory.Measure.addHaar_affineSubspace, Submodule.span, Set.image, Singleton.singleton, DFunLike.coe