α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t ↑rx
e : size t = ls + size rl
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs
rw [hl.2.1] at e
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : delta * ls < rs
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs
rw [hl.2.1, hr.2.1, delta] at h
case inl
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
H : size rl + size rr ≤ 1
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs

case inr.intro
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs
rcases hr.3.1 with (H | ⟨hr₁, hr₂⟩)
case inr.intro
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : ?m.359131
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs

case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
⊢ ?m.359131
case inr.intro
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs
suffices H₂
case inr.intro
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : ?m.359131
H₁ : ?m.359138
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs

case H₁
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : ?m.359131
⊢ ?m.359138

case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
⊢ ?m.359131
case inr.intro
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : ?m.359131
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs

case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
⊢ ?m.359131
suffices H₁
case inr.intro.refine'_1
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
H₁ : size t = 0 → size rr ≤ 1
⊢ 2 * size t ≤ 9 * size rr + 5 ∨ size t ≤ 3

case inr.intro.refine'_2
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
H₁ : size t = 0 → size rr ≤ 1
⊢ size (Ordnode.balanceL t rx rr) = ls + rs

case H₁
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
⊢ size t = 0 → size rr ≤ 1

case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
⊢ 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
case inr.intro
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : ?m.359131
H₁ : ?m.359138
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs

case H₁
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : ?m.359131
⊢ ?m.359138

case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
⊢ ?m.359131
refine' ⟨Valid'.balanceL_aux v hr.right H₁ H₂ _, _⟩
no goals
case inl
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
H : size rl + size rr ≤ 1
⊢ Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ size (Ordnode.balanceL t rx rr) = ls + rs
linarith
case inr.intro.refine'_1
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
H₁ : size t = 0 → size rr ≤ 1
⊢ 2 * (size ll + size lr + 1 + size rl) ≤ 9 * size rr + 5 ∨ size ll + size lr + 1 + size rl ≤ 3
case inr.intro.refine'_1
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
H₁ : size t = 0 → size rr ≤ 1
⊢ 2 * size t ≤ 9 * size rr + 5 ∨ size t ≤ 3
rw [e]
no goals
case inr.intro.refine'_1
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
H₁ : size t = 0 → size rr ≤ 1
⊢ 2 * (size ll + size lr + 1 + size rl) ≤ 9 * size rr + 5 ∨ size ll + size lr + 1 + size rl ≤ 3
exact Or.inl (Valid'.merge_lemma h hr₁)
case inr.intro.refine'_2
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
H₁ : size t = 0 → size rr ≤ 1
⊢ size ll + size lr + 1 + size rl + size rr + 1 = size ll + size lr + 1 + (size rl + size rr + 1)
case inr.intro.refine'_2
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
H₁ : size t = 0 → size rr ≤ 1
⊢ size (Ordnode.balanceL t rx rr) = ls + rs
rw [balanceL_eq_balance v.2 hr.2.2.2 H₁ H₂, balance_eq_balance' v.3 hr.3.2.2 v.2 hr.2.2.2,
  size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
no goals
case inr.intro.refine'_2
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
H₁ : size t = 0 → size rr ≤ 1
⊢ size ll + size lr + 1 + size rl + size rr + 1 = size ll + size lr + 1 + (size rl + size rr + 1)
abel
case H₁
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
⊢ size ll + size lr + size rl + 1 = 0 → size rr ≤ 1
case H₁
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
⊢ size t = 0 → size rr ≤ 1
rw [e, add_right_comm]
no goals
case H₁
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
H₂ : 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
⊢ size ll + size lr + size rl + 1 = 0 → size rr ≤ 1
rintro ⟨⟩
case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
a✝¹ : 1 ≤ size t
a✝ : 1 ≤ size rr
⊢ size rr ≤ delta * size t
case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
⊢ 1 ≤ size t → 1 ≤ size rr → size rr ≤ delta * size t
intro _ _
case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
a✝¹ : 1 ≤ size t
a✝ : 1 ≤ size rr
⊢ size rr ≤ delta * (size ll + size lr + 1 + size rl)
case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
a✝¹ : 1 ≤ size t
a✝ : 1 ≤ size rr
⊢ size rr ≤ delta * size t
rw [e]
case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ 3 * size rl
a✝¹ : 1 ≤ size t
a✝ : 1 ≤ size rr
⊢ size rr ≤ 3 * (size ll + size lr + 1 + size rl)
case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ delta * size rl
a✝¹ : 1 ≤ size t
a✝ : 1 ≤ size rr
⊢ size rr ≤ delta * (size ll + size lr + 1 + size rl)
unfold delta at hr₂ ⊢
no goals
case H₂
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (size ll + size lr + 1) < size rl + size rr + 1
v : Valid' o₁ t ↑rx
e : size t = size ll + size lr + 1 + size rl
hr₁ : size rl ≤ delta * size rr
hr₂ : size rr ≤ 3 * size rl
a✝¹ : 1 ≤ size t
a✝ : 1 ≤ size rr
⊢ size rr ≤ 3 * (size ll + size lr + 1 + size rl)
linarith