awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ Eq (α := ℝ) ((0 : (a : E) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ Eq (α := ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
exact if hf : DifferentiableWithinAt ℝ f s a then
    h.hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt hy hy'
  else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Premises used: Real, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ Eq (α := ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
classical
  exact if hf : DifferentiableWithinAt ℝ f s a then
    h.hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt hy hy'
  else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Premises used: Real, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
h₁ : ∀ (y : E), Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((0 : (a : E) → ℝ) y : ℝ)
⊢ f' = 0

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
h₁ : y ∈ posTangentConeAt univ a
h₂ : -y ∈ posTangentConeAt univ a
⊢ Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((0 : (a : E) → ℝ) y : ℝ)

Tactic:
apply (h.on univ).hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt, Set.univ, IsLocalMinOn.hasFDerivWithinAt_eq_zero, IsLocalMin.on
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
h₁ : Membership.mem (γ := Set E) univ y
⊢ y ∈ posTangentConeAt univ a

Tactic:
rw [posTangentConeAt_univ]

Premises used: posTangentConeAt_univ
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
h₁ : Membership.mem (γ := Set E) univ (-y)
⊢ -y ∈ posTangentConeAt univ a

Tactic:
rw [posTangentConeAt_univ]

Premises used: posTangentConeAt_univ
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ Membership.mem (γ := Set E) univ y

Tactic:
apply mem_univ

Premises used: Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ Membership.mem (γ := Set E) univ (-y)

Tactic:
apply mem_univ

Premises used: Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMin f a
⊢ Eq (α := E →L[ℝ] ℝ) (fderiv ℝ f a) 0

Tactic:
if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
  else fderiv_zero_of_not_differentiableAt hf

Premises used: dite, fderiv_zero_of_not_differentiableAt, DifferentiableAt.hasFDerivAt, IsLocalMin.hasFDerivAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMin f a
⊢ Eq (α := E →L[ℝ] ℝ) (fderiv ℝ f a) 0

Tactic:
exact if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
  else fderiv_zero_of_not_differentiableAt hf

Premises used: Real, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMin f a
⊢ Eq (α := E →L[ℝ] ℝ) (fderiv ℝ f a) 0

Tactic:
classical
  exact if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
  else fderiv_zero_of_not_differentiableAt hf

Premises used: Real, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMax f a
hf : HasFDerivAt f f' a
⊢ f' = 0

Tactic:
neg_eq_zero.1 <| h.neg.hasFDerivAt_eq_zero hf.neg

Premises used: neg_eq_zero, IsLocalMax.neg, Iff.mp, IsLocalMin.hasFDerivAt_eq_zero, HasFDerivAt.neg
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMax f a
⊢ Eq (α := E →L[ℝ] ℝ) (fderiv ℝ f a) 0

Tactic:
if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
  else fderiv_zero_of_not_differentiableAt hf

Premises used: IsLocalMax.hasFDerivAt_eq_zero, dite, fderiv_zero_of_not_differentiableAt, DifferentiableAt.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMax f a
⊢ Eq (α := E →L[ℝ] ℝ) (fderiv ℝ f a) 0

Tactic:
exact if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
  else fderiv_zero_of_not_differentiableAt hf

Premises used: Real, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalMax f a
⊢ Eq (α := E →L[ℝ] ℝ) (fderiv ℝ f a) 0

Tactic:
classical
  exact if hf : DifferentiableAt ℝ f a then h.hasFDerivAt_eq_zero hf.hasFDerivAt
  else fderiv_zero_of_not_differentiableAt hf

Premises used: Real, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalExtr f a
⊢ HasFDerivAt f f' a → f' = 0

Tactic:
h.elim IsLocalMin.hasFDerivAt_eq_zero IsLocalMax.hasFDerivAt_eq_zero

Premises used: IsLocalMax.hasFDerivAt_eq_zero, IsLocalExtr.elim, IsLocalMin.hasFDerivAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
a : E
h : IsLocalExtr f a
⊢ Eq (α := E →L[ℝ] ℝ) (fderiv ℝ f a) 0

Tactic:
h.elim IsLocalMin.fderiv_eq_zero IsLocalMax.fderiv_eq_zero

Premises used: IsLocalMax.fderiv_eq_zero, IsLocalExtr.elim, IsLocalMin.fderiv_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
mp : 1 ∈ posTangentConeAt s a → a ∈ closure (Ioi a ∩ s)
mpr : a ∈ closure (Ioi a ∩ s) → 1 ∈ posTangentConeAt s a
⊢ 1 ∈ posTangentConeAt s a ↔ a ∈ closure (Ioi a ∩ s)

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
mp :
  ∀ (ι : Type) (l : Filter ι) (hl : l.NeBot) (c : ι → ℝ≥0) (d : ι → ℝ) (hd₀ : Tendsto d l (𝓝 0))
    (hd : ∀ᶠ (n : ι) in l, a + d n ∈ s) (hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)),
    a ∈ closure (Ioi a ∩ s)
⊢ a ∈ closure (Ioi a ∩ s)

Tactic:
rcases exists_fun_of_mem_tangentConeAt h with ⟨ι, l, hl, c, d, hd₀, hd, hcd⟩

Premises used: exists_fun_of_mem_tangentConeAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
⊢ Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)

Tactic:
simpa only [add_zero] using tendsto_const_nhds.add hd₀

Premises used: tendsto_const_nhds, Filter.Tendsto.add, add_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
⊢ Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)

Tactic:
have : Tendsto (a + d ·) l (𝓝 a) := by
      simpa only [add_zero] using tendsto_const_nhds.add hd₀
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)
mp : ∀ᶠ (x : ι) in l, a + d x ∈ Ioi a ∩ s
⊢ a ∈ closure (Ioi a ∩ s)

