case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r'
⊢ size l = 0 → size r ≤ 1

case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r'
⊢ 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r'
⊢ balanceL l x r = balance' l x r
rw [← balance_eq_balance' hl hr sl sr, balanceL_eq_balance sl sr]
case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r'
l0 : size l = 0
⊢ size r ≤ 1
case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r'
⊢ size l = 0 → size r ≤ 1
intro l0
case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' 0 ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz 0 r'
l0 : size l = 0
⊢ size r ≤ 1
case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r'
l0 : size l = 0
⊢ size r ≤ 1
rw [l0] at H
case H1.inl.intro.intro.inl.refl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l0 : size l = 0
H : BalancedSz 0 (size r)
⊢ size r ≤ 1

case H1.inr.intro.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l0 : size l = 0
r' : ℕ
e : Raised (size r) r'
H : BalancedSz 0 r'
⊢ size r ≤ 1
case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' 0 ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz 0 r'
l0 : size l = 0
⊢ size r ≤ 1
rcases H with (⟨_, ⟨⟨⟩⟩ | ⟨⟨⟩⟩, H⟩ | ⟨r', e, H⟩)
no goals
case H1.inr.intro.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l0 : size l = 0
r' : ℕ
e : Raised (size r) r'
H : BalancedSz 0 r'
⊢ size r ≤ 1
exact le_trans (raised_iff.1 e).1 (balancedSz_zero.1 H.symm)
no goals
case H1.inl.intro.intro.inl.refl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l0 : size l = 0
H : BalancedSz 0 (size r)
⊢ size r ≤ 1
exact balancedSz_zero.1 H.symm
case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r'
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
⊢ size r ≤ delta * size l
case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r'
⊢ 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
intro l1 _
case H2.inl.intro.intro.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
l' : ℕ
e : Raised l' (size l)
H : l' + size r ≤ 1
⊢ size r ≤ delta * size l

case H2.inl.intro.intro.inr.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
l' : ℕ
e : Raised l' (size l)
left✝ : l' ≤ delta * size r
H₂ : size r ≤ delta * l'
⊢ size r ≤ delta * size l

case H2.inr.intro.intro.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
r' : ℕ
e : Raised (size r) r'
H : size l + r' ≤ 1
⊢ size r ≤ delta * size l

case H2.inr.intro.intro.inr.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
r' : ℕ
e : Raised (size r) r'
left✝ : size l ≤ delta * r'
H₂ : r' ≤ delta * size l
⊢ size r ≤ delta * size l
case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r'
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
⊢ size r ≤ delta * size l
rcases H with (⟨l', e, H | ⟨_, H₂⟩⟩ | ⟨r', e, H | ⟨_, H₂⟩⟩)
no goals
case H2.inl.intro.intro.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
l' : ℕ
e : Raised l' (size l)
H : l' + size r ≤ 1
⊢ size r ≤ delta * size l
exact le_trans (le_trans (Nat.le_add_left _ _) H) (mul_pos (by decide) l1 : (0 : ℕ) < _)
no goals
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
l' : ℕ
e : Raised l' (size l)
H : l' + size r ≤ 1
⊢ 0 < delta
decide
no goals
case H2.inl.intro.intro.inr.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
l' : ℕ
e : Raised l' (size l)
left✝ : l' ≤ delta * size r
H₂ : size r ≤ delta * l'
⊢ size r ≤ delta * size l
exact le_trans H₂ (Nat.mul_le_mul_left _ (raised_iff.1 e).1)
case H2.inr.intro.intro.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
r' : ℕ
e : Raised (size r) r'
H : size l + r' ≤ 1
left✝ : size r ≤ r'
right✝ : r' ≤ size r + 1
⊢ size r ≤ delta * size l
case H2.inr.intro.intro.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
r' : ℕ
e : Raised (size r) r'
H : size l + r' ≤ 1
⊢ size r ≤ delta * size l
cases raised_iff.1 e
case H2.inr.intro.intro.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
r' : ℕ
e : Raised (size r) r'
H : size l + r' ≤ 1
left✝ : size r ≤ r'
right✝ : r' ≤ size r + 1
⊢ size r ≤ 3 * size l
case H2.inr.intro.intro.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
r' : ℕ
e : Raised (size r) r'
H : size l + r' ≤ 1
left✝ : size r ≤ r'
right✝ : r' ≤ size r + 1
⊢ size r ≤ delta * size l
unfold delta
no goals
case H2.inr.intro.intro.inl.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
r' : ℕ
e : Raised (size r) r'
H : size l + r' ≤ 1
left✝ : size r ≤ r'
right✝ : r' ≤ size r + 1
⊢ size r ≤ 3 * size l
linarith
no goals
case H2.inr.intro.intro.inr.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Balanced l
hr : Balanced r
sl : Sized l
sr : Sized r
l1 : 1 ≤ size l
a✝ : 1 ≤ size r
r' : ℕ
e : Raised (size r) r'
left✝ : size l ≤ delta * r'
H₂ : r' ≤ delta * size l
⊢ size r ≤ delta * size l
exact le_trans (raised_iff.1 e).1 H₂