no goals
n : ℕ∞
x✝ : Decidable (↑n).Dom
⊢ toWithTop ↑n = n
induction n with
| none => simp
| some n =>
  simp only [toWithTop_natCast', ofENat_some]
  rfl
no goals
case none
x✝ : Decidable (↑Option.none).Dom
⊢ toWithTop ↑Option.none = Option.none
simp
case some
n : ℕ
x✝ : Decidable (↑(Option.some n)).Dom
⊢ ↑n = Option.some n
case some
n : ℕ
x✝ : Decidable (↑(Option.some n)).Dom
⊢ toWithTop ↑(Option.some n) = Option.some n
simp only [toWithTop_natCast', ofENat_some]
no goals
case some
n : ℕ
x✝ : Decidable (↑(Option.some n)).Dom
⊢ ↑n = Option.some n
rfl