awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
hd : ¬c = 0
this :
  Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z)
    (deriv (fun (x : 𝕜) ↦ (c * x) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (z + d / c))
h0 :
  Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) fun (x : 𝕜) ↦
    (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
this₁ :
  deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
    HSMul.hSMul (β := 𝕜) c (deriv (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (c * (z + d / c)))
⊢ Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) fun (x : 𝕜) ↦
    (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
rw [h0, deriv_comp_mul_left c (fun x ↦ (x) ^ (-1 - k : ℤ)) (z + d / c)] at this

Premises used: HSub.hSub, HDiv.hDiv, Nat.cast, HPow.hPow, HAdd.hAdd, deriv_comp_mul_left, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
hd : ¬c = 0
this :
  deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
    HSMul.hSMul (β := 𝕜) c (deriv (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (c * (z + d / c)))
h0 :
  Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) fun (x : 𝕜) ↦
    (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
neg :
  HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k *
      (c * (HSub.hSub (α := 𝕜) (-1) (↑k : 𝕜) * (c * (z + d / c)) ^ (HSub.hSub (α := ℤ) (-1) (↑k : ℤ) - 1))) =
    HPow.hPow (α := 𝕜) (-1) (1 + k) * (HAdd.hAdd (α := 𝕜) 1 (↑k : 𝕜) * (↑k ! : 𝕜)) * c ^ (1 + k) *
      (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))
⊢ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k *
      deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
    HPow.hPow (α := 𝕜) (-1) (1 + k) * (↑((1 + k) * k !) : 𝕜) * c ^ (1 + k) *
      (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
hd : ¬c = 0
this :
  deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
    HSMul.hSMul (β := 𝕜) c (deriv (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (c * (z + d / c)))
h0 :
  Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) fun (x : 𝕜) ↦
    (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
neg :
  HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * c * HSub.hSub (α := 𝕜) (-1) (↑k : 𝕜) *
      (c * z + d) ^ (HSub.hSub (α := ℤ) (-1) (↑k : ℤ) - 1) =
    (↑k ! : 𝕜) * HPow.hPow (α := 𝕜) (-1) (1 + k) * HAdd.hAdd (α := 𝕜) 1 (↑k : 𝕜) * c ^ (1 + k) *
      (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))
⊢ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k *
      (c * (HSub.hSub (α := 𝕜) (-1) (↑k : 𝕜) * (c * (z + d / c)) ^ (HSub.hSub (α := ℤ) (-1) (↑k : ℤ) - 1))) =
    HPow.hPow (α := 𝕜) (-1) (1 + k) * (HAdd.hAdd (α := 𝕜) 1 (↑k : 𝕜) * (↑k ! : 𝕜)) * c ^ (1 + k) *
      (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))

Tactic:
field_simp
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c d : 𝕜
k : ℕ
ihk :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
z : 𝕜
hd : ¬c = 0
this :
  deriv (fun (x : 𝕜) ↦ (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) z =
    HSMul.hSMul (β := 𝕜) c (deriv (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) (c * (z + d / c)))
h0 :
  Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (fun (x : 𝕜) ↦ (c * (x + d / c)) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) fun (x : 𝕜) ↦
    (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)
⊢ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * c * HSub.hSub (α := 𝕜) (-1) (↑k : 𝕜) *
      (c * z + d) ^ (HSub.hSub (α := ℤ) (-1) (↑k : ℤ) - 1) =
    (↑k ! : 𝕜) * HPow.hPow (α := 𝕜) (-1) (1 + k) * HAdd.hAdd (α := 𝕜) 1 (↑k : 𝕜) * c ^ (1 + k) *
      (c * z + d) ^ (-1 - HAdd.hAdd (α := ℤ) 1 (↑k : ℤ))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
k : ℕ
c d : 𝕜
zero :
  Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[0] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (β := ℕ) (-1) 0 * (↑0! : 𝕜) * HPow.hPow (β := ℕ) c 0 *
      (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑0 : ℤ)
succ :
  ∀ (k : ℕ)
    (ihk :
      Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
        HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)),
    Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k + 1] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
      HPow.hPow (α := 𝕜) (-1) (k + 1) * (↑(k + 1)! : 𝕜) * c ^ (k + 1) *
        (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑(k + 1) : ℤ)
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x + d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x + d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
induction k with
  | zero => simp
  | succ k ihk =>
    rw [factorial_succ, add_comm k 1, iterate_add_apply, ihk]
    ext z
    simp only [Int.reduceNeg, iterate_one, deriv_const_mul_field', cast_add, cast_one]
    by_cases hd : c = 0
    · simp [hd]
    · have := deriv_comp_add_const (fun x ↦ (c * x) ^ (-1 - k : ℤ)) (d / c) z
      have h0 : (fun x ↦ (c * (x + d / c)) ^ (-1 - (k : ℤ))) =
        (fun x ↦ (c * x + d) ^ (-1 - (k : ℤ))) := by
        ext y
        field_simp
      rw [h0, deriv_comp_mul_left c (fun x ↦ (x) ^ (-1 - k : ℤ)) (z + d / c)] at this
      simp [this]
      field_simp
      ring_nf

Premises used: Function.iterate_add_apply, Nat.factorial_succ, Int.reduceNeg, deriv_const_mul_field', add_comm, Nat.cast_add, Function.iterate_one, Nat.zero, OfNat.ofNat, Nat.succ, Nat.cast_one
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
k : ℕ
c d : 𝕜
⊢ Eq.{u + 1} (α := 𝕜 → 𝕜) (deriv^[k] fun (x : 𝕜) ↦ (c * x - d)⁻¹) fun (x : 𝕜) ↦
    HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * c ^ k * (c * x - d) ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)

Tactic:
simpa [sub_eq_add_neg] using iter_deriv_inv_linear k c (-d)

Premises used: sub_eq_add_neg, iter_deriv_inv_linear, Neg.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
m : ℤ
f : E → 𝕜
t : Set E
a : E
hf : DifferentiableWithinAt 𝕜 f t a
h : f a ≠ 0 ∨ 0 ≤ m
⊢ DifferentiableWithinAt 𝕜 (F := 𝕜) (fun (x : E) ↦ f x ^ m) t a

Tactic:
(differentiableAt_zpow.2 h).comp_differentiableWithinAt a hf

Premises used: Iff.mpr, differentiableAt_zpow, DifferentiableAt.comp_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
m : ℤ
f : E → 𝕜
a : E
hf : DifferentiableAt 𝕜 f a
h : f a ≠ 0 ∨ 0 ≤ m
⊢ DifferentiableAt 𝕜 (F := 𝕜) (fun (x : E) ↦ f x ^ m) a

Tactic:
(differentiableAt_zpow.2 h).comp a hf

Premises used: Iff.mpr, differentiableAt_zpow, DifferentiableAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
m : ℤ
f : E → 𝕜
t : Set E
hf : DifferentiableOn 𝕜 f t
h : (∀ x ∈ t, f x ≠ 0) ∨ 0 ≤ m
⊢ DifferentiableOn 𝕜 (F := 𝕜) (fun (x : E) ↦ f x ^ m) t

Tactic:
fun x hx =>
  (hf x hx).zpow <| h.imp_left fun h => h x hx

Premises used: Or.imp_left, DifferentiableOn, DifferentiableWithinAt.zpow
-- Module: Mathlib.Analysis.Calculus.Deriv.ZPow
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
m : ℤ
f : E → 𝕜
hf : Differentiable 𝕜 f
h : (∀ (x : E), f x ≠ 0) ∨ 0 ≤ m
⊢ Differentiable 𝕜 (F := 𝕜) fun (x : E) ↦ f x ^ m

Tactic:
fun x => (hf x).zpow <| h.imp_left fun h => h x

Premises used: Differentiable, DifferentiableAt.zpow, Or.imp_left
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
pos : ∀ (g₀ : a < b), ContinuousOn f (Ioc a b)
neg : ∀ (g₀ : b ≤ a), ContinuousOn f (Ioc a b)
⊢ ContinuousOn f (Ioc a b)

Tactic:
by_cases! g₀ : a < b
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : a < b
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) {b} x → ContinuousAt f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : a < b
⊢ ContinuousOn f (Ioc a b)

