awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Bernstein (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : TopologicalSpace E
inst_2 : IsTopologicalAddGroup E
inst_3 : Module ℝ E
inst_4 : ContinuousSMul ℝ E
inst_5 : LocallyConvexSpace ℝ E
f : C((↑I : Type), E)
this_1 : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
U : Set E
hU₀ : Membership.mem (γ := Filter E) (𝓝 0) U
hUc : Convex ℝ U
C : ℝ
hC :
  ∀ (x y : (↑I : Type)),
    gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) ≤ C
hC₀ : 0 ≤ C
δ : ℝ
hδ₀ : δ > 0
hδ :
  ∀ (x y : (↑I : Type)),
    dist x y < δ →
      gauge U (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) x : E) ((f : (a : (↑I : Type)) → E) y : E)) <
        1 / 2
nhds_zero : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
nh : C / HPow.hPow (β := ℕ) δ 2 / (↑n : ℝ) < 1 / 2
hn₀ : n ≠ 0
x : (↑I : Type)
S : Finset (Fin (n + 1)) := {k : Fin (n + 1) | dist k/ₙ x < δ}
k :
  LE.le (α := ℝ)
    (∑ k ∈ Sᶜ,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))))
    (∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ))
k₁ :
  ∑ k ∈ Sᶜ, HMul.hMul (β := ℝ) C ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ) =
    C * ∑ k ∈ Sᶜ, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x
⊢ ∑ k ∈ Sᶜ,
      HMul.hMul (α := ℝ) ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
        (gauge U
          (HSub.hSub (α := E) (β := E) ((f : (a : (↑I : Type)) → E) k/ₙ : E) ((f : (a : (↑I : Type)) → E) x : E))) <
    1 / 2
