internlm/Lean-Github huggingface dataset:
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ (∀ (a : G₁), f a = 1 → a = 1) → ker f = ⊥
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ range f = ⊤ ↔ Function.Surjective ⇑f
Tactic:
constructor
Proof state after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ range f = ⊤ → Function.Surjective ⇑f

case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ Function.Surjective ⇑f → range f = ⊤
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ range f = ⊤ → Function.Surjective ⇑f
Tactic:
intro hrange y
Proof state after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
⊢ ∃ a, f a = y
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
⊢ ∃ a, f a = y
Tactic:
have hy : y ∈ (⊤ : Subgroup G₂) := by
  sorry
Proof state after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ ⊤
⊢ ∃ a, f a = y
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
hy : y ∈ ⊤
⊢ ∃ a, f a = y
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hrange : range f = ⊤
y : G₂
⊢ y ∈ ⊤
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ Function.Surjective ⇑f → range f = ⊤
Tactic:
intro hsurj
Proof state after:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
⊢ range f = ⊤
Theorem: Tutorial.GroupHom.range_eq_top
Proof state before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
hsurj : Function.Surjective ⇑f
⊢ range f = ⊤
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.homToPerm_injective
Proof state before:
G : Type
inst✝ : Group G
⊢ Function.Injective ⇑(homToPerm G)
Tactic:
rw [injective_iff_map_eq_one]
Proof state after:
G : Type
inst✝ : Group G
⊢ ∀ (a : G), (homToPerm G) a = 1 → a = 1
Theorem: Tutorial.homToPerm_injective
Proof state before:
G : Type
inst✝ : Group G
⊢ ∀ (a : G), (homToPerm G) a = 1 → a = 1
Tactic:
intro a h
Proof state after:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ a = 1
Theorem: Tutorial.homToPerm_injective
Proof state before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ a = 1
Tactic:
calc
  a = a * 1 := by simp
  _ = (homToPerm G a) 1 := by
    sorry
  _ = 1 := by
    sorry
