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

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

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

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

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ HasDerivAt (g ∘ f) (g' * f') a

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

case eq2
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
⊢ (fun x => f x - f a) =O[𝓝 a] fun x => x - a
Tactic:
have h₂ :=
  calc (fun x ↦ (f x - f a) * g' - (x - a) * (g' * f'))
    _ = fun x ↦ g' * (f x - f a - (x - a) * f') := ?eq3
    _ =O[𝓝 a] fun x ↦ f x - f a - (x - a) * f' := ?eq4
    _ =o[𝓝 a] fun x ↦ x - a                    := ?eq5
State after:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
h₂ : (fun x => (f x - f a) * g' - (x - a) * (g' * f')) =o[𝓝 a] fun x => x - a
⊢ HasDerivAt (g ∘ f) (g' * f') a

case eq3
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => (f x - f a) * g' - (x - a) * (g' * f')) = fun x => g' * (f x - f a - (x - a) * f')

case eq4
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => g' * (f x - f a - (x - a) * f')) =O[𝓝 a] fun x => f x - f a - (x - a) * f'

case eq5
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a

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

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

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
h₂ : (fun x => (f x - f a) * g' - (x - a) * (g' * f')) =o[𝓝 a] fun x => x - a
⊢ HasDerivAt (g ∘ f) (g' * f') a

case eq3
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => (f x - f a) * g' - (x - a) * (g' * f')) = fun x => g' * (f x - f a - (x - a) * f')

case eq4
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => g' * (f x - f a - (x - a) * f')) =O[𝓝 a] fun x => f x - f a - (x - a) * f'

case eq5
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a

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

case eq2
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
⊢ (fun x => f x - f a) =O[𝓝 a] fun x => x - a
Tactic:
apply h₁.triangle h₂
State after:
case eq3
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => (f x - f a) * g' - (x - a) * (g' * f')) = fun x => g' * (f x - f a - (x - a) * f')

case eq4
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => g' * (f x - f a - (x - a) * f')) =O[𝓝 a] fun x => f x - f a - (x - a) * f'

case eq5
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a

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

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

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
⊢ (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => f x - f a
Tactic:
case eq1 =>
  apply hg.comp_tendsto
  apply hf.continuousAt
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
⊢ (fun x => f x - f a) =O[𝓝 a] fun x => x - a
Tactic:
case eq2 =>
  apply hf.isBigO_sub
State after:
no goals

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

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => g' * (f x - f a - (x - a) * f')) =O[𝓝 a] fun x => f x - f a - (x - a) * f'
Tactic:
case eq4 =>
  apply isBigO_const_mul_self
State after:
no goals

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

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
⊢ (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => f x - f a
Tactic:
apply hg.comp_tendsto
State after:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
⊢ Tendsto (fun x => f x) (𝓝 a) (𝓝 (f a))

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
⊢ Tendsto (fun x => f x) (𝓝 a) (𝓝 (f a))
Tactic:
apply hf.continuousAt
State after:
no goals

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
⊢ (fun x => f x - f a) =O[𝓝 a] fun x => x - a
Tactic:
apply hf.isBigO_sub
State after:
no goals

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

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

State before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' (f a)
h₁ : (fun x => g (f x) - g (f a) - (f x - f a) * g') =o[𝓝 a] fun x => x - a
⊢ (fun x => g' * (f x - f a - (x - a) * f')) =O[𝓝 a] fun x => f x - f a - (x - a) * f'
Tactic:
apply isBigO_const_mul_self
State after:
no goals

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