Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2022 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov

! This file was ported from Lean 3 source module data.enat.basic
! leanprover-community/mathlib commit ceb887ddf3344dab425292e497fa2af91498437c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Nat.SuccPred
import Mathlib.Algebra.CharZero.Lemmas
import Mathlib.Algebra.Order.Sub.WithTop
import Mathlib.Algebra.Order.Ring.WithTop

/-!
# Definition and basic properties of extended natural numbers

In this file we define `ENat` (notation: `β„•βˆž`) to be `WithTop β„•` and prove some basic lemmas
about this type.

## Implementation details

There are two natural coercions from `β„•` to `WithTop β„• = ENat`: `WithTop.some` and `Nat.cast`.  In
Lean 3, this difference was hidden in typeclass instances. Since these instances were definitionally
equal, we did not duplicate generic lemmas about `WithTop Ξ±` and `WithTop.some` coercion for `ENat`
and `Nat.cast` coercion. If you need to apply a lemma about `WithTop`, you may either rewrite back
and forth using `ENat.some_eq_coe`, or restate the lemma for `ENat`.
-/

/-- Extended natural numbers `β„•βˆž = WithTop β„•`. -/
def 
ENat: Type
ENat : 
Type: Type 1
Type :=
  
WithTop: Type ?u.3 β†’ Type ?u.3
WithTop 
β„•: Type
β„•
deriving Zero,
  -- AddCommMonoidWithOne,
  CanonicallyOrderedCommSemiring, Nontrivial,
  LinearOrder, Bot, Top, CanonicallyLinearOrderedAddMonoid, Sub,
  LinearOrderedAddCommMonoidWithTop, WellFoundedRelation, Inhabited
  -- OrderBot, OrderTop, OrderedSub,  SuccOrder, WellFoundedLt, CharZero
#align enat 
ENat: Type
ENat

-- Porting Note: In `Data.Nat.ENatPart` proofs timed out when having
-- the `deriving AddCommMonoidWithOne`, and it seems to work without.

/-- Extended natural numbers `β„•βˆž = WithTop β„•`. -/
notation "β„•βˆž" => 
ENat: Type
ENat

namespace ENat

--Porting note: instances that derive failed to find

instance: OrderBot β„•βˆž
instance : 
OrderBot: (Ξ± : Type ?u.7602) β†’ [inst : LE Ξ±] β†’ Type ?u.7602
OrderBot 
β„•βˆž: Type
β„•βˆž := 
WithTop.orderBot: {Ξ± : Type ?u.7773} β†’ [inst : LE Ξ±] β†’ [inst_1 : OrderBot Ξ±] β†’ OrderBot (WithTop Ξ±)
WithTop.orderBot

instance: OrderTop β„•βˆž
instance : 
OrderTop: (Ξ± : Type ?u.8131) β†’ [inst : LE Ξ±] β†’ Type ?u.8131
OrderTop 
β„•βˆž: Type
β„•βˆž := 
WithTop.orderTop: {Ξ± : Type ?u.8302} β†’ [inst : LE Ξ±] β†’ OrderTop (WithTop Ξ±)
WithTop.orderTop

instance: OrderedSub β„•βˆž
instance : 
OrderedSub: (Ξ± : Type ?u.8522) β†’ [inst : LE Ξ±] β†’ [inst : Add Ξ±] β†’ [inst : Sub Ξ±] β†’ Prop
OrderedSub 
β„•βˆž: Type
β„•βˆž := 
inferInstanceAs: βˆ€ (Ξ± : Sort ?u.8884) [i : Ξ±], Ξ±
inferInstanceAs (
OrderedSub: (Ξ± : Type ?u.8885) β†’ [inst : LE Ξ±] β†’ [inst : Add Ξ±] β†’ [inst : Sub Ξ±] β†’ Prop
OrderedSub (
WithTop: Type ?u.8886 β†’ Type ?u.8886
WithTop 
β„•: Type
β„•))

instance: SuccOrder β„•βˆž
instance : 
SuccOrder: (Ξ± : Type ?u.9106) β†’ [inst : Preorder Ξ±] β†’ Type ?u.9106
SuccOrder 
β„•βˆž: Type
β„•βˆž := 
inferInstanceAs: (Ξ± : Sort ?u.9272) β†’ [i : Ξ±] β†’ Ξ±
inferInstanceAs (
SuccOrder: (Ξ± : Type ?u.9273) β†’ [inst : Preorder Ξ±] β†’ Type ?u.9273
SuccOrder (
WithTop: Type ?u.9274 β†’ Type ?u.9274
WithTop 
β„•: Type
β„•))

instance: WellFoundedLT β„•βˆž
instance : 
WellFoundedLT: (Ξ± : Type ?u.9762) β†’ [inst : LT Ξ±] β†’ Prop
WellFoundedLT 
β„•βˆž: Type
β„•βˆž := 
inferInstanceAs: βˆ€ (Ξ± : Sort ?u.9933) [i : Ξ±], Ξ±
inferInstanceAs (
WellFoundedLT: (Ξ± : Type ?u.9934) β†’ [inst : LT Ξ±] β†’ Prop
WellFoundedLT (
WithTop: Type ?u.9935 β†’ Type ?u.9935
WithTop 
β„•: Type
β„•))

