awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
⊢ s ⊆ Set.range (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))

Tactic:
simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, subset_rfl]

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq, subset_rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
⊢ LE.le (α := Submodule K E) (span K s)
    (span K (Set.range (ι := { x : E // x ∈ s }) (Subtype.val (p := fun (x : E) ↦ x ∈ s))))

Tactic:
exact span_mono (by simp only [Subtype.range_coe_subtype, Set.setOf_mem_eq, subset_rfl])

Premises used: Submodule.span_mono
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
⊢ Eq (α := Submodule ℤ E) (span ℤ s) (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))

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

Premises used: Subtype.range_coe_subtype, Module.Basis.coe_mk
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
refine_1 :
  (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
      Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))).Finite
⊢ (↑(Submodule.map (mkQ (span ℤ s)) L) : Set (E ⧸ span ℤ s)).Finite

Tactic:
rw [show span ℤ s = span ℤ (Set.range b) by simp [b, Basis.coe_mk, Subtype.range_coe_subtype]]
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
refine_1 :
  ∀ (this : Fintype (↑s : Type u_2)),
    (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
        Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))).Finite
⊢ (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
      Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))).Finite

Tactic:
have : Fintype s := h_lind.setFinite.fintype
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this : Fintype (↑s : Type u_2)
⊢ (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
      Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))).Finite

Tactic:
Set.Finite.of_finite_image (f := ((↑) : _ → E) ∘ quotientEquiv b) ?_
      (Function.Injective.injOn (Subtype.coe_injective.comp (quotientEquiv b).injective))

Premises used: Set.Finite.of_finite_image
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this : Fintype (↑s : Type u_2)
refine_1 :
  Set.Finite (α := E)
    (Function.comp (β := (↑(fundamentalDomain b) : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ fundamentalDomain b))
        (⇑(quotientEquiv b) :
          (a : E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E))) → (↑(fundamentalDomain b) : Type u_2)) ''
      (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
        Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))))
⊢ (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
      Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))).Finite

Tactic:
refine Set.Finite.of_finite_image (f := ((↑) : _ → E) ∘ quotientEquiv b) ?_
      (Function.Injective.injOn (Subtype.coe_injective.comp (quotientEquiv b).injective))

Premises used: Set.Finite.of_finite_image
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this : Fintype (↑s : Type u_2)
change : (fundamentalDomain b ∩ (↑L.toAddSubgroup : Set E)).Finite
⊢ (fundamentalDomain b ∩ (↑L : Set E)).Finite

Tactic:
change ((fundamentalDomain b) ∩ L.toAddSubgroup).Finite

Premises used: Set.Finite, Inter.inter, SetLike.coe, Submodule.toAddSubgroup, ZSpan.fundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this : Fintype (↑s : Type u_2)
⊢ DiscreteTopology.{u_2} ↥L.toAddSubgroup

Tactic:
have : DiscreteTopology L.toAddSubgroup := (inferInstance : DiscreteTopology L)
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : DiscreteTopology.{u_2} ↥L.toAddSubgroup
⊢ (fundamentalDomain b ∩ (↑L.toAddSubgroup : Set E)).Finite

Tactic:
Metric.finite_isBounded_inter_isClosed
        DiscreteTopology.isDiscrete (fundamentalDomain_isBounded b) inferInstance

Premises used: DiscreteTopology.isDiscrete, inferInstance, Metric.finite_isBounded_inter_isClosed, ZSpan.fundamentalDomain_isBounded
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : DiscreteTopology.{u_2} ↥L.toAddSubgroup
⊢ (fundamentalDomain b ∩ (↑L.toAddSubgroup : Set E)).Finite

Tactic:
exact Metric.finite_isBounded_inter_isClosed
        DiscreteTopology.isDiscrete (fundamentalDomain_isBounded b) inferInstance

Premises used: DiscreteTopology.isDiscrete, inferInstance, Metric.finite_isBounded_inter_isClosed, ZSpan.fundamentalDomain_isBounded
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this : Fintype (↑s : Type u_2)
⊢ (fundamentalDomain b ∩ (↑L : Set E)).Finite

Tactic:
have : ((fundamentalDomain b) ∩ L).Finite := by
      change ((fundamentalDomain b) ∩ L.toAddSubgroup).Finite
      have : DiscreteTopology L.toAddSubgroup := (inferInstance : DiscreteTopology L)
      exact Metric.finite_isBounded_inter_isClosed
        DiscreteTopology.isDiscrete (fundamentalDomain_isBounded b) inferInstance
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
⊢ Set.Finite (α := E)
    (Function.comp (β := (↑(fundamentalDomain b) : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ fundamentalDomain b))
        (⇑(quotientEquiv b) :
          (a : E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E))) → (↑(fundamentalDomain b) : Type u_2)) ''
      (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
        Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))))

Tactic:
Set.Finite.subset this ?_

