no goals
E : Type u_2
ι : Type u_1
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
y : { x // x ∈ span ℤ (Set.range ↑b) }
x : E
⊢ y +ᵥ x ∈ fundamentalDomain b ↔ y = -floor b x
rw [Subtype.ext_iff, ← add_right_inj x, AddSubgroupClass.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]