awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
refine_1 :
  ∀ (q : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (x x_1 : E) (h : x ≈ x_1), Eq (α := (↑(fundamentalDomain b) : Type u_1)) (fractRestrict b x) (fractRestrict b x_1)
⊢ HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) →
    (↑(fundamentalDomain b) : Type u_1)

Tactic:
refine fun q => Quotient.liftOn q (fractRestrict b) (fun _ _ h => ?_)

Premises used: Quotient.liftOn, ZSpan.fractRestrict
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
q : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x x_1 : E
h : x ≈ x_1
refine_1 :
  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-x + x_1)
⊢ Eq (α := (↑(fundamentalDomain b) : Type u_1)) (fractRestrict b x) (fractRestrict b x_1)

Tactic:
rw [Subtype.mk.injEq, fractRestrict_apply, fractRestrict_apply, fract_eq_fract]

Premises used: ZSpan.fractRestrict_apply, Subtype.mk.injEq, ZSpan.fract_eq_fract
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
q : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x x_1 : E
h : x ≈ x_1
⊢ Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-x + x_1)

Tactic:
QuotientAddGroup.leftRel_apply.mp h

Premises used: QuotientAddGroup.leftRel_apply, Set.Mem, Iff.mp
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
q : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x x_1 : E
h : x ≈ x_1
⊢ Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-x + x_1)

Tactic:
exact QuotientAddGroup.leftRel_apply.mp h

