L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift (#List BoundedFormula.encoding.Γ) ≤ lift (max ℵ₀ (lift (#α) + lift (card L)))
L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ (#(n : ℕ) × BoundedFormula L α n) ≤ max ℵ₀ (lift (#α) + lift (card L))
refine' lift_le.1 (BoundedFormula.encoding.card_le_card_list.trans _)
L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift (#(k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ) ≤ max ℵ₀ (lift (lift (#α) + lift (card L))) ∧
    ℵ₀ ≤ max ℵ₀ (lift (lift (#α) + lift (card L)))
L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift (#List BoundedFormula.encoding.Γ) ≤ lift (max ℵ₀ (lift (#α) + lift (card L)))
rw [encoding_Γ, mk_list_eq_max_mk_aleph0, lift_max, lift_aleph0, lift_max, lift_aleph0,
  max_le_iff]
L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift (#(k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ) ≤ max ℵ₀ (lift (lift (#α) + lift (card L)))
L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift (#(k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ) ≤ max ℵ₀ (lift (lift (#α) + lift (card L))) ∧
    ℵ₀ ≤ max ℵ₀ (lift (lift (#α) + lift (card L)))
refine' ⟨_, le_max_left _ _⟩
L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift (lift (ℵ₀ + (lift (#α) + lift (#(i : ℕ) × Functions L i))) + lift (lift (#(n : ℕ) × Relations L n) + lift ℵ₀)) ≤
    max ℵ₀ (lift (lift (#α) + lift (card L)))
L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift (#(k : ℕ) × Term L (α ⊕ Fin k) ⊕ (n : ℕ) × Relations L n ⊕ ℕ) ≤ max ℵ₀ (lift (lift (#α) + lift (card L)))
rw [mk_sum, Term.card_sigma, mk_sum, ← add_eq_max le_rfl, mk_sum, mk_nat]
L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ ℵ₀ + (lift (#α) + lift (#(i : ℕ) × Functions L i)) + (lift (#(n : ℕ) × Relations L n) + ℵ₀) ≤
    max ℵ₀ (lift (#α) + lift (card L))
L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ lift (lift (ℵ₀ + (lift (#α) + lift (#(i : ℕ) × Functions L i))) + lift (lift (#(n : ℕ) × Relations L n) + lift ℵ₀)) ≤
    max ℵ₀ (lift (lift (#α) + lift (card L)))
simp only [lift_add, lift_lift, lift_aleph0]
no goals
L : Language
M : Type w
N : Type ?u.158067
P : Type ?u.158070
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
⊢ ℵ₀ + (lift (#α) + lift (#(i : ℕ) × Functions L i)) + (lift (#(n : ℕ) × Relations L n) + ℵ₀) ≤
    max ℵ₀ (lift (#α) + lift (card L))
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]