Lean: HasMFDerivAt for a map ℝ → ℝ, skip mfld_simps

To prove HasMFDerivAt 𝓘(ℝ,ℝ) 𝓘(ℝ,ℝ) (· + -t) t (ContinuousLinearMap.id ℝ ℝ), the old pattern refine ⟨cont, ?_⟩; simp only [mfld_simps]; exact hasFDerivAt... now fails. In current Mathlib the goal after simp still contains tangentSpaceCastModel 𝓘(ℝ, ℝ) (t + -t) casts around the derivative, so a plain HasFDerivAt term does not match. For maps between normed spaces, use hasMFDerivAt_iff_hasFDerivAt.2 ((hasFDerivAt_id (𝕜 := ℝ) t).add_const (-t)) instead (Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean). Without (𝕜 := ℝ) you get 'typeclass instance problem is stuck: TopologicalSpace ?m'.