case nil
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
hm : Valid' (↑x) nil ↑y
Hm : 0 < size nil
H :
  size l = 0 ∧ size nil = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size nil ∧
        delta * size l ≤ size nil + size r ∧ 3 * (size nil + size r) ≤ 16 * size l + 9 ∧ size nil ≤ delta * size r
⊢ Valid' o₁ (Ordnode.node4L l x nil y r) o₂

case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
H :
  size l = 0 ∧ size (Ordnode.node s ml z mr) = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size (Ordnode.node s ml z mr) ∧
        delta * size l ≤ size (Ordnode.node s ml z mr) + size r ∧
          3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9 ∧
            size (Ordnode.node s ml z mr) ≤ delta * size r
⊢ Valid' o₁ (Ordnode.node4L l x (Ordnode.node s ml z mr) y r) o₂
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hm : Valid' (↑x) m ↑y
hr : Valid' (↑y) r o₂
Hm : 0 < size m
H :
  size l = 0 ∧ size m = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size m ∧
        delta * size l ≤ size m + size r ∧ 3 * (size m + size r) ≤ 16 * size l + 9 ∧ size m ≤ delta * size r
⊢ Valid' o₁ (Ordnode.node4L l x m y r) o₂
cases' m with s ml z mr
case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
H :
  size l = 0 ∧ size (Ordnode.node s ml z mr) = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size (Ordnode.node s ml z mr) ∧
        delta * size l ≤ size (Ordnode.node s ml z mr) + size r ∧
          3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9 ∧
            size (Ordnode.node s ml z mr) ≤ delta * size r
this :
  BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
⊢ Valid' o₁ (Ordnode.node4L l x (Ordnode.node s ml z mr) y r) o₂

case this
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
H :
  size l = 0 ∧ size (Ordnode.node s ml z mr) = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size (Ordnode.node s ml z mr) ∧
        delta * size l ≤ size (Ordnode.node s ml z mr) + size r ∧
          3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9 ∧
            size (Ordnode.node s ml z mr) ≤ delta * size r
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
H :
  size l = 0 ∧ size (Ordnode.node s ml z mr) = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size (Ordnode.node s ml z mr) ∧
        delta * size l ≤ size (Ordnode.node s ml z mr) + size r ∧
          3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9 ∧
            size (Ordnode.node s ml z mr) ≤ delta * size r
⊢ Valid' o₁ (Ordnode.node4L l x (Ordnode.node s ml z mr) y r) o₂
suffices :
  BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case this
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
H :
  size l = 0 ∧ size (Ordnode.node s ml z mr) = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size (Ordnode.node s ml z mr) ∧
        delta * size l ≤ size (Ordnode.node s ml z mr) + size r ∧
          3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9 ∧
            size (Ordnode.node s ml z mr) ≤ delta * size r
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case node
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
H :
  size l = 0 ∧ size (Ordnode.node s ml z mr) = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size (Ordnode.node s ml z mr) ∧
        delta * size l ≤ size (Ordnode.node s ml z mr) + size r ∧
          3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9 ∧
            size (Ordnode.node s ml z mr) ≤ delta * size r
this :
  BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
⊢ Valid' o₁ (Ordnode.node4L l x (Ordnode.node s ml z mr) y r) o₂

case this
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
H :
  size l = 0 ∧ size (Ordnode.node s ml z mr) = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size (Ordnode.node s ml z mr) ∧
        delta * size l ≤ size (Ordnode.node s ml z mr) + size r ∧
          3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9 ∧
            size (Ordnode.node s ml z mr) ≤ delta * size r
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
exact Valid'.node' (hl.node' hm.left this.1) (hm.right.node' hr this.2.1) this.2.2
case this.inl.intro.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size (Ordnode.node s ml z mr) = 1
r0 : size r ≤ 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)

case this.inr.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size (Ordnode.node s ml z mr)
lr₁ : delta * size l ≤ size (Ordnode.node s ml z mr) + size r
lr₂ : 3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9
mr₂ : size (Ordnode.node s ml z mr) ≤ delta * size r
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case this
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
H :
  size l = 0 ∧ size (Ordnode.node s ml z mr) = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size (Ordnode.node s ml z mr) ∧
        delta * size l ≤ size (Ordnode.node s ml z mr) + size r ∧
          3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9 ∧
            size (Ordnode.node s ml z mr) ≤ delta * size r
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
rcases H with (⟨l0, m1, r0⟩ | ⟨l0, mr₁, lr₁, lr₂, mr₂⟩)
no goals
case nil
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
hm : Valid' (↑x) nil ↑y
Hm : 0 < size nil
H :
  size l = 0 ∧ size nil = 1 ∧ size r ≤ 1 ∨
    0 < size l ∧
      ratio * size r ≤ size nil ∧
        delta * size l ≤ size nil + size r ∧ 3 * (size nil + size r) ≤ 16 * size l + 9 ∧ size nil ≤ delta * size r
