awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
α : Type u_1
β : Type u_2
inst : CommRing β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
f : α → β
inst_3 : DecidablePred fun (x : α) ↦ f x ≤ 0
s : Finset α
h0 : Even #({x ∈ s | f x ≤ 0})
rw : HMul.hMul (α := β) (∏ x ∈ s, if f x ≤ 0 then -1 else 1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₁ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s with ¬f x ≤ 0, 1) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₂ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) 1 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₃ : HMul.hMul (α := β) (∏ x ∈ s with f x ≤ 0, -1) (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₄ : HPow.hPow (α := β) (-1) #({x ∈ s | f x ≤ 0}) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₅ : HPow.hPow (α := β) (-1) (#({x ∈ s | f x ≤ 0}) % 2) * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₆ : HPow.hPow (α := β) (β := ℕ) (-1) 0 * ∏ x ∈ s, f x = ∏ x ∈ s, f x
rw₇ : HMul.hMul (α := β) 1 (∏ x ∈ s, f x) = ∏ x ∈ s, f x
rw₈ rw₉ : Eq.{u_2 + 1} (α := β) (∏ x ∈ s, f x) (∏ x ∈ s, f x)
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x) (∏ x ∈ s, f x)

Tactic:
rw [Finset.prod_mul_distrib, Finset.prod_ite, Finset.prod_const_one, mul_one,
        Finset.prod_const, neg_one_pow_eq_pow_mod_two, Nat.even_iff.1 h0, pow_zero, one_mul]

Premises used: Finset.prod_mul_distrib, neg_one_pow_eq_pow_mod_two, Finset.prod_const, pow_zero, Finset.prod_const_one, Finset.prod_ite, Iff.mp, Nat.even_iff, mul_one, one_mul
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
hn : Even n
rcases : ∀ (n : ℕ), LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + n), (m - (↑k : ℤ)))
⊢ LE.le (α := ℤ) 0 (∏ k ∈ Finset.range n, (m - (↑k : ℤ)))

Tactic:
rcases hn with ⟨n, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
⊢ LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 0), (m - (↑k : ℤ)))

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + n), (m - (↑k : ℤ)))
⊢ LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))

Tactic:
rw [← two_mul] at ihn

Premises used: two_mul
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
succ :
  0 ≤
    (∏ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 1 1 * n), (m - (↑x : ℤ))) *
      ((m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n) : ℤ)) * (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n + 1) : ℤ)))
⊢ LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + 1 + (n + 1)), (m - (↑k : ℤ)))

Tactic:
rw [← two_mul, mul_add, mul_one, ← one_add_one_eq_two, ← add_assoc,
      Finset.prod_range_succ, Finset.prod_range_succ, mul_assoc]

Premises used: add_assoc, mul_assoc, two_mul, one_add_one_eq_two, Finset.prod_range_succ, mul_add, mul_one
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
⊢ 0 ≤
    (∏ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 1 1 * n), (m - (↑x : ℤ))) *
      ((m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n) : ℤ)) * (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n + 1) : ℤ)))

Tactic:
mul_nonneg ihn ?_

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
succ : 0 ≤ (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n) : ℤ)) * (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n + 1) : ℤ))
⊢ 0 ≤
    (∏ x ∈ Finset.range (HAdd.hAdd (α := ℕ) 1 1 * n), (m - (↑x : ℤ))) *
      ((m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n) : ℤ)) * (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n + 1) : ℤ)))

Tactic:
refine mul_nonneg ihn ?_

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
succ : ∀ (k : ℕ), 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))
⊢ 0 ≤ (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n) : ℤ)) * (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n + 1) : ℤ))

Tactic:
generalize (1 + 1) * n = k

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
k : ℕ
succ : ∀ (hmk : m ≤ (↑k : ℤ)), 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))
succ₁ : ∀ (hmk : (↑k : ℤ) < m), 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))
⊢ 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))

Tactic:
rcases le_or_gt m k with hmk | hmk

