awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Fintype ι
inst_5 : Unique ι
k : K
x : ι
rw :
  Eq.{u_3 + 1} (α := K)
    ((↑(Int.floor.{u_3} (α := K)
            ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) k : ι →₀ K) : (a : ι) → K) x : K)) :
        K) :
      K)
    (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑⌊k⌋ : K) : (a : ι) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑(floor (Basis.singleton ι K) k) : K) : ι →₀ K) :
          (a : ι) → K)
        x :
      K)
    (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑⌊k⌋ : K) : (a : ι) → K) x : K)
have rw₁ : Eq.{u_3 + 1} (α := K) ((↑⌊k⌋ : K) : K)
  (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑⌊k⌋ : K) : (a : ι) → K) x : K)
Tactic: rw [repr_floor_apply, Basis.singleton_repr, Basis.singleton_repr]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Fintype ι
inst_5 : Unique ι
k : K
x : ι
rw :
  Eq.{u_3 + 1} (α := K)
    ((↑(Int.floor.{u_3} (α := K)
            ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) k : ι →₀ K) : (a : ι) → K) x : K)) :
        K) :
      K)
    (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑⌊k⌋ : K) : (a : ι) → K) x : K)
rw₁ :
  Eq.{u_3 + 1} (α := K) ((↑⌊k⌋ : K) : K)
    (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑⌊k⌋ : K) : (a : ι) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑(floor (Basis.singleton ι K) k) : K) : ι →₀ K) :
          (a : ι) → K)
        x :
      K)
    (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (↑⌊k⌋ : K) : (a : ι) → K) x : K)
have rw₂ : Eq.{u_3 + 1} (α := K) (↑⌊k⌋ : K) (↑⌊k⌋ : K)
Tactic: rw [repr_floor_apply, Basis.singleton_repr, Basis.singleton_repr]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Fintype ι
inst_5 : Unique ι
k : K
x : ι
⊢ Eq.{u_3 + 1} (α := K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K)
              (fract.{u_3, u_2, u_3} (ι := ι) (K := K) (Basis.singleton ι K) k) :
            ι →₀ K) :
          (a : ι) → K)
        x :
      K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x : K)
have rw : Eq.{u_3 + 1} (α := K)
  (Int.fract ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) k : ι →₀ K) : (a : ι) → K) x) : K)
  ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x : K)
Tactic: rw [repr_fract_apply, Basis.singleton_repr, Basis.singleton_repr]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Fintype ι
inst_5 : Unique ι
k : K
x : ι
rw :
  Eq.{u_3 + 1} (α := K)
    (Int.fract ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) k : ι →₀ K) : (a : ι) → K) x) : K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x : K)
⊢ Eq.{u_3 + 1} (α := K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K)
              (fract.{u_3, u_2, u_3} (ι := ι) (K := K) (Basis.singleton ι K) k) :
            ι →₀ K) :
          (a : ι) → K)
        x :
      K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x : K)
have rw₁ : Int.fract k = (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x
Tactic: rw [repr_fract_apply, Basis.singleton_repr, Basis.singleton_repr]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
Goal:
ι : Type u_2
K : Type u_3
inst : NormedField K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorRing K
inst_4 : Fintype ι
inst_5 : Unique ι
k : K
x : ι
rw :
  Eq.{u_3 + 1} (α := K)
    (Int.fract ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) k : ι →₀ K) : (a : ι) → K) x) : K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x : K)
rw₁ : Int.fract k = (((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x
⊢ Eq.{u_3 + 1} (α := K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K)
              (fract.{u_3, u_2, u_3} (ι := ι) (K := K) (Basis.singleton ι K) k) :
            ι →₀ K) :
          (a : ι) → K)
        x :
      K)
    ((((Basis.repr (Basis.singleton ι K) : (a : K) → ι →₀ K) (Int.fract k) : ι →₀ K) : (a : ι) → K) x : K)
