-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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
⊢ fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have 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))
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⟩