instance: CharZero β„•βˆž
instance : 
CharZero: (R : Type ?u.10101) β†’ [inst : AddMonoidWithOne R] β†’ Prop
CharZero 
β„•βˆž: Type
β„•βˆž := 
inferInstanceAs: βˆ€ (Ξ± : Sort ?u.10303) [i : Ξ±], Ξ±
inferInstanceAs (
CharZero: (R : Type ?u.10304) β†’ [inst : AddMonoidWithOne R] β†’ Prop
CharZero (
WithTop: Type ?u.10305 β†’ Type ?u.10305
WithTop 
β„•: Type
β„•))

instance: IsWellOrder β„•βˆž fun x x_1 => x < x_1
instance : 
IsWellOrder: (Ξ± : Type ?u.10510) β†’ (Ξ± β†’ Ξ± β†’ Prop) β†’ Prop
IsWellOrder 
β„•βˆž: Type
β„•βˆž 
(Β· < Β·): β„•βˆž β†’ β„•βˆž β†’ Prop
(Β· < Β·) where

variable {
m: β„•βˆž
m 
n: β„•βˆž
n : 
β„•βˆž: Type
β„•βˆž}

/-- Lemmas about `WithTop` expect (and can output) `WithTop.some` but the normal form for coercion
`β„• β†’ β„•βˆž` is `Nat.cast`. -/
@[simp] theorem 
some_eq_coe: WithTop.some = Nat.cast
some_eq_coe : (
WithTop.some: {Ξ± : Type ?u.10918} β†’ Ξ± β†’ WithTop Ξ±
WithTop.some : 
β„•: Type
β„• β†’ 
β„•βˆž: Type
β„•βˆž) = 
Nat.cast: {R : Type ?u.10923} β†’ [inst : NatCast R] β†’ β„• β†’ R
Nat.cast := 
rfl: βˆ€ {Ξ± : Sort ?u.11047} {a : Ξ±}, a = a
rfl

--Porting note: `simp` and `norm_cast` can prove it
--@[simp, norm_cast]
theorem 
coe_zero: ↑0 = 0
coe_zero : ((
0: ?m.11068
0 : 
β„•: Type
β„•) : 
β„•βˆž: Type
β„•βˆž) = 
0: ?m.11123
0 :=
  
rfl: βˆ€ {Ξ± : Sort ?u.11159} {a : Ξ±}, a = a
rfl
#align enat.coe_zero 
ENat.coe_zero: ↑0 = 0
ENat.coe_zero

--Porting note: `simp` and `norm_cast` can prove it
--@[simp, norm_cast]
theorem 
coe_one: ↑1 = 1
coe_one : ((
1: ?m.11176
1 : 
β„•: Type
β„•) : 
β„•βˆž: Type
β„•βˆž) = 
1: ?m.11231
1 :=
  
rfl: βˆ€ {Ξ± : Sort ?u.11269} {a : Ξ±}, a = a
rfl
#align enat.coe_one 
ENat.coe_one: ↑1 = 1
ENat.coe_one

--Porting note: `simp` and `norm_cast` can prove it
--@[simp, norm_cast]
theorem 
coe_add: βˆ€ (m n : β„•), ↑(m + n) = ↑m + ↑n
coe_add (
m: β„•
m 
n: β„•
n : 
β„•: Type
β„•) : ↑(
m: β„•
m + 
n: β„•
n) = (
m: β„•
m + 
n: β„•
n : 
β„•βˆž: Type
β„•βˆž) :=
  
rfl: βˆ€ {Ξ± : Sort ?u.11897} {a : Ξ±}, a = a
rfl
#align enat.coe_add 
ENat.coe_add: βˆ€ (m n : β„•), ↑(m + n) = ↑m + ↑n
ENat.coe_add

@[simp, norm_cast]
theorem 
coe_sub: βˆ€ (m n : β„•), ↑(m - n) = ↑m - ↑n
coe_sub (
m: β„•
m 
n: β„•
n : 
β„•: Type
β„•) : ↑(
m: β„•
m - 
n: β„•
n) = (
m: β„•
m - 
n: β„•
n : 
β„•βˆž: Type
β„•βˆž) :=
  
rfl: βˆ€ {Ξ± : Sort ?u.12203} {a : Ξ±}, a = a
rfl
#align enat.coe_sub 
ENat.coe_sub: βˆ€ (m n : β„•), ↑(m - n) = ↑m - ↑n
ENat.coe_sub

--Porting note: `simp` and `norm_cast` can prove it
--@[simp, norm_cast]
theorem 
coe_mul: βˆ€ (m n : β„•), ↑(m * n) = ↑m * ↑n
coe_mul (
m: β„•
m 
n: β„•
n : 
β„•: Type
β„•) : ↑(
m: β„•
m * 
n: β„•
n) = (
m: β„•
m * 
n: β„•
n : 
β„•βˆž: Type
β„•βˆž) :=
  
WithTop.coe_mul: βˆ€ {Ξ± : Type ?u.12613} [inst : DecidableEq Ξ±] [inst_1 : MulZeroClass Ξ±] {a b : Ξ±}, ↑(a * b) = ↑a * ↑b
WithTop.coe_mul
#align enat.coe_mul 
ENat.coe_mul: βˆ€ (m n : β„•), ↑(m * n) = ↑m * ↑n
ENat.coe_mul

instance 
canLift: CanLift β„•βˆž β„• Nat.cast fun n => n β‰  ⊀
canLift : 
CanLift: (Ξ± : Sort ?u.12913) β†’ (Ξ² : Sort ?u.12912) β†’ outParam (Ξ² β†’ Ξ±) β†’ outParam (Ξ± β†’ Prop) β†’ Type
CanLift 
β„•βˆž: Type
β„•βˆž 
β„•: Type
β„• 
(↑): β„• β†’ β„•βˆž
(↑) fun 
n: ?m.12960
n => 
n: ?m.12960
n β‰  
⊀: ?m.12965
⊀ :=
  
