awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
inst_10 : MeasurableSpace F
inst_11 : BorelSpace F
hf : Continuous f
this_1 : MeasurableSpace 𝕜 := borel 𝕜
this_2 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
⊢ Measurable.{u_2, u_3} (β := F) fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2

Tactic:
(measurable_deriv_with_param this).comp measurable_prodMk_right

Premises used: measurable_deriv_with_param, Measurable.comp, deriv, measurable_prodMk_right, lineDeriv
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
inst_10 : MeasurableSpace F
inst_11 : BorelSpace F
hf : Continuous f
this_1 : MeasurableSpace 𝕜 := borel 𝕜
this_2 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
⊢ Measurable.{u_2, u_3} (β := F) fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2

Tactic:
exact (measurable_deriv_with_param this).comp measurable_prodMk_right

Premises used: measurable_deriv_with_param, Measurable.comp, measurable_prodMk_right
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
this_1 : MeasurableSpace 𝕜 := borel 𝕜
this_2 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
⊢ StronglyMeasurable.{u_2, u_3} (β := F) fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2

Tactic:
(stronglyMeasurable_deriv_with_param this).comp_measurable measurable_prodMk_right

Premises used: deriv, measurable_prodMk_right, MeasureTheory.StronglyMeasurable.comp_measurable, stronglyMeasurable_deriv_with_param, lineDeriv
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
this_1 : MeasurableSpace 𝕜 := borel 𝕜
this_2 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
⊢ StronglyMeasurable.{u_2, u_3} (β := F) fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2

Tactic:
exact (stronglyMeasurable_deriv_with_param this).comp_measurable measurable_prodMk_right

Premises used: measurable_prodMk_right, MeasureTheory.StronglyMeasurable.comp_measurable, stronglyMeasurable_deriv_with_param
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
inst_10 : MeasurableSpace F
inst_11 : BorelSpace F
hf : Continuous f
μ : Measure (E × E)
⊢ AEMeasurable.{u_2, u_3} (β := F) (fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2) μ

Tactic:
(measurable_lineDeriv_uncurry hf).aemeasurable

Premises used: Measurable.aemeasurable, measurable_lineDeriv_uncurry
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
μ : Measure (E × E)
⊢ AEStronglyMeasurable.{u_2, u_3} (β := F) (fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2) μ

Tactic:
(stronglyMeasurable_lineDeriv_uncurry hf).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, stronglyMeasurable_lineDeriv_uncurry
-- Module: Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : QuadraticMap 𝕜 E F
a b : E
⊢ HasLineDerivAt.{u_1, u_3, u_2} 𝕜 (F := F) (⇑f : (a : E) → F) (polar (⇑f : (a : E) → F) a b) a b

Tactic:
simpa [HasLineDerivAt, QuadraticMap.map_add, f.map_smul] using
    ((hasDerivAt_const (0 : 𝕜) (f a)).add <|
      ((hasDerivAt_id 0).mul (hasDerivAt_id 0)).smul (hasDerivAt_const 0 (f b))).add
      ((hasDerivAt_id 0).smul (hasDerivAt_const 0 (polar f a b)))

Premises used: HasDerivAt.add, QuadraticMap.map_smul, QuadraticMap.map_add, hasDerivAt_const, QuadraticMap.polar, HasDerivAt.mul, HasLineDerivAt, OfNat.ofNat, HasDerivAt.smul, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : QuadraticMap 𝕜 E F
a b : E
⊢ LineDifferentiableAt.{u_1, u_3, u_2} 𝕜 (F := F) (⇑f : (a : E) → F) a b

Tactic:
(f.hasLineDerivAt a b).lineDifferentiableAt

Premises used: HasLineDerivAt.lineDifferentiableAt, QuadraticMap.hasLineDerivAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : QuadraticMap 𝕜 E F
h : ∀ (a b : E), Eq.{u_3 + 1} (α := F) (lineDeriv 𝕜 (⇑f : (a : E) → F) a b) (polar (⇑f : (a : E) → F) a b)
⊢ Eq (α := (x v : E) → F) (lineDeriv 𝕜 (⇑f : (a : E) → F)) (polar (⇑f : (a : E) → F))

Tactic:
ext a b
-- Module: Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : QuadraticMap 𝕜 E F
a b : E
⊢ Eq.{u_3 + 1} (α := F) (lineDeriv 𝕜 (⇑f : (a : E) → F) a b) (polar (⇑f : (a : E) → F) a b)

Tactic:
(f.hasLineDerivAt a b).lineDeriv

Premises used: HasLineDerivAt.lineDeriv, QuadraticMap.hasLineDerivAt
-- Module: Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : QuadraticMap 𝕜 E F
a b : E
⊢ Eq.{u_3 + 1} (α := F) (lineDeriv 𝕜 (⇑f : (a : E) → F) a b) (polar (⇑f : (a : E) → F) a b)

Tactic:
exact (f.hasLineDerivAt a b).lineDeriv

