[GOAL]
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id r with rs
[GOAL]
case nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id l with ls ll lx lr
[GOAL]
case nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact ι x
[GOAL]
case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id ll with lls
[GOAL]
case nil.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' lr with _ _ lrx
[GOAL]
case nil.node.nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
⊢ Ordnode α
[PROOFSTEP]
exact node 2 l x nil
[GOAL]
case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
size✝ : ℕ
l✝ : Ordnode α
lrx : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node 3 (ι lx) lrx ι x
[GOAL]
case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id lr with lrs lrl lrx lrr
[GOAL]
case nil.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node 3 ll lx ι x
[GOAL]
case nil.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact
  if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
  else node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx (node (size lrr + 1) lrr x nil)
[GOAL]
case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id l with ls ll lx lr
[GOAL]
case node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node (rs + 1) nil x r
[GOAL]
case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
refine' if ls > delta * rs then _ else node (ls + rs + 1) l x r
[GOAL]
case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id ll with lls
[GOAL]
case node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact nil
[GOAL]
case node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id lr with lrs lrl lrx lrr
[GOAL]
case node.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact nil
[GOAL]
case node.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact
  if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (rs + lrs + 1) lr x r)
  else node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx (node (size lrr + rs + 1) lrr x r)
[GOAL]
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id l with ls
[GOAL]
case nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id r with rs rl rx rr
[GOAL]
case nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact ι x
[GOAL]
case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id rr with rrs
[GOAL]
case nil.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' rl with _ _ rlx
[GOAL]
case nil.node.nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node 2 nil x r
[GOAL]
case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rx : α
rr : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
rlx : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node 3 (ι x) rlx ι rx
[GOAL]
case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id rl with rls rll rlx rlr
[GOAL]
case nil.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node 3 (ι x) rx rr
[GOAL]
case nil.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact
  if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
  else node (rs + 1) (node (size rll + 1) nil x rll) rlx (node (size rlr + rrs + 1) rlr rx rr)
[GOAL]
case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id r with rs rl rx rr
[GOAL]
case node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node (ls + 1) l x nil
[GOAL]
case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
refine' if rs > delta * ls then _ else node (ls + rs + 1) l x r
[GOAL]
case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id rr with rrs
[GOAL]
case node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact nil
[GOAL]
case node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id rl with rls rll rlx rlr
[GOAL]
case node.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact nil
[GOAL]
case node.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l✝¹ : Ordnode α
x✝¹ : α
r✝¹ : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact
  if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
  else node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx (node (size rlr + rrs + 1) rlr rx rr)
[GOAL]
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id l with ls ll lx lr
[GOAL]
case nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id r with rs rl rx rr
[GOAL]
case nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact ι x
[GOAL]
case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id rl with rls rll rlx rlr
[GOAL]
case nil.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases id rr
[GOAL]
case nil.node.nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node 2 nil x r
[GOAL]
case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node 3 (ι x) rx rr
[GOAL]
case nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id rr with rrs
[GOAL]
case nil.node.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node 3 (ι x) rlx ι rx
[GOAL]
case nil.node.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact
  if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
  else node (rs + 1) (node (size rll + 1) nil x rll) rlx (node (size rlr + rrs + 1) rlr rx rr)
[GOAL]
case node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id r with rs rl rx rr
[GOAL]
case node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id ll with lls
[GOAL]
case node.nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' lr with _ _ lrx
[GOAL]
case node.nil.nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
⊢ Ordnode α
[PROOFSTEP]
exact node 2 l x nil
[GOAL]
case node.nil.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
size✝ : ℕ
l✝ : Ordnode α
lrx : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node 3 (ι lx) lrx ι x
[GOAL]
case node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id lr with lrs lrl lrx lrr
[GOAL]
case node.nil.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact node 3 ll lx ι x
[GOAL]
case node.nil.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact
  if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
  else node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx (node (size lrr + 1) lrr x nil)
[GOAL]
case node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
refine' if delta * ls < rs then _ else if delta * rs < ls then _ else node (ls + rs + 1) l x r
[GOAL]
case node.node.refine'_1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id rl with rls rll rlx rlr
[GOAL]
case node.node.refine'_1.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact nil
[GOAL]
case node.node.refine'_1.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id rr with rrs
[GOAL]
case node.node.refine'_1.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact nil
[GOAL]
case node.node.refine'_1.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact
  if rls < ratio * rrs then node (ls + rs + 1) (node (ls + rls + 1) l x rl) rx rr
  else node (ls + rs + 1) (node (ls + size rll + 1) l x rll) rlx (node (size rlr + rrs + 1) rlr rx rr)
[GOAL]
case node.node.refine'_2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id ll with lls
[GOAL]
case node.node.refine'_2.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact nil
[GOAL]
case node.node.refine'_2.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
cases' id lr with lrs lrl lrx lrr
[GOAL]
case node.node.refine'_2.node.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact nil
[GOAL]
case node.node.refine'_2.node.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α
[PROOFSTEP]
exact
  if lrs < ratio * lls then node (ls + rs + 1) ll lx (node (lrs + rs + 1) lr x r)
  else node (ls + rs + 1) (node (lls + size lrl + 1) ll lx lrl) lrx (node (size lrr + rs + 1) lrr x r)
[GOAL]
α : Type u_1
x : α
inst✝ : DecidableEq α
⊢ (t : Ordnode α) → Decidable (Emem x t)
[PROOFSTEP]
dsimp [Emem]
[GOAL]
α : Type u_1
x : α
inst✝ : DecidableEq α
⊢ (t : Ordnode α) → Decidable (Any (Eq x) t)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
⊢ (t : Ordnode α) → Decidable (Amem x t)
[PROOFSTEP]
dsimp [Amem]
[GOAL]
α : Type u_1
inst✝¹ : LE α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
x : α
⊢ (t : Ordnode α) → Decidable (Any (fun y => x ≤ y ∧ y ≤ x) t)
[PROOFSTEP]
infer_instance
