awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Finite ι
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
μ : Measure E
⊢ IsAddFundamentalDomain (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (fundamentalDomain b) μ
have intro : ∀ (val : Fintype ι),
  IsAddFundamentalDomain (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) (fundamentalDomain b) μ
Tactic: cases nonempty_fintype ι
-- 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 : 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)
have convert! : VAddInvariantMeasure (↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) E μ
Tactic: convert! (ZSpan.isAddFundamentalDomain b μ).measure_ne_zero (NeZero.ne μ)
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
⊢ (μ : (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)
have this : FiniteDimensional ℝ E
Tactic: have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
-- 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 : DecidableEq ι
inst_4 : MeasurableSpace E
μ : Measure E
inst_5 : BorelSpace E
inst_6 : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ 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)
have h : fundamentalDomain b = (⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) ⁻¹' fundamentalDomain b₀
Tactic: convert! μ.addHaar_preimage_linearEquiv (b.equiv b₀ (Equiv.refl ι)) (fundamentalDomain b₀)
-- 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 : 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₀
⊢ (μ : (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)
have h₁ : Eq (α := ℝ) ((b₀.det : (a : ι → E) → ℝ) (⇑b : (a : ι) → E) : ℝ)
  ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑(b.equiv b₀ (Equiv.refl ι)).symm : E →ₗ[ℝ] E) : ℝ)
Tactic: convert! μ.addHaar_preimage_linearEquiv (b.equiv b₀ (Equiv.refl ι)) (fundamentalDomain b₀)
-- 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 : DecidableEq ι
inst_4 : MeasurableSpace E
μ : Measure E
inst_5 : BorelSpace E
inst_6 : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ fundamentalDomain b = (⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) ⁻¹' fundamentalDomain b₀
have h : (⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) '' fundamentalDomain b = fundamentalDomain b₀
Tactic: rw [Set.eq_preimage_iff_image_eq (LinearEquiv.bijective _), map_fundamentalDomain,
      Basis.map_equiv, Equiv.refl_symm, Basis.reindex_refl]
-- 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 : 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₀
⊢ fundamentalDomain b = (⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) ⁻¹' fundamentalDomain b₀
have h₁ : fundamentalDomain (b.map (b.equiv b₀ (Equiv.refl ι))) = fundamentalDomain b₀
Tactic: rw [Set.eq_preimage_iff_image_eq (LinearEquiv.bijective _), map_fundamentalDomain,
      Basis.map_equiv, Equiv.refl_symm, Basis.reindex_refl]
-- 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 : 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₀
⊢ fundamentalDomain b = (⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) ⁻¹' fundamentalDomain b₀
have h₂ : fundamentalDomain (b₀.reindex (Equiv.refl ι).symm) = fundamentalDomain b₀
Tactic: rw [Set.eq_preimage_iff_image_eq (LinearEquiv.bijective _), map_fundamentalDomain,
      Basis.map_equiv, Equiv.refl_symm, Basis.reindex_refl]
-- 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 : 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₀
⊢ fundamentalDomain b = (⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) ⁻¹' fundamentalDomain b₀
have h₃ : fundamentalDomain (b₀.reindex (Equiv.refl ι)) = fundamentalDomain b₀
Tactic: rw [Set.eq_preimage_iff_image_eq (LinearEquiv.bijective _), map_fundamentalDomain,
      Basis.map_equiv, Equiv.refl_symm, Basis.reindex_refl]
-- 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 : 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₀
⊢ fundamentalDomain b = (⇑(b.equiv b₀ (Equiv.refl ι)) : (a : E) → E) ⁻¹' fundamentalDomain b₀
have h₄ : fundamentalDomain b₀ = fundamentalDomain b₀
Tactic: rw [Set.eq_preimage_iff_image_eq (LinearEquiv.bijective _), map_fundamentalDomain,
      Basis.map_equiv, Equiv.refl_symm, Basis.reindex_refl]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
b : Basis ι ℝ (ι → ℝ)
⊢ ((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (fundamentalDomain (ι := ι) (K := ℝ) b) =
    ENNReal.ofReal |Matrix.det.{0, u_2} (n := ι) ((Matrix.of : (a : ι → ι → ℝ) → Matrix ι ι ℝ) (⇑b : (a : ι) → ι → ℝ))|
have 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 : ι) → ι → ℝ)))|
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
⊢ fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have this : FiniteDimensional ℝ E
Tactic: have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
-- 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
this : FiniteDimensional ℝ E
⊢ fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have rw : Eq (α := ENNReal)
  ((μ : (a : Set E) → ENNReal) (parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b) : ENNReal)
  (0 : ENNReal)
Tactic: rw [← measure_symmDiff_eq_zero_iff, symmDiff_of_le (fundamentalDomain_subset_parallelepiped b)]
-- 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
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)
have refine : ∀ (i : ι),
  Ne (α := AffineSubspace ℝ E)
    (AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
      AffineSubspace ℝ E)
    (⊤ : AffineSubspace ℝ E)
Tactic: refine measure_mono_null this
      (measure_iUnion_null_iff.mpr fun i ↦ Measure.addHaar_affineSubspace μ _ ?_)
-- 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
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)
i : ι
⊢ Ne (α := AffineSubspace ℝ E)
    (AffineSubspace.mk' ((b : (a : ι) → E) i) (span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))) :
      AffineSubspace ℝ E)
    (⊤ : AffineSubspace ℝ E)
have refine : VSub.vsub (P := E) (0 : E) ((b : (a : ι) → E) i : E) ∉ span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))
Tactic: refine (ne_of_mem_of_not_mem' (AffineSubspace.mem_top _ _ 0)
      (AffineSubspace.mem_mk'.not.mpr ?_)).symm
-- 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
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)
i : ι
⊢ VSub.vsub (P := E) (0 : E) ((b : (a : ι) → E) i : E) ∉ span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))
have simp_rw : ((b : (a : ι) → E) i : E) ∉ span ℝ (Set.image (α := ι) (⇑b : (a : ι) → E) (Set.univ \ {i}))
Tactic: simp_rw [vsub_eq_sub, zero_sub, neg_mem_iff]
-- 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
this : FiniteDimensional ℝ E
⊢ Eq (α := ENNReal)
    ((μ : (a : Set E) → ENNReal) (parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E) \ fundamentalDomain b) :
      ENNReal)
    (0 : ENNReal)
have suffices : 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)
Tactic: 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
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
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 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 : ℝ)
Tactic: 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
Cleared hypotheses: hx
-- 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
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 obtain : ∀ (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
Tactic: obtain ⟨i, hi⟩ := hx.2
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (hypothesis)
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
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₁ : Eq (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)
Tactic: have : b.repr x i = 1 := le_antisymm (hx.1 i).2 (hi (hx.1 i).1)
-- 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
this_1 : 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 rw : 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: rw [← b.sum_repr x, ← Finset.sum_erase_add _ _ (Finset.mem_univ i), this, one_smul, ← vadd_eq_add]
-- 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
this_1 : 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 refine : ∀ (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)
Tactic: refine Set.mem_iUnion.mpr ⟨i, AffineSubspace.vadd_mem_mk' _
    (sum_smul_mem _ _ (fun i hi ↦ Submodule.subset_span ?_))⟩
-- 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
⊢ fundamentalDomain b =ᶠ[ae μ] parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)
have have : ∀ (this : FiniteDimensional ℝ 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⟩