WithTop.canLift: {Ξ± : Type ?u.12993} β†’ CanLift (WithTop Ξ±) Ξ± WithTop.some fun r => r β‰  ⊀
WithTop.canLift
#align enat.can_lift 
ENat.canLift: CanLift β„•βˆž β„• Nat.cast fun n => n β‰  ⊀
ENat.canLift

/-- Conversion of `β„•βˆž` to `β„•` sending `∞` to `0`. -/
def 
toNat: β„•βˆž β†’*β‚€ β„•
toNat : 
MonoidWithZeroHom: (M : Type ?u.13081) β†’
  (N : Type ?u.13080) β†’ [inst : MulZeroOneClass M] β†’ [inst : MulZeroOneClass N] β†’ Type (max?u.13081?u.13080)
MonoidWithZeroHom 
β„•βˆž: Type
β„•βˆž 
β„•: Type
β„•
    where
  toFun := 
WithTop.untop': {Ξ± : Type ?u.13289} β†’ Ξ± β†’ WithTop Ξ± β†’ Ξ±
WithTop.untop' 
0: ?m.13295
0
  map_one' := 
rfl: βˆ€ {Ξ± : Sort ?u.13327} {a : Ξ±}, a = a
rfl
  map_zero' := 
rfl: βˆ€ {Ξ± : Sort ?u.13308} {a : Ξ±}, a = a
rfl
  map_mul' := 
WithTop.untop'_zero_mul: βˆ€ {Ξ± : Type ?u.13338} [inst : DecidableEq Ξ±] [inst_1 : MulZeroClass Ξ±] (a b : WithTop Ξ±),
  WithTop.untop' 0 (a * b) = WithTop.untop' 0 a * WithTop.untop' 0 b
WithTop.untop'_zero_mul
#align enat.to_nat 
ENat.toNat: β„•βˆž β†’*β‚€ β„•
ENat.toNat

@[simp]
theorem 
toNat_coe: βˆ€ (n : β„•), ↑toNat ↑n = n
toNat_coe (
n: β„•
n : 
β„•: Type
β„•) : 
toNat: β„•βˆž β†’*β‚€ β„•
toNat 
n: β„•
n = 
n: β„•
n :=
  
rfl: βˆ€ {Ξ± : Sort ?u.14928} {a : Ξ±}, a = a
rfl
#align enat.to_nat_coe 
ENat.toNat_coe: βˆ€ (n : β„•), ↑toNat ↑n = n
ENat.toNat_coe

@[simp]
theorem 
toNat_top: ↑toNat ⊀ = 0
toNat_top : 
toNat: β„•βˆž β†’*β‚€ β„•
toNat 
⊀: ?m.15536
⊀ = 
0: ?m.15562
0 :=
  
rfl: βˆ€ {Ξ± : Sort ?u.15587} {a : Ξ±}, a = a
rfl
#align enat.to_nat_top 
ENat.toNat_top: ↑toNat ⊀ = 0
ENat.toNat_top

--Porting note: new definition copied from `WithTop`
/-- Recursor for `ENat` using the preferred forms `⊀` and `↑a`. -/
@[elab_as_elim]
def 
recTopCoe: {C : β„•βˆž β†’ Sort ?u.15629} β†’ C ⊀ β†’ ((a : β„•) β†’ C ↑a) β†’ (n : β„•βˆž) β†’ C n
recTopCoe {
C: β„•βˆž β†’ Sort ?u.15629
C : 
β„•βˆž: Type
β„•βˆž β†’ 
Sort _: Type ?u.15629
Sort
Sort _: Type ?u.15629
 _} (
h₁: C ⊀
h₁ : 
C: β„•βˆž β†’ Sort ?u.15629
C 
⊀: ?m.15633
⊀) (
hβ‚‚: (a : β„•) β†’ C ↑a
hβ‚‚ : βˆ€ 
a: β„•
a : 
β„•: Type
β„•, 
C: β„•βˆž β†’ Sort ?u.15629
C 
a: β„•
a) : βˆ€ 
n: β„•βˆž
n : 
β„•βˆž: Type
β„•βˆž, 
C: β„•βˆž β†’ Sort ?u.15629
C 
n: β„•βˆž
n
| 
none: {Ξ± : Type ?u.15720} β†’ Option Ξ±
none => 
h₁: C ⊀
h₁
| 
Option.some: {Ξ± : Type ?u.15731} β†’ Ξ± β†’ Option Ξ±
Option.some 
a: β„•
a => 
hβ‚‚: (a : β„•) β†’ C ↑a
hβ‚‚ 
a: β„•
a

--Porting note: new theorem copied from `WithTop`
@[simp]
theorem 
recTopCoe_top: βˆ€ {C : β„•βˆž β†’ Sort u_1} (d : C ⊀) (f : (a : β„•) β†’ C ↑a), recTopCoe d f ⊀ = d
recTopCoe_top {
C: β„•βˆž β†’ Sort ?u.15951
C : 
β„•βˆž: Type
β„•βˆž β†’ 
Sort _: Type ?u.15951
Sort
Sort _: Type ?u.15951
 _} (
d: C ⊀
d : 
C: β„•βˆž β†’ Sort ?u.15951
C 
⊀: ?m.15955
⊀) (
f: (a : β„•) β†’ C ↑a
f : βˆ€ 
a: β„•
a : 
β„•: Type
β„•, 
C: β„•βˆž β†’ Sort ?u.15951
C 
a: β„•
a) :
    @
