awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
⊢ t.dual.dual.Bounded o₁ o₂

Tactic:
have := Bounded.dual h
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.dual.Bounded o₂ o₁
this : t.dual.dual.Bounded o₁ o₂
rwa : ∀ (this : t.Bounded o₁ o₂), t.Bounded o₁ o₂
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : t.Bounded o₁ o₂), t.Bounded o₁ o₂
⊢ t.Bounded o₁ o₂

Tactic:
rwa [dual_dual, OrderDual.Preorder.dual_dual] at this

Premises used: OrderDual.Preorder.dual_dual, Ordnode.dual_dual
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded nil o₁ o₂
top : ∀ (h : Bounded nil o₁ ⊤), Bounded.{u_1} (α := α) nil ⊥ ⊤
coe : ∀ (a : α) (h : Bounded nil o₁ (↑a : WithTop α)), Bounded nil ⊥ (↑a : WithTop α)
⊢ Bounded nil ⊥ o₂

Tactic:
cases o₂
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
h : Bounded nil o₁ ⊤
⊢ Bounded.{u_1} (α := α) nil ⊥ ⊤

Tactic:
trivial
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
a : α
h : Bounded nil o₁ (↑a : WithTop α)
⊢ Bounded nil ⊥ (↑a : WithTop α)

Tactic:
trivial
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded nil o₁ o₂
bot : ∀ (h : Bounded nil ⊥ o₂), Bounded.{u_1} (α := α) nil ⊥ ⊤
coe : ∀ (a : α) (h : Bounded nil (↑a : WithBot α) o₂), Bounded nil (↑a : WithBot α) ⊤
⊢ Bounded nil o₁ ⊤

Tactic:
cases o₁
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
o₂ : WithTop α
h : Bounded nil ⊥ o₂
⊢ Bounded.{u_1} (α := α) nil ⊥ ⊤

Tactic:
trivial
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
o₂ : WithTop α
a : α
h : Bounded nil (↑a : WithBot α) o₂
⊢ Bounded nil (↑a : WithBot α) ⊤

Tactic:
trivial
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : t.Bounded o₁ o₂
⊢ t.Bounded ⊥ ⊤

Tactic:
h.weak_left.weak_right

Premises used: Ordnode.Bounded.weak_left, Ordnode.Bounded.weak_right
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ (↑x : WithTop α)
h₂ : t₂.Bounded (↑x : WithBot α) o₂
⊢ All (fun (y : α) ↦ All (fun (z : α) ↦ y < z) t₂) t₁

Tactic:
h₁.mem_lt.imp fun y yx => ?_

Premises used: Ordnode.All.imp, Ordnode.Bounded.mem_lt
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ (↑x : WithTop α)
h₂ : t₂.Bounded (↑x : WithBot α) o₂
refine : ∀ (y : α) (yx : y < x), All (fun (z : α) ↦ y < z) t₂
⊢ All (fun (y : α) ↦ All (fun (z : α) ↦ y < z) t₂) t₁

Tactic:
refine h₁.mem_lt.imp fun y yx => ?_

Premises used: Ordnode.All.imp, Ordnode.Bounded.mem_lt
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ (↑x : WithTop α)
h₂ : t₂.Bounded (↑x : WithBot α) o₂
y : α
yx : y < x
⊢ All (fun (z : α) ↦ y < z) t₂

Tactic:
h₂.mem_gt.imp fun z xz => lt_trans yx xz

Premises used: lt_trans, Ordnode.All.imp, Ordnode.Bounded.mem_gt
-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : t₁.Bounded o₁ (↑x : WithTop α)
h₂ : t₂.Bounded (↑x : WithBot α) o₂
y : α
yx : y < x
⊢ All (fun (z : α) ↦ y < z) t₂

Tactic:
exact h₂.mem_gt.imp fun z xz => lt_trans yx xz

