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

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

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

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

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

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

State before:
case h
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
x✝ : ℝ
⊢ f x✝ * g x✝ - f a * g a - (x✝ - a) * (f' * g a + f a * g') =
    g a * (f x✝ - f a - (x✝ - a) * f') + (f a * (g x✝ - g a - (x✝ - a) * g') + (f x✝ - f a) * (g x✝ - g a))
Tactic:
ring
State after:
no goals

State before:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
⊢ (fun x => g a * (f x - f a - (x - a) * f') + (f a * (g x - g a - (x - a) * g') + (f x - f a) * (g x - g a))) =o[𝓝 a]
    fun x => x - a
Tactic:
have hf' : (fun x ↦ g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x ↦ x - a := by
  apply IsLittleO.const_mul_left hf
State after:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
⊢ (fun x => g a * (f x - f a - (x - a) * f') + (f a * (g x - g a - (x - a) * g') + (f x - f a) * (g x - g a))) =o[𝓝 a]
    fun x => x - a

State before:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
⊢ (fun x => g a * (f x - f a - (x - a) * f') + (f a * (g x - g a - (x - a) * g') + (f x - f a) * (g x - g a))) =o[𝓝 a]
    fun x => x - a
Tactic:
have hg' : (fun x ↦ f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x ↦ x - a := by
  apply IsLittleO.const_mul_left hg
State after:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
⊢ (fun x => g a * (f x - f a - (x - a) * f') + (f a * (g x - g a - (x - a) * g') + (f x - f a) * (g x - g a))) =o[𝓝 a]
    fun x => x - a

State before:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
⊢ (fun x => g a * (f x - f a - (x - a) * f') + (f a * (g x - g a - (x - a) * g') + (f x - f a) * (g x - g a))) =o[𝓝 a]
    fun x => x - a
Tactic:
have hfg :=
  calc (fun x ↦ (f x - f a) * (g x - g a))
    _ =o[𝓝 a] fun x ↦ (x - a) * 1      := ?eq3
    _ = fun x ↦ x - a                   := ?eq4
State after:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
hfg : (fun x => (f x - f a) * (g x - g a)) =o[𝓝 a] fun x => x - a
⊢ (fun x => g a * (f x - f a - (x - a) * f') + (f a * (g x - g a - (x - a) * g') + (f x - f a) * (g x - g a))) =o[𝓝 a]
    fun x => x - a

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

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

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

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

case eq4
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
⊢ (fun x => (x - a) * 1) = fun x => x - a
Tactic:
apply IsLittleO.add hf'
State after:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
hfg : (fun x => (f x - f a) * (g x - g a)) =o[𝓝 a] fun x => x - a
⊢ (fun x => f a * (g x - g a - (x - a) * g') + (f x - f a) * (g x - g a)) =o[𝓝 a] fun x => x - a

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

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

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

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

case eq4
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
⊢ (fun x => (x - a) * 1) = fun x => x - a
Tactic:
apply IsLittleO.add hg'
State after:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
hfg : (fun x => (f x - f a) * (g x - g a)) =o[𝓝 a] fun x => x - a
⊢ (fun x => (f x - f a) * (g x - g a)) =o[𝓝 a] fun x => x - a

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

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

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

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

case eq4
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
⊢ (fun x => (x - a) * 1) = fun x => x - a
Tactic:
apply hfg
State after:
case eq3
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
⊢ (fun x => (f x - f a) * (g x - g a)) =o[𝓝 a] fun x => (x - a) * 1

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

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

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

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

State before:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
⊢ (fun x => (f x - f a) * (g x - g a)) =o[𝓝 a] fun x => (x - a) * 1
Tactic:
have hg'' : (fun x ↦ g x - g a) =o[𝓝 a] fun _ ↦ (1 : ℝ) := by
  rw [Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff]
  apply hg.continuousAt
State after:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
hg'' : (fun x => g x - g a) =o[𝓝 a] fun x => 1
⊢ (fun x => (f x - f a) * (g x - g a)) =o[𝓝 a] fun x => (x - a) * 1

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

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

State before:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
⊢ (fun x => g x - g a) =o[𝓝 a] fun x => 1
Tactic:
rw [Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff]
State after:
f✝ : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
f : ℝ → ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
hf' : (fun x => g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
hg' : (fun x => f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x => x - a
⊢ Tendsto (fun x => g x) (𝓝 a) (𝓝 (g a))

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

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

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

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

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