awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ 0 ≤ deriv f x
c : ℝ
hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
⊢ IsLocalMax f b

Tactic:
isLocalMax_of_deriv_Ioo ha.1 hc.1 h
    (fun _ hx => (ha.2 hx).1.differentiableWithinAt)
    (fun _ hx => (hc.2 hx).1.differentiableWithinAt)
    (fun _ hx => (ha.2 hx).2) (fun x hx => (hc.2 hx).2)

Premises used: DifferentiableAt.differentiableWithinAt, And.right, And.left, isLocalMax_of_deriv_Ioo
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ 0 ≤ deriv f x
c : ℝ
hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
⊢ IsLocalMax f b

Tactic:
exact isLocalMax_of_deriv_Ioo ha.1 hc.1 h
    (fun _ hx => (ha.2 hx).1.differentiableWithinAt)
    (fun _ hx => (hc.2 hx).1.differentiableWithinAt)
    (fun _ hx => (ha.2 hx).2) (fun x hx => (hc.2 hx).2)

Premises used: DifferentiableAt.differentiableWithinAt, And.right, And.left, isLocalMax_of_deriv_Ioo
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
obtain : ∀ (a : ℝ) (ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0), IsLocalMin f b
⊢ IsLocalMin f b

Tactic:
obtain ⟨a, ha⟩ := (nhdsLT_basis b).eventually_iff.mp <| hd₀.and h₀

Premises used: Filter.Eventually.and, nhdsLT_basis, Iff.mp, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
obtain : ∀ (c : ℝ) (hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≥ 0), IsLocalMin f b
⊢ IsLocalMin f b

Tactic:
obtain ⟨c, hc⟩ := (nhdsGT_basis b).eventually_iff.mp <| hd₁.and h₁

Premises used: nhdsGT_basis, Filter.Eventually.and, Iff.mp, Filter.HasBasis.eventually_iff
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
c : ℝ
hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≥ 0
⊢ IsLocalMin f b

Tactic:
isLocalMin_of_deriv_Ioo ha.1 hc.1 h
    (fun _ hx => (ha.2 hx).1.differentiableWithinAt)
    (fun _ hx => (hc.2 hx).1.differentiableWithinAt)
    (fun _ hx => (ha.2 hx).2) (fun x hx => (hc.2 hx).2)

Premises used: DifferentiableAt.differentiableWithinAt, And.right, And.left, isLocalMin_of_deriv_Ioo
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, DifferentiableAt ℝ f x
hd₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≥ 0
a : ℝ
ha : a < b ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a b → DifferentiableAt ℝ f x ∧ deriv f x ≤ 0
c : ℝ
hc : b < c ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo b c → DifferentiableAt ℝ f x ∧ deriv f x ≥ 0
⊢ IsLocalMin f b

Tactic:
exact isLocalMin_of_deriv_Ioo ha.1 hc.1 h
    (fun _ hx => (ha.2 hx).1.differentiableWithinAt)
    (fun _ hx => (hc.2 hx).1.differentiableWithinAt)
    (fun _ hx => (ha.2 hx).2) (fun x hx => (hc.2 hx).2)

Premises used: DifferentiableAt.differentiableWithinAt, And.right, And.left, isLocalMin_of_deriv_Ioo
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd : ∀ᶠ (x : ℝ) in 𝓝[≠] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, 0 ≤ deriv f x
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, deriv f x ≤ 0
⊢ {x : ℝ | (fun (x : ℝ) ↦ DifferentiableAt ℝ f x) x} ∈ 𝓝[≠] b

Tactic:
tauto
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd : ∀ᶠ (x : ℝ) in 𝓝[≠] b, DifferentiableAt ℝ f x
h₀ : ∀ᶠ (x : ℝ) in 𝓝[<] b, deriv f x ≤ 0
h₁ : ∀ᶠ (x : ℝ) in 𝓝[>] b, 0 ≤ deriv f x
⊢ {x : ℝ | (fun (x : ℝ) ↦ DifferentiableAt ℝ f x) x} ∈ 𝓝[≠] b

Tactic:
tauto
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
rw :
  (∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
      Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType)
        ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)) ∧
    ∀ᶠ (x : ℝ) in pure x₀,
      Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType)
        ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
⊢ ∀ᶠ (x : ℝ) in 𝓝 x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)

Tactic:
rw [← nhdsNE_sup_pure x₀, eventually_sup]

Premises used: Filter.eventually_sup, nhdsNE_sup_pure
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
⊢ ∀ᶠ (x : ℝ) in pure x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
refine :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
⊢ (∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
      Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType)
        ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)) ∧
    ∀ᶠ (x : ℝ) in pure x₀,
      Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType)
        ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)

