So i am currently learning Lean4 and i am really confused about the refine command. I just cant figure out where my mistake is in the following simple code:

example (x y : X) : 0 ≤ dist x y := by
  have h : 0 ≤ 2*dist x y := by
    have h' := dist_triangle x y x
    rw [dist_comm y x, dist_self, <-two_mul] at h'
  refine @easy3 _ _ (0 : ℝ) (2 * dist x y) (2⁻¹) h _

The first part is fine. The easy3 theorem is

theorem easy3 (h : a ≤ b) (h' : 0 ≤ c) : a * c ≤ b * c

Lean4 tells me that i have a type mismatch type mismatch and that it expects to obtain something of type 0 ≤ dist x y. But this is not what i want. Thank you for helping me!