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

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) (𝓝[<] 1) atBot

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)) (𝓝[<] 1) atBot

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

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

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)) 1

Tactic:
have tendstoBot : Tendsto (fun p ↦ log (q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot := 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]
  apply tendsto_atBot_add_const_left
  exact tendsto_log_one_sub_sub_log_nhdsLT_one_atBot

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

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:
q : ℕ
tendstoBot : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ ¬ContinuousAt (deriv (qaryEntropy q)) 1

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

Result:
q : ℕ
tendstoBot : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ Disjoint (𝓝 (deriv (qaryEntropy q) 1)) atBot

q : ℕ
tendstoBot : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ (fun p => log (↑q - 1) + log (1 - p) - log p) =ᶠ[𝓝[<] 1] deriv (qaryEntropy q)

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

Tactic:
filter_upwards [Ioo_mem_nhdsLT (show 1 - 2⁻¹ < (1 : ℝ) by norm_num)]

Result:
case h
q : ℕ
tendstoBot : Tendsto (fun p => log (↑q - 1) + log (1 - p) - log p) (𝓝[<] 1) atBot
⊢ ∀ a ∈ Ioo (1 - 2⁻¹) 1, 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)) (𝓝[<] 1) atBot

Tactic:
apply tendsto_atBot_add_const_left

Result:
case hf
q : ℕ
this : (fun p => log (↑q - 1) + log (1 - p) - log p) = fun p => log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun x => log (1 - x) - log x) (𝓝[<] 1) atBot

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

Tactic:
linarith [show (1 : ℝ) = 2⁻¹ + 2⁻¹ by norm_num]

Result:
no goals

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

Tactic:
norm_num

Result:
no goals

Proof state:
case hf
q : ℕ
this : (fun p => log (↑q - 1) + log (1 - p) - log p) = fun p => log (↑q - 1) + (log (1 - p) - log p)
⊢ Tendsto (fun x => log (1 - x) - log x) (𝓝[<] 1) atBot

Tactic:
exact tendsto_log_one_sub_sub_log_nhdsLT_one_atBot

Result:
no goals

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

Tactic:
simp_all only [mem_Ioo, ne_eq]

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

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

Tactic:
simp only [disjoint_nhds_atBot_iff, not_isBot, not_false_eq_true]

Result:
no goals

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

Tactic:
simp_all only [mem_Ioo, ne_eq]

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

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

Tactic:
norm_num

Result:
no goals

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

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) (𝓝[<] 1) atBot

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

Tactic:
intros

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

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

Tactic:
apply (deriv_qaryEntropy _ _).symm

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

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