⊢ Valid' o₁ (Ordnode.node4L l x nil y r) o₂
cases Hm
case this.inl.intro.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
r0 : size r ≤ 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case this.inl.intro.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size (Ordnode.node s ml z mr) = 1
r0 : size r ≤ 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
rw [hm.2.size_eq, Nat.succ_inj', add_eq_zero_iff] at m1
case this.inl.intro.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
r0 : size r ≤ 1
⊢ BalancedSz 0 0 ∧ BalancedSz 0 (size r) ∧ BalancedSz (0 + 0 + 1) (0 + size r + 1)
case this.inl.intro.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
r0 : size r ≤ 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
rw [l0, m1.1, m1.2]
case this.inl.intro.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
⊢ size r ≤ 1 → BalancedSz 0 0 ∧ BalancedSz 0 (size r) ∧ BalancedSz (0 + 0 + 1) (0 + size r + 1)
case this.inl.intro.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
r0 : size r ≤ 1
⊢ BalancedSz 0 0 ∧ BalancedSz 0 (size r) ∧ BalancedSz (0 + 0 + 1) (0 + size r + 1)
revert r0
no goals
case this.inl.intro.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
⊢ size r ≤ 1 → BalancedSz 0 0 ∧ BalancedSz 0 (size r) ∧ BalancedSz (0 + 0 + 1) (0 + size r + 1)
rcases size r with (_ | _ | _) <;>
[decide; decide; (intro r0; unfold BalancedSz delta; linarith)]
case this.inl.intro.intro.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
n✝ : ℕ
r0 : Nat.succ (Nat.succ n✝) ≤ 1
⊢ BalancedSz 0 0 ∧ BalancedSz 0 (Nat.succ (Nat.succ n✝)) ∧ BalancedSz (0 + 0 + 1) (0 + Nat.succ (Nat.succ n✝) + 1)
case this.inl.intro.intro.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
n✝ : ℕ
⊢ Nat.succ (Nat.succ n✝) ≤ 1 →
    BalancedSz 0 0 ∧ BalancedSz 0 (Nat.succ (Nat.succ n✝)) ∧ BalancedSz (0 + 0 + 1) (0 + Nat.succ (Nat.succ n✝) + 1)
intro r0
case this.inl.intro.intro.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
n✝ : ℕ
r0 : Nat.succ (Nat.succ n✝) ≤ 1
⊢ (0 + 0 ≤ 1 ∨ 0 ≤ 3 * 0 ∧ 0 ≤ 3 * 0) ∧
    (0 + Nat.succ (Nat.succ n✝) ≤ 1 ∨ 0 ≤ 3 * Nat.succ (Nat.succ n✝) ∧ Nat.succ (Nat.succ n✝) ≤ 3 * 0) ∧
      (0 + 0 + 1 + (0 + Nat.succ (Nat.succ n✝) + 1) ≤ 1 ∨
        0 + 0 + 1 ≤ 3 * (0 + Nat.succ (Nat.succ n✝) + 1) ∧ 0 + Nat.succ (Nat.succ n✝) + 1 ≤ 3 * (0 + 0 + 1))
case this.inl.intro.intro.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
n✝ : ℕ
r0 : Nat.succ (Nat.succ n✝) ≤ 1
⊢ BalancedSz 0 0 ∧ BalancedSz 0 (Nat.succ (Nat.succ n✝)) ∧ BalancedSz (0 + 0 + 1) (0 + Nat.succ (Nat.succ n✝) + 1)
unfold BalancedSz delta
no goals
case this.inl.intro.intro.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : size l = 0
m1 : size ml = 0 ∧ size mr = 0
n✝ : ℕ
r0 : Nat.succ (Nat.succ n✝) ≤ 1
⊢ (0 + 0 ≤ 1 ∨ 0 ≤ 3 * 0 ∧ 0 ≤ 3 * 0) ∧
    (0 + Nat.succ (Nat.succ n✝) ≤ 1 ∨ 0 ≤ 3 * Nat.succ (Nat.succ n✝) ∧ Nat.succ (Nat.succ n✝) ≤ 3 * 0) ∧
      (0 + 0 + 1 + (0 + Nat.succ (Nat.succ n✝) + 1) ≤ 1 ∨
        0 + 0 + 1 ≤ 3 * (0 + Nat.succ (Nat.succ n✝) + 1) ∧ 0 + Nat.succ (Nat.succ n✝) + 1 ≤ 3 * (0 + 0 + 1))
linarith
case this.inr.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size (Ordnode.node s ml z mr)
lr₁ : delta * size l ≤ size (Ordnode.node s ml z mr) + size r
lr₂ : 3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9
mr₂ : size (Ordnode.node s ml z mr) ≤ delta * size r
r0 : size r = 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)

