Theorem: Tutorial.hasDerivAt_pow (Solution/Advanced/Analysis/Lecture1.lean)

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' : ℝ
n : ℕ
a : ℝ
⊢ HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
Tactic:
induction n
State after:
case zero
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
⊢ HasDerivAt (fun x => x ^ (Nat.zero + 1)) ((↑Nat.zero + 1) * a ^ Nat.zero) a

case succ
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n✝ : ℕ
n_ih✝ : HasDerivAt (fun x => x ^ (n✝ + 1)) ((↑n✝ + 1) * a ^ n✝) a
⊢ HasDerivAt (fun x => x ^ (Nat.succ n✝ + 1)) ((↑(Nat.succ n✝) + 1) * a ^ Nat.succ n✝) a

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
⊢ HasDerivAt (fun x => x ^ (Nat.zero + 1)) ((↑Nat.zero + 1) * a ^ Nat.zero) a
Tactic:
case zero => simp [hasDerivAt_iff_isLittleO_nhds_zero]
State after:
no goals

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (Nat.succ n + 1)) ((↑(Nat.succ n) + 1) * a ^ Nat.succ n) a
Tactic:
case succ n ih =>
  rw [Nat.succ_eq_add_one]
  suffices HasDerivAt (fun x => x ^ (n + 1) * x) (((n + 1) * a ^ n) * a + a ^ (n + 1) * 1) a by
    apply IsLittleO.congr_left this
    intro x
    simp
    ring
  apply ih.mul (hasDerivAt_id a)
State after:
no goals

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
⊢ HasDerivAt (fun x => x ^ (Nat.zero + 1)) ((↑Nat.zero + 1) * a ^ Nat.zero) a
Tactic:
simp [hasDerivAt_iff_isLittleO_nhds_zero]
State after:
no goals

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (Nat.succ n + 1)) ((↑(Nat.succ n) + 1) * a ^ Nat.succ n) a
Tactic:
rw [Nat.succ_eq_add_one]
State after:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (n + 1 + 1)) ((↑(n + 1) + 1) * a ^ (n + 1)) a

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (n + 1 + 1)) ((↑(n + 1) + 1) * a ^ (n + 1)) a
Tactic:
suffices HasDerivAt (fun x => x ^ (n + 1) * x) (((n + 1) * a ^ n) * a + a ^ (n + 1) * 1) a by
  apply IsLittleO.congr_left this
  intro x
  simp
  ring
State after:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
⊢ HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
Tactic:
apply ih.mul (hasDerivAt_id a)
State after:
no goals

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
⊢ HasDerivAt (fun x => x ^ (n + 1 + 1)) ((↑(n + 1) + 1) * a ^ (n + 1)) a
Tactic:
apply IsLittleO.congr_left this
State after:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
⊢ ∀ (x : ℝ),
    (fun x => x ^ (n + 1) * x) x - (fun x => x ^ (n + 1) * x) a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) =
      (fun x => x ^ (n + 1 + 1)) x - (fun x => x ^ (n + 1 + 1)) a - (x - a) * ((↑(n + 1) + 1) * a ^ (n + 1))

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
⊢ ∀ (x : ℝ),
    (fun x => x ^ (n + 1) * x) x - (fun x => x ^ (n + 1) * x) a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) =
      (fun x => x ^ (n + 1 + 1)) x - (fun x => x ^ (n + 1 + 1)) a - (x - a) * ((↑(n + 1) + 1) * a ^ (n + 1))
Tactic:
intro x
State after:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
x : ℝ
⊢ (fun x => x ^ (n + 1) * x) x - (fun x => x ^ (n + 1) * x) a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) =
    (fun x => x ^ (n + 1 + 1)) x - (fun x => x ^ (n + 1 + 1)) a - (x - a) * ((↑(n + 1) + 1) * a ^ (n + 1))

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
x : ℝ
⊢ (fun x => x ^ (n + 1) * x) x - (fun x => x ^ (n + 1) * x) a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) =
    (fun x => x ^ (n + 1 + 1)) x - (fun x => x ^ (n + 1 + 1)) a - (x - a) * ((↑(n + 1) + 1) * a ^ (n + 1))
Tactic:
simp
State after:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
x : ℝ
⊢ x ^ (n + 1) * x - a ^ (n + 1) * a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1)) =
    x ^ (n + 1 + 1) - a ^ (n + 1 + 1) - (x - a) * ((↑n + 1 + 1) * a ^ (n + 1))

State before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' a : ℝ
n : ℕ
ih : HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
this : HasDerivAt (fun x => x ^ (n + 1) * x) ((↑n + 1) * a ^ n * a + a ^ (n + 1) * 1) a
x : ℝ
⊢ x ^ (n + 1) * x - a ^ (n + 1) * a - (x - a) * ((↑n + 1) * a ^ n * a + a ^ (n + 1)) =
    x ^ (n + 1 + 1) - a ^ (n + 1 + 1) - (x - a) * ((↑n + 1 + 1) * a ^ (n + 1))
Tactic:
ring
State after:
no goals