-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem Zlattice.FG [hs : IsZLattice K L] : L.FG

Proof state:
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ (Submodule.map (span ℤ s).mkQ L).FG

Tactic:
refine fg_def.mpr ⟨map (span ℤ s).mkQ L, ?_, span_eq _⟩

Result:
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ (↑(Submodule.map (span ℤ s).mkQ L)).Finite

Proof state:
case intro.intro.intro.refine_1.intro.intro.intro.intro.refine_2
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ span ℤ s ≤ L

Tactic:
exact span_le.mpr h_incl

Result:
no goals

Proof state:
case intro.intro.intro.refine_1.intro.intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
x : E
h_mem : x ∈ ↑L
⊢ fract b x ∈ fundamentalDomain b

Tactic:
exact fract_mem_fundamentalDomain b x

Result:
no goals

Proof state:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
⊢ span ℤ s = span ℤ (Set.range ⇑b)

Tactic:
simp [b, Basis.coe_mk, Subtype.range_coe_subtype]

Result:
no goals

Proof state:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : DiscreteTopology ↥L.toAddSubgroup
⊢ (fundamentalDomain b ∩ ↑L.toAddSubgroup).Finite

Tactic:
exact Metric.finite_isBounded_inter_isClosed (fundamentalDomain_isBounded b) inferInstance

Result:
no goals

Proof state:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ ⊤ ≤ span K (Set.range Subtype.val)

Tactic:
rw [← hs.span_top, ← h_span]

Result:
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
⊢ span K s ≤ span K (Set.range Subtype.val)

Proof state:
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
⊢ (Subtype.val ∘ ⇑(quotientEquiv b) '' ↑(Submodule.map (span ℤ (Set.range ⇑b)).mkQ L)).Finite

Tactic:
refine Set.Finite.subset this ?_

Result:
case intro.intro.intro.refine_1
K : Type u_1
inst✝⁷ : NormedLinearOrderedField K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
this✝ : Fintype ↑s
this : (fundamentalDomain b ∩ ↑L).Finite
⊢ Subtype.val ∘ ⇑(quotientEquiv b) '' ↑(Submodule.map (span ℤ (Set.range ⇑b)).mkQ L) ⊆ fundamentalDomain b ∩ ↑L