Premises used: Nat.cast, le_or_gt
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
k : ℕ
hmk : m ≤ (↑k : ℤ)
⊢ m ≤ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1

Tactic:
have : m ≤ k + 1 := hmk.trans (lt_add_one (k : ℤ)).le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
k : ℕ
hmk : m ≤ (↑k : ℤ)
this : m ≤ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1
⊢ 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))

Tactic:
mul_nonneg_of_nonpos_of_nonpos (sub_nonpos_of_le hmk) _

Premises used: mul_nonneg_of_nonpos_of_nonpos, sub_nonpos_of_le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
k : ℕ
hmk : m ≤ (↑k : ℤ)
this : m ≤ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1
succ : m - (↑(k + 1) : ℤ) ≤ 0
⊢ 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))

Tactic:
convert! mul_nonneg_of_nonpos_of_nonpos (sub_nonpos_of_le hmk) _

Premises used: mul_nonneg_of_nonpos_of_nonpos, sub_nonpos_of_le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
k : ℕ
hmk : m ≤ (↑k : ℤ)
this : m ≤ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1
⊢ m - HAdd.hAdd (α := ℤ) (↑k : ℤ) 1 ≤ 0

Tactic:
sub_nonpos_of_le this

Premises used: sub_nonpos_of_le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
k : ℕ
hmk : m ≤ (↑k : ℤ)
this : m ≤ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1
⊢ m - (↑(k + 1) : ℤ) ≤ 0

Tactic:
convert! sub_nonpos_of_le this

Premises used: sub_nonpos_of_le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
k : ℕ
hmk : (↑k : ℤ) < m
⊢ 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))

Tactic:
mul_nonneg (sub_nonneg_of_le hmk.le) (sub_nonneg_of_le hmk)

Premises used: mul_nonneg, sub_nonneg_of_le, LT.lt.le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
k : ℕ
hmk : (↑k : ℤ) < m
⊢ 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))

Tactic:
exact mul_nonneg (sub_nonneg_of_le hmk.le) (sub_nonneg_of_le hmk)

Premises used: mul_nonneg, sub_nonneg_of_le, LT.lt.le
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
zero : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 0), (m - (↑k : ℤ)))
succ :
  ∀ (n : ℕ) (ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + n), (m - (↑k : ℤ)))),
    LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + 1 + (n + 1)), (m - (↑k : ℤ)))
⊢ LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + n), (m - (↑k : ℤ)))

Tactic:
induction n with
  | zero => simp
  | succ n ihn =>
    rw [← two_mul] at ihn
    rw [← two_mul, mul_add, mul_one, ← one_add_one_eq_two, ← add_assoc,
      Finset.prod_range_succ, Finset.prod_range_succ, mul_assoc]
    refine mul_nonneg ihn ?_; generalize (1 + 1) * n = k
    rcases le_or_gt m k with hmk | hmk
    · have : m ≤ k + 1 := hmk.trans (lt_add_one (k : ℤ)).le
      convert! mul_nonneg_of_nonpos_of_nonpos (sub_nonpos_of_le hmk) _
      convert! sub_nonpos_of_le this
    · exact mul_nonneg (sub_nonneg_of_le hmk.le) (sub_nonneg_of_le hmk)

Premises used: add_assoc, mul_assoc, two_mul, one_add_one_eq_two, HAdd.hAdd, Finset.prod_range_succ, mul_add, mul_one, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 (↑n : ℤ)
⊢ LT.lt (α := ℤ) 0 (∏ k ∈ Finset.range n, (m - (↑k : ℤ)))

Tactic:
(int_prod_range_nonneg m n hn).lt_of_ne fun h => hm ?_

Premises used: int_prod_range_nonneg, LE.le.lt_of_ne
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 (↑n : ℤ)
refine : ∀ (h : Eq (α := ℤ) 0 (∏ k ∈ Finset.range n, (m - (↑k : ℤ)))), Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) m
⊢ LT.lt (α := ℤ) 0 (∏ k ∈ Finset.range n, (m - (↑k : ℤ)))

