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

State before:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ c + ↑m = ↑n + ↑m ↔ c = ↑n
Tactic:
rw [WithTop.add_right_cancel_iff]
State after:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ ↑m ≠ ⊤

State before:
α : Type u_1
c : ℕ∞
m n : ℕ
⊢ ↑m ≠ ⊤
Tactic:
exact WithTop.coe_ne_top
State after:
no goals