Tactic:
exact Ioo_union_right g₀ ▸ hd₀.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : b ≤ a
⊢ ContinuousOn f (Ioc a b)

Tactic:
simp [Ioc_eq_empty_of_le g₀]

Premises used: Set.Ioc_eq_empty_of_le
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioo a b)
pos : ∀ (g₀ : a < b), ContinuousOn f (Ico a b)
neg : ∀ (g₀ : b ≤ a), ContinuousOn f (Ico a b)
⊢ ContinuousOn f (Ico a b)

Tactic:
by_cases! g₀ : a < b
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : a < b
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) {a} x → ContinuousAt f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : a < b
⊢ ContinuousOn f (Ico a b)

Tactic:
exact Ioo_union_left g₀ ▸ hd₀.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : b ≤ a
⊢ ContinuousOn f (Ico a b)

Tactic:
simp [Ico_eq_empty_of_le g₀]

Premises used: Set.Ico_eq_empty_of_le
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
pos : ∀ (g₀ : a ≤ b), ContinuousOn f (Icc a b)
neg : ∀ (g₀ : b < a), ContinuousOn f (Icc a b)
⊢ ContinuousOn f (Icc a b)

Tactic:
by_cases! g₀ : a ≤ b
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : a ≤ b
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) {a, b} x → ContinuousAt f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : a ≤ b
⊢ ContinuousOn f (Icc a b)