Tactic:
apply mem_closure_of_tendsto this

Premises used: mem_closure_of_tendsto
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)
h₁ : ∀ (n : ι) (hcdn : 0 < c n • d n) (hdn : a + d n ∈ s), a + d n ∈ Ioi a ∩ s
⊢ ∀ᶠ (x : ι) in l, a + d x ∈ Ioi a ∩ s

Tactic:
filter_upwards [hcd.eventually_const_lt one_pos, hd] with n hcdn hdn

Premises used: Filter.Tendsto.eventually_const_lt, one_pos
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)
n : ι
hcdn : 0 < c n • d n
hdn : a + d n ∈ s
⊢ a + d n ∈ Ioi a ∩ s

Tactic:
⟨?_, hdn⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)
n : ι
hcdn : 0 < c n • d n
hdn : a + d n ∈ s
h₁ : a + d n ∈ Ioi a
⊢ a + d n ∈ Ioi a ∩ s

Tactic:
refine ⟨?_, hdn⟩
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)
n : ι
hcdn : 0 < c n • d n
hdn : a + d n ∈ s
⊢ a + d n ∈ Ioi a

Tactic:
simpa using pos_of_mul_pos_right hcdn

Premises used: pos_of_mul_pos_right
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : a ∈ closure (Ioi a ∩ s)
mpr : ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + HSMul.hSMul (β := ℝ) t 1 ∈ s
⊢ 1 ∈ posTangentConeAt s a

Tactic:
apply mem_posTangentConeAt_of_frequently_mem

Premises used: mem_posTangentConeAt_of_frequently_mem
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : a ∈ closure (Ioi a ∩ s)
⊢ ∃ᶠ (a_1 : ℝ) in 𝓝 0, a + a_1 ∈ Ioi a ∩ s

Tactic:
rw [mem_closure_iff_frequently, ← map_add_left_nhds_zero, frequently_map] at h

Premises used: mem_closure_iff_frequently, Filter.frequently_map, map_add_left_nhds_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
h : ∃ᶠ (a_1 : ℝ) in 𝓝 0, a + a_1 ∈ Ioi a ∩ s
⊢ ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + HSMul.hSMul (β := ℝ) t 1 ∈ s

