feat(analysis/calculus/fderiv): define has_strict_fderiv_at (#2249)

* Move code aroud

* general constructions (product, chain rule) before arithmetic;
* bundled `E →L[𝕜] F` maps before unbundled

* Use `maps_to` instead of `f '' _ ⊆ _`

* feat(analysis/calculus/fderiv): define `has_strict_fderiv_at`

Prove strict differentiability of all functions found in this file, cleanup.

* Update src/analysis/calculus/fderiv.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Docs, var name

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/algebra/pi_instances.lean

@@ -250,6 +250,8 @@ lemma snd.is_monoid_hom [monoid α] [monoid β] : is_monoid_hom (prod.snd : α 
 
 @[simp] lemma fst_sub [add_group α] [add_group β] : (p - q).1 = p.1 - q.1 := rfl
 @[simp] lemma snd_sub [add_group α] [add_group β] : (p - q).2 = p.2 - q.2 := rfl
+@[simp] lemma mk_sub_mk [add_group α] [add_group β] {a₁ a₂ : α} {b₁ b₂ : β} :
+  (a₁, b₁) - (a₂, b₂) = (a₁ - a₂, b₁ - b₂) := rfl
 
 /-- Given monoids `α, β`, the natural projection homomorphism from `α × β` to `α`. -/
 @[to_additive prod.add_monoid_hom.fst "Given add_monoids `α, β`, the natural projection homomorphism from `α × β` to `α`."]

src/analysis/asymptotics.lean

@@ -407,6 +407,12 @@ lemma is_O_fst_prod : is_O f' (λ x, (f' x, g' x)) l := is_O_with_fst_prod.is_O
 
 lemma is_O_snd_prod : is_O g' (λ x, (f' x, g' x)) l := is_O_with_snd_prod.is_O
 
+lemma is_O_fst_prod' {f' : α → E' × F'} : is_O (λ x, (f' x).1) f' l :=
+is_O_fst_prod
+
+lemma is_O_snd_prod' {f' : α → E' × F'} : is_O (λ x, (f' x).2) f' l :=
+is_O_snd_prod
+
 section
 
 variables (f' k')