Premises used: QuotientAddGroup.leftRel_apply, Iff.mp
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
x y : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
refine_2 :
  ∀ (a b_1 : E),
    Eq (α := (↑(fundamentalDomain b) : Type u_1))
        (Quotient.liftOn (s := quotientRel (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ⟦a⟧
          (fractRestrict b) ⋯)
        (Quotient.liftOn (s := quotientRel (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ⟦b_1⟧
          (fractRestrict b) ⋯) →
      Eq (α :=
        HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ⟦a⟧
        ⟦b_1⟧
⊢ Eq (α := (↑(fundamentalDomain b) : Type u_1)) (Quotient.liftOn x (fractRestrict b) ⋯)
      (Quotient.liftOn y (fractRestrict b) ⋯) →
    x = y

Tactic:
induction x, y using Quotient.inductionOn₂
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
a b_1 : E
hxy :
  Eq (α := (↑(fundamentalDomain b) : Type u_1))
    (Quotient.liftOn (s := quotientRel (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ⟦a⟧
      (fractRestrict b) ⋯)
    (Quotient.liftOn (s := quotientRel (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ⟦b_1⟧
      (fractRestrict b) ⋯)
⊢ fract b a = fract b b_1

Tactic:
rw [Quotient.liftOn_mk (s := quotientRel (span ℤ (Set.range b))), fractRestrict,
      Quotient.liftOn_mk (s := quotientRel (span ℤ (Set.range b))), fractRestrict,
      Subtype.mk.injEq] at hxy

Premises used: Subtype.mk.injEq, Quotient.liftOn_mk, ZSpan.fractRestrict
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
a b_1 : E
hxy : fract b a = fract b b_1
refine_2 : ((span ℤ (Set.range (⇑b : (a : ι) → E))).quotientRel : E → E → Prop) a b_1
⊢ Eq (α := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ⟦a⟧ ⟦b_1⟧

Tactic:
apply Quotient.sound'

Premises used: Quotient.sound'
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
a b_1 : E
hxy : fract b a = fract b b_1
refine_2 :
  Membership.mem (γ := AddSubgroup E)
    (toAddSubgroup (module_M := AddCommGroup.toIntModule E)
      (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (-a + b_1)
refine_2₁ :
  Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) (-a + b_1)
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : fract b a = fract b b_1
⊢ ((span ℤ (Set.range (⇑b : (a : ι) → E))).quotientRel : E → E → Prop) a b_1

Tactic:
rwa [QuotientAddGroup.leftRel_apply, mem_toAddSubgroup, ← fract_eq_fract]

Premises used: QuotientAddGroup.leftRel_apply, Submodule.mem_toAddSubgroup, ZSpan.fract_eq_fract
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
x : (↑(fundamentalDomain b) : Type u_1)
refine_3 :
  ∀ (a : E),
    ∃ (a_1 :
      HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))),
      Eq (α := (↑(fundamentalDomain b) : Type u_1)) (Quotient.liftOn a_1 (fractRestrict b) ⋯) (fractRestrict b a)
⊢ ∃ (a : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))),
    Quotient.liftOn a (fractRestrict b) ⋯ = x

Tactic:
obtain ⟨a, rfl⟩ := fractRestrict_surjective b x

Premises used: ZSpan.fractRestrict_surjective, rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
a : E
⊢ ∃ (a_1 : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))),
    Eq (α := (↑(fundamentalDomain b) : Type u_1)) (Quotient.liftOn a_1 (fractRestrict b) ⋯) (fractRestrict b a)

Tactic:
⟨Quotient.mk'' a, rfl⟩

Premises used: Quotient.mk'', Exists.intro, rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
a : E
⊢ ∃ (a_1 : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))),
    Eq (α := (↑(fundamentalDomain b) : Type u_1)) (Quotient.liftOn a_1 (fractRestrict b) ⋯) (fractRestrict b a)

Tactic:
exact ⟨Quotient.mk'' a, rfl⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
x : E
⊢ Eq (α := (↑(fundamentalDomain b) : Type u_1))
    ((quotientEquiv b : (a : E ⧸ span ℤ (Set.range (⇑b : (a : ι) → E))) → (↑(fundamentalDomain b) : Type u_1))
        (Submodule.Quotient.mk x) :
      (↑(fundamentalDomain b) : Type u_1))
    (fractRestrict b x : (↑(fundamentalDomain b) : Type u_1))

Tactic:
rfl

Premises used: ZSpan.fractRestrict, rfl
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
x : (↑(fundamentalDomain b) : Type u_1)
rw : (↑x : E) = fract b (↑x : E)
⊢ Eq (α := HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    ((Equiv.symm (quotientEquiv b) :
          (a : (↑(fundamentalDomain b) : Type u_1)) → E ⧸ span ℤ (Set.range (⇑b : (a : ι) → E)))
        x :
      HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
    (Submodule.Quotient.mk (↑x : E) :
      HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))

Tactic:
rw [Equiv.symm_apply_eq, quotientEquiv_apply_mk b ↑x, Subtype.ext_iff, fractRestrict_apply]

Premises used: ZSpan.fractRestrict_apply, ZSpan.quotientEquiv_apply_mk, Equiv.symm_apply_eq, Subtype.ext_iff, Subtype.val
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
x : (↑(fundamentalDomain b) : Type u_1)
⊢ (↑x : E) = fract b (↑x : E)

Tactic:
(fract_eq_self.mpr x.prop).symm

Premises used: Iff.mpr, ZSpan.fract_eq_self, Subtype.prop, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace K E
b : Basis ι K E
inst_3 : LinearOrder K
inst_4 : IsStrictOrderedRing K
inst_5 : FloorRing K
inst_6 : Fintype ι
x : (↑(fundamentalDomain b) : Type u_1)
⊢ (↑x : E) = fract b (↑x : E)

Tactic:
exact (fract_eq_self.mpr x.prop).symm

Premises used: Iff.mpr, ZSpan.fract_eq_self, Subtype.prop, Eq.symm
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
intro :
  ∀ (val : Fintype ι), DiscreteTopology.{u_2} ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
⊢ DiscreteTopology.{u_2} ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
⊢ DiscreteTopology.{u_2} ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))

Tactic:
discreteTopology_iff_isOpen_singleton_zero.mpr ⟨Metric.ball 0 1, Metric.isOpen_ball, ?_⟩

Premises used: Iff.mpr, Metric.ball, Metric.isOpen_ball, And.intro, Exists.intro, OfNat.ofNat, discreteTopology_iff_isOpen_singleton_zero
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
intro :
  Eq (α := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))))
    (Subtype.val (p := fun (x : ι → ℝ) ↦
        Membership.mem (γ := Submodule ℤ (ι → ℝ)) (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
          x) ⁻¹'
      Metric.ball 0 1)
    {0}
⊢ DiscreteTopology.{u_2} ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))

Tactic:
refine discreteTopology_iff_isOpen_singleton_zero.mpr ⟨Metric.ball 0 1, Metric.isOpen_ball, ?_⟩
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
intro :
  ∀ (x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))),
    Membership.mem (γ := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))))
        (Subtype.val (p := fun (x : ι → ℝ) ↦
            Membership.mem (γ := Submodule ℤ (ι → ℝ))
              (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) x) ⁻¹'
          Metric.ball 0 1)
        x ↔
      Membership.mem (γ := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))) {0} x
