internlm/Lean-Github huggingface dataset:
Theorem: Tutorial.HasDerivAt.add
Proof 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
Proof 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')
Theorem: Tutorial.HasDerivAt.add
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.add
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.const_mul
Proof state before:
f : ℝ → ℝ
f' a c : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => c * f x - c * f a - (x - a) * (c * f')) =o[𝓝 a] fun x => x - a
Tactic:
calc (fun x ↦  c * f x - c * f a - (x - a) * (c * f'))
  _ = fun x ↦ c * (f x - f a - (x - a) * f') := ?eq1
  _ =o[𝓝 a] fun x ↦ x - a                   := ?eq2
Proof state after:
case eq1
f : ℝ → ℝ
f' a c : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => c * f x - c * f a - (x - a) * (c * f')) = fun x => c * (f x - f a - (x - a) * f')

case eq2
f : ℝ → ℝ
f' a c : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => c * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
Theorem: Tutorial.HasDerivAt.const_mul
Proof state before:
f : ℝ → ℝ
f' a c : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => c * f x - c * f a - (x - a) * (c * f')) = fun x => c * (f x - f a - (x - a) * f')
Tactic:
case eq1 =>
  funext x
  ring
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.const_mul
Proof state before:
f : ℝ → ℝ
f' a c : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => c * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
Tactic:
case eq2 =>
  apply IsLittleO.const_mul_left hf c
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.const_mul
Proof state before:
f : ℝ → ℝ
f' a c : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => c * f x - c * f a - (x - a) * (c * f')) = fun x => c * (f x - f a - (x - a) * f')
Tactic:
funext x
Proof state after:
case h
f : ℝ → ℝ
f' a c : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
x : ℝ
⊢ c * f x - c * f a - (x - a) * (c * f') = c * (f x - f a - (x - a) * f')
Theorem: Tutorial.HasDerivAt.const_mul
Proof state before:
case h
f : ℝ → ℝ
f' a c : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
x : ℝ
⊢ c * f x - c * f a - (x - a) * (c * f') = c * (f x - f a - (x - a) * f')
Tactic:
ring
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.const_mul
Proof state before:
f : ℝ → ℝ
f' a c : ℝ
hf : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => c * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x => x - a
Tactic:
apply IsLittleO.const_mul_left hf c
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.isBigO_sub
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => (x - a) * f') = fun x => f' * (x - a)
Tactic:
case eq1 =>
  funext x
  ring
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.isBigO_sub
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => f' * (x - a)) =O[𝓝 a] fun x => x - a
Tactic:
case eq2 =>
  apply isBigO_const_mul_self
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.isBigO_sub
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => (x - a) * f') = fun x => f' * (x - a)
Tactic:
funext x
Proof state after:
case h
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
x : ℝ
⊢ (x - a) * f' = f' * (x - a)
Theorem: Tutorial.HasDerivAt.isBigO_sub
Proof state before:
case h
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
x : ℝ
⊢ (x - a) * f' = f' * (x - a)
Tactic:
ring
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.isBigO_sub
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => f' * (x - a)) =O[𝓝 a] fun x => x - a
Tactic:
apply isBigO_const_mul_self
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof 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))
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof 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')
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.comp
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof 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))
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof 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
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof 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
Theorem: Tutorial.HasDerivAt.mul
Proof 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'
Proof 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
Theorem: Tutorial.HasDerivAt.mul
Proof 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'
Proof 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
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof 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
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof 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
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof 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
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.mul
Proof 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''
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof 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
Theorem: Tutorial.HasDerivAt.mul
Proof 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
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_pow
Proof state before:
f : ℝ → ℝ
f' a✝ : ℝ
g : ℝ → ℝ
g' : ℝ
n : ℕ
a : ℝ
⊢ HasDerivAt (fun x => x ^ (n + 1)) ((↑n + 1) * a ^ n) a
Tactic:
induction n
Proof 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
Theorem: Tutorial.hasDerivAt_pow
Proof 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]
Proof state after:
no goals