defeq for the tangent space

Stream: mathlib4

[Yury G. Kudryashov]

Some lemmas in mathlib (ab)use the definitional equality between docs3#tangent_space and the model nored space using forced type cast.

[Yury G. Kudryashov]

Lean 4 likes it less than Lean 3.

[Yury G. Kudryashov]

I suggest that we add TangentSpace.out for this type of lemmas.

[Yury G. Kudryashov]

Example lemmas: docs3#mfderiv_add, docs3#mfderiv_congr_point

[Yury G. Kudryashov]

This non-reducible defeq is responsible for some of the remaining errors in #5454

[Heather Macbeth]

This was always an abuse (at least in the case of docs#mfderiv_add which is the one I've thought about most) -- happy to see it wrapped in some way.

[Yury G. Kudryashov]

BTW, is there any reason to use 1 instead of .id in lemmas like docs3#tangent_bundle.continuous_linear_map_at_model_space?

[Heather Macbeth]

@Floris van Doorn I think you wrote that lemma? For sphere eversion maybe?

[Yury G. Kudryashov]

BTW, #5439 and #5451 are ready for review

[Yury G. Kudryashov]

I think, it's easier to leave it as is for now (forcing types here and there) and decide later while forward-porting the sphere eversion project or writing some new code.

[Yury G. Kudryashov]

I'm away for an hour or two, so I marked #5454 as help-wanted

[Floris van Doorn]

Yes, I definitely did abuse some defeq of tangent_space. Maybe an explicit (continuous linear) equivalence is the way to go, but I conjecture it will be not very nice: the tangent space $T_x(M \times M')$ will then be only equivalent to $T_{\pi_1(x)}M\times T_{\pi_2(x)}M'$, and I preferred to silently identify them.

[Yury G. Kudryashov]

OK, I'll leave it as is for now.