Tactic:
refine (int_prod_range_nonneg m n hn).lt_of_ne fun h => hm ?_

Premises used: int_prod_range_nonneg, LE.le.lt_of_ne
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 (↑n : ℤ)
h : Eq (α := ℤ) 0 (∏ k ∈ Finset.range n, (m - (↑k : ℤ)))
⊢ ∃ a ∈ Finset.range n, m - (↑a : ℤ) = 0

Tactic:
rw [eq_comm, Finset.prod_eq_zero_iff] at h

Premises used: eq_comm, Finset.prod_eq_zero_iff
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 (↑n : ℤ)
h : ∃ a ∈ Finset.range n, m - (↑a : ℤ) = 0
obtain : ∀ (a : ℕ) (ha : a ∈ Finset.range n) (h : m - (↑a : ℤ) = 0), Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) m
⊢ Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) m

Tactic:
obtain ⟨a, ha, h⟩ := h
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 (↑n : ℤ)
a : ℕ
ha : a ∈ Finset.range n
h : m - (↑a : ℤ) = 0
rw : Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) (↑a : ℤ)
⊢ Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) m

Tactic:
rw [sub_eq_zero.1 h]

Premises used: sub_eq_zero, Iff.mp
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 (↑n : ℤ)
a : ℕ
ha : a ∈ Finset.range n
h : m - (↑a : ℤ) = 0
⊢ Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) (↑a : ℤ)

Tactic:
⟨Int.natCast_nonneg _, Int.ofNat_lt.2 <| Finset.mem_range.1 ha⟩

Premises used: Iff.mpr, Set.Mem, setOf, Int.ofNat_lt, Finset.mem_range, Set.Ico, And.intro, Iff.mp, Int.natCast_nonneg
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 (↑n : ℤ)
a : ℕ
ha : a ∈ Finset.range n
h : m - (↑a : ℤ) = 0
⊢ Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) (↑a : ℤ)

Tactic:
exact ⟨Int.natCast_nonneg _, Int.ofNat_lt.2 <| Finset.mem_range.1 ha⟩
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ m) (Ioi 0)
hf'' : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → LT.lt (α := ℝ) (0 : ℝ) (deriv^[2] (fun (x : ℝ) ↦ x ^ m) x : ℝ)
⊢ StrictConvexOn ℝ (β := ℝ) (Ioi 0) fun (x : ℝ) ↦ x ^ m

Tactic:
apply strictConvexOn_of_deriv2_pos' (convex_Ioi 0)

Premises used: strictConvexOn_of_deriv2_pos', OfNat.ofNat, convex_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ m) (Ioi 0)

Tactic:
(continuousOn_zpow₀ m).mono fun x hx => ne_of_gt hx

Premises used: ne_of_gt, ContinuousOn.mono, continuousOn_zpow₀
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ m) (Ioi 0)

Tactic:
exact (continuousOn_zpow₀ m).mono fun x hx => ne_of_gt hx

Premises used: ne_of_gt, ContinuousOn.mono, continuousOn_zpow₀
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < x

Tactic:
rw [mem_Ioi] at hx

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hf'' : 0 < (∏ i ∈ Finset.range 2, HSub.hSub (α := ℝ) (↑m : ℝ) (↑i : ℝ)) * x ^ (m - (↑2 : ℤ))
⊢ LT.lt (α := ℝ) (0 : ℝ) (deriv^[2] (fun (x : ℝ) ↦ x ^ m) x : ℝ)

Tactic:
rw [iter_deriv_zpow]

Premises used: iter_deriv_zpow
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (∏ i ∈ Finset.range 2, HSub.hSub (α := ℝ) (↑m : ℝ) (↑i : ℝ)) * x ^ (m - (↑2 : ℤ))

Tactic:
mul_pos ?_ (zpow_pos hx _)