Premises used: lt_trans, Ordnode.All.imp, Ordnode.Bounded.mem_gt
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
⊢ size.{u_1} (α := α) nil = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
sz : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ (node sz l x r).size = sz

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r nil : Ordnode α
node : (rs : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases id r with _ | rs

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r nil : Ordnode α
nil₁ : (ls : ℕ) → (ll : Ordnode α) → (lx : α) → (lr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id l with _ | ⟨ls, ll, lx, lr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

Tactic:
exact ι x
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr nil : Ordnode α
nil₁ : (lls : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases id ll with _ | lls

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr nil : Ordnode α
nil₁ : ℕ → Ordnode α → (lrx : α) → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases lr with _ | ⟨_, _, lrx⟩
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
⊢ Ordnode α

Tactic:
exact node 2 l x nil

Premises used: Ordnode.node, Ordnode.nil, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
size : ℕ
l_1 : Ordnode α
lrx : α
r_1 : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 (ι lx) lrx ι x

Premises used: Ordnode.node, Ordnode.singleton, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 nil : Ordnode α
nil₁ : (lrs : ℕ) → (lrl : Ordnode α) → (lrx : α) → (lrr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 ll lx ι x

Premises used: Ordnode.node, Ordnode.singleton, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α

Tactic:
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)

Premises used: Ordnode.size, Ordnode.node, HAdd.hAdd, Ordnode.nil, Ordnode.ratio, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 node : Ordnode α
node₁ : (ls : ℕ) → (ll : Ordnode α) → (lx : α) → (lr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id l with _ | ⟨ls, ll, lx, lr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
⊢ Ordnode α

Tactic:
exact node (rs + 1) nil x r

Premises used: Ordnode.node, HAdd.hAdd, Ordnode.nil, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr node : Ordnode α
node₁ : (lls : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases id ll with _ | lls

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
⊢ Ordnode α

Tactic:
exact nil

Premises used: Ordnode.nil
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l_2 : Ordnode α
x_2 : α
r_2 node : Ordnode α
node₁ : (lrs : ℕ) → (lrl : Ordnode α) → (lrx : α) → (lrr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l_2 : Ordnode α
x_2 : α
r_2 : Ordnode α
⊢ Ordnode α

Tactic:
exact nil

Premises used: Ordnode.nil
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l_2 : Ordnode α
x_2 : α
r_2 : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α

Tactic:
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)

Premises used: Ordnode.size, Ordnode.node, HAdd.hAdd, Ordnode.ratio, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r nil : Ordnode α
node : (ls : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases id l with _ | ls

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r nil : Ordnode α
nil₁ : (rs : ℕ) → (rl : Ordnode α) → (rx : α) → (rr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id r with _ | ⟨rs, rl, rx, rr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr nil : Ordnode α
nil₁ : (rrs : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases id rr with _ | rrs

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr nil : Ordnode α
nil₁ : ℕ → Ordnode α → (rlx : α) → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases rl with _ | ⟨_, _, rlx⟩
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
exact node 2 nil x r

Premises used: Ordnode.node, Ordnode.nil, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rx : α
rr : Ordnode α
size : ℕ
l_1 : Ordnode α
rlx : α
r_1 : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 (ι x) rlx ι rx

Premises used: Ordnode.node, Ordnode.singleton, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 nil : Ordnode α
nil₁ : (rls : ℕ) → (rll : Ordnode α) → (rlx : α) → (rlr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 (ι x) rx rr

Premises used: Ordnode.node, Ordnode.singleton, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

Tactic:
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)

Premises used: Ordnode.size, Ordnode.node, HAdd.hAdd, Ordnode.nil, Ordnode.ratio, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 node : Ordnode α
node₁ : (rs : ℕ) → (rl : Ordnode α) → (rx : α) → (rr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id r with _ | ⟨rs, rl, rx, rr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
⊢ Ordnode α

Tactic:
exact node (ls + 1) l x nil

Premises used: Ordnode.node, HAdd.hAdd, Ordnode.nil, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr node : Ordnode α
node₁ : (rrs : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases id rr with _ | rrs

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
exact nil

Premises used: Ordnode.nil
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l_2 : Ordnode α
x_2 : α
r_2 node : Ordnode α
node₁ : (rls : ℕ) → (rll : Ordnode α) → (rlx : α) → (rlr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l_2 : Ordnode α
x_2 : α
r_2 : Ordnode α
⊢ Ordnode α

Tactic:
exact nil

Premises used: Ordnode.nil
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rrs : ℕ
l_2 : Ordnode α
x_2 : α
r_2 : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

Tactic:
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)

Premises used: Ordnode.size, Ordnode.node, HAdd.hAdd, Ordnode.ratio, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r nil : Ordnode α
node : (ls : ℕ) → (ll : Ordnode α) → (lx : α) → (lr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id l with _ | ⟨ls, ll, lx, lr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr nil : Ordnode α
nil₁ : (rls : ℕ) → (rll : Ordnode α) → (rlx : α) → (rlr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr nil : Ordnode α
nil₁ : ℕ → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
cases id rr

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
exact node 2 nil x r

Premises used: Ordnode.node, Ordnode.nil, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
size : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 (ι x) rx rr

Premises used: Ordnode.node, Ordnode.singleton, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr nil : Ordnode α
nil₁ : (rrs : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases id rr with _ | rrs

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
⊢ Ordnode α

Tactic:
exact node 3 (ι x) rlx ι rx

Premises used: Ordnode.node, Ordnode.singleton, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
⊢ Ordnode α

Tactic:
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)

Premises used: Ordnode.size, Ordnode.node, HAdd.hAdd, Ordnode.nil, Ordnode.ratio, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr node : Ordnode α
node₁ : (rs : ℕ) → (rl : Ordnode α) → (rx : α) → (rr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id r with _ | ⟨rs, rl, rx, rr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr node : Ordnode α
node₁ : (lls : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases id ll with _ | lls

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr node : Ordnode α
node₁ : ℕ → Ordnode α → (lrx : α) → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases lr with _ | ⟨_, _, lrx⟩
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
lls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 node : Ordnode α
node₁ : (lrs : ℕ) → (lrl : Ordnode α) → (lrx : α) → (lrr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr node node₁ : Ordnode α
⊢ Ordnode α

Tactic:
refine
        if delta * ls < rs then ?_ else if delta * rs < ls then ?_ else node (ls + rs + 1) l x r

Premises used: Ordnode.node, Ordnode.delta, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr node : Ordnode α
node₁ : (rls : ℕ) → (rll : Ordnode α) → (rlx : α) → (rlr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
exact nil

Premises used: Ordnode.nil
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : 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 node : Ordnode α
node₁ : (rrs : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases id rr with _ | rrs

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : 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 α

Tactic:
exact nil

Premises used: Ordnode.nil
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : 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_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
⊢ Ordnode α

Tactic:
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)

Premises used: Ordnode.size, Ordnode.node, HAdd.hAdd, Ordnode.ratio, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr node : Ordnode α
node₁ : (lls : ℕ) → Ordnode α → α → Ordnode α → Ordnode α
⊢ Ordnode α

Tactic:
rcases id ll with _ | lls

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 node : Ordnode α
node₁ : (lrs : ℕ) → (lrl : Ordnode α) → (lrx : α) → (lrr : Ordnode α) → Ordnode α
⊢ Ordnode α

Tactic:
rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩

Premises used: id
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
⊢ Ordnode α

Tactic:
exact nil

Premises used: Ordnode.nil
-- Module: Mathlib.Data.Ordmap.Ordnode
Goal:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
lls : ℕ
l_1 : Ordnode α
x_1 : α
r_1 : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ Ordnode α

Tactic:
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)

Premises used: Ordnode.size, Ordnode.node, HAdd.hAdd, Ordnode.ratio, OfNat.ofNat
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
x y : α
xy : x ≤ y
t : Ordnode α
o : WithTop α
h : Valid' (↑y : WithBot α) t o
⊢ Valid' (↑x : WithBot α) t o

Tactic:
⟨h.1.mono_left xy, h.2, h.3⟩

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, Ordnode.Bounded.mono_left, Ordnode.Valid'.ord, Ordnode.Valid'.mk
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
x y : α
xy : x ≤ y
t : Ordnode α
o : WithBot α
h : Valid' o t (↑x : WithTop α)
⊢ Valid' o t (↑y : WithTop α)

Tactic:
⟨h.1.mono_right xy, h.2, h.3⟩

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, Ordnode.Bounded.mono_right, Ordnode.Valid'.ord, Ordnode.Valid'.mk
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
h : t₁.Bounded o₁ (↑x : WithTop α)
H : Valid' (↑x : WithBot α) t₂ o₂
⊢ Valid' o₁ t₂ o₂

Tactic:
⟨h.trans_left H.1, H.2, H.3⟩

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, Ordnode.Valid'.ord, Ordnode.Bounded.trans_left, Ordnode.Valid'.mk
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ t₁ (↑x : WithTop α)
h : t₂.Bounded (↑x : WithBot α) o₂
⊢ Valid' o₁ t₁ o₂

Tactic:
⟨H.1.trans_right h, H.2, H.3⟩

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, Ordnode.Bounded.trans_right, Ordnode.Valid'.ord, Ordnode.Valid'.mk
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ t o₂
h₁ : Bounded nil o₁ (↑x : WithTop α)
h₂ : All (fun (x_1 : α) ↦ x_1 < x) t
⊢ Valid' o₁ t (↑x : WithTop α)

Tactic:
⟨H.1.of_lt h₁ h₂, H.2, H.3⟩

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, Ordnode.Valid'.ord, Ordnode.Bounded.of_lt, Ordnode.Valid'.mk
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
x : α
o₁ : WithBot α
o₂ : WithTop α
H : Valid' o₁ t o₂
h₁ : Bounded nil (↑x : WithBot α) o₂
h₂ : All (fun (x_1 : α) ↦ x_1 > x) t
⊢ Valid' (↑x : WithBot α) t o₂

Tactic:
⟨H.1.of_gt h₁ h₂, H.2, H.3⟩

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, Ordnode.Bounded.of_gt, Ordnode.Valid'.ord, Ordnode.Valid'.mk
-- Module: Mathlib.Data.Ordmap.Ordset
Goal:
α : Type u_1
inst : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₁ t o₂
⊢ t.Valid

Tactic:
⟨h.1.weak, h.2, h.3⟩

Premises used: Ordnode.Valid'.bal, Ordnode.Valid'.sz, Ordnode.Valid, Ordnode.Bounded.weak, Ordnode.Valid'.ord, Ordnode.Valid'.mk