English
If l and r are Balanced and sized, and H describes how l or r can grow, then balanceL equals balance'.
Русский
Если l и r сбалансированы и имеют размеры, и задано условие роста H, то balanceL = balance'.
LaTeX
$$hl.Balanced → hr.Balanced → sl.Sized → sr.Sized → (∃ 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$$
Lean4
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 :=
by
rw [← balance_eq_balance' hl hr sl sr, balanceL_eq_balance sl sr]
· intro l0; rw [l0] at H
rcases H with (⟨_, ⟨⟨⟩⟩ | ⟨⟨⟩⟩, H⟩ | ⟨r', e, H⟩)
· exact balancedSz_zero.1 H.symm
exact le_trans (raised_iff.1 e).1 (balancedSz_zero.1 H.symm)
· intro l1 _
rcases H with (⟨l', e, H | ⟨_, H₂⟩⟩ | ⟨r', e, H | ⟨_, H₂⟩⟩)
· exact le_trans (le_trans (Nat.le_add_left _ _) H) (mul_pos (by decide) l1 : (0 : ℕ) < _)
· exact le_trans H₂ (Nat.mul_le_mul_left _ (raised_iff.1 e).1)
· cases raised_iff.1 e; unfold delta; cutsat
· exact le_trans (raised_iff.1 e).1 H₂
