case inl.intro.inl
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : Nat.dist (size l) l' ≤ 1
h : l' + size r ≤ 1
⊢ size r ≤ 3 * (size l + 1)

case inl.intro.inr.intro
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : Nat.dist (size l) l' ≤ 1
left✝ : l' ≤ delta * size r
h₂ : size r ≤ delta * l'
⊢ size r ≤ 3 * (size l + 1)

case inr.intro.inl
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l r : Ordnode α
r' : ℕ
hr : Nat.dist (size r) r' ≤ 1
h : size l + r' ≤ 1
⊢ size r ≤ 3 * (size l + 1)

case inr.intro.inr.intro
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l r : Ordnode α
r' : ℕ
hr : Nat.dist (size r) r' ≤ 1
left✝ : size l ≤ delta * r'
h₂ : r' ≤ delta * size l
⊢ size r ≤ 3 * (size l + 1)
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
⊢ size r ≤ 3 * (size l + 1)
rcases H2 with (⟨hl, rfl⟩ | ⟨hr, rfl⟩) <;> rcases H1 with (h | ⟨_, h₂⟩)
case inl
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
l0 : size l = 0
⊢ 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3

case inr
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
l0 : size l > 0
⊢ 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
⊢ 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
cases' Nat.eq_zero_or_pos (size l) with l0 l0
case inr
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
l0 : 1 ≤ size l
⊢ 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
case inr
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
l0 : size l > 0
⊢ 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
change 1 ≤ _ at l0
case inr.h
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
l0 : 1 ≤ size l
⊢ 2 * size r ≤ 9 * size l + 5
case inr
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
l0 : 1 ≤ size l
⊢ 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
apply Or.inl
no goals
case inr.h
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
l0 : 1 ≤ size l
⊢ 2 * size r ≤ 9 * size l + 5
linarith
case inl.h
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
l0 : size l = 0
⊢ size r ≤ 3
case inl
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
l0 : size l = 0
⊢ 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
apply Or.inr
no goals
case inl.h
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : Nat.dist (size l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l'
this : size r ≤ 3 * (size l + 1)
l0 : size l = 0
⊢ size r ≤ 3
rwa [l0] at this
no goals
case inl.intro.inl
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : Nat.dist (size l) l' ≤ 1
h : l' + size r ≤ 1
⊢ size r ≤ 3 * (size l + 1)
exact le_trans (Nat.le_add_left _ _) (le_trans h (Nat.le_add_left _ _))
no goals
case inl.intro.inr.intro
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : Nat.dist (size l) l' ≤ 1
left✝ : l' ≤ delta * size r
h₂ : size r ≤ delta * l'
⊢ size r ≤ 3 * (size l + 1)
exact
  le_trans h₂
    (Nat.mul_le_mul_left _ <| le_trans (Nat.dist_tri_right _ _) (Nat.add_le_add_left hl _))
no goals
case inr.intro.inl
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l r : Ordnode α
r' : ℕ
hr : Nat.dist (size r) r' ≤ 1
h : size l + r' ≤ 1
⊢ size r ≤ 3 * (size l + 1)
exact
  le_trans (Nat.dist_tri_left' _ _)
    (le_trans (add_le_add hr (le_trans (Nat.le_add_left _ _) h)) (by linarith))
no goals
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l r : Ordnode α
r' : ℕ
hr : Nat.dist (size r) r' ≤ 1
h : size l + r' ≤ 1
⊢ 1 + 1 ≤ 3 * (size l + 1)
linarith
case inr.intro.inr.intro
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l r : Ordnode α
r' : ℕ
hr : Nat.dist (size r) r' ≤ 1
left✝ : size l ≤ delta * r'
h₂ : r' ≤ delta * size l
⊢ size r ≤ 3 * size l + 3
case inr.intro.inr.intro
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l r : Ordnode α
r' : ℕ
hr : Nat.dist (size r) r' ≤ 1
left✝ : size l ≤ delta * r'
h₂ : r' ≤ delta * size l
⊢ size r ≤ 3 * (size l + 1)
rw [Nat.mul_succ]
no goals
case inr.intro.inr.intro
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l r : Ordnode α
r' : ℕ
hr : Nat.dist (size r) r' ≤ 1
left✝ : size l ≤ delta * r'
h₂ : r' ≤ delta * size l
⊢ size r ≤ 3 * size l + 3
exact le_trans (Nat.dist_tri_right' _ _) (add_le_add h₂ (le_trans hr (by decide)))
no goals
α✝ : Type ?u.331855
inst✝ : Preorder α✝
α : Type u_1
l r : Ordnode α
r' : ℕ
hr : Nat.dist (size r) r' ≤ 1
left✝ : size l ≤ delta * r'
h₂ : r' ≤ delta * size l
⊢ 1 ≤ 3
decide