Theorem: Tutorial.HasDerivAt.mul (Tutorial/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 =>
  sorry
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:
case eq2 =>
  have hf' : (fun x ↦ g a * (f x - f a - (x - a) * f')) =o[𝓝 a] fun x ↦ x - a := by
    sorry
  have hg' : (fun x ↦ f a * (g x - g a - (x - a) * g')) =o[𝓝 a] fun x ↦ x - a := by
    sorry
  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
  sorry
  case eq3 =>
    have hg'' : (fun x ↦ g x - g a) =o[𝓝 a] fun _ ↦ (1 : ℝ) := by
      rw [Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff]
      sorry
    sorry
  case eq4 =>
    sorry
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:
sorry
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
  sorry
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
  sorry
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:
sorry
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 => (f x - f a) * (g x - g a)) =o[𝓝 a] fun x => (x - a) * 1
Tactic:
case eq3 =>
  have hg'' : (fun x ↦ g x - g a) =o[𝓝 a] fun _ ↦ (1 : ℝ) := by
    rw [Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff]
    sorry
  sorry
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:
case eq4 =>
  sorry
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:
sorry
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:
sorry
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]
  sorry
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:
sorry
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 => 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:
sorry
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:
sorry
State after:
no goals