Tactic:
refine ⟨?_, by simpa⟩
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
⊢ Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))

Tactic:
have h_tendsto := hasDerivAt_iff_tendsto_slope.mp
    (differentiableAt_of_deriv_ne_zero <| ne_of_gt hf).hasDerivAt
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
h :
  ∀ (x : ℝ) (hx₀ : 0 < slope f x₀ x) (hx₁ : Membership.mem (γ := Set ℝ) {x₀}ᶜ x),
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)

Tactic:
filter_upwards [(h_tendsto.eventually <| eventually_gt_nhds hf),
    self_mem_nhdsWithin] with x hx₀ hx₁

Premises used: eventually_gt_nhds, self_mem_nhdsWithin, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
x : ℝ
hx₀ : 0 < slope f x₀ x
hx₁ : Membership.mem (γ := Set ℝ) {x₀}ᶜ x
⊢ x ≠ x₀

Tactic:
rw [mem_compl_iff, mem_singleton_iff, ← Ne.eq_def] at hx₁

Premises used: Ne.eq_def, Set.mem_singleton_iff, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
x : ℝ
hx₀ : 0 < slope f x₀ x
hx₁ : x ≠ x₀
h :
  ∀ (hx' : x < x₀),
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
h₁ :
  ∀ (hx' : x₀ < x),
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
⊢ Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)

Tactic:
obtain (hx' | hx') := hx₁.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
x : ℝ
hx₀ : 0 < slope f x₀ x
hx₁ : x ≠ x₀
hx' : x < x₀
h : Eq (α := SignType) (-1 : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
h₁ h₂ : Eq (α := SignType) (-1) (-1)
⊢ Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)

Tactic:
rw [sign_neg (neg_of_slope_pos hx' hx₀ hx), sign_neg (sub_neg.mpr hx')]

Premises used: sub_neg, Iff.mpr, sign_neg, neg_of_slope_pos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
x : ℝ
hx₀ : 0 < slope f x₀ x
hx₁ : x ≠ x₀
hx' : x₀ < x
h : Eq (α := SignType) (1 : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
h₁ h₂ : Eq (α := SignType) 1 1
⊢ Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)

Tactic:
rw [sign_pos (pos_of_slope_pos hx' hx₀ hx), sign_pos (sub_pos.mpr hx')]

Premises used: Iff.mpr, sub_pos, sign_pos, pos_of_slope_pos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ < 0
hx : f x₀ = 0
⊢ GT.gt (α := ℝ) (deriv (fun (x : ℝ) ↦ -f x) x₀) 0

Tactic:
simpa [deriv.neg]

Premises used: deriv.neg
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ < 0
hx : f x₀ = 0
⊢ Eq (α := ℝ) ((fun (x : ℝ) ↦ -f x) x₀) 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ < 0
hx : f x₀ = 0
⊢ ∀ᶠ (x : ℝ) in 𝓝 x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)

Tactic:
simpa [Left.sign_neg, -neg_sub, ← neg_sub x₀] using
    eventually_nhdsWithin_sign_eq_of_deriv_pos
      (f := (-f ·)) (x₀ := x₀) (by simpa [deriv.neg]) (by simpa)

Premises used: neg_sub, eventually_nhdsWithin_sign_eq_of_deriv_pos, Left.sign_neg
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
x : ℝ
hx' :
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
    ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
h : ∀ (hx : x < x₀), deriv f x < 0
⊢ x ∈ Iio x₀ → deriv f x < 0

Tactic:
(hx : x < x₀)
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
h :
  ∀ (x : ℝ)
    (hx' :
      Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
        ((sign : (a : ℝ) → SignType) (x - x₀) : SignType))
    (hx : x < x₀), deriv f x < 0
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x₀, deriv f b < 0

Tactic:
filter_upwards [nhdsLT_le_nhdsNE _ h₀, self_mem_nhdsWithin] with x hx' (hx : x < x₀)

Premises used: self_mem_nhdsWithin, nhdsLT_le_nhdsNE
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
x : ℝ
hx' :
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
    ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
hx : x < x₀
h : ∀ (hx : x - x₀ < 0), deriv f x < 0
h₁ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType) (-1 : SignType)), deriv f x < 0
h₂ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType) (-1 : SignType)), deriv f x < 0
h₃ h₄ h₅ h₆ : ∀ (hx : deriv f x < 0), deriv f x < 0
⊢ deriv f x < 0

