-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
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)
⊢ ℵ₀ + (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)
have 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)
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]