Proof state after:
no goals
Theorem: Tutorial.homToPerm_injective
Proof state before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ a = a * 1
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.homToPerm_injective
Proof state before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ a * 1 = ((homToPerm G) a) 1
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.homToPerm_injective
Proof state before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ ((homToPerm G) a) 1 = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_isLittleO
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
Tactic:
rfl
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_isLittleO_nhds_zero
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ (fun h => f (a + h) - f a - h * f') =o[𝓝 0] fun h => h
Tactic:
rw [hasDerivAt_iff_isLittleO, ← map_add_left_nhds_zero a, Asymptotics.isLittleO_map]
Proof state after:
f : ℝ → ℝ
f' a : ℝ
⊢ ((fun x => f x - f a - (x - a) * f') ∘ fun x => a + x) =o[𝓝 0] ((fun x => x - a) ∘ fun x => a + x) ↔
    (fun h => f (a + h) - f a - h * f') =o[𝓝 0] fun h => h
Theorem: Tutorial.hasDerivAt_iff_tendsto
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝[≠] a) (𝓝 0)
Tactic:
calc HasDerivAt f f' a
  _ ↔ Tendsto (fun x ↦ (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0)      := ?iff1
  _ ↔ Tendsto (fun x ↦ (f x - f a - (x - a) * f') / (x - a)) (𝓝[≠] a) (𝓝 0)   := ?iff2
Proof state after:
case iff1
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0)

case iff2
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝[≠] a) (𝓝 0)
Theorem: Tutorial.hasDerivAt_iff_tendsto
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0)
Tactic:
case iff1 => rw [hasDerivAt_iff_isLittleO, Asymptotics.isLittleO_iff_tendsto (by intro _ h; simp [sub_eq_zero.1 h])]
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝[≠] a) (𝓝 0)
Tactic:
case iff2 => exact .symm <| tendsto_inf_principal_nhds_iff_of_forall_eq <| by simp
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0)
Tactic:
rw [hasDerivAt_iff_isLittleO, Asymptotics.isLittleO_iff_tendsto (by intro _ h; simp [sub_eq_zero.1 h])]
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ ∀ (x : ℝ), x - a = 0 → f x - f a - (x - a) * f' = 0
Tactic:
intro _ h
Proof state after:
f : ℝ → ℝ
f' a x✝ : ℝ
h : x✝ - a = 0
⊢ f x✝ - f a - (x✝ - a) * f' = 0
Theorem: Tutorial.hasDerivAt_iff_tendsto
Proof state before:
f : ℝ → ℝ
f' a x✝ : ℝ
h : x✝ - a = 0
⊢ f x✝ - f a - (x✝ - a) * f' = 0
Tactic:
simp [sub_eq_zero.1 h]
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝 a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a - (x - a) * f') / (x - a)) (𝓝[≠] a) (𝓝 0)
Tactic:
exact .symm <| tendsto_inf_principal_nhds_iff_of_forall_eq <| by simp
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ ∀ a_1 ∉ {a}ᶜ, (f a_1 - f a - (a_1 - a) * f') / (a_1 - a) = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto_slope
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
Tactic:
calc HasDerivAt f f' a
  _ ↔ Tendsto (fun x ↦ (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0) := ?iff1
  _ ↔ Tendsto (fun x ↦ (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0)                     := ?iff2
  _ ↔ Tendsto (fun x ↦ (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')                         := ?iff3
Proof state after:
case iff1
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0)

case iff2
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0)

case iff3
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
Theorem: Tutorial.hasDerivAt_iff_tendsto_slope
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0)
Tactic:
case iff1 => simp only [hasDerivAt_iff_tendsto, sub_div, mul_div_right_comm]
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto_slope
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0)
Tactic:
case iff2 => exact tendsto_congr' <| (Set.EqOn.eventuallyEq fun _ h ↦ (by field_simp [sub_ne_zero.2 h])).filter_mono inf_le_right
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto_slope
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
Tactic:
case iff3 => rw [← nhds_translation_sub f', tendsto_comap_iff]; rfl
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto_slope
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ HasDerivAt f f' a ↔ Tendsto (fun x => (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0)
Tactic:
simp only [hasDerivAt_iff_tendsto, sub_div, mul_div_right_comm]
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto_slope
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - (x - a) / (x - a) * f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0)
Tactic:
exact tendsto_congr' <| (Set.EqOn.eventuallyEq fun _ h ↦ (by field_simp [sub_ne_zero.2 h])).filter_mono inf_le_right
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto_slope
Proof state before:
f : ℝ → ℝ
f' a x✝ : ℝ
h : x✝ ∈ {a}ᶜ
⊢ (f x✝ - f a) / (x✝ - a) - (x✝ - a) / (x✝ - a) * f' = (f x✝ - f a) / (x✝ - a) - f'
Tactic:
field_simp [sub_ne_zero.2 h]
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_iff_tendsto_slope
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
Tactic:
rw [← nhds_translation_sub f', tendsto_comap_iff]
Proof state after:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto ((fun x => x - f') ∘ fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 0)
Theorem: Tutorial.hasDerivAt_iff_tendsto_slope
Proof state before:
f : ℝ → ℝ
f' a : ℝ
⊢ Tendsto (fun x => (f x - f a) / (x - a) - f') (𝓝[≠] a) (𝓝 0) ↔
    Tendsto ((fun x => x - f') ∘ fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 0)
Tactic:
rfl
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_const
Proof state before:
f : ℝ → ℝ
f' a c : ℝ
⊢ HasDerivAt (fun x => c) 0 a
Tactic:
rw [hasDerivAt_iff_isLittleO]
Proof state after:
f : ℝ → ℝ
f' a c : ℝ
⊢ (fun x => c - c - (x - a) * 0) =o[𝓝 a] fun x => x - a
Theorem: Tutorial.hasDerivAt_const
Proof state before:
f : ℝ → ℝ
f' a c : ℝ
⊢ (fun x => c - c - (x - a) * 0) =o[𝓝 a] fun x => x - a
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.hasDerivAt_id
Proof state before:
f : ℝ → ℝ
f' a✝ a : ℝ
⊢ HasDerivAt id 1 a
Tactic:
rw [hasDerivAt_iff_isLittleO]
Proof state after:
f : ℝ → ℝ
f' a✝ a : ℝ
⊢ (fun x => id x - id a - (x - a) * 1) =o[𝓝 a] fun x => x - a
Theorem: Tutorial.hasDerivAt_id
Proof state before:
f : ℝ → ℝ
f' a✝ a : ℝ
⊢ (fun x => id x - id a - (x - a) * 1) =o[𝓝 a] fun x => x - a
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.add
Proof state before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
⊢ HasDerivAt (fun x => f x + g x) (f' + g') a
Tactic:
rw [hasDerivAt_iff_isLittleO] at *
Proof state after:
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')) =o[𝓝 a] fun x => x - a
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')) =o[𝓝 a] fun x => x - a
Tactic:
calc (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') := ?eq1
  _ =o[𝓝 a] fun x ↦ x - a                                            := ?eq2
Proof state after:
case eq1
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')

case eq2
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
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:
case eq1 =>
  sorry
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:
case eq2 =>
  sorry
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 + 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:
sorry
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:
sorry
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.const_mul
Proof state before:
f : ℝ → ℝ
f' a c : ℝ
hf : HasDerivAt f f' a
⊢ HasDerivAt (fun x => c * f x) (c * f') a
Tactic:
rw [hasDerivAt_iff_isLittleO] at *
Proof state after:
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
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:
sorry
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.neg
Proof state before:
f : ℝ → ℝ
f' a : ℝ
hf : HasDerivAt f f' a
this : HasDerivAt (fun x => -1 * f x) (-1 * f') a
⊢ HasDerivAt (fun x => -f x) (-f') a
Tactic:
simpa using this
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.sub
Proof state before:
f : ℝ → ℝ
f' a : ℝ
g : ℝ → ℝ
g' : ℝ
hf : HasDerivAt f f' a
hg : HasDerivAt g g' a
this : HasDerivAt (fun x => f x + -g x) (f' + -g') a
⊢ HasDerivAt (fun x => f x - g x) (f' - g') a
Tactic:
simpa [sub_eq_add_neg] using this
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.isBigO_sub
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ (fun x => f x - f a) =O[𝓝 a] fun x => x - a
Tactic:
rw [hasDerivAt_iff_isLittleO] at h
Proof state after:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => f x - f a) =O[𝓝 a] fun x => x - a
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 - f a) =O[𝓝 a] fun x => x - a
Tactic:
rw [h.isBigO.congr_of_sub]
Proof state after:
f : ℝ → ℝ
f' a : ℝ
h : (fun x => f x - f a - (x - a) * f') =o[𝓝 a] fun x => x - a
⊢ (fun x => (x - a) * f') =O[𝓝 a] fun x => x - a
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') =O[𝓝 a] fun x => x - a
Tactic:
calc (fun x ↦ (x - a) * f')
  _ = fun x ↦ f' * (x - a)  := ?eq1
  _ =O[𝓝 a] fun x ↦ x - a  := ?eq2
Proof state after:
case eq1
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)

case eq2
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
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 =>
  sorry
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 =>
  sorry
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:
sorry
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:
sorry
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.continuousAt
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
Tactic:
have : Tendsto (fun x ↦ f x - f a + f a) (𝓝 a) (𝓝 (0 + f a)) := by
  apply Tendsto.add _ tendsto_const_nhds
  apply h.isBigO_sub.trans_tendsto
  rw [← sub_self a]
  apply tendsto_id.sub tendsto_const_nhds
Proof state after:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
this : Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (0 + f a))
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
Theorem: Tutorial.HasDerivAt.continuousAt
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
this : Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (0 + f a))
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
Tactic:
rw [zero_add] at this
Proof state after:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
this : Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (f a))
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
Theorem: Tutorial.HasDerivAt.continuousAt
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
this : Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (f a))
⊢ Tendsto f (𝓝 a) (𝓝 (f a))
Tactic:
exact this.congr (by simp)
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.continuousAt
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (0 + f a))
Tactic:
apply Tendsto.add _ tendsto_const_nhds
Proof state after:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => f x - f a) (𝓝 a) (𝓝 0)
Theorem: Tutorial.HasDerivAt.continuousAt
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => f x - f a) (𝓝 a) (𝓝 0)
Tactic:
apply h.isBigO_sub.trans_tendsto
Proof state after:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => x - a) (𝓝 a) (𝓝 0)
Theorem: Tutorial.HasDerivAt.continuousAt
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => x - a) (𝓝 a) (𝓝 0)
Tactic:
rw [← sub_self a]
Proof state after:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => x - a) (𝓝 a) (𝓝 (a - a))
Theorem: Tutorial.HasDerivAt.continuousAt
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
⊢ Tendsto (fun x => x - a) (𝓝 a) (𝓝 (a - a))
Tactic:
apply tendsto_id.sub tendsto_const_nhds
Proof state after:
no goals
Theorem: Tutorial.HasDerivAt.continuousAt
Proof state before:
f : ℝ → ℝ
f' a : ℝ
h : HasDerivAt f f' a
this : Tendsto (fun x => f x - f a + f a) (𝓝 a) (𝓝 (f a))
⊢ ∀ (x : ℝ), f x - f a + f a = f x
Tactic:
simp
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)
⊢ 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
Proof 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
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
⊢ 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
Proof 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