simp only [Finset.mem_Ioc, Finset.mem_singleton]
case a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ m ∈ Finset.Ioc k (1 + k) ↔ m ∈ {k + 1}
case a
φ : ℝ → ℂ
a b : ℝ
k : ℤ
b_eq_kpOne : b = ↑k + 1
φDiff : ∀ x ∈ [[a, b]], HasDerivAt φ (deriv φ x) x
derivφCont : ContinuousOn (deriv φ) [[a, b]]
flb_eq_k : ⌊b⌋ = k + 1
m : ℤ
⊢ k < m ∧ m ≤ 1 + k ↔ m = k + 1