case intro
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ a + ↑c = b + ↑c ↔ a = b
a b c : PartENat
hc : c ≠ ⊤
⊢ a + c = b + c ↔ a = b
rcases ne_top_iff.1 hc with ⟨c, rfl⟩
case intro.refine_2.refine_2
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ∀ (n n_1 : ℕ), ↑n_1 + ↑c = ↑n + ↑c ↔ n_1 = n
case intro
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ a + ↑c = b + ↑c ↔ a = b
refine PartENat.casesOn a ?_ ?_
<;> refine PartENat.casesOn b ?_ ?_
<;> simp [add_eq_top_iff, natCast_ne_top, @eq_comm _ (⊤ : PartENat)]
no goals
case intro.refine_2.refine_2
a b : PartENat
c : ℕ
hc : ↑c ≠ ⊤
⊢ ∀ (n n_1 : ℕ), ↑n_1 + ↑c = ↑n + ↑c ↔ n_1 = n
simp only [←Nat.cast_add, add_left_cancel_iff, PartENat.natCast_inj, add_comm, forall_const]