L : Language
L' : Language
⊢ ((sum fun i => lift (#Functions L i)) + sum fun i => lift (#Functions L' i)) +
      ((sum fun i => lift (#Relations L i)) + sum fun i => lift (#Relations L' i)) =
    ((sum fun i => lift (#Functions L i)) + sum fun i => lift (#Relations L i)) +
      ((sum fun i => lift (#Functions L' i)) + sum fun i => lift (#Relations L' i))
L : Language
L' : Language
⊢ card (Language.sum L L') = lift (card L) + lift (card L')
simp only [card_eq_card_functions_add_card_relations, card_functions_sum, card_relations_sum,
  sum_add_distrib', lift_add, lift_sum, lift_lift]
no goals
L : Language
L' : Language
⊢ ((sum fun i => lift (#Functions L i)) + sum fun i => lift (#Functions L' i)) +
      ((sum fun i => lift (#Relations L i)) + sum fun i => lift (#Relations L' i)) =
    ((sum fun i => lift (#Functions L i)) + sum fun i => lift (#Relations L i)) +
      ((sum fun i => lift (#Functions L' i)) + sum fun i => lift (#Relations L' i))
simp only [add_assoc, add_comm (Cardinal.sum fun i => (#L'.Functions i).lift)]