Tactic:
rwa [← sub_neg, ← sign_eq_neg_one_iff, ← hx', sign_eq_neg_one_iff] at hx

Premises used: sub_neg, sign_eq_neg_one_iff
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
x : ℝ
hx' :
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
    ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
h : ∀ (hx : x₀ < x), deriv f x < 0
⊢ x ∈ Ioi x₀ → deriv f x < 0

Tactic:
(hx : x₀ < x)
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
h :
  ∀ (x : ℝ)
    (hx' :
      Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
        ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType))
    (hx : x₀ < x), deriv f x < 0
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] x₀, deriv f b < 0

Tactic:
filter_upwards [nhdsGT_le_nhdsNE _ h₀, self_mem_nhdsWithin] with x hx' (hx : x₀ < x)

Premises used: nhdsGT_le_nhdsNE, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
x : ℝ
hx' :
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
    ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
hx : x₀ < x
h : ∀ (hx : x₀ - x < 0), deriv f x < 0
h₁ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType) (-1 : SignType)), deriv f x < 0
h₂ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType) (-1 : SignType)), deriv f x < 0
h₃ h₄ h₅ h₆ : ∀ (hx : deriv f x < 0), deriv f x < 0
⊢ deriv f x < 0

Tactic:
rwa [← sub_neg, ← sign_eq_neg_one_iff, ← hx', sign_eq_neg_one_iff] at hx

Premises used: sub_neg, sign_eq_neg_one_iff
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
x : ℝ
hx' :
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
    ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
h : ∀ (hx : x₀ < x), deriv f x > 0
⊢ x ∈ Ioi x₀ → deriv f x > 0

Tactic:
(hx : x₀ < x)
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
h :
  ∀ (x : ℝ)
    (hx' :
      Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
        ((sign : (a : ℝ) → SignType) (x - x₀) : SignType))
    (hx : x₀ < x), deriv f x > 0
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] x₀, deriv f b > 0

Tactic:
filter_upwards [nhdsGT_le_nhdsNE _ h₀, self_mem_nhdsWithin] with x hx' (hx : x₀ < x)

Premises used: nhdsGT_le_nhdsNE, self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
x : ℝ
hx' :
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
    ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
hx : x₀ < x
h : ∀ (hx : 0 < x - x₀), deriv f x > 0
h₁ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType) (1 : SignType)), deriv f x > 0
h₂ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType) (1 : SignType)), deriv f x > 0
h₃ h₄ h₅ h₆ : ∀ (hx : 0 < deriv f x), deriv f x > 0
⊢ deriv f x > 0

Tactic:
rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx

Premises used: sub_pos, sign_eq_one_iff
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
x : ℝ
hx' :
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
    ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
h : ∀ (hx : x < x₀), deriv f x > 0
⊢ x ∈ Iio x₀ → deriv f x > 0

Tactic:
(hx : x < x₀)
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
h :
  ∀ (x : ℝ)
    (hx' :
      Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
        ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType))
    (hx : x < x₀), deriv f x > 0
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x₀, deriv f b > 0

Tactic:
filter_upwards [nhdsLT_le_nhdsNE _ h₀, self_mem_nhdsWithin] with x hx' (hx : x < x₀)

Premises used: self_mem_nhdsWithin, nhdsLT_le_nhdsNE
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
x : ℝ
hx' :
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
    ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
hx : x < x₀
h : ∀ (hx : 0 < x₀ - x), deriv f x > 0
h₁ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType) (1 : SignType)), deriv f x > 0
h₂ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType) (1 : SignType)), deriv f x > 0
h₃ h₄ h₅ h₆ : ∀ (hx : 0 < deriv f x), deriv f x > 0
⊢ deriv f x > 0

Tactic:
rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx

Premises used: sub_pos, sign_eq_one_iff
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h : ContinuousAt f x₀
hf :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
⊢ ∀ᶠ (b : ℝ) in 𝓝[<] x₀, deriv f b > 0

Tactic:
have hl := deriv_pos_left_of_sign_deriv hf
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h : ContinuousAt f x₀
hf :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
hl : ∀ᶠ (b : ℝ) in 𝓝[<] x₀, deriv f b > 0
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] x₀, deriv f b < 0

Tactic:
have hg := deriv_neg_right_of_sign_deriv hf
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h : ContinuousAt f x₀
hf :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
hl : ∀ᶠ (b : ℝ) in 𝓝[<] x₀, deriv f b > 0
hg : ∀ᶠ (b : ℝ) in 𝓝[>] x₀, deriv f b < 0
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] x₀, deriv f x ≠ 0

