[Merged by Bors] - feat(Analysis/Calculus/DSlope): add eq_smul_dslope_of_zero and iterated version

Mathlib/Analysis/Calculus/DSlope.lean

@@ -141,3 +141,19 @@ theorem differentiableOn_dslope_of_notMem (h : a ∉ s) :
 theorem differentiableAt_dslope_of_ne (h : b ≠ a) :
     DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b := by
   simp only [← differentiableWithinAt_univ, differentiableWithinAt_dslope_of_ne h]
+
+lemma sub_smul_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (hf : f a = 0) (b : 𝕜) :
+    (b - a) • dslope f a b = f b := by
+  simp [hf]
+
+lemma pow_sub_smul_iterate_dslope_of_zero {f : 𝕜 → E} {a : 𝕜} (n : ℕ)
+    (hf : ∀ k < n, (Function.swap dslope a)^[k] f a = 0) (b : 𝕜) :
+    (b - a) ^ n • (Function.swap dslope a)^[n] f b = f b := by
+  induction n generalizing f with
+  | zero => simp
+  | succ n ih =>
+    rw [Function.iterate_succ_apply', pow_succ, mul_smul]
+    have hf_n : (Function.swap dslope a)^[n] f a = 0 := hf n (Nat.lt_succ_self n)
+    have hf_lt : ∀ k < n, (Function.swap dslope a)^[k] f a = 0 :=
+      fun k hk => hf k (Nat.lt_trans hk (Nat.lt_succ_self n))
+    rw [sub_smul_dslope_of_zero hf_n b, ih hf_lt]