have k₂ : C * ∑ k ∈ Sᶜ, (bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x ≤
  C *
    ∑ k ∈ Sᶜ,
      HMul.hMul (β := ℝ) (HPow.hPow (β := ℕ) ((↑x : ℝ) - (↑k/ₙ : ℝ)) 2 / HPow.hPow (β := ℕ) δ 2)
        ((bernstein n (↑k : ℕ) : (a : (↑I : Type)) → ℝ) x : ℝ)
Tactic: calc
      ∑ k ∈ Sᶜ, bernstein n k x * gauge U (f k/ₙ - f x) ≤ ∑ k ∈ Sᶜ, C * bernstein n k x := by
        simp only [mul_comm (bernstein n _ x)]
        gcongr
        apply hC
      _ = C * ∑ k ∈ Sᶜ, bernstein n k x := by rw [Finset.mul_sum]
      _ ≤ C * ∑ k ∈ Sᶜ, ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by
        gcongr with k hk
        conv_lhs => rw [← one_mul (bernstein _ _ _)]
        gcongr
        simpa [one_le_div₀, hδ₀, sq_le_sq, S, abs_of_pos, ← Real.dist_eq, dist_comm (x : ℝ)]
          using hk
      -- Again enlarging the sum from `Sᶜ` to all of `Fin (n+1)`
      _ ≤ C * ∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 / δ ^ 2 * bernstein n k x := by
        gcongr; exact Sᶜ.subset_univ
      _ = C * (∑ k : Fin (n + 1), ((x : ℝ) - k/ₙ) ^ 2 * bernstein n k x) / δ ^ 2 := by
        simp only [← mul_div_right_comm, ← mul_div_assoc, ← Finset.sum_div]
      -- `bernstein.variance` and `x ∈ [0,1]` gives the uniform bound
      _ = C / δ ^ 2 * x * (1 - x) / n := by rw [variance hn₀]; ring
      _ ≤ C / δ ^ 2 * 1 * 1 / n := by gcongr <;> unit_interval
      _ < 1 / 2 := by simpa only [mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
⊢ binEntropy 2⁻¹ = log 2
have norm_num : 1 / 2 * log 2 + 1 / 2 * log 2 = log 2
Tactic: norm_num [binEntropy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
⊢ 1 / 2 * log 2 + 1 / 2 * log 2 = log 2
have simp : 2⁻¹ * log 2 + 2⁻¹ * log 2 = log 2
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
⊢ binEntropy (2⁻¹ + p) = binEntropy (2⁻¹ - p)
have rw : binEntropy (1 - (2⁻¹ + p)) = binEntropy (2⁻¹ - p)
Tactic: rw [← binEntropy_one_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹
have this : 0 < 1 - p
Tactic: have : 0 < 1 - p := sub_pos.2 hp₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this : 0 < 1 - p
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹
have this₁ : 0 < log p⁻¹
Tactic: have : 0 < log p⁻¹ := log_pos <| (one_lt_inv₀ hp₀).2 hp₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
hp₀ : 0 < p
hp₁ : p < 1
this_1 : 0 < 1 - p
this : 0 < log p⁻¹
⊢ 0 < p * log p⁻¹ + (1 - p) * log (1 - p)⁻¹
have this₁ : 0 < log (1 - p)⁻¹
Tactic: have : 0 < log (1 - p)⁻¹ := log_pos <| (one_lt_inv₀ ‹_›).2 (sub_lt_self _ hp₀)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
⊢ 0 ≤ binEntropy p
have inl : ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1), 0 ≤ binEntropy 0
Tactic: obtain rfl | hp₀ := hp₀.eq_or_lt
Cleared hypotheses: p, hp₀, hp₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp₀ : 0 ≤ p
hp₁ : p ≤ 1
inl : ∀ (hp₀ : LE.le (α := ℝ) 0 0) (hp₁ : LE.le (α := ℝ) 0 1), 0 ≤ binEntropy 0
⊢ 0 ≤ binEntropy p
have inr : ∀ (hp₀ : 0 < p), 0 ≤ binEntropy p
Tactic: obtain rfl | hp₀ := hp₀.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
⊢ 0 ≤ binEntropy p
have inr : ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1), 0 ≤ binEntropy 1
Tactic: obtain rfl | hp₁ := hp₁.eq_or_lt
Cleared hypotheses: p, hp₀_1, hp₁, hp₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp₀_1 : 0 ≤ p
hp₁ : p ≤ 1
hp₀ : 0 < p
inr : ∀ (hp₀ : LE.le (α := ℝ) 0 1) (hp₁ : LE.le (α := ℝ) 1 1) (hp₀ : LT.lt (α := ℝ) 0 1), 0 ≤ binEntropy 1
⊢ 0 ≤ binEntropy p
have inr₁ : ∀ (hp₁ : p < 1), 0 ≤ binEntropy p
Tactic: obtain rfl | hp₁ := hp₁.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
⊢ binEntropy p < 0
have rw : p * -log p + (1 - p) * -log (1 - p) < 0
Tactic: rw [binEntropy, log_inv, log_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
this : -p * log p < (1 - p) * log (1 - p)
⊢ p * -log p + (1 - p) * -log (1 - p) < 0
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
⊢ p * -log p + (1 - p) * -log (1 - p) < 0
have suffices : -p * log p < (1 - p) * log (1 - p)
Tactic: suffices -p * log p < (1 - p) * log (1 - p) by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
⊢ -p * log p < (1 - p) * log (1 - p)
have pos : ∀ (hp' : p < -1), -p * log p < (1 - p) * log (1 - p)
Tactic: by_cases hp' : p < -1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
pos : ∀ (hp' : p < -1), -p * log p < (1 - p) * log (1 - p)
⊢ -p * log p < (1 - p) * log (1 - p)
have neg : ∀ (hp' : ¬p < -1), -p * log p < (1 - p) * log (1 - p)
Tactic: by_cases hp' : p < -1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
hp' : p < -1
⊢ log p < log (1 - p)
have rw : log (-p) < log (1 - p)
Tactic: rw [← log_neg_eq_log]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p < 1 - p
have linarith : 1 - p ≤ -p → -1 + (1 - p - -p) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
hp : p < 0
hp' : p < -1
⊢ -p * log p < (1 - p) * log (1 - p)
have this : 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
hp' : p < -1
this : log p < log (1 - p)
⊢ -p * log p < (1 - p) * log (1 - p)
have 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
Tactic: nlinarith [log_pos_of_lt_neg_one hp']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p ≤ 0
have inr : ∀ (this : ∀ {p : ℝ} (hp : p < 0) (hp' : ¬p < -1) (h : -1 < p), -p * log p ≤ 0) (h : ¬-1 < p), -p * log p ≤ 0
Tactic: wlog h : -1 < p
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ -p * log p ≤ 0
have wlog : ∀ {p : ℝ} (hp : p < 0) (hp' : ¬p < -1) (h : -1 < p), -p * log p ≤ 0
Tactic: wlog h : -1 < p
Cleared hypotheses: hp, hp'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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 = -1
have linarith : p < -1 → -1 - p + (p - -1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ p = -1
have linarith₁ : -1 < p → p - -1 + (-1 - p) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p_1 p : ℝ
hp : p < 0
hp' : ¬p < -1
h : -1 < p
⊢ -p * log p ≤ 0
have nlinarith : 0 < -p * log p → 0 - -p * log p + (0 - (p - 0) * (log p - 0)) = 0
Tactic: nlinarith [log_neg_of_lt_zero hp h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
hp : p < 0
hp' : ¬p < -1
⊢ -p * log p < (1 - p) * log (1 - p)
have this : -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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : -p * log p ≤ 0
⊢ 1 < 1 - p
have linarith : 1 - p ≤ 1 → p - 0 + (1 - p - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p < 0
hp' : ¬p < -1
this : -p * log p ≤ 0
⊢ -p * log p < (1 - p) * log (1 - p)
have 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
Tactic: nlinarith [(log_pos (by linarith) : 0 < log (1 - p))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p ≤ 0
⊢ binEntropy p ≤ 0
have inl : ∀ (hp : LE.le (α := ℝ) 0 0), binEntropy 0 ≤ 0
Tactic: obtain rfl | hp := hp.eq_or_lt
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : p ≤ 0
inl : ∀ (hp : LE.le (α := ℝ) 0 0), binEntropy 0 ≤ 0
⊢ binEntropy p ≤ 0
have inr : ∀ (hp : p < 0), binEntropy p ≤ 0
Tactic: obtain rfl | hp := hp.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : 1 < p
⊢ binEntropy p < 0
have rw : binEntropy (1 - p) < 0
Tactic: rw [← binEntropy_one_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
hp : 1 ≤ p
⊢ binEntropy p ≤ 0
have rw : binEntropy (1 - p) ≤ 0
Tactic: rw [← binEntropy_one_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
⊢ binEntropy p = 0 ↔ p = 0 ∨ p = 1
have refine : ∀ (h : binEntropy p = 0), p = 0 ∨ p = 1
Tactic: refine ⟨fun h ↦ ?_, by rintro (rfl | rfl) <;> simp⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
h : binEntropy p = 0
⊢ p = 0 ∨ p = 1
have contrapose! : ∀ (h : p ≠ 0 ∧ p ≠ 1), binEntropy p ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
⊢ binEntropy p ≠ 0
have inl : ∀ (hp₀ : p < 0), binEntropy p ≠ 0
Tactic: obtain hp₀ | hp₀ := h.1.lt_or_gt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
inl : ∀ (hp₀ : p < 0), binEntropy p ≠ 0
⊢ binEntropy p ≠ 0
have inr : ∀ (hp₀ : 0 < p), binEntropy p ≠ 0
Tactic: obtain hp₀ | hp₀ := h.1.lt_or_gt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
⊢ binEntropy p ≠ 0
have inr : ∀ (hp₁ : 1 < p), binEntropy p ≠ 0
Tactic: obtain hp₁ | hp₁ := h.2.lt_or_gt.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
h : p ≠ 0 ∧ p ≠ 1
hp₀ : 0 < p
inr : ∀ (hp₁ : 1 < p), binEntropy p ≠ 0
⊢ binEntropy p ≠ 0
have inr₁ : ∀ (hp₁ : p < 1), binEntropy p ≠ 0
Tactic: obtain hp₁ | hp₁ := h.2.lt_or_gt.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
⊢ binEntropy p < log 2 ↔ p ≠ 2⁻¹
have refine_1 : binEntropy p < log 2 → p ≠ 2⁻¹
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
refine_1 : binEntropy p < log 2 → p ≠ 2⁻¹
⊢ binEntropy p < log 2 ↔ p ≠ 2⁻¹
have refine_2 : ∀ (h : p ≠ 2⁻¹), binEntropy p < log 2
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
h : p ≠ 2⁻¹
⊢ binEntropy p < log 2
have refine_2 : ∀ (this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2) (hp : ¬p < 2⁻¹), binEntropy p < log 2
Tactic: wlog hp : p < 2⁻¹
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ binEntropy p < log 2
have wlog : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
Tactic: wlog hp : p < 2⁻¹
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ 1 - p < 2⁻¹
have rw : HSub.hSub (α := ℝ) 1 2⁻¹ < p
Tactic: rw [sub_lt_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ HSub.hSub (α := ℝ) 1 2⁻¹ < p
have 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
Tactic: norm_num at *
Cleared hypotheses: h, this, hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
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
have linarith : p ≤ 1 / 2 → p < 1 / 2 → 2 / 2 = 1
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ 1 / 2 < p
have linarith₁ : p ≤ 1 / 2 → p < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ 1 / 2 < p
have linarith₂ : p ≤ 1 / 2 → p < 1 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ 1 / 2 < p
have linarith₉ : p ≤ 1 / 2 → 1 / 2 < p → 2 / 2 = 1
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ 1 / 2 < p
have linarith₁₀ : p ≤ 1 / 2 → 1 / 2 < p → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ 1 / 2 < p
have linarith₁₁ : p ≤ 1 / 2 → 1 / 2 < p → GT.gt (α := ℝ) 2 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ 1 / 2 < p
have linarith₁₈ : p ≤ 1 / 2 → p < 1 / 2 → 2 * p - HMul.hMul (α := ℝ) 1 1 + (HMul.hMul (α := ℝ) 1 1 - 2 * p) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
⊢ 1 / 2 < p
have linarith₁₉ : p ≤ 1 / 2 → 1 / 2 < p → HMul.hMul (α := ℝ) 1 1 - 2 * p + (2 * p - HMul.hMul (α := ℝ) 1 1) = 0
Tactic: linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p : ℝ
h : p ≠ 2⁻¹
this : ∀ {p : ℝ} (h : p ≠ 2⁻¹) (hp : p < 2⁻¹), binEntropy p < log 2
hp : ¬p < 2⁻¹
⊢ binEntropy p < log 2
have hp₁ : 1 - p < 2⁻¹
Tactic: have hp : 1 - p < 2⁻¹ := by
      rw [sub_lt_comm]; norm_num at *; linarith +splitNe
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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 p < log 2
have refine_2 : binEntropy (1 - p) < log 2
Tactic: rw [← binEntropy_one_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
⊢ binEntropy p < log 2
have inl : ∀ (hp₀ : p ≤ 0), binEntropy p < log 2
Tactic: obtain hp₀ | hp₀ := le_or_gt p 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
inl : ∀ (hp₀ : p ≤ 0), binEntropy p < log 2
⊢ binEntropy p < log 2
have inr : ∀ (hp₀ : 0 < p), binEntropy p < log 2
Tactic: obtain hp₀ | hp₀ := le_or_gt p 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
⊢ binEntropy p < log 2
have hp₁ : 0 < 1 - p
Tactic: have hp₁ : 0 < 1 - p := sub_pos.2 <| hp.trans <| by norm_num
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
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
have rw : 1 - p ≠ 0
Tactic: rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
rw : 1 - p ≠ 0
⊢ log (p * p⁻¹ + (1 - p) * (1 - p)⁻¹) = log 2
have rw₁ : p ≠ 0
Tactic: rw [mul_inv_cancel₀, mul_inv_cancel₀, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p_1 p : ℝ
h : p ≠ 2⁻¹
hp : p < 2⁻¹
hp₀ : 0 < p
hp₁ : 0 < 1 - p
⊢ binEntropy p < log 2
have _ : log (p * p⁻¹ + (1 - p) * (1 - 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
⊢ binEntropy p ≤ log 2
have inl : binEntropy 2⁻¹ ≤ log 2
Tactic: obtain rfl | hp := eq_or_ne p 2⁻¹
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
p : ℝ
inl : binEntropy 2⁻¹ ≤ log 2
⊢ binEntropy p ≤ log 2
have inr : ∀ (hp : p ≠ 2⁻¹), binEntropy p ≤ log 2
Tactic: obtain rfl | hp := eq_or_ne p 2⁻¹