recTopCoe: {C : β„•βˆž β†’ Sort ?u.16032} β†’ C ⊀ β†’ ((a : β„•) β†’ C ↑a) β†’ (n : β„•βˆž) β†’ C n
recTopCoe 
C: β„•βˆž β†’ Sort ?u.15951
C 
d: C ⊀
d 
f: (a : β„•) β†’ C ↑a
f 
⊀: ?m.16039
⊀ = 
d: C ⊀
d :=
  
rfl: βˆ€ {Ξ± : Sort ?u.16061} {a : Ξ±}, a = a
rfl

--Porting note: new theorem copied from `WithTop`
@[simp]
theorem 
recTopCoe_coe: βˆ€ {C : β„•βˆž β†’ Sort u_1} (d : C ⊀) (f : (a : β„•) β†’ C ↑a) (x : β„•), recTopCoe d f ↑x = f x
recTopCoe_coe {
C: β„•βˆž β†’ Sort ?u.16101
C : 
β„•βˆž: Type
β„•βˆž β†’ 
Sort _: Type ?u.16101
Sort
Sort _: Type ?u.16101
 _} (
d: C ⊀
d : 
C: β„•βˆž β†’ Sort ?u.16101
C 
⊀: ?m.16105
⊀) (
f: (a : β„•) β†’ C ↑a
f : βˆ€ 
a: β„•
a : 
β„•: Type
β„•, 
C: β„•βˆž β†’ Sort ?u.16101
C 
a: β„•
a) (
x: β„•
x : 
β„•: Type
β„•) :
    @
recTopCoe: {C : β„•βˆž β†’ Sort ?u.16184} β†’ C ⊀ β†’ ((a : β„•) β†’ C ↑a) β†’ (n : β„•βˆž) β†’ C n
recTopCoe 
C: β„•βˆž β†’ Sort ?u.16101
C 
d: C ⊀
d 
f: (a : β„•) β†’ C ↑a
f ↑
x: β„•
x = 
f: (a : β„•) β†’ C ↑a
f 
x: β„•
x :=
  
rfl: βˆ€ {Ξ± : Sort ?u.16229} {a : Ξ±}, a = a
rfl

--Porting note: new theorem copied from `WithTop`
@[simp]
theorem 
top_ne_coe: βˆ€ (a : β„•), ⊀ β‰  ↑a
top_ne_coe (
a: β„•
a : 
β„•: Type
β„•) : 
⊀: ?m.16277
⊀ β‰  (
a: β„•
a : 
β„•βˆž: Type
β„•βˆž) :=
  
fun.: ⊀ = ↑a β†’ False
fun
fun.: ⊀ = ↑a β†’ False
.

--Porting note: new theorem copied from `WithTop`
@[simp]
theorem 
coe_ne_top: βˆ€ (a : β„•), ↑a β‰  ⊀
coe_ne_top (
a: β„•
a : 
β„•: Type
β„•) : (
a: β„•
a : 
β„•βˆž: Type
β„•βˆž) β‰  
⊀: ?m.16518
⊀ :=
  
fun.: ↑a = ⊀ β†’ False
fun
fun.: ↑a = ⊀ β†’ False
.

--Porting note: new theorem copied from `WithTop`
@[simp]
theorem 
top_sub_coe: βˆ€ (a : β„•), ⊀ - ↑a = ⊀
top_sub_coe (
a: β„•
a : 
β„•: Type
β„•) : (
⊀: ?m.16658
⊀ : 
β„•βˆž: Type
β„•βˆž) - 
a: β„•
a = 
⊀: ?m.16684
⊀ :=
  
WithTop.top_sub_coe: βˆ€ {Ξ± : Type ?u.16835} [inst : Sub Ξ±] [inst_1 : Zero Ξ±] {a : Ξ±}, ⊀ - ↑a = ⊀
WithTop.top_sub_coe

--Porting note: new theorem copied from `WithTop`
theorem 
sub_top: βˆ€ (a : β„•βˆž), a - ⊀ = 0
sub_top (
a: β„•βˆž
a : 
β„•βˆž: Type
β„•βˆž) : 
a: β„•βˆž
a - 
⊀: ?m.16967
⊀ = 
0: ?m.16999
0 :=
  
WithTop.sub_top: βˆ€ {Ξ± : Type ?u.17101} [inst : Sub Ξ±] [inst_1 : Zero Ξ±] {a : WithTop Ξ±}, a - ⊀ = 0
WithTop.sub_top

@[simp]
theorem 
coe_toNat_eq_self: βˆ€ {n : β„•βˆž}, ↑(↑toNat n) = n ↔ n β‰  ⊀
coe_toNat_eq_self : 
ENat.toNat: β„•βˆž β†’*β‚€ β„•
ENat.toNat (
n: β„•βˆž
n : 
β„•βˆž: Type
β„•βˆž) = 
n: β„•βˆž
n ↔ 
n: β„•βˆž
n β‰  
⊀: ?m.19270
⊀ :=
  
