Commit 2023-03-16 19:28 19ace550

fix a typo in Topology.Homotopy.Basic (#2921) The prop' field used continuous_to_fun instead of continuous_toFun. Lean 4 silently introduced an implicit argument continuous_to_fun, so one had to specify it in the .prop theorem below. Also golf a proof using new Lean 4 rfl for structures.