no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.131601
α : Type ?u.131604
β : Type u_3
ι : Type ?u.131610
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c : E
⊢ ConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
simpa only [add_comm c] using hf.translate_right c