-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem fundamentalDomain_ae_parallelepiped [Fintype ι] [MeasurableSpace E] (μ : Measure E)
    [BorelSpace E] [Measure.IsAddHaarMeasure μ] :
    fundamentalDomain b =ᵐ[μ] parallelepiped b

Proof state:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Tactic:
obtain ⟨i, hi⟩ := hx.2

Result:
case intro
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
i : ι
hi : 0 ≤ (b.repr x) i → 1 ≤ (b.repr x) i
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Proof state:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
this : parallelepiped ⇑b \ fundamentalDomain b ⊆ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
⊢ μ (parallelepiped ⇑b \ fundamentalDomain b) = 0

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

Result:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
this : parallelepiped ⇑b \ fundamentalDomain b ⊆ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
i : ι
⊢ AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))) ≠ ⊤

Proof state:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
this : parallelepiped ⇑b \ fundamentalDomain b ⊆ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
i : ι
⊢ AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))) ≠ ⊤

Tactic:
refine (ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0)
  (AffineSubspace.mem_mk'_iff_vsub_mem.not.mpr ?_)).symm

Result:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
this : parallelepiped ⇑b \ fundamentalDomain b ⊆ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
i : ι
⊢ 0 -ᵥ b i ∉ span ℝ (⇑b '' (Set.univ \ {i}))

Proof state:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
⊢ fundamentalDomain b =ᶠ[ae μ] parallelepiped ⇑b

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

Result:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
⊢ μ (parallelepiped ⇑b \ fundamentalDomain b) = 0

Proof state:
case intro
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
i : ι
hi : 0 ≤ (b.repr x) i → 1 ≤ (b.repr x) i
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Tactic:
have : b.repr x i = 1 := le_antisymm (hx.1 i).2 (hi (hx.1 i).1)

Result:
case intro
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
i : ι
hi : 0 ≤ (b.repr x) i → 1 ≤ (b.repr x) i
this : (b.repr x) i = 1
⊢ x ∈ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Proof state:
case intro
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
i : ι
hi : 0 ≤ (b.repr x) i → 1 ≤ (b.repr x) i
this : (b.repr x) i = 1
⊢ ∑ x_1 ∈ Finset.univ.erase i, (b.repr x) x_1 • b x_1 +ᵥ b i ∈
    ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))

Tactic:
refine Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _
  (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩

Result:
case intro
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
i✝ : ι
hi✝ : 0 ≤ (b.repr x) i✝ → 1 ≤ (b.repr x) i✝
this : (b.repr x) i✝ = 1
i : ι
hi : i ∈ Finset.univ.erase i✝
⊢ b i ∈ ⇑b '' (Set.univ \ {i✝})

Proof state:
case intro
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
x : E
hx : (∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1) ∧ ∃ x_1, 0 ≤ (b.repr x) x_1 → 1 ≤ (b.repr x) x_1
i✝ : ι
hi✝ : 0 ≤ (b.repr x) i✝ → 1 ≤ (b.repr x) i✝
this : (b.repr x) i✝ = 1
i : ι
hi : i ∈ Finset.univ.erase i✝
⊢ b i ∈ ⇑b '' (Set.univ \ {i✝})

Tactic:
exact ⟨i, Set.mem_diff_singleton.mpr ⟨trivial, Finset.ne_of_mem_erase hi⟩, rfl⟩

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
this : parallelepiped ⇑b \ fundamentalDomain b ⊆ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
i : ι
⊢ 0 -ᵥ b i ∉ span ℝ (⇑b '' (Set.univ \ {i}))

Tactic:
simp_rw [vsub_eq_sub, zero_sub, neg_mem_iff]

Result:
E : Type u_1
ι : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝³ : Fintype ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
this✝ : FiniteDimensional ℝ E
this : parallelepiped ⇑b \ fundamentalDomain b ⊆ ⋃ i, ↑(AffineSubspace.mk' (b i) (span ℝ (⇑b '' (Set.univ \ {i}))))
i : ι
⊢ b i ∉ span ℝ (⇑b '' (Set.univ \ {i}))