awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
n : ℕ
ih :
  ∀ {f : 𝕜 → E} (hf : ∀ k < n, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0),
    (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f b = f b
f : 𝕜 → E
hf : ∀ k < n + 1, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0
⊢ (b - a) ^ (n + 1) • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n + 1] f b = f b
have succ : (b - a) ^ (n + 1) •
    swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f)
      b =
  f b
Tactic: rw [Function.iterate_succ_apply', pow_succ, mul_smul,
      sub_smul_dslope_of_zero (hf n n.lt_succ_self), ih (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
n : ℕ
ih :
  ∀ {f : 𝕜 → E} (hf : ∀ k < n, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0),
    (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f b = f b
f : 𝕜 → E
hf : ∀ k < n + 1, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0
succ :
  (b - a) ^ (n + 1) •
      swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a
        ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f) b =
    f b
⊢ (b - a) ^ (n + 1) • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n + 1] f b = f b
have succ₁ : ((b - a) ^ n * (b - a)) •
    swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f)
      b =
  f b
Tactic: rw [Function.iterate_succ_apply', pow_succ, mul_smul,
      sub_smul_dslope_of_zero (hf n n.lt_succ_self), ih (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
n : ℕ
ih :
  ∀ {f : 𝕜 → E} (hf : ∀ k < n, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0),
    (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f b = f b
f : 𝕜 → E
hf : ∀ k < n + 1, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0
succ :
  (b - a) ^ (n + 1) •
      swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a
        ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f) b =
    f b
succ₁ :
  ((b - a) ^ n * (b - a)) •
      swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a
        ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f) b =
    f b
⊢ (b - a) ^ (n + 1) • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n + 1] f b = f b
have succ₂ : (b - a) ^ n •
    (b - a) •
      swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a
        ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f) b =
  f b
Tactic: rw [Function.iterate_succ_apply', pow_succ, mul_smul,
      sub_smul_dslope_of_zero (hf n n.lt_succ_self), ih (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
n : ℕ
ih :
  ∀ {f : 𝕜 → E} (hf : ∀ k < n, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0),
    (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f b = f b
f : 𝕜 → E
hf : ∀ k < n + 1, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0
succ :
  (b - a) ^ (n + 1) •
      swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a
        ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f) b =
    f b
succ₁ :
  ((b - a) ^ n * (b - a)) •
      swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a
        ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f) b =
    f b
succ₂ :
  (b - a) ^ n •
      (b - a) •
        swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a
          ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f) b =
    f b
