-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.balance'_lemma {α l l' r r'} (H1 : BalancedSz l' r')
    (H2 : Nat.dist (@size α l) l' ≤ 1 ∧ size r = r' ∨ Nat.dist (size r) r' ≤ 1 ∧ size l = l') :
    2 * @size α r ≤ 9 * size l + 5 ∨ size r ≤ 3

Proof state:
case inl.intro.inl
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
h : l' + r.size ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
exact le_trans (Nat.le_add_left _ _) (le_trans h (Nat.le_add_left _ _))

Result:
no goals

Proof state:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'
⊢ 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3

Tactic:
suffices @size α r ≤ 3 * (size l + 1) by omega

Result:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'
⊢ r.size ≤ 3 * (l.size + 1)

Proof state:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
rcases H2 with (⟨hl, rfl⟩ | ⟨hr, rfl⟩) <;> rcases H1 with (h | ⟨_, h₂⟩)

Result:
case inl.intro.inl
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
h : l' + r.size ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

case inl.intro.inr.intro
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
left✝ : l' ≤ delta * r.size
h₂ : r.size ≤ delta * l'
⊢ r.size ≤ 3 * (l.size + 1)

case inr.intro.inl
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

case inr.intro.inr.intro
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * (l.size + 1)

Proof state:
case inr.intro.inr.intro
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
rw [Nat.mul_succ]

Result:
case inr.intro.inr.intro
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * l.size + 3

Proof state:
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ 1 + 1 ≤ 3 * (l.size + 1)

Tactic:
omega

Result:
no goals

Proof state:
case inr.intro.inl
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
h : l.size + r' ≤ 1
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
exact
  le_trans (Nat.dist_tri_left' _ _)
    (le_trans (add_le_add hr (le_trans (Nat.le_add_left _ _) h)) (by omega))

Result:
no goals

Proof state:
case inl.intro.inr.intro
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
left✝ : l' ≤ delta * r.size
h₂ : r.size ≤ delta * l'
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
exact
  le_trans h₂
    (Nat.mul_le_mul_left _ <| le_trans (Nat.dist_tri_right _ _) (Nat.add_le_add_left hl _))

Result:
no goals

Proof state:
case inr.intro.inr.intro
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ r.size ≤ 3 * l.size + 3

Tactic:
exact le_trans (Nat.dist_tri_right' _ _) (add_le_add h₂ (le_trans hr (by decide)))

Result:
no goals

Proof state:
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'
this : r.size ≤ 3 * (l.size + 1)
⊢ 2 * r.size ≤ 9 * l.size + 5 ∨ r.size ≤ 3

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
left✝ : l.size ≤ delta * r'
h₂ : r' ≤ delta * l.size
⊢ 1 ≤ 3

Tactic:
decide

Result:
no goals