Tactic:
simpa [nhdsWithin, frequently_inf_principal] using h

Premises used: nhdsWithin, Filter.frequently_inf_principal
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
rw : (∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∩ Ioi a) ↔ ∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∧ x ∈ Ioi a
⊢ 1 ∈ posTangentConeAt s a ↔ ∃ᶠ (x : ℝ) in 𝓝[>] a, x ∈ s

Tactic:
rw [one_mem_posTangentConeAt_iff_mem_closure, mem_closure_iff_frequently,
    frequently_nhdsWithin_iff, inter_comm]

Premises used: mem_closure_iff_frequently, one_mem_posTangentConeAt_iff_mem_closure, Set.inter_comm, frequently_nhdsWithin_iff
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
s : Set ℝ
a : ℝ
⊢ (∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∩ Ioi a) ↔ ∃ᶠ (x : ℝ) in 𝓝 a, x ∈ s ∧ x ∈ Ioi a

Tactic:
simp_rw [mem_inter_iff]

Premises used: Set.mem_inter_iff
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
f : ℝ → ℝ
f' a : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ f' = 0

Tactic:
simpa using DFunLike.congr_fun (h.hasFDerivAt_eq_zero (hasDerivAt_iff_hasFDerivAt.1 hf)) 1

Premises used: DFunLike.congr_fun, hasDerivAt_iff_hasFDerivAt, Iff.mp, IsLocalMin.hasFDerivAt_eq_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
f : ℝ → ℝ
a : ℝ
h : IsLocalMin f a
⊢ deriv f a = 0

Tactic:
if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt
  else deriv_zero_of_not_differentiableAt hf

Premises used: IsLocalMin.hasDerivAt_eq_zero, DifferentiableAt.hasDerivAt, deriv_zero_of_not_differentiableAt, dite
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
f : ℝ → ℝ
a : ℝ
h : IsLocalMin f a
⊢ deriv f a = 0

Tactic:
exact if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt
  else deriv_zero_of_not_differentiableAt hf

Premises used: Real, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
f : ℝ → ℝ
a : ℝ
h : IsLocalMin f a
⊢ deriv f a = 0

Tactic:
classical
  exact if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt
  else deriv_zero_of_not_differentiableAt hf

Premises used: Real, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
f : ℝ → ℝ
f' a : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ f' = 0

Tactic:
neg_eq_zero.1 <| h.neg.hasDerivAt_eq_zero hf.neg

Premises used: IsLocalMin.hasDerivAt_eq_zero, HasDerivAt.neg, neg_eq_zero, IsLocalMax.neg, Iff.mp
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
f : ℝ → ℝ
a : ℝ
h : IsLocalMax f a
⊢ deriv f a = 0

Tactic:
if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt
  else deriv_zero_of_not_differentiableAt hf

Premises used: DifferentiableAt.hasDerivAt, deriv_zero_of_not_differentiableAt, dite, IsLocalMax.hasDerivAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
f : ℝ → ℝ
a : ℝ
h : IsLocalMax f a
⊢ deriv f a = 0

Tactic:
exact if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt
  else deriv_zero_of_not_differentiableAt hf

Premises used: Real, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
f : ℝ → ℝ
a : ℝ
h : IsLocalMax f a
⊢ deriv f a = 0

Tactic:
classical
  exact if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt
  else deriv_zero_of_not_differentiableAt hf

Premises used: Real, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
f : ℝ → ℝ
f' a : ℝ
h : IsLocalExtr f a
⊢ HasDerivAt f f' a → f' = 0

Tactic:
h.elim IsLocalMin.hasDerivAt_eq_zero IsLocalMax.hasDerivAt_eq_zero

Premises used: IsLocalMin.hasDerivAt_eq_zero, IsLocalExtr.elim, IsLocalMax.hasDerivAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
f : ℝ → ℝ
a : ℝ
h : IsLocalExtr f a
⊢ deriv f a = 0

