α : Type u_1
l r : Ordnode α
H : (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r'
⊢ (∃ l', Raised l' (size r) ∧ BalancedSz l' (size l)) ∨ ∃ r', Raised (size l) r' ∧ BalancedSz (size r) r'
α : Type u_1
l r : Ordnode α
H : (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r'
⊢ (∃ l', Raised l' (size (dual r)) ∧ BalancedSz l' (size (dual l))) ∨
    ∃ r', Raised (size (dual l)) r' ∧ BalancedSz (size (dual r)) r'
rw [size_dual, size_dual]
no goals
α : Type u_1
l r : Ordnode α
H : (∃ l', Raised (size l) l' ∧ BalancedSz l' (size r)) ∨ ∃ r', Raised r' (size r) ∧ BalancedSz (size l) r'
⊢ (∃ l', Raised l' (size r) ∧ BalancedSz l' (size l)) ∨ ∃ r', Raised (size l) r' ∧ BalancedSz (size r) r'
exact
  H.symm.imp (Exists.imp fun _ => And.imp_right BalancedSz.symm)
    (Exists.imp fun _ => And.imp_right BalancedSz.symm)