L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ((sum fun i => lift (#Functions L i)) + sum fun i => lift (#BoundedFormula L Empty (i + 1))) =
    sum fun i => #BoundedFormula L Empty (i + 1)
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (#(n : ℕ) × Functions (Language.sum L (skolem₁ L)) n) = (#(n : ℕ) × BoundedFormula L Empty (n + 1))
simp only [card_functions_sum, skolem₁_Functions, mk_sigma, sum_add_distrib']
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ((sum fun i => lift (#Functions L i)) + sum fun i => #BoundedFormula L Empty (i + 1)) =
    sum fun i => #BoundedFormula L Empty (i + 1)
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ((sum fun i => lift (#Functions L i)) + sum fun i => lift (#BoundedFormula L Empty (i + 1))) =
    sum fun i => #BoundedFormula L Empty (i + 1)
conv_lhs => enter [2, 1, i]; rw [lift_id'.{u, v}]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (sum fun i => lift (#Functions L i)) ≤ sum fun i => #BoundedFormula L Empty (i + 1)

L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ℵ₀ ≤ sum fun i => #BoundedFormula L Empty (i + 1)
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ((sum fun i => lift (#Functions L i)) + sum fun i => #BoundedFormula L Empty (i + 1)) =
    sum fun i => #BoundedFormula L Empty (i + 1)
rw [add_comm, add_eq_max, max_eq_left]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
⊢ lift (#Functions L n) ≤ (#BoundedFormula L Empty (n + 1))
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ (sum fun i => lift (#Functions L i)) ≤ sum fun i => #BoundedFormula L Empty (i + 1)
refine' sum_le_sum _ _ fun n => _
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
⊢ Nonempty (Functions L n ↪ BoundedFormula L Empty (n + 1))
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
⊢ lift (#Functions L n) ≤ (#BoundedFormula L Empty (n + 1))
rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{_, _, v}]
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
f g : Functions L n
h : (fun f => func f default =' func f default) f = (fun f => func f default =' func f default) g
⊢ f = g
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
⊢ Nonempty (Functions L n ↪ BoundedFormula L Empty (n + 1))
refine' ⟨⟨fun f => (func f default).bdEqual (func f default), fun f g h => _⟩⟩
case refl
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
f : Functions L n
⊢ f = f
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
f g : Functions L n
h : (fun f => func f default =' func f default) f = (fun f => func f default =' func f default) g
⊢ f = g
rcases h with ⟨rfl, ⟨rfl⟩⟩
no goals
case refl
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
n : ℕ
f : Functions L n
⊢ f = f
rfl
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ℵ₀ ≤ (#(i : ℕ) × BoundedFormula L Empty (i + 1))
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ℵ₀ ≤ sum fun i => #BoundedFormula L Empty (i + 1)
rw [← mk_sigma]
no goals
L : Language
M : Type w
inst✝¹ : Nonempty M
inst✝ : Structure L M
⊢ ℵ₀ ≤ (#(i : ℕ) × BoundedFormula L Empty (i + 1))
exact infinite_iff.1 (Infinite.of_injective (fun n => ⟨n, ⊥⟩) fun x y xy =>
  (Sigma.mk.inj_iff.1 xy).1)