-- Module: Mathlib.ModelTheory.Encoding
Goal:
L : Language
α : Type u'
rw :
  ℵ₀ + (lift.{max (max u v) (max u u') v, u'} #α + lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i)) +
        lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n) +
      ℵ₀ ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₁ :
  ℵ₀ +
      (ℵ₀ +
          (lift.{max (max u v) (max u u') v, u'} #α +
            lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i)) +
        lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₂ :
  ℵ₀ +
        (ℵ₀ +
          (lift.{max (max u v) (max u u') v, u'} #α +
            lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i))) +
      lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₃ :
  ℵ₀ + ℵ₀ +
        (lift.{max (max u v) (max u u') v, u'} #α + lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i)) +
      lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₄ :
  ℵ₀ + (lift.{max (max u v) (max u u') v, u'} #α + lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i)) +
      lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₅ :
  ℵ₀ +
      (lift.{max (max u v) (max u u') v, u'} #α + lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
        lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₆ :
  max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α + lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
        lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₇ :
  max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₈ :
  max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} #L.Symbols)
rw₉ :
  max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        lift.{max u' (max u u') v, max u v} #(Sum.{u, v} ((l : ℕ) × L.Functions l) ((l : ℕ) × L.Relations l)))
rw₁₀ :
  max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        lift.{max u' (max u u') v, max u v}
          (lift.{v, u} #((l : ℕ) × L.Functions l) + lift.{u, v} #((l : ℕ) × L.Relations l)))
rw₁₁ :
  max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u u') v, max u v} (lift.{v, u} #((l : ℕ) × L.Functions l)) +
          lift.{max (max u u') v, max u v} (lift.{u, v} #((l : ℕ) × L.Relations l))))
rw₁₂ :
  max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u u') v, u} #((l : ℕ) × L.Functions l) +
          lift.{max (max u u') v, max u v} (lift.{u, v} #((l : ℕ) × L.Relations l))))
rw₁₃ rw₁₄ :
  max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n))) ≤
    max ℵ₀
      (lift.{max (max u v) (max u u') v, u'} #α +
        (lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i) +
          lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n)))
⊢ ℵ₀ + (lift.{max (max u v) (max u u') v, u'} #α + lift.{max (max u' v) (max u u') v, u} #((i : ℕ) × L.Functions i)) +
      (lift.{max (max u u') v, v} #((n : ℕ) × L.Relations n) + ℵ₀) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)

Tactic:
rw [← add_assoc, add_comm, ← add_assoc, ← add_assoc, aleph0_add_aleph0, add_assoc,
    add_eq_max le_rfl, add_assoc, card, Symbols, mk_sum, lift_add, lift_lift, lift_lift]

Premises used: le_rfl, FirstOrder.Language.card, Cardinal.lift_lift, add_assoc, add_comm, Cardinal.add_eq_max, Cardinal.aleph0_add_aleph0, Cardinal.mk_sum, FirstOrder.Language.Symbols, Cardinal.lift_add