English
The dual of balanceL equals balanceR on the duals: dual (balanceL l x r) = balanceR (dual r) x (dual l).
Русский
Дуал balanceL равен balanceR на дуалах: dual(balanceL(l,x,r)) = balanceR(dual(r)) x (dual(l)).
LaTeX
$$$$\operatorname{dual}(\operatorname{balanceL}(l, x, r)) = \operatorname{balanceR}(\operatorname{dual}(r)) \ x \ (\operatorname{dual}(l)).$$$$
Lean4
theorem dual_balanceL (l : Ordnode α) (x : α) (r : Ordnode α) : dual (balanceL l x r) = balanceR (dual r) x (dual l) :=
by
unfold balanceL balanceR
obtain - | ⟨rs, rl, rx, rr⟩ := r
· obtain - | ⟨ls, ll, lx, lr⟩ := l; · rfl
obtain - | ⟨lls, lll, llx, llr⟩ := ll <;> obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr <;> dsimp only [dual, id] <;>
try rfl
split_ifs with h <;> repeat simp [add_comm]
· obtain - | ⟨ls, ll, lx, lr⟩ := l; · rfl
dsimp only [dual, id]
split_ifs; swap; · simp [add_comm]
obtain - | ⟨lls, lll, llx, llr⟩ := ll <;> obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr <;> try rfl
dsimp only [dual, id]
split_ifs with h <;> simp [add_comm]
