-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem ZLattice.isAddFundamentalDomain {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] {L : Submodule ℤ E} [DiscreteTopology L] [IsZLattice ℝ L] [Finite ι]
    (b : Basis ι ℤ L) [MeasurableSpace E] [OpensMeasurableSpace E] (μ : Measure E) :
    IsAddFundamentalDomain L (fundamentalDomain (b.ofZLatticeBasis ℝ)) μ

Proof state:
case h.e'_1.h.e'_2.h.h.e'_4
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
x✝ : E
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

case h.e'_3.e'_6
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
e_1✝ : ↥L = ↥(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)))
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

case h.e'_4.e'_6
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
e_1✝ : ↥L = ↥(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)))
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

Tactic:
all_goals exact (b.ofZLatticeBasis_span ℝ).symm

Result:
no goals

Proof state:
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
⊢ IsAddFundamentalDomain (↥L) (fundamentalDomain (Basis.ofZLatticeBasis ℝ L b)) μ

Tactic:
convert ZSpan.isAddFundamentalDomain (b.ofZLatticeBasis ℝ) μ

Result:
case h.e'_1.h.e'_2.h.h.e'_4
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
x✝ : E
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

case h.e'_3.e'_6
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
e_1✝ : ↥L = ↥(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)))
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

case h.e'_4.e'_6
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
e_1✝ : ↥L = ↥(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)))
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

Proof state:
case h.e'_4.e'_6
ι : Type u_3
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝⁴ : DiscreteTopology ↥L
inst✝³ : IsZLattice ℝ L
inst✝² : Finite ι
b : Basis ι ℤ ↥L
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
e_1✝ : ↥L = ↥(span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)))
⊢ L = span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b))

Tactic:
exact (b.ofZLatticeBasis_span ℝ).symm

Result:
no goals