ENat.recTopCoe: βˆ€ {C : β„•βˆž β†’ Sort ?u.19296}, C ⊀ β†’ (βˆ€ (a : β„•), C ↑a) β†’ βˆ€ (n : β„•βˆž), C n
ENat.recTopCoe (
Goals accomplished! πŸ™
m, n: β„•βˆž

↑(↑toNat ⊀) = ⊀ ↔ ⊀ β‰  ⊀
Goals accomplished! πŸ™
) (fun 
_: ?m.19318
_ => 
Goals accomplished! πŸ™
m, n: β„•βˆž

x✝: β„•

↑(↑toNat ↑x✝) = ↑x✝ ↔ ↑x✝ β‰  ⊀
Goals accomplished! πŸ™
) 
n: β„•βˆž
n
#align enat.coe_to_nat_eq_self 
ENat.coe_toNat_eq_self: βˆ€ {n : β„•βˆž}, ↑(↑toNat n) = n ↔ n β‰  ⊀
ENat.coe_toNat_eq_self

alias 
coe_toNat_eq_self: βˆ€ {n : β„•βˆž}, ↑(↑toNat n) = n ↔ n β‰  ⊀
coe_toNat_eq_self ↔ _ 
coe_toNat: βˆ€ {n : β„•βˆž}, n β‰  ⊀ β†’ ↑(↑toNat n) = n
coe_toNat
#align enat.coe_to_nat 
ENat.coe_toNat: βˆ€ {n : β„•βˆž}, n β‰  ⊀ β†’ ↑(↑toNat n) = n
ENat.coe_toNat

theorem 
coe_toNat_le_self: βˆ€ (n : β„•βˆž), ↑(↑toNat n) ≀ n
coe_toNat_le_self (
n: β„•βˆž
n : 
β„•βˆž: Type
β„•βˆž) : ↑(
toNat: β„•βˆž β†’*β‚€ β„•
toNat 
n: β„•βˆž
n) ≀ 
n: β„•βˆž
n :=
  
ENat.recTopCoe: βˆ€ {C : β„•βˆž β†’ Sort ?u.20711}, C ⊀ β†’ (βˆ€ (a : β„•), C ↑a) β†’ βˆ€ (n : β„•βˆž), C n
ENat.recTopCoe 
le_top: βˆ€ {Ξ± : Type ?u.20733} [inst : LE Ξ±] [inst_1 : OrderTop Ξ±] {a : Ξ±}, a ≀ ⊀
le_top (fun 
_: ?m.20789
_ => 
le_rfl: βˆ€ {Ξ± : Type ?u.20791} [inst : Preorder Ξ±] {a : Ξ±}, a ≀ a
le_rfl) 
n: β„•βˆž
n
#align enat.coe_to_nat_le_self 
ENat.coe_toNat_le_self: βˆ€ (n : β„•βˆž), ↑(↑toNat n) ≀ n
ENat.coe_toNat_le_self

theorem 
toNat_add: βˆ€ {m n : β„•βˆž}, m β‰  ⊀ β†’ n β‰  ⊀ β†’ ↑toNat (m + n) = ↑toNat m + ↑toNat n
toNat_add {
m: β„•βˆž
m 
n: β„•βˆž
n : 
β„•βˆž: Type
β„•βˆž} (
hm: m β‰  ⊀
hm : 
m: β„•βˆž
m β‰  
⊀: ?m.20977
⊀) (
hn: n β‰  ⊀
hn : 
n: β„•βˆž
n β‰  
⊀: ?m.21007
⊀) : 
toNat: β„•βˆž β†’*β‚€ β„•
toNat (
m: β„•βˆž
m + 
n: β„•βˆž
n) = 
toNat: β„•βˆž β†’*β‚€ β„•
toNat 
m: β„•βˆž
m + 
toNat: β„•βˆž β†’*β‚€ β„•
toNat 
n: β„•βˆž
n := 
Goals accomplished! πŸ™
m✝, n✝, m, n: β„•βˆž

hm: m β‰  ⊀

hn: n β‰  ⊀

↑toNat (m + n) = ↑toNat m + ↑toNat n
m✝, n✝, n: β„•βˆž

hn: n β‰  ⊀

m: β„•

intro
↑toNat (↑m + n) = ↑toNat ↑m + ↑toNat n
m✝, n✝, m, n: β„•βˆž

hm: m β‰  ⊀

hn: n β‰  ⊀

↑toNat (m + n) = ↑toNat m + ↑toNat n
m✝, n✝: β„•βˆž

m, n: β„•

intro.intro
↑toNat (↑m + ↑n) = ↑toNat ↑m + ↑toNat ↑n
m✝, n✝, m, n: β„•βˆž

hm: m β‰  ⊀

hn: n β‰  ⊀

↑toNat (m + n) = ↑toNat m + ↑toNat n
Goals accomplished! πŸ™

#align enat.to_nat_add 
ENat.toNat_add: βˆ€ {m n : β„•βˆž}, m β‰  ⊀ β†’ n β‰  ⊀ β†’ ↑toNat (m + n) = ↑toNat m + ↑toNat n
ENat.toNat_add

theorem 
toNat_sub: βˆ€ {n : β„•βˆž}, n β‰  ⊀ β†’ βˆ€ (m : β„•βˆž), ↑toNat (m - n) = ↑toNat m - ↑toNat n
toNat_sub {
n: β„•βˆž
n : 
β„•βˆž: Type
β„•βˆž} (
hn: n β‰  ⊀
hn : 
n: β„•βˆž
n β‰  
⊀: ?m.23337
⊀) (
m: β„•βˆž
m : 
β„•βˆž: Type
β„•βˆž) : 
toNat: β„•βˆž β†’*β‚€ β„•
toNat (
m: β„•βˆž
m - 
n: β„•βˆž
n) = 
toNat: β„•βˆž β†’*β‚€ β„•
toNat 
m: β„•βˆž
m - 
toNat: β„•βˆž β†’*β‚€ β„•
toNat 
n: β„•βˆž
n := 
Goals accomplished! πŸ™
m✝, n✝, n: β„•βˆž

