awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
⊢ Eq.{u_2 + 1} (α := β) (∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x) (∏ x ∈ s, f x)
have rw₈ : Eq.{u_2 + 1} (α := β) (∏ x ∈ s, 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
n : ℕ
hn : Even n
⊢ LE.le (α := ℤ) 0 (∏ k ∈ Finset.range n, (m - (↑k : ℤ)))
have rcases : ∀ (n : ℕ), LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + n), (m - (↑k : ℤ)))
Tactic: rcases hn with ⟨n, rfl⟩
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (hypothesis)
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + n), (m - (↑k : ℤ)))
⊢ LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + 1 + (n + 1)), (m - (↑k : ℤ)))
have ihn₁ : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
Tactic: rw [← two_mul] at ihn
Cleared hypotheses: ihn
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
⊢ LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + 1 + (n + 1)), (m - (↑k : ℤ)))
have 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) : ℤ)))
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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) : ℤ)))
have succ : 0 ≤ (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n) : ℤ)) * (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n + 1) : ℤ))
Tactic: refine mul_nonneg ihn ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
⊢ 0 ≤ (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n) : ℤ)) * (m - (↑(HAdd.hAdd (α := ℕ) 1 1 * n + 1) : ℤ))
have succ : ∀ (k : ℕ), 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))
Tactic: generalize (1 + 1) * n = k
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
k : ℕ
⊢ 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))
have succ : ∀ (hmk : m ≤ (↑k : ℤ)), 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))
Tactic: rcases le_or_gt m k with hmk | hmk
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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) : ℤ))
⊢ 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))
have succ₁ : ∀ (hmk : (↑k : ℤ) < m), 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))
Tactic: rcases le_or_gt m k with hmk | hmk
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (hypothesis)
Goal:
m : ℤ
n : ℕ
ihn : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (2 * n), (m - (↑k : ℤ)))
k : ℕ
hmk : m ≤ (↑k : ℤ)
⊢ 0 ≤ (m - (↑k : ℤ)) * (m - (↑(k + 1) : ℤ))
have this : m ≤ HAdd.hAdd (α := ℤ) (↑k : ℤ) 1
Tactic: have : m ≤ k + 1 := hmk.trans (lt_add_one (k : ℤ)).le
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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) : ℤ))
have succ : m - (↑(k + 1) : ℤ) ≤ 0
Tactic: convert! mul_nonneg_of_nonpos_of_nonpos (sub_nonpos_of_le hmk) _
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
n : ℕ
⊢ LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + n), (m - (↑k : ℤ)))
have zero : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 0), (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)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
n : ℕ
zero : LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 0), (m - (↑k : ℤ)))
⊢ LE.le (α := ℤ) 0 (∏ k ∈ Finset.range (n + n), (m - (↑k : ℤ)))
have 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 : ℤ)))
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)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 (↑n : ℤ)
⊢ LT.lt (α := ℤ) 0 (∏ k ∈ Finset.range n, (m - (↑k : ℤ)))
have refine : ∀ (h : Eq (α := ℤ) 0 (∏ k ∈ Finset.range n, (m - (↑k : ℤ)))), Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) m
Tactic: refine (int_prod_range_nonneg m n hn).lt_of_ne fun h => hm ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (hypothesis)
Goal:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 (↑n : ℤ)
h : Eq (α := ℤ) 0 (∏ k ∈ Finset.range n, (m - (↑k : ℤ)))
⊢ Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) m
have h₁ : ∃ a ∈ Finset.range n, m - (↑a : ℤ) = 0
Tactic: rw [eq_comm, Finset.prod_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
n : ℕ
hn : Even n
hm : m ∉ Ico 0 (↑n : ℤ)
h : ∃ a ∈ Finset.range n, m - (↑a : ℤ) = 0
⊢ Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) m
have obtain : ∀ (a : ℕ) (ha : a ∈ Finset.range n) (h : m - (↑a : ℤ) = 0), Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) m
Tactic: obtain ⟨a, ha, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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 : ℤ)) m
have rw : Membership.mem (γ := Set ℤ) (Ico 0 (↑n : ℤ)) (↑a : ℤ)
Tactic: rw [sub_eq_zero.1 h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
⊢ StrictConvexOn ℝ (β := ℝ) (Ioi 0) fun (x : ℝ) ↦ x ^ m
have hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ m) (Ioi 0)
Tactic: apply strictConvexOn_of_deriv2_pos' (convex_Ioi 0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
hf : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ x ^ m) (Ioi 0)
⊢ StrictConvexOn ℝ (β := ℝ) (Ioi 0) fun (x : ℝ) ↦ x ^ m
have hf'' : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → LT.lt (α := ℝ) (0 : ℝ) (deriv^[2] (fun (x : ℝ) ↦ x ^ m) x : ℝ)
Tactic: apply strictConvexOn_of_deriv2_pos' (convex_Ioi 0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (hypothesis)
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ LT.lt (α := ℝ) (0 : ℝ) (deriv^[2] (fun (x : ℝ) ↦ x ^ m) x : ℝ)
have hx₁ : 0 < x
Tactic: rw [mem_Ioi] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ LT.lt (α := ℝ) (0 : ℝ) (deriv^[2] (fun (x : ℝ) ↦ x ^ m) x : ℝ)
have hf'' : 0 < (∏ i ∈ Finset.range 2, HSub.hSub (α := ℝ) (↑m : ℝ) (↑i : ℝ)) * x ^ (m - (↑2 : ℤ))
Tactic: rw [iter_deriv_zpow]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ 0 < (∏ i ∈ Finset.range 2, HSub.hSub (α := ℝ) (↑m : ℝ) (↑i : ℝ)) * x ^ (m - (↑2 : ℤ))
have hf'' : LT.lt (α := ℝ) 0 (∏ i ∈ Finset.range 2, HSub.hSub (α := ℝ) (↑m : ℝ) (↑i : ℝ))
Tactic: refine mul_pos ?_ (zpow_pos hx _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ LT.lt (α := ℝ) 0 (∏ i ∈ Finset.range 2, HSub.hSub (α := ℝ) (↑m : ℝ) (↑i : ℝ))
have hf'' : LT.lt (α := ℤ) 0 (∏ i ∈ Finset.range 2, (m - (↑i : ℤ)))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
⊢ LT.lt (α := ℤ) 0 (∏ i ∈ Finset.range 2, (m - (↑i : ℤ)))
have hf'' : ∀ (hm : Membership.mem (γ := Set ℤ) (Ico 0 (↑2 : ℤ)) m), False
Tactic: refine int_prod_range_pos (by decide) fun hm => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (hypothesis)
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : Membership.mem (γ := Set ℤ) (Ico 0 (↑2 : ℤ)) m
⊢ False
have hm₂ : m ∈ (↑(Finset.Ico 0 (↑2 : ℤ)) : Set ℤ)
Tactic: rw [← Finset.coe_Ico] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (hypothesis)
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : m ∈ (↑(Finset.Ico 0 (↑2 : ℤ)) : Set ℤ)
⊢ False
have hm₂ : Membership.mem (γ := Finset ℤ) (Finset.Ico 0 2) m
Tactic: norm_cast at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
m : ℤ
hm₀ : m ≠ 0
hm₁ : m ≠ 1
x : ℝ
hx : 0 < x
hm : Membership.mem (γ := Finset ℤ) (Finset.Ico 0 2) m
⊢ False
have 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
Tactic: fin_cases hm
Cleared hypotheses: m, hm₀, hm₁, hm
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
⊢ False
have 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
Tactic: fin_cases hm
Cleared hypotheses: m, hm₀, hm₁, hm
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun (x : ℝ) ↦ √x * log x) ((2 + log x) / (2 * √x)) x
have h : (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
Tactic: convert! (hasDerivAt_sqrt hx).mul (hasDerivAt_log hx) using 1
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
have h : 2 / (2 * √x) + 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
h : 2 / (2 * √x) + log x / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
have h₁ : (√x)⁻¹ + 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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⁻¹
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
have h₂ : (√x)⁻¹ + 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
have h₃ : (√x)⁻¹ + log x / (2 * √x) = 1 / (2 * √x) * log x + 1 / √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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
have h₄ : log x / (2 * √x) + (√x)⁻¹ = 1 / (2 * √x) * log x + 1 / √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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
have h₅ : log x / (2 * √x) + (√x)⁻¹ = (2 * √x)⁻¹ * log x + 1 / √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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
have h₆ : log x / (2 * √x) + (√x)⁻¹ = (2 * √x)⁻¹ * log 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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)⁻¹
⊢ (2 + log x) / (2 * √x) = 1 / (2 * √x) * log x + √x * x⁻¹
have h₇ : log x / (2 * √x) + (√x)⁻¹ = log x / (2 * √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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
⊢ deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)
have inl : ∀ (hx : 0 < x), deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)
Tactic: rcases lt_or_ge 0 x with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
inl : ∀ (hx : 0 < x), deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)
⊢ deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)
have inr : ∀ (hx : x ≤ 0), deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)
Tactic: rcases lt_or_ge 0 x with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : x ≤ 0
⊢ deriv (fun (x : ℝ) ↦ √x * log x) x = (2 + log x) / (2 * √x)
have inr : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ √x * log x) x) 0
Tactic: rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : x ≤ 0
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ √x * log x) x) 0
have inr : HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ √x * log x) 0 (Iic 0) x
Tactic: refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ √x * log x) 0 (Iic 0) x
have inr : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Iic 0) x), √x * log x = 0
Tactic: refine (hasDerivWithinAt_const x _ 0).congr_of_mem (fun x hx => ?_) hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x_1 : ℝ
hx_1 : x_1 ≤ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic 0) x
⊢ √x * log x = 0
have inr : 0 * log x = 0
Tactic: rw [sqrt_eq_zero_of_nonpos hx, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x_1 : ℝ
hx_1 : x_1 ≤ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic 0) x
inr : 0 * log x = 0
⊢ √x * log x = 0
have inr₁ : Eq (α := ℝ) 0 0
Tactic: rw [sqrt_eq_zero_of_nonpos hx, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
⊢ deriv^[2] (fun (x : ℝ) ↦ √x * log x) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)
have simp : deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)
Tactic: simp only [Nat.iterate, deriv_sqrt_mul_log']
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
⊢ deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)
have inl : ∀ (hx : x ≤ 0), 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
inl : ∀ (hx : x ≤ 0), 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)
have inr : ∀ (hx : 0 < x), 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : x ≤ 0
⊢ deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)
have inl : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x) 0
Tactic: rw [sqrt_eq_zero_of_nonpos hx, zero_pow three_ne_zero, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : x ≤ 0
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x) 0
have inl : HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) 0 (Iic 0) x
Tactic: refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) 0 (Iic 0) x
have inl : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Iic 0) x), (2 + log x) / (2 * √x) = 0
Tactic: refine (hasDerivWithinAt_const _ _ 0).congr_of_mem (fun x hx => ?_) hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x_1 : ℝ
hx_1 : x_1 ≤ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic 0) x
⊢ (2 + log x) / (2 * √x) = 0
have inl : (2 + log x) / HMul.hMul (α := ℝ) 2 0 = 0
Tactic: rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
⊢ (2 + log x) / (2 * √x) = 0
have inl₁ : (2 + log x) / 0 = 0
Tactic: rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
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
⊢ (2 + log x) / (2 * √x) = 0
have inl₂ : Eq (α := ℝ) 0 0
Tactic: rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (hypothesis)
Goal:
x : ℝ
hx : 0 < x
⊢ deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)
have h₀ : √x ≠ 0
Tactic: have h₀ : √x ≠ 0 := sqrt_ne_zero'.2 hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
⊢ deriv (fun (x : ℝ) ↦ (2 + log x) / (2 * √x)) x = -log x / (4 * HPow.hPow (β := ℕ) (√x) 3)
have h : -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) =
  (x⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / HPow.hPow (β := ℕ) (2 * √x) 2
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
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
⊢ -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) =
    (x⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / HPow.hPow (β := ℕ) (2 * √x) 2
have h : -log x / (4 * HPow.hPow (β := ℕ) (√x) 3) =
  ((√x * √x)⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / HPow.hPow (β := ℕ) (2 * √x) 2
Tactic: nth_rw 3 [← mul_self_sqrt hx.le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.SpecificFunctions.Deriv (goal)
Goal:
⊢ StrictConcaveOn ℝ (β := ℝ) (Ioi 1) fun (x : ℝ) ↦ √x * log x
have apply : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ √x * log x) (Ioi 1)
Tactic: apply strictConcaveOn_of_deriv2_neg' (convex_Ioi 1) _ fun x hx => ?_