case this.inr.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size (Ordnode.node s ml z mr)
lr₁ : delta * size l ≤ size (Ordnode.node s ml z mr) + size r
lr₂ : 3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9
mr₂ : size (Ordnode.node s ml z mr) ≤ delta * size r
r0 : size r > 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case this.inr.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size (Ordnode.node s ml z mr)
lr₁ : delta * size l ≤ size (Ordnode.node s ml z mr) + size r
lr₂ : 3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9
mr₂ : size (Ordnode.node s ml z mr) ≤ delta * size r
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
cases' Nat.eq_zero_or_pos (size r) with r0 r0
case this.inr.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case this.inr.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size (Ordnode.node s ml z mr)
lr₁ : delta * size l ≤ size (Ordnode.node s ml z mr) + size r
lr₂ : 3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9
mr₂ : size (Ordnode.node s ml z mr) ≤ delta * size r
r0 : size r > 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
rw [hm.2.size_eq] at lr₁ lr₂ mr₁ mr₂
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)

case neg
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case this.inr.intro.intro.intro.intro.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
by_cases mm : size ml + size mr ≤ 1
case neg.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case neg
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
rcases hm.3.1.resolve_left mm with ⟨mm₁, mm₂⟩
case neg.intro.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml = 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)

case neg.intro.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case neg.intro
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
cases' Nat.eq_zero_or_pos (size ml) with ml0 ml0
case neg.intro.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case neg.intro.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
have : 2 * size l ≤ size ml + size mr + 1 := by
  have := Nat.mul_le_mul_left ratio lr₁
  rw [mul_left_comm, mul_add] at this
  have := le_trans this (add_le_add_left mr₁ _)
  rw [← Nat.succ_mul] at this
  exact (mul_le_mul_left (by decide)).1 this
case neg.intro.inr.refine'_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size l ≤ delta * size ml

case neg.intro.inr.refine'_2
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size ml ≤ delta * size l

case neg.intro.inr.refine'_3
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size mr ≤ delta * size r

case neg.intro.inr.refine'_4
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size r ≤ delta * size mr

case neg.intro.inr.refine'_5
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size l + size ml + 1 ≤ delta * (size mr + size r + 1)