Tactic:
replace hf := (nhdsLT_sup_nhdsGT x₀) ▸
    eventually_sup.mpr ⟨hl.mono fun x hx => hx.ne', hg.mono fun x hx => hx.ne⟩
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h : ContinuousAt f x₀
hl : ∀ᶠ (b : ℝ) in 𝓝[<] x₀, deriv f b > 0
hg : ∀ᶠ (b : ℝ) in 𝓝[>] x₀, deriv f b < 0
hf : ∀ᶠ (x : ℝ) in 𝓝[≠] x₀, deriv f x ≠ 0
⊢ IsLocalMax f x₀

Tactic:
isLocalMax_of_deriv h (hf.mono fun x hx ↦ differentiableAt_of_deriv_ne_zero hx)
    (hl.mono fun _ => le_of_lt) (hg.mono fun _ => le_of_lt)

Premises used: le_of_lt, Filter.Eventually.mono, differentiableAt_of_deriv_ne_zero, isLocalMax_of_deriv
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h : ContinuousAt f x₀
hl : ∀ᶠ (b : ℝ) in 𝓝[<] x₀, deriv f b > 0
hg : ∀ᶠ (b : ℝ) in 𝓝[>] x₀, deriv f b < 0
hf : ∀ᶠ (x : ℝ) in 𝓝[≠] x₀, deriv f x ≠ 0
⊢ IsLocalMax f x₀

Tactic:
exact isLocalMax_of_deriv h (hf.mono fun x hx ↦ differentiableAt_of_deriv_ne_zero hx)
    (hl.mono fun _ => le_of_lt) (hg.mono fun _ => le_of_lt)

Premises used: le_of_lt, Filter.Eventually.mono, differentiableAt_of_deriv_ne_zero, isLocalMax_of_deriv
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h : ContinuousAt f x₀
hf :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
⊢ IsLocalMin f x₀

Tactic:
neg_neg f ▸ (isLocalMax_of_sign_deriv (f := (-f ·)) h.neg ?foo |>.neg)

Premises used: isLocalMax_of_sign_deriv, Eq.rec, neg_neg, ContinuousAt.neg, IsLocalMax.neg
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h : ContinuousAt f x₀
hf :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
foo :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv (fun (x : ℝ) ↦ -f x) x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
⊢ IsLocalMin f x₀

Tactic:
refine neg_neg f ▸ (isLocalMax_of_sign_deriv (f := (-f ·)) h.neg ?foo |>.neg)
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
h : ContinuousAt f x₀
hf :
  ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType)
      ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv (fun (x : ℝ) ↦ -f x) x) : SignType)
      ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)

Tactic:
simpa [Left.sign_neg, -neg_sub, ← neg_sub _ x₀, deriv.neg]

Premises used: neg_sub, deriv.neg, Left.sign_neg
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv (deriv f) x₀ > 0
hd : deriv f x₀ = 0
hc : ContinuousAt f x₀
⊢ IsLocalMin f x₀

Tactic:
isLocalMin_of_sign_deriv hc <| nhdsWithin_le_nhds <|
    eventually_nhdsWithin_sign_eq_of_deriv_pos hf hd

Premises used: eventually_nhdsWithin_sign_eq_of_deriv_pos, nhdsWithin_le_nhds, isLocalMin_of_sign_deriv
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv (deriv f) x₀ < 0
hd : deriv f x₀ = 0
hc : ContinuousAt f x₀
⊢ GT.gt (α := ℝ) (deriv (deriv fun (x : ℝ) ↦ -f x) x₀) 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv (deriv f) x₀ < 0
hd : deriv f x₀ = 0
hc : ContinuousAt f x₀
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ -f x) x₀) 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv (deriv f) x₀ < 0
hd : deriv f x₀ = 0
hc : ContinuousAt f x₀
⊢ IsLocalMax f x₀

Tactic:
simpa using isLocalMin_of_deriv_deriv_pos (by simpa) (by simpa) hc.neg |>.neg

Premises used: isLocalMin_of_deriv_deriv_pos, IsLocalMin.neg, ContinuousAt.neg
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : DifferentiableOn 𝕜 f (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ DiffContOnCl 𝕜 f s

Tactic:
⟨h.mono subset_closure, h.continuousOn⟩

Premises used: DiffContOnCl.mk, DifferentiableOn.continuousOn, subset_closure, DifferentiableOn.mono
-- Module: Mathlib.Analysis.Calculus.DiffContOnCl
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : Differentiable 𝕜 f
⊢ DiffContOnCl 𝕜 f s

Tactic:
⟨h.differentiableOn, h.continuous.continuousOn⟩

Premises used: DiffContOnCl.mk, Continuous.continuousOn, Differentiable.differentiableOn, Differentiable.continuous