Premises used: HasLineDerivAt.lineDeriv, QuadraticMap.hasLineDerivAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
s t : Set E
hst : s ≤ t
⊢ LE.le.{u} (α := Set E) ((fun (s : Set E) ↦ posTangentConeAt s a) s) ((fun (s : Set E) ↦ posTangentConeAt s a) t)

Tactic:
tangentConeAt_mono hst

Premises used: tangentConeAt_mono
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
s t : Set E
hst : s ≤ t
⊢ LE.le.{u} (α := Set E) ((fun (s : Set E) ↦ posTangentConeAt s a) s) ((fun (s : Set E) ↦ posTangentConeAt s a) t)

Tactic:
exact tangentConeAt_mono hst

Premises used: tangentConeAt_mono
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s
⊢ NeBot (α := ℝ≥0) (𝓝[>] 0 ⊓ 𝓟 {x_1 : ℝ≥0 | x + (↑x_1 : ℝ) • y ∈ s})

Tactic:
rw [← NNReal.coe_zero, ← NNReal.map_coe_nhdsGT, frequently_map, frequently_iff_neBot] at h

Premises used: NNReal.coe_zero, NNReal.map_coe_nhdsGT, Filter.frequently_map, Filter.frequently_iff_neBot
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : NeBot (α := ℝ≥0) (𝓝[>] 0 ⊓ 𝓟 {x_1 : ℝ≥0 | x + (↑x_1 : ℝ) • y ∈ s})
hc₀ : Tendsto (α := ℝ≥0) id (𝓝[>] 0 ⊓ 𝓟 {t : ℝ≥0 | x + (↑t : ℝ) • y ∈ s}) (𝓝[≠] 0)
hmem : ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0 ⊓ 𝓟 {t : ℝ≥0 | x + (↑t : ℝ) • y ∈ s}, x + id n • y ∈ s
apply : ℝ≥0 → ℝ≥0
⊢ y ∈ posTangentConeAt s x

Tactic:
apply mem_tangentConeAt_of_add_smul_mem (l := 𝓝[>] (0 : ℝ≥0) ⊓ 𝓟 {t | x + (t : ℝ) • y ∈ s})

Premises used: mem_tangentConeAt_of_add_smul_mem
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : NeBot (α := ℝ≥0) (𝓝[>] 0 ⊓ 𝓟 {x_1 : ℝ≥0 | x + (↑x_1 : ℝ) • y ∈ s})
⊢ Tendsto (α := ℝ≥0) id (𝓝[>] 0 ⊓ 𝓟 {t : ℝ≥0 | x + (↑t : ℝ) • y ∈ s}) (𝓝[≠] 0)

Tactic:
tendsto_id'.mpr <| inf_le_left.trans <| nhdsGT_le_nhdsNE _

Premises used: Iff.mpr, Filter.tendsto_id', nhdsGT_le_nhdsNE, inf_le_left, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : NeBot (α := ℝ≥0) (𝓝[>] 0 ⊓ 𝓟 {x_1 : ℝ≥0 | x + (↑x_1 : ℝ) • y ∈ s})
⊢ Tendsto (α := ℝ≥0) id (𝓝[>] 0 ⊓ 𝓟 {t : ℝ≥0 | x + (↑t : ℝ) • y ∈ s}) (𝓝[≠] 0)

Tactic:
exact tendsto_id'.mpr <| inf_le_left.trans <| nhdsGT_le_nhdsNE _

Premises used: Iff.mpr, Filter.tendsto_id', nhdsGT_le_nhdsNE, inf_le_left, LE.le.trans
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : NeBot (α := ℝ≥0) (𝓝[>] 0 ⊓ 𝓟 {x_1 : ℝ≥0 | x + (↑x_1 : ℝ) • y ∈ s})
⊢ ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0 ⊓ 𝓟 {t : ℝ≥0 | x + (↑t : ℝ) • y ∈ s}, x + id n • y ∈ s

Tactic:
simp [eventually_inf_principal, NNReal.smul_def]

Premises used: Filter.eventually_inf_principal, NNReal.smul_def
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : [x -[ℝ] y] ⊆ s
⊢ y - x ∈ posTangentConeAt s x

Tactic:
sub_mem_posTangentConeAt_of_openSegment_subset <| (openSegment_subset_segment ..).trans h

Premises used: Set.Mem, HasSubset.Subset.trans, openSegment_subset_segment, sub_mem_posTangentConeAt_of_openSegment_subset
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : [x -[ℝ] x + y] ⊆ s
⊢ y ∈ posTangentConeAt s x

Tactic:
simpa using sub_mem_posTangentConeAt_of_segment_subset h

Premises used: sub_mem_posTangentConeAt_of_segment_subset
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : E
⊢ posTangentConeAt univ a = univ

Tactic:
tangentConeAt_univ

Premises used: tangentConeAt_univ
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
rcases :
  ∀ (ι : Type u) (l : Filter ι) (hl : l.NeBot) (c : ι → ℝ≥0) (d : ι → E) (hd₀ : Tendsto d l (𝓝 0))
    (hd : ∀ᶠ (n : ι) in l, a + d n ∈ s) (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)),
    LE.le (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) (0 : ℝ)
