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

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

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

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