Premises used: zpow_pos, mul_pos
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hf'' : LT.lt (α := ℝ) 0 (∏ i ∈ Finset.range 2, HSub.hSub (α := ℝ) (↑m : ℝ) (↑i : ℝ))
⊢ 0 < (∏ i ∈ Finset.range 2, HSub.hSub (α := ℝ) (↑m : ℝ) (↑i : ℝ)) * x ^ (m - (↑2 : ℤ))

Tactic:
refine mul_pos ?_ (zpow_pos hx _)

Premises used: zpow_pos, mul_pos
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hf'' : LT.lt (α := ℤ) 0 (∏ i ∈ Finset.range 2, (m - (↑i : ℤ)))
⊢ LT.lt (α := ℝ) 0 (∏ i ∈ Finset.range 2, HSub.hSub (α := ℝ) (↑m : ℝ) (↑i : ℝ))

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ Even (α := ℕ) 2

Tactic:
decide
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hf'' : ∀ (hm : Membership.mem (γ := Set ℤ) (Ico 0 (↑2 : ℤ)) m), False
⊢ LT.lt (α := ℤ) 0 (∏ i ∈ Finset.range 2, (m - (↑i : ℤ)))

Tactic:
refine int_prod_range_pos (by decide) fun hm => ?_

Premises used: int_prod_range_pos
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : Membership.mem (γ := Set ℤ) (Ico 0 (↑2 : ℤ)) m
⊢ m ∈ (↑(Finset.Ico 0 (↑2 : ℤ)) : Set ℤ)

Tactic:
rw [← Finset.coe_Ico] at hm

Premises used: Finset.coe_Ico
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ (↑(Finset.Ico 0 (↑2 : ℤ)) : Set ℤ)
⊢ Membership.mem (γ := Finset ℤ) (Finset.Ico 0 2) m

Tactic:
norm_cast at hm
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : Membership.mem (γ := Finset ℤ) (Finset.Ico 0 2) m
hf'' :
  ∀ (hm₀ : Ne (α := ℤ) ((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0) : (a : ℕ) → ℤ) 0 : ℤ) (0 : ℤ))
    (hm₁ : Ne (α := ℤ) ((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0) : (a : ℕ) → ℤ) 0 : ℤ) (1 : ℤ)),
    False
hf''₁ :
  ∀ (hm₀ : Ne (α := ℤ) ((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0) : (a : ℕ) → ℤ) 1 : ℤ) (0 : ℤ))
    (hm₁ : Ne (α := ℤ) ((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0) : (a : ℕ) → ℤ) 1 : ℤ) (1 : ℤ)),
    False
⊢ False

Tactic:
fin_cases hm
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : 0 < x
hm₀ : Ne (α := ℤ) ((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0) : (a : ℕ) → ℤ) 0 : ℤ) (0 : ℤ)
hm₁ : Ne (α := ℤ) ((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0) : (a : ℕ) → ℤ) 0 : ℤ) (1 : ℤ)
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : 0 < x
hm₀ : Ne (α := ℤ) ((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0) : (a : ℕ) → ℤ) 1 : ℤ) (0 : ℤ)
hm₁ : Ne (α := ℤ) ((Function.Embedding.trans Nat.castEmbedding (addLeftEmbedding 0) : (a : ℕ) → ℤ) 1 : ℤ) (1 : ℤ)
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt ((fun (x : ℝ) ↦ √x) * log) (1 / (2 * √x) * log x + √x * x⁻¹) x

Tactic:
(hasDerivAt_sqrt hx).mul (hasDerivAt_log hx)

