-- 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
have have₁ have₂ :
  ∀ (this : FiniteDimensional ℝ E), fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have₃ :
  ∀ (this : FiniteDimensional ℝ E),
    Eq (α := ENNReal)
      ((μ : (a : Set E) → ENNReal) (parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b) :
        ENNReal)
      (0 : ENNReal)
have₄ :
  ∀ (this : FiniteDimensional ℝ E),
    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)
have₅ :
  ∀ (this : FiniteDimensional ℝ E) ⦃x : E⦄
    (hx : x ∈ parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b),
    Membership.mem (γ := Set E)
      (⋃ (i : ι),
        (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
              AffineSubspace ℝ E) :
          Set E))
      x
have₆ :
  ∀ (this : FiniteDimensional ℝ E) ⦃x : E⦄
    (hx :
      (∀ (i : ι),
          LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
            LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
        ∃ (x_1 : ι),
          LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
            LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)),
    Membership.mem (γ := Set E)
      (⋃ (i : ι),
        (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
              AffineSubspace ℝ E) :
          Set E))
      x
have₇ :
  ∀ (this : FiniteDimensional ℝ E) ⦃x : E⦄
    (hx :
      (∀ (i : ι),
          LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
            LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
        ∃ (x_1 : ι),
          LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
            LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ))
    (i : ι)
    (hi :
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)),
    Membership.mem (γ := Set E)
      (⋃ (i : ι),
        (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
              AffineSubspace ℝ E) :
          Set E))
      x
have₈ :
  ∀ (this : FiniteDimensional ℝ E) ⦃x : E⦄
    (hx :
      (∀ (i : ι),
          LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
            LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
        ∃ (x_1 : ι),
          LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
            LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ))
    (i : ι)
    (hi :
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ))
    (this : Eq (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)),
    Membership.mem (γ := Set E)
      (⋃ (i : ι),
        (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
              AffineSubspace ℝ E) :
          Set E))
      x
have₉ :
  ∀ (this : FiniteDimensional ℝ E) ⦃x : E⦄
    (hx :
      (∀ (i : ι),
          LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
            LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
        ∃ (x_1 : ι),
          LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
            LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ))
    (i : ι)
    (hi :
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ))
    (this : Eq (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)),
    Membership.mem (γ := Set E)
      (⋃ (i : ι),
        (↑(AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
              AffineSubspace ℝ E) :
          Set E))
      (HVAdd.hVAdd (α := E) (β := E)
        (∑ x_1 ∈ Finset.erase Finset.univ i,
          HSMul.hSMul (α := ℝ) (β := E) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ)
            ((b : (a : ι) → E) x_1 : E))
        ((b : (a : ι) → E) i : E))
have₁₀ :
  ∀ (this : FiniteDimensional ℝ E) ⦃x : E⦄
    (hx :
      (∀ (i : ι),
          LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
            LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) ∧
        ∃ (x_1 : ι),
          LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ) →
            LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 : ℝ))
    (i : ι)
    (hi :
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) →
        LE.le (α := ℝ) (1 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ))
    (this : Eq (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)) (i_1 : ι)
    (hi : i_1 ∈ Finset.erase Finset.univ i),
    Membership.mem.{u_1, u_1} (α := E) (γ := Set E) (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))
      ((b : (a : ι) → E) i_1 : E)
⊢ fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)

Tactic:
classical
  have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
  rw [← measure_symmDiff_eq_zero_iff, symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)]
  suffices (parallelepiped b \ fundamentalDomain b) ⊆ ⋃ i,
      AffineSubspace.mk' (b i) (span ℝ (b '' (Set.univ \ {i}))) by
    refine measure_mono_null this
      (measure_iUnion_null_iff.mpr fun i ↦ Measure.addHaar_affineSubspace μ _ ?_)
    refine (ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0)
      (AffineSubspace.mem_mk'.not.mpr ?_)).symm
    simp_rw [vsub_eq_sub, zero_sub, neg_mem_iff]
    exact linearIndependent_iff_notMem_span.mp b.linearIndependent i
  intro x hx
  simp_rw [parallelepiped_basis_eq, Set.mem_Icc, Set.mem_diff, Set.mem_setOf_eq,
    mem_fundamentalDomain, Set.mem_Ico, not_forall, not_and, not_lt] at hx
  obtain ⟨i, hi⟩ := hx.2
  have : b.repr x i = 1 := le_antisymm (hx.1 i).2 (hi (hx.1 i).1)
  rw [← b.sum_repr x, ← Finset.sum_erase_add _ _ (Finset.mem_univ i), this, one_smul, ← vadd_eq_add]
  refine Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _
    (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩
  exact ⟨i, Set.mem_diff_singleton.mpr ⟨trivial, Finset.ne_of_mem_erase hi⟩, rfl⟩

Premises used: Set.mem_Ico, Set.mem_setOf_eq, parallelepiped_basis_eq, one_smul, ZSpan.fundamentalDomain_subset_parallelepiped, not_lt, Set.mem_diff, vadd_eq_add, Set.mem_Icc, symmDiff_of_le, not_and, Classical.not_forall, MeasureTheory.measure_symmDiff_eq_zero_iff, ZSpan.mem_fundamentalDomain