awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 (dslope f a) s b
⊢ DifferentiableWithinAt 𝕜 f s b

Tactic:
simpa only [id, sub_smul_dslope f a, sub_add_cancel] using
    ((differentiableWithinAt_id.sub_const a).fun_smul h).add_const (f a)

Premises used: id, DifferentiableWithinAt.sub_const, differentiableWithinAt_id, DifferentiableWithinAt.fun_smul, sub_smul_dslope, sub_add_cancel, DifferentiableWithinAt.add_const
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
h : DifferentiableAt 𝕜 (dslope f a) b
⊢ DifferentiableAt 𝕜 f b

Tactic:
differentiableWithinAt_univ.1 h.differentiableWithinAt.of_dslope

Premises used: DifferentiableAt.differentiableWithinAt, Iff.mp, differentiableWithinAt_univ, DifferentiableWithinAt.of_dslope
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
s : Set 𝕜
h : DifferentiableOn 𝕜 (dslope f a) s
⊢ DifferentiableOn 𝕜 f s

Tactic:
fun x hx => (h x hx).of_dslope

Premises used: DifferentiableOn, DifferentiableWithinAt.of_dslope
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b

Tactic:
⟨DifferentiableWithinAt.of_dslope, fun hd => ?_⟩

Premises used: Iff.intro, DifferentiableWithinAt.of_dslope
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
refine : ∀ (hd : DifferentiableWithinAt 𝕜 f s b), DifferentiableWithinAt 𝕜 (dslope f a) s b
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b

Tactic:
refine ⟨DifferentiableWithinAt.of_dslope, fun hd => ?_⟩
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b

Tactic:
(((differentiableWithinAt_id.sub_const a).inv (sub_ne_zero.2 h)).smul
    (hd.sub_const (f a))).congr_of_eventuallyEq ?_ (dslope_of_ne _ h)

Premises used: Iff.mpr, sub_ne_zero, DifferentiableWithinAt.congr_of_eventuallyEq, DifferentiableWithinAt.inv, dslope_of_ne, DifferentiableWithinAt.sub_const, differentiableWithinAt_id, DifferentiableWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
refine : dslope f a =ᶠ[𝓝[s] b] HSMul.hSMul (α := 𝕜 → 𝕜) (β := 𝕜 → E) (fun (y : 𝕜) ↦ id y - a)⁻¹ fun (y : 𝕜) ↦ f y - f a
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b

Tactic:
refine (((differentiableWithinAt_id.sub_const a).inv (sub_ne_zero.2 h)).smul
    (hd.sub_const (f a))).congr_of_eventuallyEq ?_ (dslope_of_ne _ h)

Premises used: Iff.mpr, sub_ne_zero, DifferentiableWithinAt.congr_of_eventuallyEq, DifferentiableWithinAt.inv, dslope_of_ne, DifferentiableWithinAt.sub_const, differentiableWithinAt_id, DifferentiableWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ dslope f a =ᶠ[𝓝[s] b] HSMul.hSMul (α := 𝕜 → 𝕜) (β := 𝕜 → E) (fun (y : 𝕜) ↦ id y - a)⁻¹ fun (y : 𝕜) ↦ f y - f a

Tactic:
(eqOn_dslope_slope _ _).eventuallyEq_of_mem ?_

Premises used: Set.EqOn.eventuallyEq_of_mem, eqOn_dslope_slope, slope
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
refine : {a}ᶜ ∈ 𝓝[s] b
⊢ dslope f a =ᶠ[𝓝[s] b] HSMul.hSMul (α := 𝕜 → 𝕜) (β := 𝕜 → E) (fun (y : 𝕜) ↦ id y - a)⁻¹ fun (y : 𝕜) ↦ f y - f a

Tactic:
refine (eqOn_dslope_slope _ _).eventuallyEq_of_mem ?_

Premises used: Set.EqOn.eventuallyEq_of_mem, eqOn_dslope_slope
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ {a}ᶜ ∈ 𝓝[s] b

Tactic:
mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)

Premises used: mem_nhdsWithin_of_mem_nhds, isOpen_ne, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ {a}ᶜ ∈ 𝓝[s] b

Tactic:
exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)

Premises used: mem_nhdsWithin_of_mem_nhds, isOpen_ne, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
s : Set 𝕜
h : a ∉ s
⊢ DifferentiableOn 𝕜 (dslope f a) s ↔ DifferentiableOn 𝕜 f s