case neg.intro.inr.refine'_6
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size mr + size r + 1 ≤ delta * (size l + size ml + 1)
case neg.intro.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
refine' ⟨Or.inr ⟨_, _⟩, Or.inr ⟨_, _⟩, Or.inr ⟨_, _⟩⟩
case this.inr.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size (Ordnode.node s ml z mr)
lr₁ : delta * size l ≤ size (Ordnode.node s ml z mr) + size r
lr₂ : 3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9
mr₂ : size (Ordnode.node s ml z mr) ≤ delta * 0
r0 : size r = 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case this.inr.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size (Ordnode.node s ml z mr)
lr₁ : delta * size l ≤ size (Ordnode.node s ml z mr) + size r
lr₂ : 3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9
mr₂ : size (Ordnode.node s ml z mr) ≤ delta * size r
r0 : size r = 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
rw [r0] at mr₂
no goals
case this.inr.intro.intro.intro.intro.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size (Ordnode.node s ml z mr)
lr₁ : delta * size l ≤ size (Ordnode.node s ml z mr) + size r
lr₂ : 3 * (size (Ordnode.node s ml z mr) + size r) ≤ 16 * size l + 9
mr₂ : size (Ordnode.node s ml z mr) ≤ delta * 0
r0 : size r = 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
cases not_le_of_lt Hm mr₂
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
r1 : size r = 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
have r1 :=
  le_antisymm
    ((mul_le_mul_left (by decide)).1 (le_trans mr₁ (Nat.succ_le_succ mm) : _ ≤ ratio * 1)) r0
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
r1 : size r = 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
r1 : size r = 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
rw [r1, add_assoc] at lr₁
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
r1 : size r = 1
l1 : size l = 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
r1 : size r = 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
have l1 :=
  le_antisymm
    ((mul_le_mul_left (by decide)).1 (le_trans lr₁ (add_le_add_right mm 2) : _ ≤ delta * 1))
    l0
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
r1 : size r = 1
l1 : size l = 1
⊢ BalancedSz 1 (size ml) ∧ BalancedSz (size mr) 1 ∧ BalancedSz (1 + size ml + 1) (size mr + 1 + 1)
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
r1 : size r = 1
l1 : size l = 1
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
rw [l1, r1]
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
⊢ size ml + size mr ≤ 1 →
    BalancedSz 1 (size ml) ∧ BalancedSz (size mr) 1 ∧ BalancedSz (1 + size ml + 1) (size mr + 1 + 1)
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
r1 : size r = 1
l1 : size l = 1
⊢ BalancedSz 1 (size ml) ∧ BalancedSz (size mr) 1 ∧ BalancedSz (1 + size ml + 1) (size mr + 1 + 1)
revert mm
case pos.zero.zero
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
mm : Nat.zero + Nat.zero ≤ 1
⊢ BalancedSz 1 Nat.zero ∧ BalancedSz Nat.zero 1 ∧ BalancedSz (1 + Nat.zero + 1) (Nat.zero + 1 + 1)

case pos.zero.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
n✝ : ℕ
mm : Nat.zero + Nat.succ n✝ ≤ 1
⊢ BalancedSz 1 Nat.zero ∧ BalancedSz (Nat.succ n✝) 1 ∧ BalancedSz (1 + Nat.zero + 1) (Nat.succ n✝ + 1 + 1)

case pos.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
n✝ : ℕ
mm : Nat.succ n✝ + Nat.zero ≤ 1
⊢ BalancedSz 1 (Nat.succ n✝) ∧ BalancedSz Nat.zero 1 ∧ BalancedSz (1 + Nat.succ n✝ + 1) (Nat.zero + 1 + 1)

case pos.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
n✝¹ n✝ : ℕ
mm : Nat.succ n✝¹ + Nat.succ n✝ ≤ 1
⊢ BalancedSz 1 (Nat.succ n✝¹) ∧ BalancedSz (Nat.succ n✝) 1 ∧ BalancedSz (1 + Nat.succ n✝¹ + 1) (Nat.succ n✝ + 1 + 1)
case pos
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
⊢ size ml + size mr ≤ 1 →
    BalancedSz 1 (size ml) ∧ BalancedSz (size mr) 1 ∧ BalancedSz (1 + size ml + 1) (size mr + 1 + 1)
