n : ℕ
x✝ : Decidable (↑n).Dom
⊢ toWithTop ↑n = toWithTop ↑n
n : ℕ
x✝ : Decidable (↑n).Dom
⊢ toWithTop ↑n = ↑n
simp only [← toWithTop_some]
no goals
n : ℕ
x✝ : Decidable (↑n).Dom
⊢ toWithTop ↑n = toWithTop ↑n
congr