no goals
α : Type u_3
β : Type u_2
inst✝⁴ : LinearOrderedField α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
G : Type u_1
inst✝¹ : SMul G β
inst✝ : IsScalarTower G β β
f1 f2 : CauSeq β abv
c : G
hf : f1 ≈ f2
⊢ c • f1 ≈ c • f2
simpa [const_smul, smul_one_mul _ _] using
  mul_equiv_mul (const_equiv.mpr <| Eq.refl <| c • (1 : β)) hf