English
Under preconditions on sizes and balances, balanceR_aux yields a valid balance of the right subtree and preserves auxiliary size relations.
Русский
При предпосылках о размерах и балансе, balanceR_aux обеспечивает корректное равно распределение правого поддерева и сохраняет размерные отношения.
LaTeX
$$$\\forall l\\, x\\, r\\, o_1\\, o_2,\\; \\mathrm{Valid'} o_1 l x \\to \\mathrm{Valid'} x r o_2 \\to \\cdots \\Rightarrow \\mathrm{Valid'} o_1 (l.balanceR x r) o_2$$$
Lean4
theorem balanceL {l} {x : α} {r o₁ o₂} (hl : Valid' o₁ l x) (hr : Valid' x r o₂)
(H : (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r') :
Valid' o₁ (@balanceL α l x r) o₂ :=
by
rw [balanceL_eq_balance' hl.3 hr.3 hl.2 hr.2 H]
refine hl.balance' hr ?_
rcases H with (⟨l', e, H⟩ | ⟨r', e, H⟩)
· exact ⟨_, _, H, Or.inl ⟨e.dist_le', rfl⟩⟩
· exact ⟨_, _, H, Or.inr ⟨e.dist_le, rfl⟩⟩
