∀ {X : Type u_1} {E : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : IsTopologicalAddGroup E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] (f g : C(X, E))
  (x : ↑unitInterval × X), (ContinuousMap.Homotopy.affine f g) x = (AffineMap.lineMap (f x.2) (g x.2)) ↑x.1