-- Mathlib/Data/Ordmap/Ordset.lean
theorem balanceL_eq_balance' {l x r} (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

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

Tactic:
rw [l0] at H

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

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
l' : ℕ
e : Raised l' l.size
H : l' + r.size ≤ 1
⊢ 0 < delta

Tactic:
decide

Result:
no goals

Proof state:
case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ 1 ≤ l.size → 1 ≤ r.size → r.size ≤ delta * l.size

Tactic:
intro l1 _

Result:
case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
⊢ r.size ≤ delta * l.size

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

Tactic:
rcases H with (⟨_, ⟨⟨⟩⟩ | ⟨⟨⟩⟩, H⟩ | ⟨r', e, H⟩)

Result:
case H1.inl.intro.intro.inl.refl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l0 : l.size = 0
H : BalancedSz 0 r.size
⊢ r.size ≤ 1

case H1.inr.intro.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l0 : l.size = 0
r' : ℕ
e : Raised r.size r'
H : BalancedSz 0 r'
⊢ r.size ≤ 1

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

Tactic:
exact le_trans (le_trans (Nat.le_add_left _ _) H) (mul_pos (by decide) l1 : (0 : ℕ) < _)

Result:
no goals

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

Tactic:
exact le_trans (raised_iff.1 e).1 H₂

Result:
no goals

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ l.balanceL x r = l.balance' x r

Tactic:
rw [← balance_eq_balance' hl hr sl sr, balanceL_eq_balance sl sr]

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

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

Proof state:
case H2
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
l1 : 1 ≤ l.size
a✝ : 1 ≤ r.size
⊢ r.size ≤ delta * l.size

Tactic:
rcases H with (⟨l', e, H | ⟨_, H₂⟩⟩ | ⟨r', e, H | ⟨_, H₂⟩⟩)

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

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

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

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

Proof state:
case H1.inl.intro.intro.inl.refl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l0 : l.size = 0
H : BalancedSz 0 r.size
⊢ r.size ≤ 1

Tactic:
exact balancedSz_zero.1 H.symm

Result:
no goals

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

Tactic:
exact le_trans H₂ (Nat.mul_le_mul_left _ (raised_iff.1 e).1)

Result:
no goals

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

Tactic:
unfold delta

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

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

Tactic:
omega

Result:
no goals

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

Tactic:
cases raised_iff.1 e

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

Proof state:
case H1.inr.intro.intro
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
l0 : l.size = 0
r' : ℕ
e : Raised r.size r'
H : BalancedSz 0 r'
⊢ r.size ≤ 1

Tactic:
exact le_trans (raised_iff.1 e).1 (balancedSz_zero.1 H.symm)

Result:
no goals