chore(analysis/calculus/{f,}deriv): fix, add missing lemmas (#8574)

* use `prod.fst` and `prod.snd` in lemmas like `has_fderiv_at_fst`;
* add `has_strict_deriv_at.prod`,
  `has_strict_fderiv_at.comp_has_strict_deriv_at`;
* use `set.maps_to` in some lemmas;
* golf some proofs.

src/analysis/calculus/deriv.lean

@@ -981,8 +981,7 @@ variables {f₂ : 𝕜 → G} {f₂' : G}
 lemma has_deriv_at_filter.prod
   (hf₁ : has_deriv_at_filter f₁ f₁' x L) (hf₂ : has_deriv_at_filter f₂ f₂' x L) :
   has_deriv_at_filter (λ x, (f₁ x, f₂ x)) (f₁', f₂') x L :=
-show has_fderiv_at_filter _ _ _ _,
-by convert has_fderiv_at_filter.prod hf₁ hf₂
+hf₁.prod hf₂
 
 lemma has_deriv_within_at.prod
   (hf₁ : has_deriv_within_at f₁ f₁' s x) (hf₂ : has_deriv_within_at f₂ f₂' s x) :
@@ -993,6 +992,11 @@ lemma has_deriv_at.prod (hf₁ : has_deriv_at f₁ f₁' x) (hf₂ : has_deriv_a
   has_deriv_at (λ x, (f₁ x, f₂ x)) (f₁', f₂') x :=
 hf₁.prod hf₂
 
+lemma has_strict_deriv_at.prod (hf₁ : has_strict_deriv_at f₁ f₁' x)
+  (hf₂ : has_strict_deriv_at f₂ f₂' x) :
+  has_strict_deriv_at (λ x, (f₁ x, f₂ x)) (f₁', f₂') x :=
+hf₁.prod hf₂
+
 end cartesian_product
 
 section composition
@@ -1177,57 +1181,47 @@ end composition
 section composition_vector
 /-! ### Derivative of the composition of a function between vector spaces and a function on `𝕜` -/
 
+open continuous_linear_map
+
 variables {l : F → E} {l' : F →L[𝕜] E}
 variable (x)
 
 /-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative within a set
 equal to the Fréchet derivative of `l` applied to the derivative of `f`. -/
 theorem has_fderiv_within_at.comp_has_deriv_within_at {t : set F}
-  (hl : has_fderiv_within_at l l' t (f x)) (hf : has_deriv_within_at f f' s x) (hst : s ⊆ f ⁻¹' t) :
-  has_deriv_within_at (l ∘ f) (l' (f')) s x :=
-begin
-  rw has_deriv_within_at_iff_has_fderiv_within_at,
-  convert has_fderiv_within_at.comp x hl hf hst,
-  ext,
-  simp
-end
+  (hl : has_fderiv_within_at l l' t (f x)) (hf : has_deriv_within_at f f' s x)
+  (hst : maps_to f s t) :
+  has_deriv_within_at (l ∘ f) (l' f') s x :=
+by simpa only [one_apply, one_smul, smul_right_apply, coe_comp', (∘)]
+  using (hl.comp x hf.has_fderiv_within_at hst).has_deriv_within_at
+
+theorem has_fderiv_at.comp_has_deriv_within_at
+  (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_within_at f f' s x) :
+  has_deriv_within_at (l ∘ f) (l' f') s x :=
+hl.has_fderiv_within_at.comp_has_deriv_within_at x hf (maps_to_univ _ _)
 
 /-- The composition `l ∘ f` where `l : F → E` and `f : 𝕜 → F`, has a derivative equal to the
 Fréchet derivative of `l` applied to the derivative of `f`. -/
-theorem has_fderiv_at.comp_has_deriv_at
-  (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_at f f' x) :
-  has_deriv_at (l ∘ f) (l' (f')) x :=
-begin
-  rw has_deriv_at_iff_has_fderiv_at,
-  convert has_fderiv_at.comp x hl hf,
-  ext,
-  simp
-end
+theorem has_fderiv_at.comp_has_deriv_at (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_at f f' x) :
+  has_deriv_at (l ∘ f) (l' f') x :=
+has_deriv_within_at_univ.mp $ hl.comp_has_deriv_within_at x hf.has_deriv_within_at
 
-theorem has_fderiv_at.comp_has_deriv_within_at
-  (hl : has_fderiv_at l l' (f x)) (hf : has_deriv_within_at f f' s x) :
-  has_deriv_within_at (l ∘ f) (l' (f')) s x :=
-begin
-  rw ← has_fderiv_within_at_univ at hl,
-  exact has_fderiv_within_at.comp_has_deriv_within_at x hl hf subset_preimage_univ
-end
+theorem has_strict_fderiv_at.comp_has_strict_deriv_at
+  (hl : has_strict_fderiv_at l l' (f x)) (hf : has_strict_deriv_at f f' x) :
+  has_strict_deriv_at (l ∘ f) (l' f') x :=
+by simpa only [one_apply, one_smul, smul_right_apply, coe_comp', (∘)]
+  using (hl.comp x hf.has_strict_fderiv_at).has_strict_deriv_at
 
 lemma fderiv_within.comp_deriv_within {t : set F}
   (hl : differentiable_within_at 𝕜 l t (f x)) (hf : differentiable_within_at 𝕜 f s x)
-  (hs : s ⊆ f ⁻¹' t) (hxs : unique_diff_within_at 𝕜 s x) :
+  (hs : maps_to f s t) (hxs : unique_diff_within_at 𝕜 s x) :
   deriv_within (l ∘ f) s x = (fderiv_within 𝕜 l t (f x) : F → E) (deriv_within f s x) :=
-begin
-  apply has_deriv_within_at.deriv_within _ hxs,
-  exact (hl.has_fderiv_within_at).comp_has_deriv_within_at x (hf.has_deriv_within_at) hs
-end
+(hl.has_fderiv_within_at.comp_has_deriv_within_at x hf.has_deriv_within_at hs).deriv_within hxs
 
 lemma fderiv.comp_deriv
   (hl : differentiable_at 𝕜 l (f x)) (hf : differentiable_at 𝕜 f x) :
   deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : F → E) (deriv f x) :=
-begin
-  apply has_deriv_at.deriv _,
-  exact (hl.has_fderiv_at).comp_has_deriv_at x (hf.has_deriv_at)
-end
+(hl.has_fderiv_at.comp_has_deriv_at x hf.has_deriv_at).deriv
 
 end composition_vector
 

src/analysis/calculus/fderiv.lean

@@ -1253,30 +1253,30 @@ section fst
 
 variables {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} {p : E × F}
 
-lemma has_strict_fderiv_at_fst : has_strict_fderiv_at (fst 𝕜 E F) (fst 𝕜 E F) p :=
+lemma has_strict_fderiv_at_fst : has_strict_fderiv_at (@prod.fst E F) (fst 𝕜 E F) p :=
 (fst 𝕜 E F).has_strict_fderiv_at
 
 protected lemma has_strict_fderiv_at.fst (h : has_strict_fderiv_at f₂ f₂' x) :
   has_strict_fderiv_at (λ x, (f₂ x).1) ((fst 𝕜 F G).comp f₂') x :=
 has_strict_fderiv_at_fst.comp x h
 
 lemma has_fderiv_at_filter_fst {L : filter (E × F)} :
-  has_fderiv_at_filter (fst 𝕜 E F) (fst 𝕜 E F) p L :=
+  has_fderiv_at_filter (@prod.fst E F) (fst 𝕜 E F) p L :=
 (fst 𝕜 E F).has_fderiv_at_filter
 
 protected lemma has_fderiv_at_filter.fst (h : has_fderiv_at_filter f₂ f₂' x L) :
   has_fderiv_at_filter (λ x, (f₂ x).1) ((fst 𝕜 F G).comp f₂') x L :=
 has_fderiv_at_filter_fst.comp x h
 
-lemma has_fderiv_at_fst : has_fderiv_at (fst 𝕜 E F) (fst 𝕜 E F) p :=
+lemma has_fderiv_at_fst : has_fderiv_at (@prod.fst E F) (fst 𝕜 E F) p :=
 has_fderiv_at_filter_fst
 
 protected lemma has_fderiv_at.fst (h : has_fderiv_at f₂ f₂' x) :
   has_fderiv_at (λ x, (f₂ x).1) ((fst 𝕜 F G).comp f₂') x :=
 h.fst
 
 lemma has_fderiv_within_at_fst {s : set (E × F)} :
-  has_fderiv_within_at (fst 𝕜 E F) (fst 𝕜 E F) s p :=
+  has_fderiv_within_at (@prod.fst E F) (fst 𝕜 E F) s p :=
 has_fderiv_at_filter_fst
 
 protected lemma has_fderiv_within_at.fst (h : has_fderiv_within_at f₂ f₂' s x) :
@@ -1331,30 +1331,30 @@ section snd
 
 variables {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G} {p : E × F}
 
-lemma has_strict_fderiv_at_snd : has_strict_fderiv_at (snd 𝕜 E F) (snd 𝕜 E F) p :=
+lemma has_strict_fderiv_at_snd : has_strict_fderiv_at (@prod.snd E F) (snd 𝕜 E F) p :=
 (snd 𝕜 E F).has_strict_fderiv_at
 
 protected lemma has_strict_fderiv_at.snd (h : has_strict_fderiv_at f₂ f₂' x) :
   has_strict_fderiv_at (λ x, (f₂ x).2) ((snd 𝕜 F G).comp f₂') x :=
 has_strict_fderiv_at_snd.comp x h
 
 lemma has_fderiv_at_filter_snd {L : filter (E × F)} :
-  has_fderiv_at_filter (snd 𝕜 E F) (snd 𝕜 E F) p L :=
+  has_fderiv_at_filter (@prod.snd E F) (snd 𝕜 E F) p L :=
 (snd 𝕜 E F).has_fderiv_at_filter
 
 protected lemma has_fderiv_at_filter.snd (h : has_fderiv_at_filter f₂ f₂' x L) :
   has_fderiv_at_filter (λ x, (f₂ x).2) ((snd 𝕜 F G).comp f₂') x L :=
 has_fderiv_at_filter_snd.comp x h
 
-lemma has_fderiv_at_snd : has_fderiv_at (snd 𝕜 E F) (snd 𝕜 E F) p :=
+lemma has_fderiv_at_snd : has_fderiv_at (@prod.snd E F) (snd 𝕜 E F) p :=
 has_fderiv_at_filter_snd
 
 protected lemma has_fderiv_at.snd (h : has_fderiv_at f₂ f₂' x) :
   has_fderiv_at (λ x, (f₂ x).2) ((snd 𝕜 F G).comp f₂') x :=
 h.snd
 
 lemma has_fderiv_within_at_snd {s : set (E × F)} :
-  has_fderiv_within_at (snd 𝕜 E F) (snd 𝕜 E F) s p :=
+  has_fderiv_within_at (@prod.snd E F) (snd 𝕜 E F) s p :=
 has_fderiv_at_filter_snd
 
 protected lemma has_fderiv_within_at.snd (h : has_fderiv_within_at f₂ f₂' s x) :
@@ -1409,16 +1409,14 @@ section prod_map
 
 variables {f₂ : G → G'} {f₂' : G →L[𝕜] G'} {y : G} (p : E × G)
 
--- TODO (Lean 3.8): use `prod.map f f₂``
-
 protected theorem has_strict_fderiv_at.prod_map (hf : has_strict_fderiv_at f f' p.1)
   (hf₂ : has_strict_fderiv_at f₂ f₂' p.2) :
-  has_strict_fderiv_at (λ p : E × G, (f p.1, f₂ p.2)) (f'.prod_map f₂') p :=
+  has_strict_fderiv_at (prod.map f f₂) (f'.prod_map f₂') p :=
 (hf.comp p has_strict_fderiv_at_fst).prod (hf₂.comp p has_strict_fderiv_at_snd)
 
 protected theorem has_fderiv_at.prod_map (hf : has_fderiv_at f f' p.1)
   (hf₂ : has_fderiv_at f₂ f₂' p.2) :
-  has_fderiv_at (λ p : E × G, (f p.1, f₂ p.2)) (f'.prod_map f₂') p :=
+  has_fderiv_at (prod.map f f₂) (f'.prod_map f₂') p :=
 (hf.comp p has_fderiv_at_fst).prod (hf₂.comp p has_fderiv_at_snd)
 
 @[simp] protected theorem differentiable_at.prod_map (hf : differentiable_at 𝕜 f p.1)