Theorem: Finset.Icc_eq_Ico (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
M N : ℕ
⊢ Icc N M = Ico N (M + 1)
Tactic:
ext a
State after:
case a
M N a : ℕ
⊢ a ∈ Icc N M ↔ a ∈ Ico N (M + 1)

State before:
case a
M N a : ℕ
⊢ a ∈ Icc N M ↔ a ∈ Ico N (M + 1)
Tactic:
simp only [Finset.mem_Icc, Finset.mem_Ico]
State after:
case a
M N a : ℕ
⊢ N ≤ a ∧ a ≤ M ↔ N ≤ a ∧ a < M + 1

State before:
case a
M N a : ℕ
⊢ N ≤ a ∧ a ≤ M ↔ N ≤ a ∧ a < M + 1
Tactic:
constructor <;> intro ⟨h₁, h₂⟩ <;> omega
State after:
no goals