no goals
α : Type u_1
β : Type u_2
γ : Type ?u.8961
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
s : Set α
hf : AntilipschitzWith K (Set.restrict s f)
g : β → α
t : Set β
g_maps : MapsTo g t s
g_inv : RightInvOn g f t
x y : ↑t
⊢ edist (Set.restrict t g x) (Set.restrict t g y) ≤ ↑K * edist x y
simpa only [restrict_apply, g_inv x.mem, g_inv y.mem, Subtype.edist_eq, Subtype.coe_mk] using
  hf ⟨g x, g_maps x.mem⟩ ⟨g y, g_maps y.mem⟩