awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
hp₀_1 : LE.le (α := ℝ) 0 1
hp₁ : LE.le (α := ℝ) 1 1
hp₀ : LT.lt (α := ℝ) 0 1
⊢ 0 ≤ binEntropy 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁_1 : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ binEntropy p

Tactic:
(binEntropy_pos hp₀ hp₁).le

Premises used: LT.lt.le, Real.binEntropy_pos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁_1 : p ≤ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 ≤ binEntropy p

Tactic:
exact (binEntropy_pos hp₀ hp₁).le

Premises used: LT.lt.le, Real.binEntropy_pos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
rw : p * -log p + (1 - p) * -log (1 - p) < 0
⊢ binEntropy p < 0

Tactic:
rw [binEntropy, log_inv, log_inv]

Premises used: Real.binEntropy, Real.log_inv
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
this : -p * log p < (1 - p) * log (1 - p)
linarith :
  0 ≤ p * -log p + (1 - p) * -log (1 - p) →
    -p * log p - (1 - p) * log (1 - p) + (0 - (p * -log p + (1 - p) * -log (1 - p))) = 0
⊢ p * -log p + (1 - p) * -log (1 - p) < 0

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
suffices : -p * log p < (1 - p) * log (1 - p)
⊢ p * -log p + (1 - p) * -log (1 - p) < 0

