[GOAL]
m n : ℕ∞
⊢ ↑(↑toNat ⊤) = ⊤ ↔ ⊤ ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
m n : ℕ∞
x✝ : ℕ
⊢ ↑(↑toNat ↑x✝) = ↑x✝ ↔ ↑x✝ ≠ ⊤
[PROOFSTEP]
simp [toNat_coe]
[GOAL]
m✝ n✝ m n : ℕ∞
hm : m ≠ ⊤
hn : n ≠ ⊤
⊢ ↑toNat (m + n) = ↑toNat m + ↑toNat n
[PROOFSTEP]
lift m to ℕ using hm
[GOAL]
case intro
m✝ n✝ n : ℕ∞
hn : n ≠ ⊤
m : ℕ
⊢ ↑toNat (↑m + n) = ↑toNat ↑m + ↑toNat n
[PROOFSTEP]
lift n to ℕ using hn
[GOAL]
case intro.intro
m✝ n✝ : ℕ∞
m n : ℕ
⊢ ↑toNat (↑m + ↑n) = ↑toNat ↑m + ↑toNat ↑n
[PROOFSTEP]
rfl
[GOAL]
m✝ n✝ n : ℕ∞
hn : n ≠ ⊤
m : ℕ∞
⊢ ↑toNat (m - n) = ↑toNat m - ↑toNat n
[PROOFSTEP]
lift n to ℕ using hn
[GOAL]
case intro
m✝ n✝ m : ℕ∞
n : ℕ
⊢ ↑toNat (m - ↑n) = ↑toNat m - ↑toNat ↑n
[PROOFSTEP]
induction m using ENat.recTopCoe
[GOAL]
case intro.h₁
m n✝ : ℕ∞
n : ℕ
⊢ ↑toNat (⊤ - ↑n) = ↑toNat ⊤ - ↑toNat ↑n
[PROOFSTEP]
rw [top_sub_coe, toNat_top, zero_tsub]
[GOAL]
case intro.h₂
m n✝ : ℕ∞
n a✝ : ℕ
⊢ ↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
[PROOFSTEP]
rw [← coe_sub, toNat_coe, toNat_coe, toNat_coe]
[GOAL]
m✝ n✝ m : ℕ∞
n : ℕ
hn : n ≠ 0
⊢ ↑toNat m = n ↔ m = ↑n
[PROOFSTEP]
induction m using ENat.recTopCoe
[GOAL]
case h₁
m n✝ : ℕ∞
n : ℕ
hn : n ≠ 0
⊢ ↑toNat ⊤ = n ↔ ⊤ = ↑n
[PROOFSTEP]
simp [hn.symm]
[GOAL]
case h₂
m n✝ : ℕ∞
n : ℕ
hn : n ≠ 0
a✝ : ℕ
⊢ ↑toNat ↑a✝ = n ↔ ↑a✝ = ↑n
[PROOFSTEP]
simp [hn.symm]
[GOAL]
m✝ n m : ℕ∞
⊢ Order.succ m = m + 1
[PROOFSTEP]
cases m
[GOAL]
case none
m n : ℕ∞
⊢ Order.succ none = none + 1
[PROOFSTEP]
rfl
[GOAL]
case some
m n : ℕ∞
val✝ : ℕ
⊢ Order.succ (some val✝) = some val✝ + 1
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ∞
hm : m ≠ ⊤
⊢ ¬IsMax m
[PROOFSTEP]
rwa [isMax_iff_eq_top]
[GOAL]
m n : ℕ∞
P : ℕ∞ → Prop
a : ℕ∞
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
⊢ P a
[PROOFSTEP]
have A : ∀ n : ℕ, P n := fun n => Nat.recOn n h0 hsuc
[GOAL]
m n : ℕ∞
P : ℕ∞ → Prop
a : ℕ∞
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P a
[PROOFSTEP]
cases a
[GOAL]
case none
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
⊢ P none
[PROOFSTEP]
exact htop A
[GOAL]
case some
m n : ℕ∞
P : ℕ∞ → Prop
h0 : P 0
hsuc : ∀ (n : ℕ), P ↑n → P ↑(Nat.succ n)
htop : (∀ (n : ℕ), P ↑n) → P ⊤
A : ∀ (n : ℕ), P ↑n
val✝ : ℕ
⊢ P (some val✝)
[PROOFSTEP]
exact A _
