-- Mathlib/ModelTheory/Encoding.lean
theorem card_le : #(Σn, L.BoundedFormula α n) ≤
    max ℵ₀ (Cardinal.lift.{max u v} #α + Cardinal.lift.{u'} L.card)

Proof state:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
    ℵ₀ ⊔ lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)

Tactic:
rw [mk_sum, Term.card_sigma, mk_sum, ← add_eq_max le_rfl, mk_sum, mk_nat]

Result:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} (lift.{0, v} #((n : ℕ) × L.Relations n) + lift.{v, 0} ℵ₀)) ≤
    ℵ₀ ⊔ lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)

Proof state:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
      ℵ₀ ⊔ lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card) ∧
    ℵ₀ ≤ ℵ₀ ⊔ lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)

Tactic:
refine ⟨?_, le_max_left _ _⟩

Result:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
    ℵ₀ ⊔ lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)

Proof state:
L : Language
α : Type u'
⊢ #((n : ℕ) × L.BoundedFormula α n) ≤ ℵ₀ ⊔ (lift.{max u v, u'} #α + lift.{u', max u v} L.card)

Tactic:
refine lift_le.1 (BoundedFormula.encoding.card_le_card_list.trans ?_)

Result:
L : Language
α : Type u'
⊢ lift.{max (max u' v) u, max (max u' v) u} #(List BoundedFormula.encoding.Γ) ≤
    lift.{max (max u u') v, max (max u u') v} (ℵ₀ ⊔ (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Proof state:
L : Language
α : Type u'
⊢ ℵ₀ + (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 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]

Result:
no goals

Proof state:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v}
      (lift.{v, max u u'} (ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))) +
        lift.{max u u', v} (lift.{0, v} #((n : ℕ) × L.Relations n) + lift.{v, 0} ℵ₀)) ≤
    ℵ₀ ⊔ lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)

Tactic:
simp only [lift_add, lift_lift, lift_aleph0]

Result:
L : Language
α : Type u'
⊢ ℵ₀ + (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 u' (max u u') v, max u v} L.card)

Proof state:
L : Language
α : Type u'
⊢ lift.{max (max u' v) u, max (max u' v) u} #(List BoundedFormula.encoding.Γ) ≤
    lift.{max (max u u') v, max (max u u') v} (ℵ₀ ⊔ (lift.{max u v, u'} #α + lift.{u', max u v} L.card))

Tactic:
rw [encoding_Γ, mk_list_eq_max_mk_aleph0, lift_max, lift_aleph0, lift_max, lift_aleph0,
  max_le_iff]

Result:
L : Language
α : Type u'
⊢ lift.{max (max u u') v, max (max u u') v} #((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) ≤
      ℵ₀ ⊔ lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card) ∧
    ℵ₀ ≤ ℵ₀ ⊔ lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card)