⊢ LE.le (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) (0 : ℝ)

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

Premises used: exists_fun_of_mem_tangentConeAt
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
suffices : ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0
⊢ LE.le (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
suffices ∀ᶠ n in l, c n • (f (a + d n) - f a) ≤ 0 from
    le_of_tendsto (hf.lim hd₀ hd hcd) this
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
⊢ Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] (a + 0))

Tactic:
replace hd : Tendsto (fun n => a + d n) l (𝓝[s] (a + 0)) :=
    tendsto_nhdsWithin_iff.2 ⟨tendsto_const_nhds.add hd₀, hd⟩
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] (a + 0))
⊢ Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] a)

Tactic:
rw [add_zero] at hd

Premises used: add_zero
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] a)
⊢ ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0

Tactic:
hd.eventually h |>.mono fun n hn ↦ ?_

Premises used: Filter.Eventually.mono, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] a)
refine : ∀ (n : ι) (hn : f (a + d n) ≤ f a), c n • (f (a + d n) - f a) ≤ 0
⊢ ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0

Tactic:
refine hd.eventually h |>.mono fun n hn ↦ ?_

Premises used: Filter.Eventually.mono, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] a)
n : ι
hn : f (a + d n) ≤ f a
⊢ c n • (f (a + d n) - f a) ≤ 0

Tactic:
mul_nonpos_of_nonneg_of_nonpos (c n).coe_nonneg (sub_nonpos.2 hn)

Premises used: Iff.mpr, NNReal.coe_nonneg, mul_nonpos_of_nonneg_of_nonpos, sub_nonpos
-- Module: Mathlib.Analysis.Calculus.LocalExtr.Basic
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] a)
n : ι
hn : f (a + d n) ≤ f a
⊢ c n • (f (a + d n) - f a) ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos (c n).coe_nonneg (sub_nonpos.2 hn)

Premises used: Iff.mpr, NNReal.coe_nonneg, mul_nonpos_of_nonneg_of_nonpos, sub_nonpos
-- 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 : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
rw : LE.le (α := ℝ) ((0 : (a : E) → ℝ) y : ℝ) ((0 : (a : E) → ℝ) y : ℝ)
⊢ LE.le (α := ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Premises used: fderivWithin_zero_of_not_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 : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ LE.le (α := ℝ) ((0 : (a : E) → ℝ) y : ℝ) ((0 : (a : E) → ℝ) y : ℝ)

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 : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
⊢ LE.le (α := ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
exact
    if hf : DifferentiableWithinAt ℝ f s a then h.hasFDerivWithinAt_nonpos hf.hasFDerivWithinAt 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 : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
⊢ LE.le (α := ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
classical
  exact
    if hf : DifferentiableWithinAt ℝ f s a then h.hasFDerivWithinAt_nonpos hf.hasFDerivWithinAt 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
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ LE.le (α := ℝ) (0 : ℝ) ((f' : (a : E) → ℝ) y : ℝ)

Tactic:
simpa using h.hasFDerivWithinAt_nonpos hf hy'

Premises used: IsLocalMaxOn.hasFDerivWithinAt_nonpos
-- 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 : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
rw : Eq (α := ℝ) ((0 : (a : E) → ℝ) y : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Premises used: fderivWithin_zero_of_not_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 : IsLocalMaxOn 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 : IsLocalMaxOn 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 : IsLocalMaxOn 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
s : Set E
a y : E
h : IsLocalMinOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
⊢ LE.le (α := ℝ) (0 : ℝ) ((f' : (a : E) → ℝ) y : ℝ)

Tactic:
simpa using h.neg.hasFDerivWithinAt_nonpos hf.neg hy

Premises used: IsLocalMaxOn.hasFDerivWithinAt_nonpos, IsLocalMinOn.neg, HasFDerivWithinAt.neg
-- 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
hf : ¬DifferentiableWithinAt ℝ f s a
rw : LE.le (α := ℝ) 0 0
⊢ LE.le (α := ℝ) (0 : ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ)

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Premises used: fderivWithin_zero_of_not_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
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ LE.le (α := ℝ) 0 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
⊢ LE.le (α := ℝ) (0 : ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ)

Tactic:
exact
    if hf : DifferentiableWithinAt ℝ f s a then h.hasFDerivWithinAt_nonneg hf.hasFDerivWithinAt 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
⊢ LE.le (α := ℝ) (0 : ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ)

Tactic:
classical
  exact
    if hf : DifferentiableWithinAt ℝ f s a then h.hasFDerivWithinAt_nonneg hf.hasFDerivWithinAt 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
s : Set E
a y : E
h : IsLocalMinOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
simpa using h.neg.hasFDerivWithinAt_eq_zero hf.neg hy hy'

Premises used: IsLocalMinOn.neg, HasFDerivWithinAt.neg, IsLocalMaxOn.hasFDerivWithinAt_eq_zero
-- 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
rw : Eq (α := ℝ) ((0 : (a : E) → ℝ) y : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ) (0 : ℝ)

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Premises used: fderivWithin_zero_of_not_differentiableWithinAt