Tactic:
forall_congr' fun _ =>
    forall_congr' fun hx => differentiableWithinAt_dslope_of_ne <| ne_of_mem_of_not_mem hx h

Premises used: ne_of_mem_of_not_mem, differentiableWithinAt_dslope_of_ne, DifferentiableOn, forall_congr'
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
h : b ≠ a
⊢ DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b

Tactic:
simp only [← differentiableWithinAt_univ, differentiableWithinAt_dslope_of_ne h]

Premises used: differentiableWithinAt_dslope_of_ne, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
hf : f a = 0
b : 𝕜
⊢ (b - a) • dslope f a b = f b

Tactic:
simp [hf]
-- Module: Mathlib.Analysis.Calculus.DSlope
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : 𝕜
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:
simp
-- Module: Mathlib.Analysis.Calculus.DSlope
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
⊢ ∀ k < n, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[k] f a = 0

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.DSlope
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
succ₄ succ₅ : f b = f b
⊢ (b - a) ^ (n + 1) • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n + 1] 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)]

Premises used: Function.iterate_succ_apply', pow_succ, Nat.lt_succ_self, sub_smul_dslope_of_zero, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Calculus.DSlope
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
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
⊢ (b - a) ^ n • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope a)^[n] 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)]

Premises used: Function.iterate_succ_apply', pow_succ, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Calculus.Darboux
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
inr : ∀ (hab' : a < b), m ∈ f' '' Ioo a b
⊢ m ∈ f' '' Ioo a b

Tactic:
rcases hab.eq_or_lt with (rfl | hab')

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
a : ℝ
f f' : ℝ → ℝ
m : ℝ
hma : f' a < m
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:
(lt_asymm hma hmb).elim

Premises used: False.elim, lt_asymm
-- Module: Mathlib.Analysis.Calculus.Darboux
Goal:
a : ℝ
f f' : ℝ → ℝ
m : ℝ
hma : f' a < m
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:
exact (lt_asymm hma hmb).elim

Premises used: False.elim, lt_asymm
-- Module: Mathlib.Analysis.Calculus.Darboux
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
x : ℝ
hx : x ∈ Icc a b
⊢ HasDerivWithinAt g (f' x - m) (Icc a b) x

Tactic:
simpa using (hf x hx).sub ((hasDerivWithinAt_id x _).const_mul m)

Premises used: HasDerivWithinAt.sub, HasDerivWithinAt.const_mul, hasDerivWithinAt_id
-- Module: Mathlib.Analysis.Calculus.Darboux
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
⊢ ∀ 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)
-- Module: Mathlib.Analysis.Calculus.Darboux
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 ∈ Icc a b, IsMinOn g (Icc a b) c

Tactic:
isCompact_Icc.exists_isMinOn (nonempty_Icc.2 <| hab) fun x hx => (hg x hx).continuousWithinAt

Premises used: Iff.mpr, Set.nonempty_Icc, CompactIccSpace.isCompact_Icc, IsCompact.exists_isMinOn, HasDerivWithinAt.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.Darboux
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
inr : ∀ (c : ℝ) (cmem : c ∈ Icc a b) (hc : IsMinOn g (Icc a b) c), m ∈ f' '' Ioo a b
⊢ 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

Premises used: Iff.mpr, Set.nonempty_Icc, CompactIccSpace.isCompact_Icc, Set.Icc, IsCompact.exists_isMinOn, HasDerivWithinAt.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.Darboux
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
inr : ∀ (hac : a < c), c ∈ Ioo a b
⊢ c ∈ Ioo a b

Tactic:
rcases cmem.1.eq_or_lt with (rfl | hac)

Premises used: LE.le.eq_or_lt, And.left, rfl
-- Module: Mathlib.Analysis.Calculus.Darboux
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

Tactic:
absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right ?_ (sub_pos.2 hab'))
        (not_le_of_gt hma)

Premises used: Iff.mpr, sub_pos, nonneg_of_mul_nonneg_right, absurd, Iff.mp, not_le_of_gt, sub_nonneg
-- Module: Mathlib.Analysis.Calculus.Darboux
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
inl : 0 ≤ (b - a) * (f' a - m)
⊢ a ∈ Ioo a b

Tactic:
refine absurd (sub_nonneg.1 <| nonneg_of_mul_nonneg_right ?_ (sub_pos.2 hab'))
        (not_le_of_gt hma)

Premises used: Iff.mpr, sub_pos, nonneg_of_mul_nonneg_right, absurd, Iff.mp, not_le_of_gt, sub_nonneg
-- Module: Mathlib.Analysis.Calculus.Darboux
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
⊢ 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)
-- Module: Mathlib.Analysis.Calculus.Darboux
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
this : b - a ∈ posTangentConeAt (Icc a b) a
⊢ 0 ≤ (b - a) * (f' a - m)

Tactic:
simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply]
        using hc.localize.hasFDerivWithinAt_nonneg (hg a (left_mem_Icc.2 hab)) this

Premises used: Iff.mpr, IsLocalMinOn.hasFDerivWithinAt_nonneg, ContinuousLinearMap.one_apply, Set.left_mem_Icc, IsMinOn.localize, ContinuousLinearMap.smulRight_apply
-- Module: Mathlib.Analysis.Calculus.Darboux
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
inr₁ : ∀ (hcb : c < b), c ∈ Ioo a b
⊢ c ∈ Ioo a b

Tactic:
rcases cmem.2.eq_or_lt' with (rfl | hcb)

Premises used: And.right, LE.le.eq_or_lt', rfl
-- Module: Mathlib.Analysis.Calculus.Darboux
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

Tactic:
absurd (sub_nonpos.1 <| nonpos_of_mul_nonneg_right ?_ (sub_lt_zero.2 hab'))
        (not_le_of_gt hmb)

Premises used: Iff.mpr, sub_lt_zero, nonpos_of_mul_nonneg_right, absurd, Iff.mp, sub_nonpos, not_le_of_gt
-- Module: Mathlib.Analysis.Calculus.Darboux
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
inr : 0 ≤ (a - b) * (f' b - m)
⊢ b ∈ Ioo a b

Tactic:
refine absurd (sub_nonpos.1 <| nonpos_of_mul_nonneg_right ?_ (sub_lt_zero.2 hab'))
        (not_le_of_gt hmb)

Premises used: Iff.mpr, sub_lt_zero, nonpos_of_mul_nonneg_right, absurd, Iff.mp, sub_nonpos, not_le_of_gt
-- Module: Mathlib.Analysis.Calculus.Darboux
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
rw₁ rw₂ : Icc a b ⊆ Icc a b
⊢ segment ℝ b a ⊆ Icc a b

Tactic:
rw [segment_symm, segment_eq_Icc hab]

Premises used: segment_symm, segment_eq_Icc
-- Module: Mathlib.Analysis.Calculus.Darboux
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
⊢ 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])
-- Module: Mathlib.Analysis.Calculus.Darboux
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
this : a - b ∈ posTangentConeAt (Icc a b) b
⊢ 0 ≤ (a - b) * (f' b - m)

Tactic:
simpa only [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply]
        using hc.localize.hasFDerivWithinAt_nonneg (hg b (right_mem_Icc.2 hab)) this

Premises used: Iff.mpr, Set.right_mem_Icc, IsLocalMinOn.hasFDerivWithinAt_nonneg, ContinuousLinearMap.one_apply, IsMinOn.localize, ContinuousLinearMap.smulRight_apply
-- Module: Mathlib.Analysis.Calculus.Darboux
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
hcb : c < b
⊢ c ∈ Ioo a b

Tactic:
⟨hac, hcb⟩

Premises used: Set.Mem, setOf, And.intro, Set.Ioo
-- Module: Mathlib.Analysis.Calculus.Darboux
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
hcb : c < b
⊢ c ∈ Ioo a b

Tactic:
exact ⟨hac, hcb⟩
-- Module: Mathlib.Analysis.Calculus.Darboux
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

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⟩
-- Module: Mathlib.Analysis.Calculus.Darboux
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
right : f' c = m
⊢ m ∈ f' '' Ioo a b

Tactic:
use c, cmem'
-- Module: Mathlib.Analysis.Calculus.Darboux
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
right : f' c - m = 0
⊢ f' c = m

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Calculus.Darboux
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
rwa : c ∈ interior (Icc a b)
rwa₁ rwa₂ rwa₃ rwa₄ : c ∈ Ioo a b
⊢ Icc a b ∈ 𝓝 c

Tactic:
rwa [← mem_interior_iff_mem_nhds, interior_Icc]

Premises used: mem_interior_iff_mem_nhds, interior_Icc
-- Module: Mathlib.Analysis.Calculus.Darboux
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

Tactic:
have : Icc a b ∈ 𝓝 c := by rwa [← mem_interior_iff_mem_nhds, interior_Icc]