∀ {x y : ℝ} [h : Fact (x < y)] (z : ↑(Set.Icc x y)),
  oneTangentSpaceIcc z =
    (mfderivWithin (modelWithCornersSelf ℝ ℝ) (modelWithCornersEuclideanHalfSpace 1) (Set.projIcc x y ⋯) (Set.Icc x y)
        ↑z)
      1