hn: n β‰  ⊀

m: β„•βˆž

↑toNat (m - n) = ↑toNat m - ↑toNat n
m✝, n✝, m: β„•βˆž

n: β„•

intro
↑toNat (m - ↑n) = ↑toNat m - ↑toNat ↑n
m✝, n✝, n: β„•βˆž

hn: n β‰  ⊀

m: β„•βˆž

↑toNat (m - n) = ↑toNat m - ↑toNat n
m, n✝: β„•βˆž

n: β„•

intro.h₁
↑toNat (⊀ - ↑n) = ↑toNat ⊀ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
m✝, n✝, n: β„•βˆž

hn: n β‰  ⊀

m: β„•βˆž

↑toNat (m - n) = ↑toNat m - ↑toNat n
m, n✝: β„•βˆž

n: β„•

intro.h₁
↑toNat (⊀ - ↑n) = ↑toNat ⊀ - ↑toNat ↑n
m, n✝: β„•βˆž

n: β„•

intro.h₁
↑toNat (⊀ - ↑n) = ↑toNat ⊀ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
m, n✝: β„•βˆž

n: β„•

intro.h₁
↑toNat (⊀ - ↑n) = ↑toNat ⊀ - ↑toNat ↑n
m, n✝: β„•βˆž

n: β„•

intro.h₁
↑toNat ⊀ = ↑toNat ⊀ - ↑toNat ↑n
m, n✝: β„•βˆž

n: β„•

intro.h₁
↑toNat (⊀ - ↑n) = ↑toNat ⊀ - ↑toNat ↑n
m, n✝: β„•βˆž

n: β„•

intro.h₁
0 = 0 - ↑toNat ↑n
m, n✝: β„•βˆž

n: β„•

intro.h₁
↑toNat (⊀ - ↑n) = ↑toNat ⊀ - ↑toNat ↑n
m, n✝: β„•βˆž

n: β„•

intro.h₁
0 = 0
Goals accomplished! πŸ™
m✝, n✝, n: β„•βˆž

hn: n β‰  ⊀

m: β„•βˆž

↑toNat (m - n) = ↑toNat m - ↑toNat n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
↑toNat ↑(a✝ - n) = ↑toNat ↑a✝ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
a✝ - n = ↑toNat ↑a✝ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
a✝ - n = a✝ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
↑toNat (↑a✝ - ↑n) = ↑toNat ↑a✝ - ↑toNat ↑n
m, n✝: β„•βˆž

n, a✝: β„•

intro.hβ‚‚
a✝ - n = a✝ - n
Goals accomplished! πŸ™

#align enat.to_nat_sub 
ENat.toNat_sub: βˆ€ {n : β„•βˆž}, n β‰  ⊀ β†’ βˆ€ (m : β„•βˆž), ↑toNat (m - n) = ↑toNat m - ↑toNat n
ENat.toNat_sub

theorem 
toNat_eq_iff: βˆ€ {m : β„•βˆž} {n : β„•}, n β‰  0 β†’ (↑toNat m = n ↔ m = ↑n)
toNat_eq_iff {
m: β„•βˆž
m : 
β„•βˆž: Type
β„•βˆž} {
n: β„•
n : 
β„•: Type
β„•} (
hn: n β‰  0
hn : 
n: β„•
n β‰  
0: ?m.25456
0) : 
toNat: β„•βˆž β†’*β‚€ β„•
toNat 
m: β„•βˆž
m = 
n: β„•
n ↔ 
m: β„•βˆž
m = 
n: β„•
n := 
Goals accomplished! πŸ™
m✝, n✝, m: β„•βˆž

n: β„•

hn: n β‰  0

↑toNat m = n ↔ m = ↑n
m, n✝: β„•βˆž

n: β„•

hn: n β‰  0

h₁
↑toNat ⊀ = n ↔ ⊀ = ↑n
m, n✝: β„•βˆž

n: β„•

hn: n β‰  0

a✝: β„•

hβ‚‚
↑toNat ↑a✝ = n ↔ ↑a✝ = ↑n
m✝, n✝, m: β„•βˆž

n: β„•

hn: n β‰  0

↑toNat m = n ↔ m = ↑n
m, n✝: β„•βˆž

n: β„•

hn: n β‰  0

h₁
↑toNat ⊀ = n ↔ ⊀ = ↑n
m, n✝: β„•βˆž

n: β„•

hn: n β‰  0

a✝: β„•

hβ‚‚
↑toNat ↑a✝ = n ↔ ↑a✝ = ↑n
m✝, n✝, m: β„•βˆž

n: β„•

hn: n β‰  0

↑toNat m = n ↔ m = ↑n
Goals accomplished! πŸ™

#align enat.to_nat_eq_iff 
ENat.toNat_eq_iff: βˆ€ {m : β„•βˆž} {n : β„•}, n β‰  0 β†’ (↑toNat m = n ↔ m = ↑n)
ENat.toNat_eq_iff