have rw₂ : Int.fract k = Int.fract k
Tactic: rw [repr_fract_apply, Basis.singleton_repr, Basis.singleton_repr]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 : Finite ι
inst_7 : HasSolidNorm K
⊢ IsBounded (fundamentalDomain b)
have intro : ∀ (val : Fintype ι), IsBounded (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
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 : Finite ι
inst_7 : HasSolidNorm K
val : Fintype ι
⊢ IsBounded (fundamentalDomain b)
have intro : ∀ (x : E) (hx : x ∈ fundamentalDomain b), ‖x‖ ≤ ∑ j : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) j : E)
Tactic: refine isBounded_iff_forall_norm_le.2 ⟨∑ j, ‖b j‖, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 : Finite ι
inst_7 : HasSolidNorm K
val : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
⊢ ‖x‖ ≤ ∑ j : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) j : E)
have intro : ‖fract b x‖ ≤ ∑ j : ι, norm.{u_1} (E := E) ((b : (a : ι) → E) j : E)
Tactic: rw [← fract_eq_self.mpr hx]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw₂ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + -(↑(floor b x) : E)
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
rw₂ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + -(↑(floor b x) : E)
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw₃ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x - (↑(floor b x) : E)
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
rw₂ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + -(↑(floor b x) : E)
rw₃ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x - (↑(floor b x) : E)
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw₄ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b x
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
rw₂ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + -(↑(floor b x) : E)
rw₃ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x - (↑(floor b x) : E)
rw₄ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b x
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw₅ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b ((↑y : E) + x)
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
rw₂ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + -(↑(floor b x) : E)
rw₃ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x - (↑(floor b x) : E)
rw₄ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b x
rw₅ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b ((↑y : E) + x)
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw₆ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) + x = fract b ((↑y : E) + x)
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
rw₂ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + -(↑(floor b x) : E)
rw₃ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x - (↑(floor b x) : E)
rw₄ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b x
rw₅ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b ((↑y : E) + x)
rw₆ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) + x = fract b ((↑y : E) + x)
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw₇ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) +ᵥ x = fract b ((↑y : E) +ᵥ x)
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
rw₂ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + -(↑(floor b x) : E)
rw₃ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x - (↑(floor b x) : E)
rw₄ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b x
rw₅ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b ((↑y : E) + x)
rw₆ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) + x = fract b ((↑y : E) + x)
rw₇ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) +ᵥ x = fract b ((↑y : E) +ᵥ x)
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw₈ : y +ᵥ x ∈ fundamentalDomain b ↔ y +ᵥ x = fract b (y +ᵥ x)
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
rw₂ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + -(↑(floor b x) : E)
rw₃ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x - (↑(floor b x) : E)
rw₄ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b x
rw₅ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b ((↑y : E) + x)
rw₆ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) + x = fract b ((↑y : E) + x)
rw₇ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) +ᵥ x = fract b ((↑y : E) +ᵥ x)
rw₈ : y +ᵥ x ∈ fundamentalDomain b ↔ y +ᵥ x = fract b (y +ᵥ x)
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw₉ : y +ᵥ x ∈ fundamentalDomain b ↔ fract b (y +ᵥ x) = y +ᵥ x
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))
x : E
rw : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) = (↑(-floor b x) : E)
rw₁ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + (↑(-floor b x) : E)
rw₂ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x + -(↑(floor b x) : E)
rw₃ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = x - (↑(floor b x) : E)
rw₄ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b x
rw₅ : y +ᵥ x ∈ fundamentalDomain b ↔ x + (↑y : E) = fract b ((↑y : E) + x)
rw₆ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) + x = fract b ((↑y : E) + x)
rw₇ : y +ᵥ x ∈ fundamentalDomain b ↔ (↑y : E) +ᵥ x = fract b ((↑y : E) +ᵥ x)
rw₈ : y +ᵥ x ∈ fundamentalDomain b ↔ y +ᵥ x = fract b (y +ᵥ x)
rw₉ : y +ᵥ x ∈ fundamentalDomain b ↔ fract b (y +ᵥ x) = y +ᵥ x
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
have rw₁₀ : fract b (y +ᵥ x) = y +ᵥ x ↔ fract b (y +ᵥ x) = y +ᵥ x
Tactic: rw [Subtype.ext_iff, ← add_right_inj x, NegMemClass.coe_neg, ← sub_eq_add_neg, ← fract_apply,
    ← fract_zSpan_add b _ (Subtype.mem y), add_comm, ← vadd_eq_add, ← vadd_def, eq_comm, ←
    fract_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 : Finite ι
x : E
⊢ ∃! v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))), v +ᵥ x ∈ fundamentalDomain b
have intro : ∀ (val : Fintype ι),
  ∃! v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))), v +ᵥ x ∈ 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
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 : Finite ι
x : E
val : Fintype ι
⊢ ∃! v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))), v +ᵥ x ∈ fundamentalDomain b
have intro : (fun (v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ↦ v +ᵥ x ∈ fundamentalDomain b) (-floor b x)
Tactic: refine ⟨-floor b x, ?_, fun y h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 : Finite ι
x : E
val : Fintype ι
intro :
  (fun (v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ↦ v +ᵥ x ∈ fundamentalDomain b)
    (-floor b x)
⊢ ∃! v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))), v +ᵥ x ∈ fundamentalDomain b
have intro₁ : ∀ (y : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))))
  (h : (fun (v : ↥(span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))) ↦ v +ᵥ x ∈ fundamentalDomain b) y),
  y = -floor b x
Tactic: refine ⟨-floor b x, ?_, fun y h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
⊢ HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) ≃
    (↑(fundamentalDomain b) : Type u_1)
have refine_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 Equiv.ofBijective ?_ ⟨fun x y => ?_, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 :
  HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) →
    (↑(fundamentalDomain b) : Type u_1)
⊢ HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) ≃
    (↑(fundamentalDomain b) : Type u_1)
have refine_2 : ∀ (x y : 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 x (fractRestrict b) sorry)
      (Quotient.liftOn y (fractRestrict b) sorry) →
    x = y
Tactic: refine Equiv.ofBijective ?_ ⟨fun x y => ?_, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 :
  HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) →
    (↑(fundamentalDomain b) : Type u_1)
refine_2 :
  ∀ (x y : 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 x (fractRestrict b) ⋯)
        (Quotient.liftOn y (fractRestrict b) ⋯) →
      x = y
⊢ HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) ≃
    (↑(fundamentalDomain b) : Type u_1)
have refine_3 : ∀ (x : (↑(fundamentalDomain b) : Type u_1)),
  ∃ (a : HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E)))),
    Quotient.liftOn a (fractRestrict b) sorry = x
Tactic: refine Equiv.ofBijective ?_ ⟨fun x y => ?_, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.ZLattice.Basic (goal)
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 ι
⊢ HasQuotient.Quotient E (B := Submodule ℤ E) (span ℤ (Set.range.{u_1, u_2 + 1} (ι := ι) (⇑b : (a : ι) → E))) →
    (↑(fundamentalDomain b) : Type u_1)
have 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)
Tactic: refine fun q => Quotient.liftOn q (fractRestrict b) (fun _ _ h => ?_)