⊢ Eq (α := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))))
    (Subtype.val (p := fun (x : ι → ℝ) ↦
        Membership.mem (γ := Submodule ℤ (ι → ℝ)) (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
          x) ⁻¹'
      Metric.ball 0 1)
    {0}

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
intro : (∀ (i : ι), ‖(↑x : ι → ℝ) i‖ < 1) ↔ x = 0
⊢ Membership.mem (γ := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))))
      (Subtype.val (p := fun (x : ι → ℝ) ↦
          Membership.mem (γ := Submodule ℤ (ι → ℝ)) (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
            x) ⁻¹'
        Metric.ball 0 1)
      x ↔
    Membership.mem (γ := Set ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))) {0} x

Tactic:
rw [Set.mem_preimage, mem_ball_zero_iff, pi_norm_lt_iff zero_lt_one, Set.mem_singleton_iff]

Premises used: pi_norm_lt_iff, zero_lt_one, Set.mem_singleton_iff, Set.mem_preimage, mem_ball_zero_iff
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
intro : (∀ (i : ι), |(↑x : ι → ℝ) i| < 1) ↔ ∀ (x_1 : ι), (↑x : ι → ℝ) x_1 = 0
⊢ (∀ (i : ι), ‖(↑x : ι → ℝ) i‖ < 1) ↔ x = 0

Tactic:
simp_rw [← coe_eq_zero, funext_iff, Pi.zero_apply, Real.norm_eq_abs]

Premises used: funext_iff, Pi.zero_apply, Submodule.coe_eq_zero, Real.norm_eq_abs
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
⊢ (∀ (i : ι), |(↑x : ι → ℝ) i| < 1) ↔ ∀ (x_1 : ι), (↑x : ι → ℝ) x_1 = 0

Tactic:
forall_congr' (fun i => ?_)

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
intro : ∀ (i : ι), |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
⊢ (∀ (i : ι), |(↑x : ι → ℝ) i| < 1) ↔ ∀ (x_1 : ι), (↑x : ι → ℝ) x_1 = 0

Tactic:
refine forall_congr' (fun i => ?_)

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
intro : ∀ (y : ℤ) (hy : (↑y : ℝ) = (↑x : ι → ℝ) i), |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0
rsuffices : ∃ (y : ℤ), (↑y : ℝ) = (↑x : ι → ℝ) i
⊢ |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0

Tactic:
rsuffices ⟨y, hy⟩ : ∃ (y : ℤ), (y : ℝ) = (x : ι → ℝ) i

Premises used: Subtype.val
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
y : ℤ
hy : (↑y : ℝ) = (↑x : ι → ℝ) i
intro : LT.lt (α := ℝ) |(↑y : ℝ)| 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₁ : LT.lt (α := ℝ) (↑|y| : ℝ) 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₂ : LT.lt (α := ℝ) (↑|y| : ℝ) (↑1 : ℝ) ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₃ : |y| < 1 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₄ : y = 0 ↔ Eq (α := ℝ) (↑y : ℝ) 0
intro₅ intro₆ : y = 0 ↔ y = 0
⊢ |(↑x : ι → ℝ) i| < 1 ↔ (↑x : ι → ℝ) i = 0

Tactic:
rw [← hy, ← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff, Int.cast_eq_zero]

Premises used: Int.cast_abs, Int.cast_lt, Int.cast_eq_zero, Int.abs_lt_one_iff, Int.cast_one
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
⊢ ∃ (y : ℤ), (↑y : ℝ) = (↑x : ι → ℝ) i

Tactic:
((Pi.basisFun ℝ ι).mem_span_iff_repr_mem ℤ x).mp (SetLike.coe_mem x) i

Premises used: Real, SetLike.coe_mem, Set.Mem, setOf, Int, Iff.mp, Pi.basisFun, Set.range, Subtype.val, Module.Basis.mem_span_iff_repr_mem
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
ι : Type u_2
inst : Finite ι
val : Fintype ι
x : ↥(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ)))
i : ι
⊢ ∃ (y : ℤ), (↑y : ℝ) = (↑x : ι → ℝ) i

Tactic:
exact ((Pi.basisFun ℝ ι).mem_span_iff_repr_mem ℤ x).mp (SetLike.coe_mem x) i

