case intro
m✝ n✝ n : ℕ∞
hn : n ≠ ⊤
m : ℕ
⊢ ↑toNat (↑m + n) = ↑toNat ↑m + ↑toNat n
m✝ n✝ m n : ℕ∞
hm : m ≠ ⊤
hn : n ≠ ⊤
⊢ ↑toNat (m + n) = ↑toNat m + ↑toNat n
lift m to ℕ using hm
case intro.intro
m✝ n✝ : ℕ∞
m n : ℕ
⊢ ↑toNat (↑m + ↑n) = ↑toNat ↑m + ↑toNat ↑n
case intro
m✝ n✝ n : ℕ∞
hn : n ≠ ⊤
m : ℕ
⊢ ↑toNat (↑m + n) = ↑toNat ↑m + ↑toNat n
lift n to ℕ using hn
no goals
case intro.intro
m✝ n✝ : ℕ∞
m n : ℕ
⊢ ↑toNat (↑m + ↑n) = ↑toNat ↑m + ↑toNat ↑n
rfl