cases size ml <;> cases size mr <;> intro mm
no goals
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
⊢ 0 < ratio
decide
no goals
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : size ml + size mr ≤ 1
r1 : size r = 1
⊢ 0 < delta
decide
no goals
case pos.zero.zero
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
mm : Nat.zero + Nat.zero ≤ 1
⊢ BalancedSz 1 Nat.zero ∧ BalancedSz Nat.zero 1 ∧ BalancedSz (1 + Nat.zero + 1) (Nat.zero + 1 + 1)
decide
case pos.zero.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
n✝ : ℕ
mm : Nat.succ n✝ ≤ 1
⊢ BalancedSz 1 Nat.zero ∧ BalancedSz (Nat.succ n✝) 1 ∧ BalancedSz (1 + Nat.zero + 1) (Nat.succ n✝ + 1 + 1)
case pos.zero.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
n✝ : ℕ
mm : Nat.zero + Nat.succ n✝ ≤ 1
⊢ BalancedSz 1 Nat.zero ∧ BalancedSz (Nat.succ n✝) 1 ∧ BalancedSz (1 + Nat.zero + 1) (Nat.succ n✝ + 1 + 1)
rw [Nat.zero_eq, zero_add] at mm
case pos.zero.succ.refl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
⊢ BalancedSz 1 Nat.zero ∧ BalancedSz (Nat.succ 0) 1 ∧ BalancedSz (1 + Nat.zero + 1) (Nat.succ 0 + 1 + 1)
case pos.zero.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
n✝ : ℕ
mm : Nat.succ n✝ ≤ 1
⊢ BalancedSz 1 Nat.zero ∧ BalancedSz (Nat.succ n✝) 1 ∧ BalancedSz (1 + Nat.zero + 1) (Nat.succ n✝ + 1 + 1)
rcases mm with (_ | ⟨⟨⟩⟩)
no goals
case pos.zero.succ.refl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
⊢ BalancedSz 1 Nat.zero ∧ BalancedSz (Nat.succ 0) 1 ∧ BalancedSz (1 + Nat.zero + 1) (Nat.succ 0 + 1 + 1)
decide
case pos.succ.zero.refl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
⊢ BalancedSz 1 (Nat.succ 0) ∧ BalancedSz Nat.zero 1 ∧ BalancedSz (1 + Nat.succ 0 + 1) (Nat.zero + 1 + 1)
case pos.succ.zero
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
n✝ : ℕ
mm : Nat.succ n✝ + Nat.zero ≤ 1
⊢ BalancedSz 1 (Nat.succ n✝) ∧ BalancedSz Nat.zero 1 ∧ BalancedSz (1 + Nat.succ n✝ + 1) (Nat.zero + 1 + 1)
rcases mm with (_ | ⟨⟨⟩⟩)
no goals
case pos.succ.zero.refl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
⊢ BalancedSz 1 (Nat.succ 0) ∧ BalancedSz Nat.zero 1 ∧ BalancedSz (1 + Nat.succ 0 + 1) (Nat.zero + 1 + 1)
decide
case pos.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
n✝¹ n✝ : ℕ
mm : Nat.succ (n✝¹ + Nat.succ n✝) ≤ 1
⊢ BalancedSz 1 (Nat.succ n✝¹) ∧ BalancedSz (Nat.succ n✝) 1 ∧ BalancedSz (1 + Nat.succ n✝¹ + 1) (Nat.succ n✝ + 1 + 1)
case pos.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
n✝¹ n✝ : ℕ
mm : Nat.succ n✝¹ + Nat.succ n✝ ≤ 1
⊢ BalancedSz 1 (Nat.succ n✝¹) ∧ BalancedSz (Nat.succ n✝) 1 ∧ BalancedSz (1 + Nat.succ n✝¹ + 1) (Nat.succ n✝ + 1 + 1)
rw [Nat.succ_add] at mm
no goals
case pos.succ.succ
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + (1 + 1)
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
r1 : size r = 1
l1 : size l = 1
n✝¹ n✝ : ℕ
mm : Nat.succ (n✝¹ + Nat.succ n✝) ≤ 1
⊢ BalancedSz 1 (Nat.succ n✝¹) ∧ BalancedSz (Nat.succ n✝) 1 ∧ BalancedSz (1 + Nat.succ n✝¹ + 1) (Nat.succ n✝ + 1 + 1)
rcases mm with (_ | ⟨⟨⟩⟩)
case neg.intro.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr = 0
ml0 : size ml = 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case neg.intro.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml = 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
rw [ml0, MulZeroClass.mul_zero, le_zero_iff] at mm₂
case neg.intro.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬0 + 0 ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr = 0
ml0 : size ml = 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
case neg.intro.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr = 0
ml0 : size ml = 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
rw [ml0, mm₂] at mm
no goals
case neg.intro.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬0 + 0 ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr = 0
ml0 : size ml = 0
⊢ BalancedSz (size l) (size ml) ∧
    BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1)