⊢ (b - a) ^ (n + 1) • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n + 1] f b = f b
have succ₃ : (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f b = f b
Tactic: rw [Function.iterate_succ_apply', pow_succ, mul_smul,
      sub_smul_dslope_of_zero (hf n n.lt_succ_self), ih (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
n : ℕ
ih :
  ∀ {f : 𝕜 → E} (hf : ∀ k < n, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0),
    (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f b = f b
f : 𝕜 → E
hf : ∀ k < n + 1, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0
succ :
  (b - a) ^ (n + 1) •
      swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a
        ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f) b =
    f b
succ₁ :
  ((b - a) ^ n * (b - a)) •
      swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a
        ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f) b =
    f b
succ₂ :
  (b - a) ^ n •
      (b - a) •
        swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a
          ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f) b =
    f b
succ₃ : (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f b = f b
⊢ (b - a) ^ (n + 1) • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n + 1] f b = f b
have succ₄ : f b = f b
Tactic: rw [Function.iterate_succ_apply', pow_succ, mul_smul,
      sub_smul_dslope_of_zero (hf n n.lt_succ_self), ih (by grind)]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
n : ℕ
hf : ∀ k < n, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0
b : 𝕜
⊢ (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f b = f b
have zero : ∀ {f : 𝕜 → E} (hf : ∀ k < 0, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0),
  HPow.hPow (β := ℕ) (b - a) 0 • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[0] f b = f b
Tactic: induction n generalizing f with
  | zero => simp
  | succ n ih =>
    rw [Function.iterate_succ_apply', pow_succ, mul_smul,
      sub_smul_dslope_of_zero (hf n n.lt_succ_self), ih (by grind)]
Cleared hypotheses: f, n, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.DSlope (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
n : ℕ
hf : ∀ k < n, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0
b : 𝕜
zero :
  ∀ {f : 𝕜 → E} (hf : ∀ k < 0, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0),
    HPow.hPow (β := ℕ) (b - a) 0 • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[0] f b = f b
⊢ (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f b = f b
have succ : ∀ (n : ℕ)
  (ih :
    ∀ {f : 𝕜 → E} (hf : ∀ k < n, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0),
      (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] f b = f b)
  {f : 𝕜 → E} (hf : ∀ k < n + 1, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0),
  (b - a) ^ (n + 1) • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n + 1] f b = f b
Tactic: induction n generalizing f with
  | zero => simp
  | succ n ih =>
    rw [Function.iterate_succ_apply', pow_succ, mul_smul,
      sub_smul_dslope_of_zero (hf n n.lt_succ_self), ih (by grind)]
Cleared hypotheses: f, n, hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
⊢ m ∈ f' '' Ioo a b
have inl : ∀ (hab : a ≤ a) (hf : ∀ x ∈ Icc a a, HasDerivWithinAt f (f' x) (Icc a a) x) (hmb : m < f' a), m ∈ f' '' Ioo a a
Tactic: rcases hab.eq_or_lt with (rfl | hab')
Cleared hypotheses: b, hab, hf, hmb
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
inl : ∀ (hab : a ≤ a) (hf : ∀ x ∈ Icc a a, HasDerivWithinAt f (f' x) (Icc a a) x) (hmb : m < f' a), m ∈ f' '' Ioo a a
⊢ m ∈ f' '' Ioo a b
have inr : ∀ (hab' : a < b), m ∈ f' '' Ioo a b
Tactic: rcases hab.eq_or_lt with (rfl | hab')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (hypothesis)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
⊢ m ∈ f' '' Ioo a b
have hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
Tactic: have hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x := by
    intro x hx
    simpa using (hf x hx).sub ((hasDerivWithinAt_id x _).const_mul m)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
⊢ m ∈ f' '' Ioo a b
have inr : ∀ (c : ℝ) (cmem : c ∈ Icc a b) (hc : IsMinOn g (Icc a b) c), m ∈ f' '' Ioo a b
Tactic: obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Icc a b, IsMinOn g (Icc a b) c :=
    isCompact_Icc.exists_isMinOn (nonempty_Icc.2 <| hab) fun x hx => (hg x hx).continuousWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
⊢ c ∈ Ioo a b
have inl : ∀ (cmem : a ∈ Icc a b) (hc : IsMinOn g (Icc a b) a), a ∈ Ioo a b
Tactic: rcases cmem.1.eq_or_lt with (rfl | hac)
Cleared hypotheses: c, cmem, hc
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
inl : ∀ (cmem : a ∈ Icc a b) (hc : IsMinOn g (Icc a b) a), a ∈ Ioo a b
⊢ c ∈ Ioo a b
have inr : ∀ (hac : a < c), c ∈ Ioo a b
Tactic: rcases cmem.1.eq_or_lt with (rfl | hac)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
⊢ a ∈ Ioo a b
have inl : 0 ≤ (b - a) * (f' a - m)
Tactic: refine absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right ?_ (sub_pos.2 hab'))
        (not_le_of_gt hma)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (hypothesis)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : a ∈ Icc a b
hc : IsMinOn g (Icc a b) a
⊢ 0 ≤ (b - a) * (f' a - m)
have this : b - a ∈ posTangentConeAt (Icc a b) a
Tactic: have : b - a ∈ posTangentConeAt (Icc a b) a :=
        sub_mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.rfl)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
⊢ c ∈ Ioo a b
have inr : ∀ (cmem : b ∈ Icc a b) (hc : IsMinOn g (Icc a b) b) (hac : a < b), b ∈ Ioo a b
Tactic: rcases cmem.2.eq_or_lt' with (rfl | hcb)
Cleared hypotheses: c, cmem, hc, hac
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
hac : a < c
inr : ∀ (cmem : b ∈ Icc a b) (hc : IsMinOn g (Icc a b) b) (hac : a < b), b ∈ Ioo a b
⊢ c ∈ Ioo a b
have inr₁ : ∀ (hcb : c < b), c ∈ Ioo a b
Tactic: rcases cmem.2.eq_or_lt' with (rfl | hcb)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ b ∈ Ioo a b
have inr : 0 ≤ (a - b) * (f' b - m)
Tactic: refine absurd (sub_nonpos.1 <| nonpos_of_mul_nonneg_right ?_ (sub_lt_zero.2 hab'))
        (not_le_of_gt hmb)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ segment ℝ b a ⊆ Icc a b
have rw : segment ℝ a b ⊆ Icc a b
Tactic: rw [segment_symm, segment_eq_Icc hab]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
rw : segment ℝ a b ⊆ Icc a b
⊢ segment ℝ b a ⊆ Icc a b
have rw₁ : Icc a b ⊆ Icc a b
Tactic: rw [segment_symm, segment_eq_Icc hab]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (hypothesis)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
cmem : b ∈ Icc a b
hc : IsMinOn g (Icc a b) b
hac : a < b
⊢ 0 ≤ (a - b) * (f' b - m)
have this : a - b ∈ posTangentConeAt (Icc a b) b
Tactic: have : a - b ∈ posTangentConeAt (Icc a b) b :=
        sub_mem_posTangentConeAt_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab])
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (hypothesis)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
⊢ m ∈ f' '' Ioo a b
have cmem' : c ∈ Ioo a b
Tactic: have cmem' : c ∈ Ioo a b := by
    rcases cmem.1.eq_or_lt with (rfl | hac)
    -- Show that `c` can't be equal to `a`
    · refine absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right ?_ (sub_pos.2 hab'))
        (not_le_of_gt hma)
      have : b - a ∈ posTangentConeAt (Icc a b) a :=
        sub_mem_posTangentConeAt_of_segment_subset (segment_eq_Icc hab ▸ Subset.rfl)
      simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply]
        using hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this
    rcases cmem.2.eq_or_lt' with (rfl | hcb)
    -- Show that `c` can't be equal to `b`
    · refine absurd (sub_nonpos.1 <| nonpos_of_mul_nonneg_right ?_ (sub_lt_zero.2 hab'))
        (not_le_of_gt hmb)
      have : a - b ∈ posTangentConeAt (Icc a b) b :=
        sub_mem_posTangentConeAt_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab])
      simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply]
        using hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this
    exact ⟨hac, hcb⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ m ∈ f' '' Ioo a b
have right : f' c = m
Tactic: use c, cmem'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ f' c = m
have right : f' c - m = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ Icc a b ∈ 𝓝 c
have rwa : c ∈ interior (Icc a b)
Tactic: rwa [← mem_interior_iff_mem_nhds, interior_Icc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (hypothesis)
Goal:
a b : ℝ
f f' : ℝ → ℝ
hab : a ≤ b
hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x
m : ℝ
hma : f' a < m
hmb : m < f' b
hab' : a < b
g : ℝ → ℝ := fun (x : ℝ) ↦ f x - m * x
hg : ∀ x ∈ Icc a b, HasDerivWithinAt g (f' x - m) (Icc a b) x
c : ℝ
cmem : c ∈ Icc a b
hc : IsMinOn g (Icc a b) c
cmem' : c ∈ Ioo a b
⊢ f' c - m = 0
have this : Icc a b ∈ 𝓝 c
Tactic: have : Icc a b ∈ 𝓝 c := by rwa [← mem_interior_iff_mem_nhds, interior_Icc]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ (f' '' s).OrdConnected
have hs₁ : ∀ x ∈ f' '' s, ∀ y ∈ f' '' s, x < y → Ioo x y ⊆ f' '' s
Tactic: apply ordConnected_of_Ioo
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
⊢ m ∈ f' '' s
have hs₁ : ∀ (hab : a ≤ b), m ∈ f' '' s
Tactic: rcases le_total a b with hab | hab
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hs₁ : ∀ (hab : a ≤ b), m ∈ f' '' s
⊢ m ∈ f' '' s
have hs₂ : ∀ (hab : b ≤ a), m ∈ f' '' s
Tactic: rcases le_total a b with hab | hab
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (hypothesis)
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
⊢ m ∈ f' '' s
have this : Icc a b ⊆ s
Tactic: have : Icc a b ⊆ s := hs.out ha hb
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : a ≤ b
this : Icc a b ⊆ s
⊢ m ∈ f' '' s
have hs₁ : ∀ (c : ℝ) (cmem : c ∈ Ioo a b) (hc : f' c = m), m ∈ f' '' s
Tactic: rcases exists_hasDerivWithinAt_eq_of_gt_of_lt hab (fun x hx => (hf x <| this hx).mono this) hma
        hmb with
      ⟨c, cmem, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (hypothesis)
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
⊢ m ∈ f' '' s
have this : Icc b a ⊆ s
Tactic: have : Icc b a ⊆ s := hs.out hb ha
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : s.OrdConnected
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
a : ℝ
ha : a ∈ s
b : ℝ
hb : b ∈ s
m : ℝ
hma : f' a < m
hmb : m < f' b
hab : b ≤ a
this : Icc b a ⊆ s
⊢ m ∈ f' '' s
have hs₁ : ∀ (c : ℝ) (cmem : c ∈ Ioo b a) (hc : f' c = m), m ∈ f' '' s
Tactic: rcases exists_hasDerivWithinAt_eq_of_lt_of_gt hab (fun x hx => (hf x <| this hx).mono this) hmb
        hma with
      ⟨c, cmem, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : ∀ x ∈ s, f' x ≠ m
⊢ (∀ x ∈ s, f' x < m) ∨ ∀ x ∈ s, m < f' x
have contrapose! : ∀ (hf' : (∃ x ∈ s, m ≤ f' x) ∧ ∃ x ∈ s, f' x ≤ m), ∃ x ∈ s, f' x = m
Tactic: contrapose! hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Darboux (goal)
Goal:
f f' : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
m : ℝ
hf' : (∃ x ∈ s, m ≤ f' x) ∧ ∃ x ∈ s, f' x ≤ m
⊢ ∃ x ∈ s, f' x = m
have rcases : ∀ (b : ℝ) (hb : b ∈ s) (hmb : m ≤ f' b) (a : ℝ) (ha : a ∈ s) (hma : f' a ≤ m), ∃ x ∈ s, f' x = m
Tactic: rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x
have inl : ∀ (hx : x < 0), HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x
Tactic: obtain hx | hx := hx.lt_or_gt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
x : ℝ
hx : x ≠ 0
inl : ∀ (hx : x < 0), HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x
⊢ HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x
have inr : ∀ (hx : 0 < x), HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) x
Tactic: obtain hx | hx := hx.lt_or_gt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
⊢ HasStrictFDerivAt (fun (x : E) ↦ |f x|) (-f') x
have h : instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
    -f' = ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f'
Tactic: convert! (hasStrictDerivAt_abs_neg h₀).hasStrictFDerivAt.comp x hf using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Abs (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x < 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ -f' = ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f'
have h : ∀ (y : E),
  Eq (α := ℝ) ((-f' : (a : E) → ℝ) y : ℝ) ((ContinuousLinearMap.toSpanSingleton ℝ (-1) ∘SL f' : (a : E) → ℝ) y : ℝ)
Tactic: ext y