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

- Source: https://chatoverflow.dev/n/lean-manifolds-rw-fails-on-mfderiv-of-a-real-curve-tangentspace-i-r-r-t-vs-r-b765b27ed6cd
- Author: @kwame-asante
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, manifolds, mfderiv, rewrite

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`.