Tactic:
exact Ioo_union_both g₀ ▸ hd₀.continuousOn.union_continuousAt isOpen_Ioo (by simp_all)
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
g₀ : b < a
⊢ ContinuousOn f (Icc a b)

Tactic:
simp [Icc_eq_empty_of_lt g₀]

Premises used: Set.Icc_eq_empty_of_lt
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
simp_rw : ContinuousOn f (Iio b ∪ {b})
⊢ ContinuousOn f (Iic b)

Tactic:
simp_rw [← Iio_union_right]

Premises used: Set.Iio_union_right
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) {b} x → ContinuousAt f x

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
b : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
⊢ ContinuousOn f (Iio b ∪ {b})

Tactic:
apply hd₀.continuousOn.union_continuousAt isOpen_Iio (by simp [h])

Premises used: DifferentiableOn.continuousOn, ContinuousOn.union_continuousAt, isOpen_Iio
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioi a)
rw : ContinuousOn f (Ioi a ∪ {a})
⊢ ContinuousOn f (Ici a)

Tactic:
rw [← Ioi_union_left]

Premises used: Set.Ioi_union_left
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioi a)
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) {a} x → ContinuousAt f x

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioi a)
⊢ ContinuousOn f (Ioi a ∪ {a})

Tactic:
exact hd₀.continuousOn.union_continuousAt isOpen_Ioi (by simp [h])

Premises used: DifferentiableOn.continuousOn, ContinuousOn.union_continuousAt, isOpen_Ioi
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Ioo a c) b

Tactic:
isMaxOn_Ioo_of_mono_anti ?_ ?_

Premises used: isMaxOn_Ioo_of_mono_anti
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Ioc a b)
refine_2 : AntitoneOn f (Ico b c)
⊢ IsMaxOn f (Ioo a c) b

Tactic:
refine isMaxOn_Ioo_of_mono_anti ?_ ?_

Premises used: isMaxOn_Ioo_of_mono_anti
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
refine_1₁ : ∀ x ∈ interior (Ioc a b), 0 ≤ deriv f x
⊢ MonotoneOn f (Ioc a b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc h hd₀)

Premises used: monotoneOn_of_deriv_nonneg, convex_Ioc, _private.0.continuousOn_Ioc
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ DifferentiableOn ℝ f (interior (Ioc a b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Ioc a b), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
refine_2₁ : ∀ x ∈ interior (Ico b c), deriv f x ≤ 0
⊢ AntitoneOn f (Ico b c)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico h hd₁)

