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

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
⊢ HasDerivAt (fun x => f x + g x) (f' + g') a
Tactic:
rw [hasDerivAt_iff_isLittleO] at *
State after:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x + g x - (f a + g a) - (x - a) * (f' + g')) =o[𝓝 a] fun x => x - a

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x + g x - (f a + g a) - (x - a) * (f' + g')) =o[𝓝 a] fun x => x - a
Tactic:
calc (fun x ↦ f x + g x - (f a + g a) - (x - a) * (f' + g'))
  _ = fun x ↦ (f x - f a - (x - a) * f') + (g x - g a - (x - a) * g') := ?eq1
  _ =o[𝓝 a] fun x ↦ x - a                                            := ?eq2
State after:
case eq1
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x + g x - (f a + g a) - (x - a) * (f' + g')) = fun x =>
    f x - f a - (x - a) * f' + (g x - g a - (x - a) * g')

case eq2
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x - f a - (x - a) * f' + (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x + g x - (f a + g a) - (x - a) * (f' + g')) = fun x =>
    f x - f a - (x - a) * f' + (g x - g a - (x - a) * g')
Tactic:
case eq1 =>
  funext x
  ring
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x - f a - (x - a) * f' + (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
Tactic:
case eq2 =>
  apply IsLittleO.add hf hg
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x + g x - (f a + g a) - (x - a) * (f' + g')) = fun x =>
    f x - f a - (x - a) * f' + (g x - g a - (x - a) * g')
Tactic:
funext x
State after:
case h
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
x : ℝ
⊢ f x + g x - (f a + g a) - (x - a) * (f' + g') = f x - f a - (x - a) * f' + (g x - g a - (x - a) * g')

State before:
case h
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
x : ℝ
⊢ f x + g x - (f a + g a) - (x - a) * (f' + g') = f x - f a - (x - a) * f' + (g x - g a - (x - a) * g')
Tactic:
ring
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
hg : (fun x => g x - g a - (x - a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x - f a - (x - a) * f' + (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
Tactic:
apply IsLittleO.add hf hg
State after:
no goals