Tactic:
suffices -p * log p < (1 - p) * log (1 - p) by linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
pos : ∀ (hp' : p < -1), -p * log p < (1 - p) * log (1 - p)
neg : ∀ (hp' : ¬p < -1), -p * log p < (1 - p) * log (1 - p)
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
by_cases hp' : p < -1
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : p < -1
rw : log (-p) < log (1 - p)
⊢ log p < log (1 - p)

Tactic:
rw [← log_neg_eq_log]

Premises used: Real.log_neg_eq_log
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : p < -1
linarith : 1 - p ≤ -p → -1 + (1 - p - -p) = 0
⊢ -p < 1 - p

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : p < -1
⊢ log (-p) < log (1 - p)

Tactic:
exact log_lt_log (Left.neg_pos_iff.mpr hp) (by linarith)

Premises used: Iff.mpr, Real.log_lt_log, Left.neg_pos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : p < -1
⊢ log p < log (1 - p)

Tactic:
have : log p < log (1 - p) := by
      rw [← log_neg_eq_log]
      exact log_lt_log (Left.neg_pos_iff.mpr hp) (by linarith)
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : p < -1
this : log p < log (1 - p)
nlinarith :
  (1 - p) * log (1 - p) ≤ -p * log p →
    log p - log (1 - p) + ((1 - p) * log (1 - p) - -p * log p) + (0 - log p) + (0 - (p - 0) * (log p - log (1 - p))) = 0
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
nlinarith [log_pos_of_lt_neg_one hp']

Premises used: Real.log_pos_of_lt_neg_one
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : ¬p < -1
inr : ∀ (this : ∀ {p : ℝ} (hp : p < 0) (hp' : ¬p < -1) (h : -1 < p), -p * log p ≤ 0) (h : ¬-1 < p), -p * log p ≤ 0
wlog : ∀ {p : ℝ} (hp : p < 0) (hp' : ¬p < -1) (h : -1 < p), -p * log p ≤ 0
⊢ -p * log p ≤ 0

Tactic:
wlog h : -1 < p
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : ∀ {p : ℝ} (hp : p < 0) (hp' : ¬p < -1) (h : -1 < p), -p * log p ≤ 0
h : ¬-1 < p
linarith : p < -1 → -1 - p + (p - -1) = 0
linarith₁ : -1 < p → p - -1 + (-1 - p) = 0
⊢ p = -1

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : ∀ {p : ℝ} (hp : p < 0) (hp' : ¬p < -1) (h : -1 < p), -p * log p ≤ 0
h : ¬-1 < p
⊢ -p * log p ≤ 0

Tactic:
simp only [show p = -1 by linarith, log_neg_eq_log, log_one, le_refl, mul_zero]

Premises used: le_refl, Real.log_neg_eq_log, Real.log_one, MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
nlinarith : 0 < -p * log p → 0 - -p * log p + (0 - (p - 0) * (log p - 0)) = 0
⊢ -p * log p ≤ 0

Tactic:
nlinarith [log_neg_of_lt_zero hp h]

Premises used: Real.log_neg_of_lt_zero
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p ≤ 0

Tactic:
have : -p * log p ≤ 0 := by
      wlog h : -1 < p
      · simp only [show p = -1 by linarith, log_neg_eq_log, log_one, le_refl, mul_zero]
      · nlinarith [log_neg_of_lt_zero hp h]
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : -p * log p ≤ 0
linarith : 1 - p ≤ 1 → p - 0 + (1 - p - 1) = 0
⊢ 1 < 1 - p

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : -p * log p ≤ 0
nlinarith :
  (1 - p) * log (1 - p) ≤ -p * log p →
    -p * log p - 0 + ((1 - p) * log (1 - p) - -p * log p) + (0 - log (1 - p)) + (0 - (p - 0) * (0 - log (1 - p))) = 0
⊢ -p * log p < (1 - p) * log (1 - p)

Tactic:
nlinarith [(log_pos (by linarith) : 0 < log (1 - p))]

Premises used: Real.log_pos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p ≤ 0
inl : ∀ (hp : LE.le (α := ℝ) 0 0), binEntropy 0 ≤ 0
inr : ∀ (hp : p < 0), binEntropy p ≤ 0
⊢ binEntropy p ≤ 0

Tactic:
obtain rfl | hp := hp.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
hp : LE.le (α := ℝ) 0 0
⊢ binEntropy 0 ≤ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp_1 : p ≤ 0
hp : p < 0
⊢ binEntropy p ≤ 0

Tactic:
(binEntropy_neg_of_neg hp).le

Premises used: Real.binEntropy_neg_of_neg, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp_1 : p ≤ 0
hp : p < 0
⊢ binEntropy p ≤ 0

Tactic:
exact (binEntropy_neg_of_neg hp).le

Premises used: Real.binEntropy_neg_of_neg, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : 1 < p
rw : binEntropy (1 - p) < 0
⊢ binEntropy p < 0

Tactic:
rw [← binEntropy_one_sub]

Premises used: Real.binEntropy_one_sub
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : 1 < p
⊢ binEntropy (1 - p) < 0

Tactic:
binEntropy_neg_of_neg (sub_neg.2 hp)

Premises used: sub_neg, Iff.mpr, Real.binEntropy_neg_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : 1 < p
⊢ binEntropy (1 - p) < 0

Tactic:
exact binEntropy_neg_of_neg (sub_neg.2 hp)

Premises used: sub_neg, Iff.mpr, Real.binEntropy_neg_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : 1 ≤ p
rw : binEntropy (1 - p) ≤ 0
⊢ binEntropy p ≤ 0

Tactic:
rw [← binEntropy_one_sub]

Premises used: Real.binEntropy_one_sub
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : 1 ≤ p
⊢ binEntropy (1 - p) ≤ 0

Tactic:
binEntropy_nonpos_of_nonpos (sub_nonpos.2 hp)

Premises used: Iff.mpr, Real.binEntropy_nonpos_of_nonpos, sub_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : 1 ≤ p
⊢ binEntropy (1 - p) ≤ 0

Tactic:
exact binEntropy_nonpos_of_nonpos (sub_nonpos.2 hp)

Premises used: Iff.mpr, Real.binEntropy_nonpos_of_nonpos, sub_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ binEntropy 0 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ binEntropy 1 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
refine : ∀ (h : binEntropy p = 0), p = 0 ∨ p = 1
⊢ binEntropy p = 0 ↔ p = 0 ∨ p = 1

Tactic:
refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : binEntropy p = 0
contrapose! : ∀ (h : p ≠ 0 ∧ p ≠ 1), binEntropy p ≠ 0
⊢ p = 0 ∨ p = 1

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
inl : ∀ (hp₀ : p < 0), binEntropy p ≠ 0
inr : ∀ (hp₀ : 0 < p), binEntropy p ≠ 0
⊢ binEntropy p ≠ 0

Tactic:
obtain hp₀ | hp₀ := h.1.lt_or_gt

Premises used: And.left, Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : p < 0
⊢ binEntropy p ≠ 0

Tactic:
(binEntropy_neg_of_neg hp₀).ne

Premises used: Real.binEntropy_neg_of_neg, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : p < 0
⊢ binEntropy p ≠ 0

Tactic:
exact (binEntropy_neg_of_neg hp₀).ne

Premises used: Real.binEntropy_neg_of_neg, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
inr : ∀ (hp₁ : 1 < p), binEntropy p ≠ 0
inr₁ : ∀ (hp₁ : p < 1), binEntropy p ≠ 0
⊢ binEntropy p ≠ 0

Tactic:
obtain hp₁ | hp₁ := h.2.lt_or_gt.symm

Premises used: Or.symm, And.right, Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : 1 < p
⊢ binEntropy p ≠ 0

Tactic:
(binEntropy_neg_of_one_lt hp₁).ne

Premises used: Real.binEntropy_neg_of_one_lt, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : 1 < p
⊢ binEntropy p ≠ 0

Tactic:
exact (binEntropy_neg_of_one_lt hp₁).ne

Premises used: Real.binEntropy_neg_of_one_lt, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ binEntropy p ≠ 0

Tactic:
(binEntropy_pos hp₀ hp₁).ne'

Premises used: Real.binEntropy_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
hp₁ : p < 1
⊢ binEntropy p ≠ 0

Tactic:
exact (binEntropy_pos hp₀ hp₁).ne'

Premises used: Real.binEntropy_pos, LT.lt.ne'
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
⊢ binEntropy p < log 2 ↔ p ≠ 2⁻¹

Tactic:
⟨?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
refine_1 : binEntropy p < log 2 → p ≠ 2⁻¹
refine_2 : ∀ (h : p ≠ 2⁻¹), binEntropy p < log 2
⊢ binEntropy p < log 2 ↔ p ≠ 2⁻¹

Tactic:
refine ⟨?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : binEntropy 2⁻¹ < log 2
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 2⁻¹
refine_2 : ∀ (this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2) (hp : ¬p < 2⁻¹), binEntropy p < log 2
wlog : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
⊢ binEntropy p < log 2

Tactic:
wlog hp : p < 2⁻¹
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
hp : ¬p < 2⁻¹
rw : HSub.hSub (α := ℝ) 1 2⁻¹ < p
⊢ 1 - p < 2⁻¹

Tactic:
rw [sub_lt_comm]

Premises used: sub_lt_comm
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
hp : ¬p < 2⁻¹
norm_num :
  ∀ (h : ¬p = 1 / 2) (this : ∀ {p : ℝ} (h : ¬p = 1 / 2) (hp : p < 1 / 2), binEntropy p < log 2) (hp : 1 / 2 ≤ p),
    1 / 2 < p
⊢ HSub.hSub (α := ℝ) 1 2⁻¹ < p

Tactic:
norm_num at *
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : ¬p = 1 / 2
this : ∀ {p : ℝ} (h : ¬p = 1 / 2) (hp : p < 1 / 2), binEntropy p < log 2
hp : 1 / 2 ≤ p
linarith : p ≤ 1 / 2 → p < 1 / 2 → 2 / 2 = 1
linarith₁ : p ≤ 1 / 2 → p < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : p ≤ 1 / 2 → p < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : p ≤ 1 / 2 → p < 1 / 2 → 2 / 2 = 1
linarith₄ : p ≤ 1 / 2 → p < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : p ≤ 1 / 2 → p < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₆ : p ≤ 1 / 2 → p < 1 / 2 → 2 / 2 = 1
linarith₇ : p ≤ 1 / 2 → p < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₈ : p ≤ 1 / 2 → p < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₉ : p ≤ 1 / 2 → 1 / 2 < p → 2 / 2 = 1
linarith₁₀ : p ≤ 1 / 2 → 1 / 2 < p → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : p ≤ 1 / 2 → 1 / 2 < p → GT.gt (α := ℝ) 2 0
linarith₁₂ : p ≤ 1 / 2 → 1 / 2 < p → 2 / 2 = 1
linarith₁₃ : p ≤ 1 / 2 → 1 / 2 < p → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₄ : p ≤ 1 / 2 → 1 / 2 < p → GT.gt (α := ℝ) 2 0
linarith₁₅ : p ≤ 1 / 2 → 1 / 2 < p → 2 / 2 = 1
linarith₁₆ : p ≤ 1 / 2 → 1 / 2 < p → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₇ : p ≤ 1 / 2 → 1 / 2 < p → GT.gt (α := ℝ) 2 0
linarith₁₈ : p ≤ 1 / 2 → p < 1 / 2 → 2 * p - HMul.hMul (α := ℝ) 1 1 + (HMul.hMul (α := ℝ) 1 1 - 2 * p) = 0
linarith₁₉ : p ≤ 1 / 2 → 1 / 2 < p → HMul.hMul (α := ℝ) 1 1 - 2 * p + (2 * p - HMul.hMul (α := ℝ) 1 1) = 0
⊢ 1 / 2 < p

Tactic:
linarith +splitNe
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ 1 - p < 2⁻¹

Tactic:
have hp : 1 - p < 2⁻¹ := by
      rw [sub_lt_comm]; norm_num at *; linarith +splitNe
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
hp_1 : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
refine_2 : binEntropy (1 - p) < log 2
⊢ binEntropy p < log 2

Tactic:
rw [← binEntropy_one_sub]

Premises used: Real.binEntropy_one_sub
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
hp_1 : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
⊢ binEntropy (1 - p) < log 2

Tactic:
this hp.ne hp

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
hp_1 : ¬p < 2⁻¹
hp : 1 - p < 2⁻¹
⊢ binEntropy (1 - p) < log 2

Tactic:
exact this hp.ne hp

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
inl : ∀ (hp₀ : p ≤ 0), binEntropy p < log 2
inr : ∀ (hp₀ : 0 < p), binEntropy p < log 2
⊢ binEntropy p < log 2

Tactic:
obtain hp₀ | hp₀ := le_or_gt p 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : p ≤ 0
⊢ LT.lt (α := ℝ) 1 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : p ≤ 0
⊢ binEntropy p < log 2

Tactic:
exact (binEntropy_nonpos_of_nonpos hp₀).trans_lt <| log_pos <| by simp

Premises used: Real.binEntropy_nonpos_of_nonpos, Real.log_pos, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
⊢ LT.lt (α := ℝ) 2⁻¹ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
⊢ 0 < 1 - p

Tactic:
have hp₁ : 0 < 1 - p := sub_pos.2 <| hp.trans <| by norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ p⁻¹ ≠ (1 - p)⁻¹

Tactic:
simpa [eq_sub_iff_add_eq, ← two_mul, mul_comm, mul_eq_one_iff_eq_inv₀]

Premises used: eq_sub_iff_add_eq, two_mul, mul_eq_one_iff_eq_inv₀, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ p + (1 - p) = 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
rw : 1 - p ≠ 0
rw₁ : p ≠ 0
⊢ log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) = log 2

Tactic:
rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two]

Premises used: mul_inv_cancel₀, one_add_one_eq_two
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ 1 - p ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ p ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
_ : log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) = log 2
⊢ binEntropy p < log 2

Tactic:
calc
  _ < log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) :=
    strictConcaveOn_log_Ioi.2 (inv_pos.2 hp₀) (inv_pos.2 hp₁)
      (by simpa [eq_sub_iff_add_eq, ← two_mul, mul_comm, mul_eq_one_iff_eq_inv₀]) hp₀ hp₁ (by simp)
  _ = log 2 := by rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two] <;> positivity

Premises used: Iff.mpr, HMul.hMul, HSub.hSub, inv_pos, Real.log, Inv.inv, And.right, HAdd.hAdd, strictConcaveOn_log_Ioi, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
inl : binEntropy 2⁻¹ ≤ log 2
inr : ∀ (hp : p ≠ 2⁻¹), binEntropy p ≤ log 2
⊢ binEntropy p ≤ log 2

Tactic:
obtain rfl | hp := eq_or_ne p 2⁻¹

Premises used: Inv.inv, eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ binEntropy 2⁻¹ ≤ log 2

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p ≠ 2⁻¹
⊢ binEntropy p ≤ log 2

Tactic:
(binEntropy_lt_log_two.2 hp).le

Premises used: Iff.mpr, LT.lt.le, Real.binEntropy_lt_log_two
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p ≠ 2⁻¹
⊢ binEntropy p ≤ log 2

Tactic:
exact (binEntropy_lt_log_two.2 hp).le

Premises used: Iff.mpr, LT.lt.le, Real.binEntropy_lt_log_two
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
rw : ¬binEntropy p < log 2 ↔ p = 2⁻¹
rw₁ : ¬p ≠ 2⁻¹ ↔ p = 2⁻¹
rw₂ rw₃ : p = 2⁻¹ ↔ p = 2⁻¹
⊢ binEntropy p = log 2 ↔ p = 2⁻¹

Tactic:
rw [← binEntropy_le_log_two.not_lt_iff_eq, binEntropy_lt_log_two, not_ne_iff]

Premises used: not_ne_iff, Real.binEntropy_lt_log_two, Real.binEntropy_le_log_two, LE.le.not_lt_iff_eq
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
rw : Continuous (Y := ℝ) fun (p : ℝ) ↦ p.negMulLog + (1 - p).negMulLog
⊢ Continuous binEntropy

Tactic:
rw [binEntropy_eq_negMulLog_add_negMulLog_one_sub']

Premises used: Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub'
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
⊢ Continuous (Y := ℝ) fun (p : ℝ) ↦ p.negMulLog + (1 - p).negMulLog

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ 1 - p ≠ 0

Tactic:
rw [ne_comm, ← sub_ne_zero] at hp₁

Premises used: sub_ne_zero, ne_comm
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
simp : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ -(p * log p) + -((1 - p) * log (1 - p))) p
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) p

Tactic:
simp only [log_inv, mul_neg]

Premises used: Real.log_inv, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
funProp : p ≠ 0
funProp₁ : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ -(p * log p) + -((1 - p) * log (1 - p))) p

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
⊢ DifferentiableAt ℝ binEntropy p ↔ p ≠ 0 ∧ p ≠ 1

Tactic:
⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ differentiableAt_binEntropy h.1 h.2⟩

Premises used: And.right, And.left, And.intro, Iff.intro, Real.differentiableAt_binEntropy
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
refine_1 : ∀ (h : DifferentiableAt ℝ binEntropy p), p ≠ 0
refine_2 : ∀ (h : DifferentiableAt ℝ binEntropy p), p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p ↔ p ≠ 0 ∧ p ≠ 1

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ differentiableAt_binEntropy h.1 h.2⟩
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
refine_1 : ∀ (h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹) 0), False
refine_1₁ : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ (1 - p) * log (1 - p)⁻¹) 0
⊢ False

