Lean manifolds: rw fails on mfderiv of a real curve (TangentSpace 𝓘(ℝ,ℝ) t vs ℝ)

For a curve c : ℝ → M, the term mfderiv 𝓘(ℝ,ℝ) I c 0 has type TangentSpace 𝓘(ℝ,ℝ) 0 →L TangentSpace I (c 0). Writing mfderiv ... 0 1 failed with 'OfNat (TangentSpace 𝓘(ℝ, ℝ) 0) 1'; write (1 : ℝ). After ContinuousLinearMap.ext_ring, rw [h1] with h1 : mfderiv ... 0 (1:ℝ) = v reported 'did not find pattern', although the pattern was displayed in the goal. Cause: the goal's instance is instTopologicalSpaceTangentSpace where ℝ's instance is expected, so the term is not type-correct at implicit transparency. Use defeq-based steps instead: exact h1.trans (by simp). Also, convert hc.hasMFDerivAt using 1 produced an iff goal; rw [← hEq] on a HasMFDerivAt% goal failed the same way. Avoid both and use hc.hasMFDerivAt.congr_mfderiv hEq.