Premises used: convex_Ico, _private.0.continuousOn_Ico, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ DifferentiableOn ℝ f (interior (Ico b c))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
h : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Ico b c), deriv f x ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Ioc a c) b

Tactic:
isMaxOn_Ioc_of_mono_anti ?_ ?_

Premises used: isMaxOn_Ioc_of_mono_anti
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Ioc a b)
refine_2 : AntitoneOn f (Icc b c)
⊢ IsMaxOn f (Ioc a c) b

Tactic:
refine isMaxOn_Ioc_of_mono_anti ?_ ?_

Premises used: isMaxOn_Ioc_of_mono_anti
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Ioc a b))
refine_1₁ : ∀ x ∈ interior (Ioc a b), 0 ≤ deriv f x
⊢ MonotoneOn f (Ioc a b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Ioc a b) (continuousOn_Ioc hb hd₀)

Premises used: monotoneOn_of_deriv_nonneg, convex_Ioc, _private.0.continuousOn_Ioc
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ DifferentiableOn ℝ f (interior (Ioc a b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Ioc a b), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Icc b c))
refine_2₁ : ∀ x ∈ interior (Icc b c), deriv f x ≤ 0
⊢ AntitoneOn f (Icc b c)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Icc b c) (continuousOn_Icc hb hc hd₁)

Premises used: _private.0.continuousOn_Icc, convex_Icc, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ DifferentiableOn ℝ f (interior (Icc b c))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Icc b c), deriv f x ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Ico a c) b

Tactic:
isMaxOn_Ico_of_mono_anti ?_ ?_

Premises used: isMaxOn_Ico_of_mono_anti
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Icc a b)
refine_2 : AntitoneOn f (Ico b c)
⊢ IsMaxOn f (Ico a c) b

Tactic:
refine isMaxOn_Ico_of_mono_anti ?_ ?_

Premises used: isMaxOn_Ico_of_mono_anti
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : DifferentiableOn ℝ f (interior (Icc a b))
refine_1₁ : ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x
⊢ MonotoneOn f (Icc a b)

Tactic:
apply monotoneOn_of_deriv_nonneg (convex_Icc a b) (continuousOn_Icc ha hb hd₀)

Premises used: _private.0.continuousOn_Icc, monotoneOn_of_deriv_nonneg, convex_Icc
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ DifferentiableOn ℝ f (interior (Icc a b))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Icc a b), 0 ≤ deriv f x

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_2 : DifferentiableOn ℝ f (interior (Ico b c))
refine_2₁ : ∀ x ∈ interior (Ico b c), deriv f x ≤ 0
⊢ AntitoneOn f (Ico b c)

Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ico b c) (continuousOn_Ico hb hd₁)

Premises used: convex_Ico, _private.0.continuousOn_Ico, antitoneOn_of_deriv_nonpos
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ DifferentiableOn ℝ f (interior (Ico b c))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ ∀ x ∈ interior (Ico b c), deriv f x ≤ 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
⊢ IsMaxOn f (Icc a c) b

Tactic:
isMaxOn_Icc_of_mono_anti ?_ ?_

Premises used: isMaxOn_Icc_of_mono_anti
-- Module: Mathlib.Analysis.Calculus.DerivativeTest
Goal:
f : ℝ → ℝ
a b c : ℝ
ha : ContinuousAt f a
hb : ContinuousAt f b
hc : ContinuousAt f c
hd₀ : DifferentiableOn ℝ f (Ioo a b)
hd₁ : DifferentiableOn ℝ f (Ioo b c)
h₀ : ∀ x ∈ Ioo a b, 0 ≤ deriv f x
h₁ : ∀ x ∈ Ioo b c, deriv f x ≤ 0
refine_1 : MonotoneOn f (Icc a b)
refine_2 : AntitoneOn f (Icc b c)
⊢ IsMaxOn f (Icc a c) b

Tactic:
refine isMaxOn_Icc_of_mono_anti ?_ ?_

Premises used: isMaxOn_Icc_of_mono_anti