Tactic:
h.elim IsLocalMin.deriv_eq_zero IsLocalMax.deriv_eq_zero

Premises used: IsLocalMax.deriv_eq_zero, IsLocalExtr.elim, IsLocalMin.deriv_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
a b : E
f' : ℝ
l : Filter E
h : IsExtrFilter f l a
hd : HasLineDerivAt ℝ f f' a b
h' : Tendsto (fun (t : ℝ) ↦ a + t • b) (𝓝 0) l
⊢ IsExtrFilter f l (a + HSMul.hSMul (α := ℝ) 0 b)

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
a b : E
l : Filter E
h : IsExtrFilter f l a
h' : Tendsto (fun (t : ℝ) ↦ a + t • b) (𝓝 0) l
⊢ lineDeriv ℝ f a b = 0

Tactic:
if hd : LineDifferentiableAt ℝ f a b then
    h.hasLineDerivAt_eq_zero hd.hasLineDerivAt h'
  else
    lineDeriv_zero_of_not_lineDifferentiableAt hd

Premises used: dite, lineDeriv_zero_of_not_lineDifferentiableAt, LineDifferentiableAt.hasLineDerivAt, IsExtrFilter.hasLineDerivAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
a b : E
l : Filter E
h : IsExtrFilter f l a
h' : Tendsto (fun (t : ℝ) ↦ a + t • b) (𝓝 0) l
⊢ lineDeriv ℝ f a b = 0

Tactic:
exact if hd : LineDifferentiableAt ℝ f a b then
    h.hasLineDerivAt_eq_zero hd.hasLineDerivAt h'
  else
    lineDeriv_zero_of_not_lineDifferentiableAt hd

Premises used: Real, LineDifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
a b : E
l : Filter E
h : IsExtrFilter f l a
h' : Tendsto (fun (t : ℝ) ↦ a + t • b) (𝓝 0) l
⊢ lineDeriv ℝ f a b = 0

Tactic:
classical
  exact if hd : LineDifferentiableAt ℝ f a b then
    h.hasLineDerivAt_eq_zero hd.hasLineDerivAt h'
  else
    lineDeriv_zero_of_not_lineDifferentiableAt hd

Premises used: Real, LineDifferentiableAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
f' : ℝ
h : IsExtrOn f s a
hd : HasLineDerivAt ℝ f f' a b
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ f' = 0

Tactic:
IsExtrFilter.hasLineDerivAt_eq_zero h hd <| tendsto_principal.2 h'

Premises used: Iff.mpr, Filter.tendsto_principal, IsExtrFilter.hasLineDerivAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
h : IsExtrOn f s a
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ lineDeriv ℝ f a b = 0

Tactic:
IsExtrFilter.lineDeriv_eq_zero h <| tendsto_principal.2 h'

Premises used: Iff.mpr, Filter.tendsto_principal, IsExtrFilter.lineDeriv_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
f' : ℝ
h : IsMinOn f s a
hd : HasLineDerivAt ℝ f f' a b
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ f' = 0

Tactic:
h.isExtr.hasLineDerivAt_eq_zero hd h'

Premises used: IsMinOn.isExtr, IsExtrOn.hasLineDerivAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
h : IsMinOn f s a
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ lineDeriv ℝ f a b = 0

Tactic:
h.isExtr.lineDeriv_eq_zero h'

Premises used: IsExtrOn.lineDeriv_eq_zero, IsMinOn.isExtr
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
f' : ℝ
h : IsMaxOn f s a
hd : HasLineDerivAt ℝ f f' a b
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ f' = 0

Tactic:
h.isExtr.hasLineDerivAt_eq_zero hd h'

Premises used: IsMaxOn.isExtr, IsExtrOn.hasLineDerivAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
h : IsMaxOn f s a
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ lineDeriv ℝ f a b = 0