Tactic:
rw [DifferentiableAt.fun_add_iff_left] at h

Premises used: DifferentiableAt.fun_add_iff_left
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹) 0
⊢ False

Tactic:
simp [log_inv, mul_neg, ← neg_mul, ← negMulLog_def, differentiableAt_negMulLog_iff] at h

Premises used: Real.negMulLog_def, neg_mul, Real.log_inv, mul_neg, Real.differentiableAt_negMulLog_iff
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ HSub.hSub (α := ℝ) 1 0 ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
⊢ (HSub.hSub (α := ℝ) 1 0)⁻¹ ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 0
funProp : HSub.hSub (α := ℝ) 1 0 ≠ 0
funProp₁ : (HSub.hSub (α := ℝ) 1 0)⁻¹ ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ (1 - p) * log (1 - p)⁻¹) 0

Tactic:
fun_prop (disch := simp)
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
refine_2 :
  ∀ (h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (1 - (1 - x)) * log (1 - (1 - x))⁻¹) (HSub.hSub (α := ℝ) 1 1)),
    False
refine_2₁ : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹) 1
⊢ False

Tactic:
rw [DifferentiableAt.fun_add_iff_right, differentiableAt_iff_comp_const_sub (b := 1)] at h

Premises used: differentiableAt_iff_comp_const_sub, DifferentiableAt.fun_add_iff_right
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ (1 - (1 - x)) * log (1 - (1 - x))⁻¹) (HSub.hSub (α := ℝ) 1 1)
⊢ False