@[simp]
theorem 
succ_def: βˆ€ (m : β„•βˆž), Order.succ m = m + 1
succ_def (
m: β„•βˆž
m : 
β„•βˆž: Type
β„•βˆž) : 
Order.succ: {Ξ± : Type ?u.26948} β†’ [inst : Preorder Ξ±] β†’ [inst : SuccOrder Ξ±] β†’ Ξ± β†’ Ξ±
Order.succ 
m: β„•βˆž
m = 
m: β„•βˆž
m + 
1: ?m.27122
1 := 
Goals accomplished! πŸ™
m✝, n, m: β„•βˆž

Order.succ m = m + 1
m, n: β„•βˆž

none
Order.succ none = none + 1
m, n: β„•βˆž

val✝: β„•

some
Order.succ (some val✝) = some val✝ + 1
m✝, n, m: β„•βˆž

Order.succ m = m + 1
m, n: β„•βˆž

none
Order.succ none = none + 1
m, n: β„•βˆž

val✝: β„•

some
Order.succ (some val✝) = some val✝ + 1
m✝, n, m: β„•βˆž

Order.succ m = m + 1
Goals accomplished! πŸ™

#align enat.succ_def 
ENat.succ_def: βˆ€ (m : β„•βˆž), Order.succ m = m + 1
ENat.succ_def

theorem 
add_one_le_of_lt: m < n β†’ m + 1 ≀ n
add_one_le_of_lt (
h: m < n
h : 
m: β„•βˆž
m < 
n: β„•βˆž
n) : 
m: β„•βˆž
m + 
1: ?m.27828
1 ≀ 
n: β„•βˆž
n :=
  
m: β„•βˆž
m.
succ_def: βˆ€ (m : β„•βˆž), Order.succ m = m + 1
succ_def β–Έ 
Order.succ_le_of_lt: βˆ€ {Ξ± : Type ?u.28366} [inst : Preorder Ξ±] [inst_1 : SuccOrder Ξ±] {a b : Ξ±}, a < b β†’ Order.succ a ≀ b
Order.succ_le_of_lt 
h: m < n
h
#align enat.add_one_le_of_lt 
ENat.add_one_le_of_lt: βˆ€ {m n : β„•βˆž}, m < n β†’ m + 1 ≀ n
ENat.add_one_le_of_lt

theorem 
add_one_le_iff: m β‰  ⊀ β†’ (m + 1 ≀ n ↔ m < n)
add_one_le_iff (
hm: m β‰  ⊀
hm : 
m: β„•βˆž
m β‰  
⊀: ?m.28556
⊀) : 
m: β„•βˆž
m + 
1: ?m.28588
1 ≀ 
n: β„•βˆž
n ↔ 
m: β„•βˆž
m < 
n: β„•βˆž
n :=
  
m: β„•βˆž
m.
succ_def: βˆ€ (m : β„•βˆž), Order.succ m = m + 1
succ_def β–Έ (
Order.succ_le_iff_of_not_isMax: βˆ€ {Ξ± : Type ?u.29296} [inst : Preorder Ξ±] [inst_1 : SuccOrder Ξ±] {a b : Ξ±}, Β¬IsMax a β†’ (Order.succ a ≀ b ↔ a < b)
Order.succ_le_iff_of_not_isMax <| 
Goals accomplished! πŸ™
m, n: β„•βˆž

hm: m β‰  ⊀

Β¬IsMax m
m, n: β„•βˆž

hm: m β‰  ⊀

Β¬IsMax m
m, n: β„•βˆž

hm: m β‰  ⊀

¬m = ⊀
m, n: β„•βˆž

hm: m β‰  ⊀

¬m = ⊀
)
#align enat.add_one_le_iff 
ENat.add_one_le_iff: βˆ€ {m n : β„•βˆž}, m β‰  ⊀ β†’ (m + 1 ≀ n ↔ m < n)
ENat.add_one_le_iff

theorem 
one_le_iff_pos: 1 ≀ n ↔ 0 < n
one_le_iff_pos : 
1: ?m.29740
1 ≀ 
n: β„•βˆž
n ↔ 
0: ?m.29957
0 < 
n: β„•βˆž
n :=
  
add_one_le_iff: βˆ€ {m n : β„•βˆž}, m β‰  ⊀ β†’ (m + 1 ≀ n ↔ m < n)
add_one_le_iff 
WithTop.zero_ne_top: βˆ€ {Ξ± : Type ?u.30242} [inst : Zero Ξ±], 0 β‰  ⊀
WithTop.zero_ne_top
#align enat.one_le_iff_pos 
ENat.one_le_iff_pos: βˆ€ {n : β„•βˆž}, 1 ≀ n ↔ 0 < n
ENat.one_le_iff_pos

theorem 
one_le_iff_ne_zero: 1 ≀ n ↔ n β‰  0
one_le_iff_ne_zero : 
1: ?m.30332
1 ≀ 
n: β„•βˆž
n ↔ 
n: β„•βˆž
n β‰  
0: ?m.30550
0 :=
  
one_le_iff_pos: βˆ€ {n : β„•βˆž}, 1 ≀ n ↔ 0 < n
one_le_iff_pos.
trans: βˆ€ {a b c : Prop}, (a ↔ b) β†’ (b ↔ c) β†’ (a ↔ c)
trans 
pos_iff_ne_zero: βˆ€ {Ξ± : Type ?u.30587} [inst : CanonicallyOrderedAddMonoid Ξ±] {a : Ξ±}, 0 < a ↔ a β‰  0
pos_iff_ne_zero
#align enat.one_le_iff_ne_zero 
ENat.one_le_iff_ne_zero: βˆ€ {n : β„•βˆž}, 1 ≀ n ↔ n β‰  0
ENat.one_le_iff_ne_zero