Tactic:
h.isExtr.lineDeriv_eq_zero h'

Premises used: IsMaxOn.isExtr, IsExtrOn.lineDeriv_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
f' : ℝ
h : IsExtrOn f s a
hd : HasLineDerivWithinAt ℝ f f' s a b
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ f' = 0

Tactic:
h.hasLineDerivAt_eq_zero (hd.hasLineDerivAt' h') h'

Premises used: HasLineDerivWithinAt.hasLineDerivAt', IsExtrOn.hasLineDerivAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
h : IsExtrOn f s a
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ lineDerivWithin ℝ f s a b = 0

Tactic:
if hd : LineDifferentiableWithinAt ℝ f s a b then
    h.hasLineDerivWithinAt_eq_zero hd.hasLineDerivWithinAt h'
  else
    lineDerivWithin_zero_of_not_lineDifferentiableWithinAt hd

Premises used: lineDerivWithin_zero_of_not_lineDifferentiableWithinAt, LineDifferentiableWithinAt.hasLineDerivWithinAt, dite, IsExtrOn.hasLineDerivWithinAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
h : IsExtrOn f s a
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ lineDerivWithin ℝ f s a b = 0

Tactic:
exact if hd : LineDifferentiableWithinAt ℝ f s a b then
    h.hasLineDerivWithinAt_eq_zero hd.hasLineDerivWithinAt h'
  else
    lineDerivWithin_zero_of_not_lineDifferentiableWithinAt hd

Premises used: Real, LineDifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
h : IsExtrOn f s a
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ lineDerivWithin ℝ f s a b = 0

Tactic:
classical
  exact if hd : LineDifferentiableWithinAt ℝ f s a b then
    h.hasLineDerivWithinAt_eq_zero hd.hasLineDerivWithinAt h'
  else
    lineDerivWithin_zero_of_not_lineDifferentiableWithinAt hd

Premises used: Real, LineDifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
f' : ℝ
h : IsMinOn f s a
hd : HasLineDerivWithinAt ℝ f f' s a b
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ f' = 0

Tactic:
h.isExtr.hasLineDerivWithinAt_eq_zero hd h'

Premises used: IsMinOn.isExtr, IsExtrOn.hasLineDerivWithinAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
h : IsMinOn f s a
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ lineDerivWithin ℝ f s a b = 0

Tactic:
h.isExtr.lineDerivWithin_eq_zero h'

Premises used: IsExtrOn.lineDerivWithin_eq_zero, IsMinOn.isExtr
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
f' : ℝ
h : IsMaxOn f s a
hd : HasLineDerivWithinAt ℝ f f' s a b
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ f' = 0

Tactic:
h.isExtr.hasLineDerivWithinAt_eq_zero hd h'

Premises used: IsMaxOn.isExtr, IsExtrOn.hasLineDerivWithinAt_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
f : E → ℝ
s : Set E
a b : E
h : IsMaxOn f s a
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ lineDerivWithin ℝ f s a b = 0

Tactic:
h.isExtr.lineDerivWithin_eq_zero h'

Premises used: IsMaxOn.isExtr, IsExtrOn.lineDerivWithin_eq_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
f : E → ℝ
a b : E
f' : ℝ
h : IsLocalExtr f a
hd : HasLineDerivAt ℝ f f' a b
⊢ Continuous[_, inst_2] fun (t : ℝ) ↦ a + t • b

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
f : E → ℝ
a b : E
f' : ℝ
h : IsLocalExtr f a
hd : HasLineDerivAt ℝ f f' a b
⊢ a + HSMul.hSMul (α := ℝ) 0 b = a

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
f : E → ℝ
a : E
h : IsLocalExtr f a
b : E
⊢ Continuous[_, inst_2] fun (t : ℝ) ↦ a + t • b

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
f : E → ℝ
a : E
h : IsLocalExtr f a
b : E
⊢ a + HSMul.hSMul (α := ℝ) 0 b = a

Tactic:
simp