case a
x : PartENat
hx : Decidable x.Dom
hy : Decidable ⊤.Dom
⊢ toWithTop x ≤ toWithTop ⊤ ↔ x ≤ ⊤

case a
x : PartENat
hx : Decidable x.Dom
n✝ : ℕ
hy : Decidable (↑n✝).Dom
⊢ toWithTop x ≤ toWithTop ↑n✝ ↔ x ≤ ↑n✝
x y : PartENat
hx : Decidable x.Dom
hy : Decidable y.Dom
⊢ toWithTop x ≤ toWithTop y ↔ x ≤ y
induction y using PartENat.casesOn generalizing hy
case a.a
n✝ : ℕ
hy : Decidable (↑n✝).Dom
hx : Decidable ⊤.Dom
⊢ toWithTop ⊤ ≤ toWithTop ↑n✝ ↔ ⊤ ≤ ↑n✝

case a.a
n✝¹ : ℕ
hy : Decidable (↑n✝¹).Dom
n✝ : ℕ
hx : Decidable (↑n✝).Dom
⊢ toWithTop ↑n✝ ≤ toWithTop ↑n✝¹ ↔ ↑n✝ ≤ ↑n✝¹
case a
x : PartENat
hx : Decidable x.Dom
n✝ : ℕ
hy : Decidable (↑n✝).Dom
⊢ toWithTop x ≤ toWithTop ↑n✝ ↔ x ≤ ↑n✝
induction x using PartENat.casesOn generalizing hx
no goals
case a
x : PartENat
hx : Decidable x.Dom
hy : Decidable ⊤.Dom
⊢ toWithTop x ≤ toWithTop ⊤ ↔ x ≤ ⊤
simp
no goals
case a.a
n✝ : ℕ
hy : Decidable (↑n✝).Dom
hx : Decidable ⊤.Dom
⊢ toWithTop ⊤ ≤ toWithTop ↑n✝ ↔ ⊤ ≤ ↑n✝
simp
no goals
case a.a
n✝¹ : ℕ
hy : Decidable (↑n✝¹).Dom
n✝ : ℕ
hx : Decidable (↑n✝).Dom
⊢ toWithTop ↑n✝ ≤ toWithTop ↑n✝¹ ↔ ↑n✝ ≤ ↑n✝¹
simp