Premises used: Real.hasDerivAt_log, HasDerivAt.mul, Real.hasDerivAt_sqrt
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≠ 0
h : (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
⊢ HasDerivAt (fun (x : ℝ) ↦ √x * log x) ((2 + log x) / (2 * √x)) x

Tactic:
convert! (hasDerivAt_sqrt hx).mul (hasDerivAt_log hx) using 1

Premises used: Real.hasDerivAt_log, HasDerivAt.mul, Real.hasDerivAt_sqrt
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≠ 0
h : 2 / (2 * √x) + log x / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
h₁ : (√x)⁻¹ + log x / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
h₂ : (√x)⁻¹ + log x / (2 * √x) = 1 / (2 * √x) * log x + √x / x
h₃ : (√x)⁻¹ + log x / (2 * √x) = 1 / (2 * √x) * log x + 1 / √x
h₄ : log x / (2 * √x) + (√x)⁻¹ = 1 / (2 * √x) * log x + 1 / √x
h₅ : log x / (2 * √x) + (√x)⁻¹ = (2 * √x)⁻¹ * log x + 1 / √x
h₆ : log x / (2 * √x) + (√x)⁻¹ = (2 * √x)⁻¹ * log x + (√x)⁻¹
h₇ h₈ : log x / (2 * √x) + (√x)⁻¹ = log x / (2 * √x) + (√x)⁻¹
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹

Tactic:
rw [add_div, div_mul_cancel_left₀ two_ne_zero, ← div_eq_mul_inv, sqrt_div_self', add_comm,
    one_div, one_div, ← div_eq_inv_mul]

Premises used: div_mul_cancel_left₀, Real.sqrt_div_self', div_eq_mul_inv, add_comm, two_ne_zero, one_div, div_eq_inv_mul, add_div
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
inl : ∀ (hx : 0 < x), deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)
inr : ∀ (hx : x ≤ 0), deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)
⊢ deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)

Tactic:
rcases lt_or_ge 0 x with hx | hx

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : 0 < x
⊢ deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)

Tactic:
(hasDerivAt_sqrt_mul_log hx.ne').deriv

Premises used: hasDerivAt_sqrt_mul_log, HasDerivAt.deriv, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : 0 < x
⊢ deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)

Tactic:
exact (hasDerivAt_sqrt_mul_log hx.ne').deriv

Premises used: hasDerivAt_sqrt_mul_log, HasDerivAt.deriv, LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≤ 0
inr : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ √x * log x) x) 0
⊢ deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)

Tactic:
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]

Premises used: Real.sqrt_eq_zero_of_nonpos, MulZeroClass.mul_zero, div_zero
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≤ 0
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ √x * log x) x) 0

Tactic:
HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)

Premises used: uniqueDiffOn_Iic, HasDerivWithinAt.deriv_eq_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≤ 0
inr : HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ √x * log x) 0 (Iic 0) x
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ √x * log x) x) 0

Tactic:
refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)

Premises used: uniqueDiffOn_Iic, HasDerivWithinAt.deriv_eq_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ √x * log x) 0 (Iic 0) x

Tactic:
(hasDerivWithinAt_const x _ 0).congr_of_mem (fun x hx => ?_) hx

Premises used: HasDerivWithinAt.congr_of_mem, hasDerivWithinAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≤ 0
inr : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Iic 0) x), √x * log x = 0
⊢ HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ √x * log x) 0 (Iic 0) x

Tactic:
refine (hasDerivWithinAt_const x _ 0).congr_of_mem (fun x hx => ?_) hx

Premises used: HasDerivWithinAt.congr_of_mem, hasDerivWithinAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x_1 : ℝ
hx_1 : x_1 ≤ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic 0) x
inr : 0 * log x = 0
inr₁ inr₂ : Eq (α := ℝ) 0 0
⊢ √x * log x = 0

Tactic:
rw [sqrt_eq_zero_of_nonpos hx, zero_mul]

Premises used: MulZeroClass.zero_mul, Real.sqrt_eq_zero_of_nonpos
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
⊢ Eq (α := (x : ℝ) → ℝ) (deriv fun (x : ℝ) ↦ √x * log x) fun (x : ℝ) ↦ (2 + log x) / (2 * √x)

Tactic:
funext deriv_sqrt_mul_log

