no goals
E : Type u_3
ι : Type u_2
K : Type u_1
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ ↑(↑b.repr ↑(ceil b m)) i = ↑⌈↑(↑b.repr m) i⌉
classical simp only [ceil, zsmul_eq_smul_cast K, b.repr.map_smul, Finsupp.single_apply,
  Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
  Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, LinearEquiv.map_sum]
no goals
E : Type u_3
ι : Type u_2
K : Type u_1
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
i : ι
⊢ ↑(↑b.repr ↑(ceil b m)) i = ↑⌈↑(↑b.repr m) i⌉
simp only [ceil, zsmul_eq_smul_cast K, b.repr.map_smul, Finsupp.single_apply,
Finset.sum_apply', Basis.repr_self, Finsupp.smul_single', mul_one, Finset.sum_ite_eq', coe_sum,
Finset.mem_univ, if_true, coe_smul_of_tower, Basis.restrictScalars_apply, LinearEquiv.map_sum]