Premises used: Set.Finite.subset
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
refine_1 :
  Function.comp (β := (↑(fundamentalDomain b) : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ fundamentalDomain b))
        (⇑(quotientEquiv b) :
          (a : E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E))) → (↑(fundamentalDomain b) : Type u_2)) ''
      (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
        Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))) ⊆
    fundamentalDomain b ∩ (↑L : Set E)
⊢ Set.Finite (α := E)
    (Function.comp (β := (↑(fundamentalDomain b) : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ fundamentalDomain b))
        (⇑(quotientEquiv b) :
          (a : E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E))) → (↑(fundamentalDomain b) : Type u_2)) ''
      (↑(Submodule.map (mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) L) :
        Set (E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))))

Tactic:
refine Set.Finite.subset this ?_

Premises used: Set.Finite.subset
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
refine_1 : fract b x ∈ fundamentalDomain b ∩ (↑L : Set E)
⊢ Function.comp (α :=
      HasQuotient.Quotient E (B := Submodule ℤ E)
        (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E))))
      (β := (↑(fundamentalDomain b) : Type u_2)) (Subtype.val (p := fun (x : E) ↦ x ∈ fundamentalDomain b))
      ((⇑(quotientEquiv b) :
          (a :
              HasQuotient.Quotient E (B := Submodule ℤ E)
                (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) →
            (↑(fundamentalDomain b) : Type u_2)) :
        (a :
            HasQuotient.Quotient E (B := Submodule ℤ E)
              (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) →
          (↑(fundamentalDomain b) : Type u_2))
      ((mkQ (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E))) :
            (a : E) → E ⧸ span ℤ (Set.range (⇑b : (a : { x : E // x ∈ s }) → E)))
          x :
        HasQuotient.Quotient E (B := Submodule ℤ E)
          (span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E)))) ∈
    fundamentalDomain b ∩ (↑L : Set E)

Tactic:
rw [Function.comp_apply, mkQ_apply, quotientEquiv_apply_mk, fractRestrict_apply]

Premises used: ZSpan.fractRestrict_apply, ZSpan.quotientEquiv_apply_mk, Submodule.mkQ_apply, Function.comp_apply
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
⊢ fract b x ∈ fundamentalDomain b ∩ (↑L : Set E)

Tactic:
⟨?_, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
refine_1 : fract b x ∈ fundamentalDomain b
refine_1₁ : fract b x ∈ (↑L : Set E)
⊢ fract b x ∈ fundamentalDomain b ∩ (↑L : Set E)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
⊢ fract b x ∈ fundamentalDomain b

Tactic:
fract_mem_fundamentalDomain b x

Premises used: ZSpan.fract_mem_fundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
⊢ fract b x ∈ fundamentalDomain b

Tactic:
exact fract_mem_fundamentalDomain b x

Premises used: ZSpan.fract_mem_fundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
refine_1 : x + -(↑(floor b x) : E) ∈ L
⊢ fract b x ∈ (↑L : Set E)

Tactic:
rw [fract, SetLike.mem_coe, sub_eq_add_neg]

Premises used: sub_eq_add_neg, SetLike.mem_coe, ZSpan.fract
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
⊢ x + -(↑(floor b x) : E) ∈ L

Tactic:
Submodule.add_mem _ h_mem
        (neg_mem (Set.mem_of_subset_of_mem ?_ (Subtype.mem (floor b x))))

Premises used: Set.Mem, Set.mem_of_subset_of_mem, ZSpan.floor, Subtype.mem, NegMemClass.neg_mem, Submodule.add_mem
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
K : Type u_1
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : HasSolidNorm K
inst_4 : FloorRing K
E : Type u_2
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace K E
inst_7 : FiniteDimensional K E
inst_8 : ProperSpace E
L : Submodule ℤ E
inst_9 : DiscreteTopology.{u_2} ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ (↑L : Set E)
h_span : Eq (α := Submodule K E) (span K s) (span K (↑L : Set E))
h_lind : LinearIndependent.{u_2, u_1, u_2} (ι := { x : E // x ∈ s }) K (Subtype.val (p := fun (x : E) ↦ x ∈ s))
b : Basis { x : E // x ∈ s } K E := Basis.mk h_lind ⋯
this_1 : Fintype (↑s : Type u_2)
this : (fundamentalDomain b ∩ (↑L : Set E)).Finite
x : E
h_mem : x ∈ (↑L : Set E)
refine_1 : (↑(span ℤ (Set.range (ι := { x : E // x ∈ s }) (⇑b : (a : { x : E // x ∈ s }) → E))) : Set E) ⊆ (↑L : Set E)
⊢ x + -(↑(floor b x) : E) ∈ L

Tactic:
refine Submodule.add_mem _ h_mem
        (neg_mem (Set.mem_of_subset_of_mem ?_ (Subtype.mem (floor b x))))

Premises used: Set.mem_of_subset_of_mem, ZSpan.floor, Subtype.mem, NegMemClass.neg_mem, Submodule.add_mem