awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (hypothesis)
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)
have h_tendsto : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
x₀ : ℝ
hf : deriv f x₀ > 0
hx : f x₀ = 0
h_tendsto : Tendsto (slope f x₀) (𝓝[≠] x₀) (𝓝 (deriv f x₀))
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
    Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
have 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)
Tactic: filter_upwards [(h_tendsto.eventually <| eventually_gt_nhds hf),
    self_mem_nhdsWithin] with x hx₀ hx₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (hypothesis)
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
⊢ Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
have hx₂ : x ≠ x₀
Tactic: rw [mem_compl_iff, mem_singleton_iff, ← Ne.eq_def] at hx₁
Cleared hypotheses: hx₁
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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₀
⊢ Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
have h : ∀ (hx' : x < x₀),
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
Tactic: obtain (hx' | hx') := hx₁.lt_or_gt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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)
⊢ Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
have h₁ : ∀ (hx' : x₀ < x),
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
Tactic: obtain (hx' | hx') := hx₁.lt_or_gt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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₀
⊢ Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
have h : Eq (α := SignType) (-1 : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
Tactic: rw [sign_neg (neg_of_slope_pos hx' hx₀ hx), sign_neg (sub_neg.mpr hx')]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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)
⊢ Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
have h₁ : Eq (α := SignType) (-1) (-1)
Tactic: rw [sign_neg (neg_of_slope_pos hx' hx₀ hx), sign_neg (sub_neg.mpr hx')]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
have h : Eq (α := SignType) (1 : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
Tactic: rw [sign_pos (pos_of_slope_pos hx' hx₀ hx), sign_pos (sub_pos.mpr hx')]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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)
⊢ Eq (α := SignType) ((sign : (a : ℝ) → SignType) (f x) : SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType)
have h₁ : Eq (α := SignType) 1 1
Tactic: rw [sign_pos (pos_of_slope_pos hx' hx₀ hx), sign_pos (sub_pos.mpr hx')]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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)
⊢ x ∈ Iio x₀ → deriv f x < 0
have h : ∀ (hx : x < x₀), deriv f x < 0
Tactic: (hx : x < x₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (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
have 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
Tactic: filter_upwards [nhdsLT_le_nhdsNE _ h₀, self_mem_nhdsWithin] with x hx' (hx : x < x₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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₀
⊢ deriv f x < 0
have h : ∀ (hx : x - x₀ < 0), deriv f x < 0
Tactic: rwa [← sub_neg, ← sign_eq_neg_one_iff, ← hx', sign_eq_neg_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x < 0
have h₁ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType) (-1 : SignType)), deriv f x < 0
Tactic: rwa [← sub_neg, ← sign_eq_neg_one_iff, ← hx', sign_eq_neg_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x < 0
have h₂ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType) (-1 : SignType)), deriv f x < 0
Tactic: rwa [← sub_neg, ← sign_eq_neg_one_iff, ← hx', sign_eq_neg_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x < 0
have h₃ : ∀ (hx : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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)
⊢ x ∈ Ioi x₀ → deriv f x < 0
have h : ∀ (hx : x₀ < x), deriv f x < 0
Tactic: (hx : x₀ < x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (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
have 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
Tactic: filter_upwards [nhdsGT_le_nhdsNE _ h₀, self_mem_nhdsWithin] with x hx' (hx : x₀ < x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x < 0
have h : ∀ (hx : x₀ - x < 0), deriv f x < 0
Tactic: rwa [← sub_neg, ← sign_eq_neg_one_iff, ← hx', sign_eq_neg_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x < 0
have h₁ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType) (-1 : SignType)), deriv f x < 0
Tactic: rwa [← sub_neg, ← sign_eq_neg_one_iff, ← hx', sign_eq_neg_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x < 0
have h₂ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType) (-1 : SignType)), deriv f x < 0
Tactic: rwa [← sub_neg, ← sign_eq_neg_one_iff, ← hx', sign_eq_neg_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x < 0
have h₃ : ∀ (hx : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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)
⊢ x ∈ Ioi x₀ → deriv f x > 0
have h : ∀ (hx : x₀ < x), deriv f x > 0
Tactic: (hx : x₀ < x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (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
have 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
Tactic: filter_upwards [nhdsGT_le_nhdsNE _ h₀, self_mem_nhdsWithin] with x hx' (hx : x₀ < x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x > 0
have h : ∀ (hx : 0 < x - x₀), deriv f x > 0
Tactic: rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x > 0
have h₁ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (x - x₀) : SignType) (1 : SignType)), deriv f x > 0
Tactic: rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x > 0
have h₂ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType) (1 : SignType)), deriv f x > 0
Tactic: rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x > 0
have h₃ : ∀ (hx : 0 < deriv f x), deriv f x > 0
Tactic: rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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)
⊢ x ∈ Iio x₀ → deriv f x > 0
have h : ∀ (hx : x < x₀), deriv f x > 0
Tactic: (hx : x < x₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
Goal:
f : ℝ → ℝ
x₀ : ℝ
h₀ :
  ∀ᶠ (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
have 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
Tactic: filter_upwards [nhdsLT_le_nhdsNE _ h₀, self_mem_nhdsWithin] with x hx' (hx : x < x₀)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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₀
⊢ deriv f x > 0
have h : ∀ (hx : 0 < x₀ - x), deriv f x > 0
Tactic: rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x > 0
have h₁ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType) (1 : SignType)), deriv f x > 0
Tactic: rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x > 0
have h₂ : ∀ (hx : Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv f x) : SignType) (1 : SignType)), deriv f x > 0
Tactic: rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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
⊢ deriv f x > 0
have h₃ : ∀ (hx : 0 < deriv f x), deriv f x > 0
Tactic: rwa [← sub_pos, ← sign_eq_one_iff, ← hx', sign_eq_one_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (hypothesis)
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)
⊢ IsLocalMax f x₀
have hl : ∀ᶠ (b : ℝ) in 𝓝[<] x₀, deriv f b > 0
Tactic: have hl := deriv_pos_left_of_sign_deriv hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (hypothesis)
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
⊢ IsLocalMax f x₀
have hg : ∀ᶠ (b : ℝ) in 𝓝[>] x₀, deriv f b < 0
Tactic: have hg := deriv_neg_right_of_sign_deriv hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (hypothesis)
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
⊢ IsLocalMax f x₀
have hf₁ : ∀ᶠ (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⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DerivativeTest (goal)
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₀
have foo : ∀ᶠ (x : ℝ) in 𝓝[≠] x₀,
  Eq (α := SignType) ((sign : (a : ℝ) → SignType) (deriv (fun (x : ℝ) ↦ -f x) x) : SignType)
    ((sign : (a : ℝ) → SignType) (x₀ - x) : SignType)
Tactic: refine neg_neg f ▸ (isLocalMax_of_sign_deriv (f := (-f ·)) h.neg ?foo |>.neg)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DiffContOnCl (goal)
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
inst_5 : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
⊢ ContinuousOn f (closedBall x r)
have inl : ∀ (h : DiffContOnCl 𝕜 f (ball x 0)), ContinuousOn f (closedBall x 0)
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DiffContOnCl (goal)
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
inst_5 : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
inl : ∀ (h : DiffContOnCl 𝕜 f (ball x 0)), ContinuousOn f (closedBall x 0)
⊢ ContinuousOn f (closedBall x r)
have inr : ∀ (hr : r ≠ 0), ContinuousOn f (closedBall x r)
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DiffContOnCl (goal)
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
inst_5 : NormedSpace ℝ E
x : E
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f (closedBall x 0)
have inl : ContinuousOn f {x}
Tactic: rw [closedBall_zero]