awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
hf : Differentiable ℝ f
C : ℝ
hf'_ge : ∀ (x : ℝ), C ≤ deriv f x
x y : ℝ
hxy : x ≤ y
⊢ C * (y - x) ≤ f y - f x

Tactic:
convex_univ.mul_sub_le_image_sub_of_le_deriv hf.continuous.continuousOn hf.differentiableOn
    (fun x _ => hf'_ge x) x trivial y trivial hxy

Premises used: Continuous.continuousOn, trivial, Convex.mul_sub_le_image_sub_of_le_deriv, convex_univ, Differentiable.differentiableOn, Differentiable.continuous
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x_1 : ℝ
hx_1 : x_1 ∈ D
y : ℝ
hy : y ∈ D
hxy : x_1 < y
x : ℝ
hx : x ∈ interior D
rw : deriv f x < C
⊢ -C < deriv (fun (y : ℝ) ↦ -f y) x

Tactic:
rw [deriv.fun_neg, neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, deriv.fun_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x_1 : ℝ
hx_1 : x_1 ∈ D
y : ℝ
hy : y ∈ D
hxy : x_1 < y
x : ℝ
hx : x ∈ interior D
⊢ deriv f x < C

Tactic:
lt_hf' x hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x_1 : ℝ
hx_1 : x_1 ∈ D
y : ℝ
hy : y ∈ D
hxy : x_1 < y
x : ℝ
hx : x ∈ interior D
⊢ deriv f x < C

Tactic:
exact lt_hf' x hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
⊢ ∀ x ∈ interior D, -C < deriv (fun (y : ℝ) ↦ -f y) x

Tactic:
have hf'_gt : ∀ x ∈ interior D, -C < deriv (fun y => -f y) x := fun x hx => by
    rw [deriv.fun_neg, neg_lt_neg_iff]
    exact lt_hf' x hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
lt_hf' : ∀ x ∈ interior D, deriv f x < C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x < y
hf'_gt : ∀ x ∈ interior D, -C < deriv (fun (y : ℝ) ↦ -f y) x
linarith : C * (y - x) ≤ f y - f x → C * (y - x) - (f y - f x) + (-C * (y - x) - (-f y - -f x)) = 0
⊢ f y - f x < C * (y - x)

Tactic:
linarith [hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x hx y hy hxy]

Premises used: ContinuousOn.neg, DifferentiableOn.neg, Convex.mul_sub_lt_image_sub_of_lt_deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
hf : Differentiable ℝ f
C : ℝ
lt_hf' : ∀ (x : ℝ), deriv f x < C
x y : ℝ
hxy : x < y
⊢ f y - f x < C * (y - x)

Tactic:
convex_univ.image_sub_lt_mul_sub_of_deriv_lt hf.continuous.continuousOn hf.differentiableOn
    (fun x _ => lt_hf' x) x trivial y trivial hxy

Premises used: Continuous.continuousOn, trivial, Convex.image_sub_lt_mul_sub_of_deriv_lt, convex_univ, Differentiable.differentiableOn, Differentiable.continuous
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x_1 : ℝ
hx_1 : x_1 ∈ D
y : ℝ
hy : y ∈ D
hxy : x_1 ≤ y
x : ℝ
hx : x ∈ interior D
rw : deriv f x ≤ C
⊢ -C ≤ deriv (fun (y : ℝ) ↦ -f y) x

Tactic:
rw [deriv.fun_neg, neg_le_neg_iff]

Premises used: deriv.fun_neg, neg_le_neg_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x_1 : ℝ
hx_1 : x_1 ∈ D
y : ℝ
hy : y ∈ D
hxy : x_1 ≤ y
x : ℝ
hx : x ∈ interior D
⊢ deriv f x ≤ C

Tactic:
le_hf' x hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x_1 : ℝ
hx_1 : x_1 ∈ D
y : ℝ
hy : y ∈ D
hxy : x_1 ≤ y
x : ℝ
hx : x ∈ interior D
⊢ deriv f x ≤ C

Tactic:
exact le_hf' x hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
⊢ ∀ x ∈ interior D, -C ≤ deriv (fun (y : ℝ) ↦ -f y) x

Tactic:
have hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (fun y => -f y) x := fun x hx => by
    rw [deriv.fun_neg, neg_le_neg_iff]
    exact le_hf' x hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
le_hf' : ∀ x ∈ interior D, deriv f x ≤ C
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (fun (y : ℝ) ↦ -f y) x
linarith : C * (y - x) < f y - f x → C * (y - x) - (f y - f x) + (-C * (y - x) - (-f y - -f x)) = 0
⊢ f y - f x ≤ C * (y - x)

Tactic:
linarith [hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x hx y hy hxy]

Premises used: ContinuousOn.neg, Convex.mul_sub_le_image_sub_of_le_deriv, DifferentiableOn.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
hf : Differentiable ℝ f
C : ℝ
le_hf' : ∀ (x : ℝ), deriv f x ≤ C
x y : ℝ
hxy : x ≤ y
⊢ f y - f x ≤ C * (y - x)

Tactic:
convex_univ.image_sub_le_mul_sub_of_deriv_le hf.continuous.continuousOn hf.differentiableOn
    (fun x _ => le_hf' x) x trivial y trivial hxy

Premises used: Continuous.continuousOn, trivial, Convex.image_sub_le_mul_sub_of_deriv_le, convex_univ, Differentiable.differentiableOn, Differentiable.continuous
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ DifferentiableOn ℝ f (interior D)

Tactic:
have : DifferentiableOn ℝ f (interior D) := fun z hz =>
    (differentiableAt_of_deriv_ne_zero (hf' z hz).ne').differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
this : DifferentiableOn ℝ f (interior D)
⊢ x < y → f x < f y

Tactic:
simpa only [zero_mul, sub_pos] using
    hD.mul_sub_lt_image_sub_of_lt_deriv hf this hf' x hx y hy

Premises used: sub_pos, MulZeroClass.zero_mul, Convex.mul_sub_lt_image_sub_of_lt_deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
hf' : ∀ (x : ℝ), 0 < deriv f x
⊢ StrictMono f

Tactic:
strictMonoOn_univ.1 <| strictMonoOn_of_deriv_pos convex_univ (fun z _ =>
    (differentiableAt_of_deriv_ne_zero (hf' z).ne').differentiableWithinAt.continuousWithinAt)
    fun x _ => hf' x

Premises used: DifferentiableAt.differentiableWithinAt, strictMonoOn_univ, LT.lt.ne', convex_univ, DifferentiableWithinAt.continuousWithinAt, Iff.mp, strictMonoOn_of_deriv_pos, differentiableAt_of_deriv_ne_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
rw : 0 < f' x
⊢ 0 < deriv f x

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]

Premises used: isOpen_interior, deriv_eqOn
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 < f' x

Tactic:
hf'₀ _ hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 < f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 < f' x

Tactic:
exact hf'₀ _ hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
rw : 0 < f' x
⊢ 0 < deriv f x

Tactic:
rw [(hf _).deriv]

Premises used: HasDerivAt.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < f' x

Tactic:
hf' _
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), 0 < f' x
x : ℝ
⊢ 0 < f' x

Tactic:
exact hf' _
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
⊢ f x ≤ f y

Tactic:
simpa only [zero_mul, sub_nonneg] using
    hD.mul_sub_le_image_sub_of_le_deriv hf hf' hf'_nonneg x hx y hy hxy

Premises used: MulZeroClass.zero_mul, Convex.mul_sub_le_image_sub_of_le_deriv, sub_nonneg
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
hf : Differentiable ℝ f
hf' : ∀ (x : ℝ), 0 ≤ deriv f x
⊢ Monotone f

Tactic:
monotoneOn_univ.1 <|
    monotoneOn_of_deriv_nonneg convex_univ hf.continuous.continuousOn hf.differentiableOn fun x _ =>
      hf' x

Premises used: Continuous.continuousOn, monotoneOn_of_deriv_nonneg, convex_univ, Iff.mp, Differentiable.differentiableOn, Differentiable.continuous, monotoneOn_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
rw : 0 ≤ f' x
⊢ 0 ≤ deriv f x

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]

Premises used: isOpen_interior, deriv_eqOn
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ f' x

Tactic:
hf'₀ _ hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, 0 ≤ f' x
x : ℝ
hx : x ∈ interior D
⊢ 0 ≤ f' x

Tactic:
exact hf'₀ _ hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
rw : 0 ≤ f' x
⊢ 0 ≤ deriv f x

Tactic:
rw [(hf _).deriv]

Premises used: HasDerivAt.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ f' x

Tactic:
hf' _
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : 0 ≤ f'
x : ℝ
⊢ 0 ≤ f' x

Tactic:
exact hf' _
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, deriv f x < 0
x : ℝ
hx : x ∈ D
y : ℝ
⊢ y ∈ D → x < y → f y < f x

Tactic:
simpa only [zero_mul, sub_lt_zero] using
    hD.image_sub_lt_mul_sub_of_deriv_lt hf
      (fun z hz => (differentiableAt_of_deriv_ne_zero (hf' z hz).ne).differentiableWithinAt) hf' x
      hx y

Premises used: sub_lt_zero, MulZeroClass.zero_mul, Convex.image_sub_lt_mul_sub_of_deriv_lt, DifferentiableAt.differentiableWithinAt, differentiableAt_of_deriv_ne_zero, LT.lt.ne
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
hf' : ∀ (x : ℝ), deriv f x < 0
⊢ StrictAnti f

Tactic:
strictAntiOn_univ.1 <| strictAntiOn_of_deriv_neg convex_univ
      (fun z _ =>
        (differentiableAt_of_deriv_ne_zero (hf' z).ne).differentiableWithinAt.continuousWithinAt)
      fun x _ => hf' x

Premises used: DifferentiableAt.differentiableWithinAt, convex_univ, DifferentiableWithinAt.continuousWithinAt, Iff.mp, strictAntiOn_of_deriv_neg, strictAntiOn_univ, differentiableAt_of_deriv_ne_zero, LT.lt.ne
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
rw : f' x < 0
⊢ deriv f x < 0

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]

Premises used: isOpen_interior, deriv_eqOn
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
⊢ f' x < 0

Tactic:
hf'₀ _ hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x < 0
x : ℝ
hx : x ∈ interior D
⊢ f' x < 0

Tactic:
exact hf'₀ _ hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
rw : f' x < 0
⊢ deriv f x < 0

Tactic:
rw [(hf _).deriv]

Premises used: HasDerivAt.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ f' x < 0

Tactic:
hf' _
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : ∀ (x : ℝ), f' x < 0
x : ℝ
⊢ f' x < 0

Tactic:
exact hf' _
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
⊢ f y ≤ f x

Tactic:
simpa only [zero_mul, sub_nonpos] using
    hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos x hx y hy hxy

Premises used: Convex.image_sub_le_mul_sub_of_deriv_le, MulZeroClass.zero_mul, sub_nonpos
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
hf : Differentiable ℝ f
hf' : ∀ (x : ℝ), deriv f x ≤ 0
⊢ Antitone f

Tactic:
antitoneOn_univ.1 <|
    antitoneOn_of_deriv_nonpos convex_univ hf.continuous.continuousOn hf.differentiableOn fun x _ =>
      hf' x

Premises used: Continuous.continuousOn, convex_univ, antitoneOn_univ, Iff.mp, Differentiable.differentiableOn, antitoneOn_of_deriv_nonpos, Differentiable.continuous
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
rw : f' x ≤ 0
⊢ deriv f x ≤ 0

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]

Premises used: isOpen_interior, deriv_eqOn
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
⊢ f' x ≤ 0

Tactic:
hf'₀ _ hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
⊢ f' x ≤ 0

Tactic:
exact hf'₀ _ hx
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
rw : f' x ≤ 0
⊢ deriv f x ≤ 0

Tactic:
rw [(hf _).deriv]

Premises used: HasDerivAt.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ f' x ≤ 0

Tactic:
hf' _
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f f' : ℝ → ℝ
hf : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : f' ≤ 0
x : ℝ
⊢ f' x ≤ 0

Tactic:
exact hf' _
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
⊢ Ioo 0 1 ⊆ I

Tactic:
have hsub : Ioo (0 : ℝ) 1 ⊆ I := Ioo_subset_Icc_self
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
⊢ MapsTo g I s

Tactic:
have hmaps : MapsTo g I s := hs.mapsTo_lineMap xs ys
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
⊢ ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t

Tactic:
have hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) (f' (g t) (y - x)) I t := fun t ht =>
    (hf _ (hmaps ht)).comp_hasDerivWithinAt t AffineMap.hasDerivWithinAt_lineMap hmaps
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
refine_1 : ContinuousOn (f ∘ g) (Icc 0 1)
refine_2 :
  ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) x_1 → HasDerivAt (f ∘ g) ((f' (g x_1) : (a : E) → ℝ) (y - x)) x_1
⊢ ∃ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧
      (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0

Tactic:
refine exists_hasDerivAt_eq_slope (f ∘ g) _ (by simp) ?_ ?_

Premises used: Function.comp, exists_hasDerivAt_eq_slope
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
⊢ ContinuousOn (f ∘ g) (Icc 0 1)

Tactic:
fun t Ht => (hfg t Ht).continuousWithinAt

Premises used: ContinuousOn, HasDerivWithinAt.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
⊢ ContinuousOn (f ∘ g) (Icc 0 1)

Tactic:
exact fun t Ht => (hfg t Ht).continuousWithinAt

Premises used: HasDerivWithinAt.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
⊢ ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) x_1 → HasDerivAt (f ∘ g) ((f' (g x_1) : (a : E) → ℝ) (y - x)) x_1

Tactic:
fun t Ht => (hfg t <| hsub Ht).hasDerivAt (Icc_mem_nhds Ht.1 Ht.2)

Premises used: And.right, And.left, HasDerivWithinAt.hasDerivAt, Icc_mem_nhds
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
⊢ ∀ (x_1 : ℝ), Membership.mem (γ := Set ℝ) (Ioo 0 1) x_1 → HasDerivAt (f ∘ g) ((f' (g x_1) : (a : E) → ℝ) (y - x)) x_1

Tactic:
exact fun t Ht => (hfg t <| hsub Ht).hasDerivAt (Icc_mem_nhds Ht.1 Ht.2)

Premises used: And.right, And.left, HasDerivWithinAt.hasDerivAt, Icc_mem_nhds
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
⊢ ∃ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧
      (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0

Tactic:
have hMVT : ∃ t ∈ Ioo (0 : ℝ) 1, f' (g t) (y - x) = (f (g 1) - f (g 0)) / (1 - 0) := by
    refine exists_hasDerivAt_eq_slope (f ∘ g) _ (by simp) ?_ ?_
    · exact fun t Ht => (hfg t Ht).continuousWithinAt
    · exact fun t Ht => (hfg t <| hsub Ht).hasDerivAt (Icc_mem_nhds Ht.1 Ht.2)
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
hMVT :
  ∃ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) t ∧
      (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
rcases :
  ∀ (t : ℝ) (Ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t)
    (hMVT' : (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0),
    ∃ z ∈ segment ℝ x y, f y - f x = (f' z : (a : E) → ℝ) (y - x)
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z : (a : E) → ℝ) (y - x)

Tactic:
rcases hMVT with ⟨t, Ht, hMVT'⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun (t : ℝ) ↦ (AffineMap.lineMap x y : (a : ℝ) → E) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t) : (a : E) → ℝ) (y - x)) I t
t : ℝ
Ht : Membership.mem (γ := Set ℝ) (Ioo 0 1) t
hMVT' : (f' (g t) : (a : E) → ℝ) (y - x) = (f (g 1) - f (g 0)) / HSub.hSub (α := ℝ) 1 0
rw :
  ∃ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) x_1 ∧
      f y - f x = (f' ((AffineMap.lineMap x y : (a : ℝ) → E) x_1) : (a : E) → ℝ) (y - x)
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z : (a : E) → ℝ) (y - x)

Tactic:
rw [segment_eq_image_lineMap, exists_mem_image]

Premises used: segment_eq_image_lineMap, Set.exists_mem_image