Theorem: WithTop.add_one_eq_coe_succ_iff (Jordan/Mathlib/Set.lean)

State before:
α : Type u_1
c : ℕ∞
n : ℕ
⊢ c + 1 = ↑(Nat.succ n) ↔ c = ↑n
Tactic:
rw [← Nat.cast_one, Nat.succ_eq_add_one, Nat.cast_add, WithTop.add_eq_add_iff]
State after:
no goals