case refine_1.refine_1
x y : PartENat
⊢ toWithTop (⊤ + ⊤) = toWithTop ⊤ + toWithTop ⊤

case refine_1.refine_2
x y : PartENat
⊢ ∀ (n : ℕ), toWithTop (↑n + ⊤) = toWithTop ↑n + toWithTop ⊤

case refine_2.refine_1
x y : PartENat
⊢ ∀ (n : ℕ), toWithTop (⊤ + ↑n) = toWithTop ⊤ + toWithTop ↑n

case refine_2.refine_2
x y : PartENat
⊢ ∀ (n n_1 : ℕ), toWithTop (↑n + ↑n_1) = toWithTop ↑n + toWithTop ↑n_1
x y : PartENat
⊢ toWithTop (x + y) = toWithTop x + toWithTop y
refine PartENat.casesOn y ?_ ?_ <;> refine PartENat.casesOn x ?_ ?_
no goals
case refine_1.refine_1
x y : PartENat
⊢ toWithTop (⊤ + ⊤) = toWithTop ⊤ + toWithTop ⊤
simp only [add_top, toWithTop_top', _root_.add_top]
no goals
case refine_1.refine_2
x y : PartENat
⊢ ∀ (n : ℕ), toWithTop (↑n + ⊤) = toWithTop ↑n + toWithTop ⊤
simp only [add_top, toWithTop_top', toWithTop_natCast', _root_.add_top, forall_const]
no goals
case refine_2.refine_1
x y : PartENat
⊢ ∀ (n : ℕ), toWithTop (⊤ + ↑n) = toWithTop ⊤ + toWithTop ↑n
simp only [top_add, toWithTop_top', toWithTop_natCast', _root_.top_add, forall_const]
no goals
case refine_2.refine_2
x y : PartENat
⊢ ∀ (n n_1 : ℕ), toWithTop (↑n + ↑n_1) = toWithTop ↑n + toWithTop ↑n_1
simp_rw [toWithTop_natCast', ← Nat.cast_add, toWithTop_natCast', forall_const]