Premises used: Real, SetLike.coe_mem, Int, Iff.mp, Pi.basisFun, Subtype.val, Module.Basis.mem_span_iff_repr_mem
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
rw :
  ∀ (a : E),
    (∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
          ((((b.repr : (a : E) → ι →₀ ℝ) a : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)) →
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1)
          ((((b.repr : (a : E) → ι →₀ ℝ) a : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)
⊢ fundamentalDomain b ⊆ parallelepiped.{u_2, u_1} (ι := ι) (⇑b : (a : ι) → E)

Tactic:
rw [fundamentalDomain, parallelepiped_basis_eq, Set.setOf_subset_setOf]

Premises used: parallelepiped_basis_eq, Set.setOf_subset_setOf, ZSpan.fundamentalDomain
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
⊢ ∀ (a : E),
    (∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
          ((((b.repr : (a : E) → ι →₀ ℝ) a : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)) →
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1)
          ((((b.repr : (a : E) → ι →₀ ℝ) a : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)

Tactic:
fun _ h i ↦ Set.Ico_subset_Icc_self (h i)

Premises used: Set.Ico_subset_Icc_self
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Fintype ι
⊢ ∀ (a : E),
    (∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Ico 0 1)
          ((((b.repr : (a : E) → ι →₀ ℝ) a : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)) →
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1)
          ((((b.repr : (a : E) → ι →₀ ℝ) a : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)

Tactic:
exact fun _ h i ↦ Set.Ico_subset_Icc_self (h i)

Premises used: Set.Ico_subset_Icc_self
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
x : E
hx : x ∈ (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
rwa :
  ∀ (hx : Membership.mem (γ := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) x),
    Membership.mem (α := ι → ℝ) (γ := Submodule ℤ (ι → ℝ))
      (span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) ((b.equivFun : (a : E) → ι → ℝ) x : ι → ℝ)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hx :
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
          ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ))
    (i : ι),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Set.range (ι := ℤ) (⇑(algebraMap ℤ ℝ) : (a : ℤ) → ℝ))
      ((((Basis.repr (Pi.basisFun ℝ ι) : (a : ι → ℝ) → ι →₀ ℝ) ((b.equivFun : (a : E) → ι → ℝ) x : ι → ℝ) : ι →₀ ℝ) :
            (a : ι) → ℝ)
          i :
        ℝ)
⊢ Membership.mem (α := ι → ℝ) (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
    ((b.equivFun : (a : E) → ι → ℝ) x : ι → ℝ)

Tactic:
rwa [SetLike.mem_coe, Basis.mem_span_iff_repr_mem] at hx ⊢

Premises used: SetLike.mem_coe, Module.Basis.mem_span_iff_repr_mem
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
⊢ Set.MapsTo (⇑b.equivFun : (a : E) → ι → ℝ) (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))

Tactic:
have h : Set.MapsTo b.equivFun (span ℤ (Set.range b)) (span ℤ (Set.range (Pi.basisFun ℝ ι))) := by
    intro _ hx
    rwa [SetLike.mem_coe, Basis.mem_span_iff_repr_mem] at hx ⊢
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
h :
  Set.MapsTo (⇑b.equivFun : (a : E) → ι → ℝ) (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ DiscreteTopology.{u_1} (↑(↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E) : Type u_1)

Tactic:
DiscreteTopology.of_continuous_injective ((continuous_equivFun_basis b).restrict h) ?_

Premises used: continuous_equivFun_basis, Continuous.restrict, DiscreteTopology.of_continuous_injective
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
h :
  Set.MapsTo (⇑b.equivFun : (a : E) → ι → ℝ) (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
convert_1 :
  DiscreteTopology.{u_2}
    (↑(↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) : Type u_2)
convert_2 :
  Function.Injective
    (Set.MapsTo.restrict (⇑b.equivFun : (a : E) → ι → ℝ)
      (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
      (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) h)
⊢ DiscreteTopology.{u_1} ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))

Tactic:
convert! DiscreteTopology.of_continuous_injective ((continuous_equivFun_basis b).restrict h) ?_
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
h :
  Set.MapsTo (⇑b.equivFun : (a : E) → ι → ℝ) (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ DiscreteTopology.{u_2}
    (↑(↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) : Type u_2)

Tactic:
discreteTopology_pi_basisFun

Premises used: ZSpan.discreteTopology_pi_basisFun
-- Module: Mathlib.Algebra.Module.ZLattice.Basic
Goal:
E : Type u_1
ι : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : Basis ι ℝ E
inst_2 : Finite ι
h :
  Set.MapsTo (⇑b.equivFun : (a : E) → ι → ℝ) (↑(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) : Set E)
    (↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ))
⊢ DiscreteTopology.{u_2}
    (↑(↑(span ℤ (Set.range (ι := ι) (⇑(Pi.basisFun ℝ ι) : (a : ι) → ι → ℝ))) : Set (ι → ℝ)) : Type u_2)

Tactic:
exact discreteTopology_pi_basisFun

Premises used: ZSpan.discreteTopology_pi_basisFun