Premises used: deriv_sqrt_mul_log, funext
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
simp : deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)
⊢ deriv^[2] (fun (x : ℝ) ↦ √x * log x) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)

Tactic:
simp only [Nat.iterate, deriv_sqrt_mul_log']

Premises used: Nat.iterate, deriv_sqrt_mul_log'
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
inl : ∀ (hx : x ≤ 0), deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)
inr : ∀ (hx : 0 < x), deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)
⊢ deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)

Tactic:
rcases le_or_gt x 0 with hx | hx

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≤ 0
inl : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x) 0
⊢ deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)

Tactic:
rw [sqrt_eq_zero_of_nonpos hx, zero_pow three_ne_zero, mul_zero, div_zero]

Premises used: Real.sqrt_eq_zero_of_nonpos, MulZeroClass.mul_zero, three_ne_zero, div_zero, zero_pow
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≤ 0
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x) 0

Tactic:
HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)

Premises used: uniqueDiffOn_Iic, HasDerivWithinAt.deriv_eq_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≤ 0
inl : HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) 0 (Iic 0) x
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x) 0

Tactic:
refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)

Premises used: uniqueDiffOn_Iic, HasDerivWithinAt.deriv_eq_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) 0 (Iic 0) x

Tactic:
(hasDerivWithinAt_const _ _ 0).congr_of_mem (fun x hx => ?_) hx

Premises used: HasDerivWithinAt.congr_of_mem, hasDerivWithinAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : x ≤ 0
inl : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Iic 0) x), (2 + log x) / (2 * √x) = 0
⊢ HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) 0 (Iic 0) x

Tactic:
refine (hasDerivWithinAt_const _ _ 0).congr_of_mem (fun x hx => ?_) hx

Premises used: HasDerivWithinAt.congr_of_mem, hasDerivWithinAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x_1 : ℝ
hx_1 : x_1 ≤ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic 0) x
inl : (2 + log x) / HMul.hMul (α := ℝ) 2 0 = 0
inl₁ : (2 + log x) / 0 = 0
inl₂ inl₃ : Eq (α := ℝ) 0 0
⊢ (2 + log x) / (2 * √x) = 0

Tactic:
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]

Premises used: Real.sqrt_eq_zero_of_nonpos, MulZeroClass.mul_zero, div_zero
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : 0 < x
⊢ √x ≠ 0

Tactic:
have h₀ : √x ≠ 0 := sqrt_ne_zero'.2 hx
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
⊢ deriv (HDiv.hDiv (α := ℝ → ℝ) (fun (x : ℝ) ↦ 2 + log x) fun (y : ℝ) ↦ 2 * √y) x =
    (x⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / HPow.hPow (β := ℕ) (2 * √x) 2

Tactic:
(((hasDerivAt_log hx.ne').const_add 2).div ((hasDerivAt_sqrt hx.ne').const_mul 2) <|
          mul_ne_zero two_ne_zero h₀).deriv

Premises used: HasDerivAt.deriv, LT.lt.ne', two_ne_zero, Real.hasDerivAt_log, HasDerivAt.const_mul, HasDerivAt.const_add, HasDerivAt.div, mul_ne_zero, OfNat.ofNat, Real.hasDerivAt_sqrt
-- Module: Mathlib.Analysis.Convex.SpecificFunctions.Deriv
Goal:
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
h :
  -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) =
    (x⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / HPow.hPow (β := ℕ) (2 * √x) 2
⊢ deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)

Tactic:
convert!
      (((hasDerivAt_log hx.ne').const_add 2).div ((hasDerivAt_sqrt hx.ne').const_mul 2) <|
          mul_ne_zero two_ne_zero h₀).deriv using 1

Premises used: HasDerivAt.deriv, LT.lt.ne', two_ne_zero, Real.hasDerivAt_log, HasDerivAt.const_mul, HasDerivAt.const_add, HasDerivAt.div, mul_ne_zero, OfNat.ofNat, Real.hasDerivAt_sqrt