-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem fundamentalDomain_measurableSet [MeasurableSpace E] [OpensMeasurableSpace E] [Finite ι] :
    MeasurableSet (fundamentalDomain b)

Proof state:
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
⊢ MeasurableSet (fundamentalDomain b)

Tactic:
cases nonempty_fintype ι

Result:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
⊢ MeasurableSet (fundamentalDomain b)

Proof state:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
⊢ MeasurableSet (fundamentalDomain b)

Tactic:
let D : Set (ι → ℝ) := Set.pi Set.univ fun _ : ι => Set.Ico (0 : ℝ) 1

Result:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x => Set.Ico 0 1
⊢ MeasurableSet (fundamentalDomain b)

Proof state:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x => Set.Ico 0 1
⊢ MeasurableSet (fundamentalDomain b)

Tactic:
rw [(_ : fundamentalDomain b = b.equivFun.toLinearMap ⁻¹' D)]

Result:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x => Set.Ico 0 1
⊢ MeasurableSet (⇑↑b.equivFun ⁻¹' D)

E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x => Set.Ico 0 1
⊢ fundamentalDomain b = ⇑↑b.equivFun ⁻¹' D

Proof state:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
⊢ MeasurableSet (fundamentalDomain b)

Tactic:
haveI : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b

Result:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
⊢ MeasurableSet (fundamentalDomain b)

Proof state:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x => Set.Ico 0 1
⊢ MeasurableSet (⇑↑b.equivFun ⁻¹' D)

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

Result:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x => Set.Ico 0 1
⊢ MeasurableSet D

Proof state:
case h
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x => Set.Ico 0 1
x✝ : E
⊢ x✝ ∈ fundamentalDomain b ↔ x✝ ∈ ⇑↑b.equivFun ⁻¹' D

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]

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x => Set.Ico 0 1
⊢ fundamentalDomain b = ⇑↑b.equivFun ⁻¹' D

Tactic:
ext

Result:
case h
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x => Set.Ico 0 1
x✝ : E
⊢ x✝ ∈ fundamentalDomain b ↔ x✝ ∈ ⇑↑b.equivFun ⁻¹' D

Proof state:
case intro
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
val✝ : Fintype ι
this : FiniteDimensional ℝ E
D : Set (ι → ℝ) := Set.univ.pi fun x => Set.Ico 0 1
⊢ MeasurableSet D

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

Result:
no goals