𝕜 : Type ?u.246282
E : Type ?u.246285
F : Type ?u.246288
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y => (-y + x) ^ (n + 1)) (-(↑n + 1) * (-t + x) ^ n) t
𝕜 : Type ?u.246282
E : Type ?u.246285
F : Type ?u.246288
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y => (x - y) ^ (n + 1)) (-(↑n + 1) * (x - t) ^ n) t
simp_rw [sub_eq_neg_add]
𝕜 : Type ?u.246282
E : Type ?u.246285
F : Type ?u.246288
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y => (-y + x) ^ (n + 1)) ((↑n + 1) * (-t + x) ^ n * -1) t
𝕜 : Type ?u.246282
E : Type ?u.246285
F : Type ?u.246288
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y => (-y + x) ^ (n + 1)) (-(↑n + 1) * (-t + x) ^ n) t
rw [← neg_one_mul, mul_comm (-1 : ℝ), mul_assoc, mul_comm (-1 : ℝ), ← mul_assoc]
case h.e'_7.h.e'_5.h.e'_5
𝕜 : Type ?u.246282
E : Type ?u.246285
F : Type ?u.246288
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t x : ℝ
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)
𝕜 : Type ?u.246282
E : Type ?u.246285
F : Type ?u.246288
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y => (-y + x) ^ (n + 1)) ((↑n + 1) * (-t + x) ^ n * -1) t
convert HasDerivAt.pow (n + 1) ((hasDerivAt_id t).neg.add_const x)
no goals
case h.e'_7.h.e'_5.h.e'_5
𝕜 : Type ?u.246282
E : Type ?u.246285
F : Type ?u.246288
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t x : ℝ
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)
simp only [Nat.cast_add, Nat.cast_one]