theorem 
le_of_lt_add_one: m < n + 1 β†’ m ≀ n
le_of_lt_add_one (
h: m < n + 1
h : 
m: β„•βˆž
m < 
n: β„•βˆž
n + 
1: ?m.30650
1) : 
m: β„•βˆž
m ≀ 
n: β„•βˆž
n :=
  
Order.le_of_lt_succ: βˆ€ {Ξ± : Type ?u.31355} [inst : Preorder Ξ±] [inst_1 : SuccOrder Ξ±] {a b : Ξ±}, a < Order.succ b β†’ a ≀ b
Order.le_of_lt_succ <| 
n: β„•βˆž
n.
succ_def: βˆ€ (m : β„•βˆž), Order.succ m = m + 1
succ_def.
symm: βˆ€ {Ξ± : Sort ?u.31522} {a b : Ξ±}, a = b β†’ b = a
symm β–Έ 
h: m < n + 1
h
#align enat.le_of_lt_add_one 
ENat.le_of_lt_add_one: βˆ€ {m n : β„•βˆž}, m < n + 1 β†’ m ≀ n
ENat.le_of_lt_add_one

@[elab_as_elim]
theorem 
nat_induction: βˆ€ {P : β„•βˆž β†’ Prop} (a : β„•βˆž), P 0 β†’ (βˆ€ (n : β„•), P ↑n β†’ P ↑(Nat.succ n)) β†’ ((βˆ€ (n : β„•), P ↑n) β†’ P ⊀) β†’ P a
nat_induction {
P: β„•βˆž β†’ Prop
P : 
β„•βˆž: Type
β„•βˆž β†’ 
Prop: Type
Prop} (
a: β„•βˆž
a : 
β„•βˆž: Type
β„•βˆž) (
h0: P 0
h0 : 
P: β„•βˆž β†’ Prop
P 
0: ?m.31556
0) (
hsuc: βˆ€ (n : β„•), P ↑n β†’ P ↑(Nat.succ n)
hsuc : βˆ€ 
n: β„•
n : 
β„•: Type
β„•, 
P: β„•βˆž β†’ Prop
P 
n: β„•
n β†’ 
P: β„•βˆž β†’ Prop
P 
n: β„•
n.
succ: β„• β†’ β„•
succ)
    (
htop: (βˆ€ (n : β„•), P ↑n) β†’ P ⊀
htop : (βˆ€ 
n: β„•
n : 
β„•: Type
β„•, 
P: β„•βˆž β†’ Prop
P 
n: β„•
n) β†’ 
P: β„•βˆž β†’ Prop
P 
⊀: ?m.31707
⊀) : 
P: β„•βˆž β†’ Prop
P 
a: β„•βˆž
a := 
Goals accomplished! πŸ™
m, n: β„•βˆž

P: β„•βˆž β†’ Prop

a: β„•βˆž

h0: P 0

hsuc: βˆ€ (n : β„•), P ↑n β†’ P ↑(Nat.succ n)

htop: (βˆ€ (n : β„•), P ↑n) β†’ P ⊀

P a
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
m, n: β„•βˆž

P: β„•βˆž β†’ Prop

a: β„•βˆž

h0: P 0

hsuc: βˆ€ (n : β„•), P ↑n β†’ P ↑(Nat.succ n)

htop: (βˆ€ (n : β„•), P ↑n) β†’ P ⊀

P a
m, n: β„•βˆž

P: β„•βˆž β†’ Prop

h0: P 0

hsuc: βˆ€ (n : β„•), P ↑n β†’ P ↑(Nat.succ n)

htop: (βˆ€ (n : β„•), P ↑n) β†’ P ⊀

A: βˆ€ (n : β„•), P ↑n

none
P 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

val✝: β„•

some
P (some val✝)
m, n: β„•βˆž

P: β„•βˆž β†’ Prop

a: β„•βˆž

h0: P 0

hsuc: βˆ€ (n : β„•), P ↑n β†’ P ↑(Nat.succ n)

htop: (βˆ€ (n : β„•), P ↑n) β†’ P ⊀

P a
m, n: β„•βˆž

P: β„•βˆž β†’ Prop

h0: P 0

hsuc: βˆ€ (n : β„•), P ↑n β†’ P ↑(Nat.succ n)

htop: (βˆ€ (n : β„•), P ↑n) β†’ P ⊀

A: βˆ€ (n : β„•), P ↑n

none
P 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

none
P 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

val✝: β„•

some
P (some val✝)
Goals accomplished! πŸ™
m, n: β„•βˆž

P: β„•βˆž β†’ Prop

a: β„•βˆž

h0: P 0

hsuc: βˆ€ (n : β„•), P ↑n β†’ P ↑(Nat.succ n)

htop: (βˆ€ (n : β„•), P ↑n) β†’ P ⊀

P a
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✝: β„•

some
P (some val✝)
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✝: β„•

some
P (some val✝)
Goals accomplished! πŸ™

#align enat.nat_induction 
ENat.nat_induction: βˆ€ {P : β„•βˆž β†’ Prop} (a : β„•βˆž), P 0 β†’ (βˆ€ (n : β„•), P ↑n β†’ P ↑(Nat.succ n)) β†’ ((βˆ€ (n : β„•), P ↑n) β†’ P ⊀) β†’ P a
ENat.nat_induction

end ENat