internlm/Lean-Github huggingface dataset:
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
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₂
Proof 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
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 =>
  sorry
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 =>
  sorry
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 =>
  sorry
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 =>
  sorry
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 =>
  sorry
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:
sorry
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:
sorry
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:
sorry
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:
sorry
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:
sorry
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
⊢ HasDerivAt (fun x => f x * g x) (f' * g a + f a * g') a
Tactic:
rw [hasDerivAt_iff_isLittleO]
Proof 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
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')) =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
Proof 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
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 =>
  sorry
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:
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
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:
sorry
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
  sorry
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
  sorry
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
⊢ (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
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 => 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
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:
sorry
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 => (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
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:
case eq4 =>
  sorry
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:
sorry
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:
sorry
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]
  sorry
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:
sorry
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 => g x - g a) =o[𝓝 a] fun x => 1
Tactic:
rw [Asymptotics.isLittleO_one_iff, tendsto_sub_nhds_zero_iff]
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
⊢ Tendsto (fun x => g x) (𝓝 a) (𝓝 (g 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
⊢ Tendsto (fun x => g x) (𝓝 a) (𝓝 (g a))
Tactic:
sorry
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:
sorry
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:
sorry
Proof state after:
no goals
Theorem: Tutorial.inv_mul_cancel_left
Proof state before:
A : Type ?u.1517
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * (a * b) = b
Tactic:
calc
  a⁻¹ * (a * b) = (a⁻¹ * a) * b := by
    sorry
  _ = 1 * b := by
    sorry
  _ = b := by
    sorry
Proof state after:
no goals
Theorem: Tutorial.inv_mul_cancel_left
Proof state before:
A : Type ?u.1517
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * (a * b) = a⁻¹ * a * b
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.inv_mul_cancel_left
Proof state before:
A : Type ?u.1517
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * a * b = 1 * b
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.inv_mul_cancel_left
Proof state before:
A : Type ?u.1517
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ 1 * b = b
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.mul_left_cancel
Proof state before:
A : Type ?u.2016
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
⊢ a * x = a * y → x = y
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.mul_one
Proof state before:
A : Type ?u.2142
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a * 1 = a
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.mul_inv_self
Proof state before:
A : Type ?u.2284
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a * a⁻¹ = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.mul_inv_cancel_left
Proof state before:
A : Type ?u.2445
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * (a⁻¹ * b) = b
Tactic:
rw [← mul_assoc]
Proof state after:
A : Type ?u.2445
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * a⁻¹ * b = b
Theorem: Tutorial.mul_inv_cancel_left
Proof state before:
A : Type ?u.2445
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * a⁻¹ * b = b
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.mul_inv_cancel_right
Proof state before:
A : Type ?u.2639
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b * b⁻¹ = a
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.inv_mul_cancel_right
Proof state before:
A : Type ?u.2795
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b⁻¹ * b = a
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.mul_right_cancel
Proof state before:
A : Type ?u.2951
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
⊢ x * a = y * a → x = y
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.inv_eq_of_mul_eq_one_left
Proof state before:
A : Type ?u.3077
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x : G
⊢ x * a = 1 → a⁻¹ = x
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.inv_one
Proof state before:
A : Type ?u.3411
G : Type
inst✝¹ : Ring A
inst✝ : Group G
⊢ 1⁻¹ = 1
Tactic:
apply inv_eq_of_mul_eq_one_left
Proof state after:
case a
A : Type ?u.3411
G : Type
inst✝¹ : Ring A
inst✝ : Group G
⊢ 1 * 1 = 1
Theorem: Tutorial.inv_one
Proof state before:
case a
A : Type ?u.3411
G : Type
inst✝¹ : Ring A
inst✝ : Group G
⊢ 1 * 1 = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.inv_inv
Proof state before:
A : Type ?u.3529
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a : G
⊢ a⁻¹⁻¹ = a
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.mul_inv_rev
Proof state before:
A : Type ?u.3654
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.mul_inv_eq_iff_eq_mul
Proof state before:
A : Type ?u.3816
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b c : G
⊢ a * b⁻¹ = c ↔ a = c * b
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.mul_inv_eq_one
Proof state before:
A : Type ?u.3960
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a * b⁻¹ = 1 ↔ a = b
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.inv_mul_eq_one
Proof state before:
A : Type ?u.4111
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * b = 1 ↔ a = b
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Subgroup.inv_mem_iff
Proof state before:
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a⁻¹ ∈ H ↔ a ∈ H
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.inv_mul_cancel_left
Proof state before:
A : Type ?u.2656
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * (a * b) = b
Tactic:
calc
  a⁻¹ * (a * b) = (a⁻¹ * a) * b := by
    rw [mul_assoc]
    _ = 1 * b := by
    simp
    _ = b := by
    simp
Proof state after:
no goals
Theorem: Tutorial.inv_mul_cancel_left
Proof state before:
A : Type ?u.2656
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * (a * b) = a⁻¹ * a * b
Tactic:
rw [mul_assoc]
Proof state after:
no goals
Theorem: Tutorial.inv_mul_cancel_left
Proof state before:
A : Type ?u.2656
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ a⁻¹ * a * b = 1 * b
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.inv_mul_cancel_left
Proof state before:
A : Type ?u.2656
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a b : G
⊢ 1 * b = b
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_left_cancel
Proof state before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
⊢ a * x = a * y → x = y
Tactic:
intro h
Proof state after:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ x = y
Theorem: Tutorial.mul_left_cancel
Proof state before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ x = y
Tactic:
calc
  x = 1 * x := by simp
  _ = (a⁻¹ * a) * x := by simp
  _ = a⁻¹ * (a * x) := by rw [mul_assoc]
  _ = a⁻¹ * (a * y) := by rw [h]
  _ = (a⁻¹ * a) * y := by rw [← mul_assoc]
  _ = 1 * y := by simp
  _ = y := by simp
Proof state after:
no goals
Theorem: Tutorial.mul_left_cancel
Proof state before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ x = 1 * x
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_left_cancel
Proof state before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ 1 * x = a⁻¹ * a * x
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.mul_left_cancel
Proof state before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ a⁻¹ * a * x = a⁻¹ * (a * x)
Tactic:
rw [mul_assoc]
Proof state after:
no goals