cases mm (by decide)
no goals
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬0 + 0 ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr = 0
ml0 : size ml = 0
⊢ 0 + 0 ≤ 1
decide
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : ratio * (delta * size l) ≤ ratio * (size ml + size mr + 1 + size r)
⊢ 2 * size l ≤ size ml + size mr + 1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
⊢ 2 * size l ≤ size ml + size mr + 1
have := Nat.mul_le_mul_left ratio lr₁
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : delta * (ratio * size l) ≤ ratio * (size ml + size mr + 1) + ratio * size r
⊢ 2 * size l ≤ size ml + size mr + 1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : ratio * (delta * size l) ≤ ratio * (size ml + size mr + 1 + size r)
⊢ 2 * size l ≤ size ml + size mr + 1
rw [mul_left_comm, mul_add] at this
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this✝ : delta * (ratio * size l) ≤ ratio * (size ml + size mr + 1) + ratio * size r
this : delta * (ratio * size l) ≤ ratio * (size ml + size mr + 1) + (size ml + size mr + 1)
⊢ 2 * size l ≤ size ml + size mr + 1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : delta * (ratio * size l) ≤ ratio * (size ml + size mr + 1) + ratio * size r
⊢ 2 * size l ≤ size ml + size mr + 1
have := le_trans this (add_le_add_left mr₁ _)
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this✝ : delta * (ratio * size l) ≤ ratio * (size ml + size mr + 1) + ratio * size r
this : delta * (ratio * size l) ≤ Nat.succ ratio * (size ml + size mr + 1)
⊢ 2 * size l ≤ size ml + size mr + 1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this✝ : delta * (ratio * size l) ≤ ratio * (size ml + size mr + 1) + ratio * size r
this : delta * (ratio * size l) ≤ ratio * (size ml + size mr + 1) + (size ml + size mr + 1)
⊢ 2 * size l ≤ size ml + size mr + 1
rw [← Nat.succ_mul] at this
no goals
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this✝ : delta * (ratio * size l) ≤ ratio * (size ml + size mr + 1) + ratio * size r
this : delta * (ratio * size l) ≤ Nat.succ ratio * (size ml + size mr + 1)
⊢ 2 * size l ≤ size ml + size mr + 1
exact (mul_le_mul_left (by decide)).1 this
no goals
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this✝ : delta * (ratio * size l) ≤ ratio * (size ml + size mr + 1) + ratio * size r
this : delta * (ratio * size l) ≤ Nat.succ ratio * (size ml + size mr + 1)
⊢ 0 < delta
decide
case neg.intro.inr.refine'_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size ml + size mr + 1 ≤ 2 * (delta * size ml)
case neg.intro.inr.refine'_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size l ≤ delta * size ml
refine' (mul_le_mul_left (by decide)).1 (le_trans this _)
case neg.intro.inr.refine'_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size ml + size mr < delta * size ml + delta * size ml
case neg.intro.inr.refine'_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size ml + size mr + 1 ≤ 2 * (delta * size ml)
rw [two_mul, Nat.succ_le_iff]
case neg.intro.inr.refine'_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size ml < delta * size ml
case neg.intro.inr.refine'_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size ml + size mr < delta * size ml + delta * size ml
refine' add_lt_add_of_lt_of_le _ mm₂
no goals
case neg.intro.inr.refine'_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size ml < delta * size ml
simpa using (mul_lt_mul_right ml0).2 (by decide : 1 < 3)
no goals
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ 0 < 2
decide
no goals
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ 1 < 3
decide
no goals
case neg.intro.inr.refine'_2
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size ml ≤ delta * size l
exact Nat.le_of_lt_succ (Valid'.node4L_lemma₁ lr₂ mr₂ mm₁)
no goals
case neg.intro.inr.refine'_3
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size mr ≤ delta * size r
exact Valid'.node4L_lemma₂ mr₂
no goals
case neg.intro.inr.refine'_4
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size r ≤ delta * size mr
exact Valid'.node4L_lemma₃ mr₁ mm₁
no goals
case neg.intro.inr.refine'_5
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size l + size ml + 1 ≤ delta * (size mr + size r + 1)
exact Valid'.node4L_lemma₄ lr₁ mr₂ mm₁
no goals
case neg.intro.inr.refine'_6
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < size (Ordnode.node s ml z mr)
l0 : 0 < size l
mr₁ : ratio * size r ≤ size ml + size mr + 1
lr₁ : delta * size l ≤ size ml + size mr + 1 + size r
lr₂ : 3 * (size ml + size mr + 1 + size r) ≤ 16 * size l + 9
mr₂ : size ml + size mr + 1 ≤ delta * size r
r0 : size r > 0
mm : ¬size ml + size mr ≤ 1
mm₁ : size ml ≤ delta * size mr
mm₂ : size mr ≤ delta * size ml
ml0 : size ml > 0
this : 2 * size l ≤ size ml + size mr + 1
⊢ size mr + size r + 1 ≤ delta * (size l + size ml + 1)
exact Valid'.node4L_lemma₅ lr₂ mr₁ mm₂