Tactic:
simp [log_inv, mul_neg, ← neg_mul, ← negMulLog_def, differentiableAt_negMulLog_iff] at h

Premises used: Real.negMulLog_def, neg_mul, Real.log_inv, mul_neg, Real.differentiableAt_negMulLog_iff
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ Ne (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
⊢ Ne (α := ℝ) 1⁻¹ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
h : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹) 1
funProp : Ne (α := ℝ) 1 0
funProp₁ : Ne (α := ℝ) 1⁻¹ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ p * log p⁻¹) 1

Tactic:
fun_prop (disch := simp)
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
pos : ∀ (hp : p ≠ 0 ∧ p ≠ 1), deriv binEntropy p = log (1 - p) - log p
neg : ∀ (hp : ¬(p ≠ 0 ∧ p ≠ 1)), deriv binEntropy p = log (1 - p) - log p
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
by_cases hp : p ≠ 0 ∧ p ≠ 1
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p ≠ 0 ∧ p ≠ 1
⊢ p ≠ 0

Tactic:
obtain ⟨hp₀, hp₁⟩ := hp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp : p ≠ 0 ∧ p ≠ 1
hp₀ : p ≠ 0
⊢ p ≠ 1

Tactic:
obtain ⟨hp₀, hp₁⟩ := hp
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
pos : -log p - 1 + -(-log (1 - p) - 1) = log (1 - p) - log p
pos₁ : DifferentiableAt ℝ negMulLog p
pos₂ : DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ (1 - p).negMulLog) p
⊢ deriv binEntropy p = log (1 - p) - log p

Tactic:
rw [binEntropy_eq_negMulLog_add_negMulLog_one_sub', deriv_fun_add, deriv_comp_const_sub,
      deriv_negMulLog hp₀, deriv_negMulLog hp₁]

Premises used: Real.deriv_negMulLog, deriv_comp_const_sub, deriv_fun_add, Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub'
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
⊢ -log p - 1 + -(-log (1 - p) - 1) = log (1 - p) - log p

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
funProp : p ≠ 0
⊢ DifferentiableAt ℝ negMulLog p

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Goal:
p : ℝ
hp₀ : p ≠ 0
hp₁ : 1 - p ≠ 0
funProp : 1 - p ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ) ↦ (1 - p).negMulLog) p

Tactic:
fun_prop