feat(geometry/manifold/mfderiv): more lemmas (#6679)

* move section `mfderiv_fderiv` up, add aliases;
* rename old `unique_mdiff_on.unique_diff_on` to `unique_mdiff_on.unique_diff_on_target_inter`;
* add a section about `continuous_linear_map`;
* more lemmas about `model_with_corners`;
* add lemmas about `ext_chart_at`.

Author: urkud

src/analysis/calculus/fderiv.lean

@@ -650,6 +650,10 @@ lemma has_fderiv_within_at.congr (h : has_fderiv_within_at f f' s x) (hs : ∀x
   (hx : f₁ x = f x) : has_fderiv_within_at f₁ f' s x :=
 h.congr_mono hs hx (subset.refl _)
 
+lemma has_fderiv_within_at.congr' (h : has_fderiv_within_at f f' s x) (hs : ∀x ∈ s, f₁ x = f x)
+  (hx : x ∈ s) : has_fderiv_within_at f₁ f' s x :=
+h.congr hs (hs x hx)
+
 lemma has_fderiv_within_at.congr_of_eventually_eq (h : has_fderiv_within_at f f' s x)
   (h₁ : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x) : has_fderiv_within_at f₁ f' s x :=
 has_fderiv_at_filter.congr_of_eventually_eq h h₁ hx