case intro
m✝ n✝ m : ℕ∞
n : ℕ
⊢ ↑toNat (m - ↑n) = ↑toNat m - ↑toNat ↑n
m✝ n✝ n : ℕ∞
hn : n ≠ ⊤
m : ℕ∞
⊢ ↑toNat (m - n) = ↑toNat m - ↑toNat n
lift n to ℕ using hn
case intro.h₁
m n✝ : ℕ∞
n : ℕ
⊢ ↑toNat (⊤ - ↑n) = ↑toNat ⊤ - ↑toNat ↑n

case intro.h₂
m n✝ : ℕ∞
n a✝ : ℕ
⊢ ↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
case intro
m✝ n✝ m : ℕ∞
n : ℕ
⊢ ↑toNat (m - ↑n) = ↑toNat m - ↑toNat ↑n
induction m using ENat.recTopCoe
no goals
case intro.h₁
m n✝ : ℕ∞
n : ℕ
⊢ ↑toNat (⊤ - ↑n) = ↑toNat ⊤ - ↑toNat ↑n
rw [top_sub_coe, toNat_top, zero_tsub]
no goals
case intro.h₂
m n✝ : ℕ∞
n a✝ : ℕ
⊢ ↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]