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

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

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

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