-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma not_continuousAt_deriv_qaryEntropy_zero :
    ¬ContinuousAt (deriv (qaryEntropy q)) 0

Proof state:
case h
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ ∀ a ∈ Ioo 0 2⁻¹, log (↑q - 1) + log (1 - a) - log a = deriv (qaryEntropy q) a

Tactic:
intros

Result:
case h
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo 0 2⁻¹
⊢ log (↑q - 1) + log (1 - a✝¹) - log a✝¹ = deriv (qaryEntropy q) a✝¹

Proof state:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo 0 2⁻¹
⊢ a✝¹ ≠ 0

Tactic:
simp_all only [zero_add, mem_Ioo, ne_eq]

Result:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : 0 < a✝¹ ∧ a✝¹ < 2⁻¹
⊢ ¬a✝¹ = 0

Proof state:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo 0 2⁻¹
⊢ a✝¹ ≠ 1

Tactic:
simp_all only [zero_add, mem_Ioo, ne_eq]

Result:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : 0 < a✝¹ ∧ a✝¹ < 2⁻¹
⊢ ¬a✝¹ = 1

Proof state:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : 0 < a✝¹ ∧ a✝¹ < 2⁻¹
⊢ ¬a✝¹ = 1

Tactic:
linarith [two_inv_lt_one (α := ℝ)]

Result:
no goals

Proof state:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ (fun p => log (↑q - 1) + log (1 - p) - log p) =ᶠ[𝓝[>] 0] deriv (qaryEntropy q)

Tactic:
filter_upwards [Ioo_mem_nhdsGT (show (0 : ℝ) < 2⁻¹ by norm_num)]

Result:
case h
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ ∀ a ∈ Ioo 0 2⁻¹, log (↑q - 1) + log (1 - a) - log a = deriv (qaryEntropy q) a

Proof state:
q : ℕ
this : (fun p => log (↑q - 1) + log (1 - p) - log p) = fun p => log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun p => log (↑q - 1) + (log (1 - p) - log p)) (𝓝[>] 0) atTop

Tactic:
exact tendsto_atTop_add_const_left _ _ tendsto_log_one_sub_sub_log_nhdsGT_atAtop

Result:
no goals

Proof state:
q : ℕ
⊢ Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop

Tactic:
have : (fun p ↦ log (q - 1) + log (1 - p) - log p)
    = (fun p ↦ log (q - 1) + (log (1 - p) - log p)) := by ext; ring

Result:
q : ℕ
this : (fun p => log (↑q - 1) + log (1 - p) - log p) = fun p => log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop

Proof state:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0

Tactic:
apply not_continuousAt_of_tendsto (Filter.Tendsto.congr' _ tendstoTop) nhdsWithin_le_nhds

Result:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ Disjoint (𝓝 (deriv (qaryEntropy q) 0)) atTop

q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ (fun p => log (↑q - 1) + log (1 - p) - log p) =ᶠ[𝓝[>] 0] deriv (qaryEntropy q)

Proof state:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ 0 < 2⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : 0 < a✝¹ ∧ a✝¹ < 2⁻¹
⊢ ¬a✝¹ = 0

Tactic:
linarith

Result:
no goals

Proof state:
q : ℕ
this : (fun p => log (↑q - 1) + log (1 - p) - log p) = fun p => log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop

Tactic:
rw [this]

Result:
q : ℕ
this : (fun p => log (↑q - 1) + log (1 - p) - log p) = fun p => log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun p => log (↑q - 1) + (log (1 - p) - log p)) (𝓝[>] 0) atTop

Proof state:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ Disjoint (𝓝 (deriv (qaryEntropy q) 0)) atTop

Tactic:
simp only [disjoint_nhds_atTop_iff, not_isTop, not_false_eq_true]

Result:
no goals

Proof state:
case h
q : ℕ
x✝ : ℝ
⊢ log (↑q - 1) + log (1 - x✝) - log x✝ = log (↑q - 1) + (log (1 - x✝) - log x✝)

Tactic:
ring

Result:
no goals

Proof state:
q : ℕ
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0

Tactic:
have tendstoTop : Tendsto (fun p ↦ log (q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop := by
  have : (fun p ↦ log (q - 1) + log (1 - p) - log p)
      = (fun p ↦ log (q - 1) + (log (1 - p) - log p)) := by ext; ring
  rw [this]
  exact tendsto_atTop_add_const_left _ _ tendsto_log_one_sub_sub_log_nhdsGT_atAtop

Result:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 0

Proof state:
q : ℕ
⊢ (fun p => log (↑q - 1) + log (1 - p) - log p) = fun p => log (↑q - 1) + (log (1 - p) - log p)

Tactic:
ext

Result:
case h
q : ℕ
x✝ : ℝ
⊢ log (↑q - 1) + log (1 - x✝) - log x✝ = log (↑q - 1) + (log (1 - x✝) - log x✝)

Proof state:
case h
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo 0 2⁻¹
⊢ log (↑q - 1) + log (1 - a✝¹) - log a✝¹ = deriv (qaryEntropy q) a✝¹

Tactic:
apply (deriv_qaryEntropy _ _).symm

Result:
q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo 0 2⁻¹
⊢ a✝¹ ≠ 0

q : ℕ
tendstoTop : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[>] 0) atTop
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioo 0 2⁻¹
⊢ a✝¹ ≠ 1