-- Mathlib/ModelTheory/Encoding.lean
theorem card_sigma : #(Σn, L.Term (α ⊕ (Fin n))) = max ℵ₀ #(α ⊕ (Σi, L.Functions i))

Proof state:
case refine_2.refine_2
L : Language
α : Type u'
⊢ Function.Injective (Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩)

Tactic:
rintro (a | a) (b | b) h

Result:
case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h :
  Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inl a = Sum.inl b

case refine_2.refine_2.inl.inr
L : Language
α : Type u'
a : α
b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inl a = Sum.inr b

case refine_2.refine_2.inr.inl
L : Language
α : Type u'
a : (i : ℕ) × L.Functions i
b : α
h :
  Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inr a = Sum.inl b

case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inr a = Sum.inr b

Proof state:
case refine_2
L : Language
α : Type u'
⊢ Infinite ((n : ℕ) × L.Term (α ⊕ Fin n)) ∧ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
refine ⟨Infinite.of_injective (fun i => ⟨i + 1, var (Sum.inr i)⟩) fun i j ij => ?_, ?_⟩

Result:
case refine_2.refine_1
L : Language
α : Type u'
i j : ℕ
ij : (fun i => ⟨i + 1, var (Sum.inr ↑i)⟩) i = (fun i => ⟨i + 1, var (Sum.inr ↑i)⟩) j
⊢ i = j

case refine_2.refine_2
L : Language
α : Type u'
⊢ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Proof state:
case refine_2.refine_2.inr.inl
L : Language
α : Type u'
a : (i : ℕ) × L.Functions i
b : α
h :
  Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inr a = Sum.inl b

Tactic:
simp only [Sum.elim_inr, Sum.elim_inl, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h

Result:
no goals

Proof state:
case refine_2.refine_2.inl.inr
L : Language
α : Type u'
a : α
b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inl a = Sum.inr b

Tactic:
simp only [Sum.elim_inl, Sum.elim_inr, Sigma.mk.inj_iff, false_and, reduceCtorEq] at h

Result:
no goals

Proof state:
case refine_1
L : Language
α : Type u'
⊢ 1 ≤ ⨆ i, #(L.Term (α ⊕ Fin i))

Tactic:
refine _root_.trans ?_ (le_ciSup (bddAbove_range _) 1)

Result:
case refine_1
L : Language
α : Type u'
⊢ 1 ≤ #(L.Term (α ⊕ Fin 1))

Proof state:
case refine_1
L : Language
α : Type u'
⊢ #((n : ℕ) × L.Term (α ⊕ Fin n)) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
rw [mk_sigma]

Result:
case refine_1
L : Language
α : Type u'
⊢ (Cardinal.sum fun i => #(L.Term (α ⊕ Fin i))) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

Proof state:
case refine_2.refine_1.refl
L : Language
α : Type u'
i : ℕ
⊢ i = i

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2.refine_1
L : Language
α : Type u'
i j : ℕ
ij : (fun i => ⟨i + 1, var (Sum.inr ↑i)⟩) i = (fun i => ⟨i + 1, var (Sum.inr ↑i)⟩) j
⊢ i = j

Tactic:
cases ij

Result:
case refine_2.refine_1.refl
L : Language
α : Type u'
i : ℕ
⊢ i = i

Proof state:
case refine_2
L : Language
α : Type u'
⊢ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
rw [max_le_iff, ← infinite_iff]

Result:
case refine_2
L : Language
α : Type u'
⊢ Infinite ((n : ℕ) × L.Term (α ⊕ Fin n)) ∧ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Proof state:
case refine_1
L : Language
α : Type u'
⊢ lift.{max u u', 0} #ℕ * ⨆ i, #(L.Term (α ⊕ Fin i)) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
rw [mk_nat, lift_aleph0, mul_eq_max_of_aleph0_le_left le_rfl, max_le_iff,
  ciSup_le_iff' (bddAbove_range _)]

Result:
case refine_1
L : Language
α : Type u'
⊢ ℵ₀ ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i) ∧ ∀ (i : ℕ), #(L.Term (α ⊕ Fin i)) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0

Proof state:
case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h : a = b
⊢ Sum.inl a = Sum.inl b

Tactic:
rw [h]

Result:
no goals

Proof state:
case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h : a.fst = b.fst ∧ HEq a.snd b.snd ∧ HEq (fun x => var (Sum.inr 0)) fun x => var (Sum.inr 0)
⊢ Sum.inr a = Sum.inr b

Tactic:
rw [Sigma.ext_iff.2 ⟨h.1, h.2.1⟩]

Result:
no goals

Proof state:
L : Language
α : Type u'
⊢ #((n : ℕ) × L.Term (α ⊕ Fin n)) = ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
L : Language
α : Type u'
⊢ #((n : ℕ) × L.Term (α ⊕ Fin n)) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

case refine_2
L : Language
α : Type u'
⊢ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Proof state:
case refine_1
L : Language
α : Type u'
⊢ Nonempty (L.Term (α ⊕ Fin 1))

Tactic:
exact ⟨var (Sum.inr 0)⟩

Result:
no goals

Proof state:
case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inr a) =
    Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inr b)
⊢ Sum.inr a = Sum.inr b

Tactic:
simp only [Sum.elim_inr, Sigma.mk.inj_iff, heq_eq_eq, func.injEq, true_and] at h

Result:
case refine_2.refine_2.inr.inr
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h : a.fst = b.fst ∧ HEq a.snd b.snd ∧ HEq (fun x => var (Sum.inr 0)) fun x => var (Sum.inr 0)
⊢ Sum.inr a = Sum.inr b

Proof state:
case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h :
  Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inl a) =
    Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) (fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩) (Sum.inl b)
⊢ Sum.inl a = Sum.inl b

Tactic:
simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and]
  at h

Result:
case refine_2.refine_2.inl.inl
L : Language
α : Type u'
a b : α
h : a = b
⊢ Sum.inl a = Sum.inl b

Proof state:
case refine_2.refine_2
L : Language
α : Type u'
⊢ Nonempty (α ⊕ (i : ℕ) × L.Functions i ↪ (n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
refine ⟨⟨Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩)
  fun F => ⟨1, func F.2 fun _ => var (Sum.inr 0)⟩, ?_⟩⟩

Result:
case refine_2.refine_2
L : Language
α : Type u'
⊢ Function.Injective (Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩) fun F => ⟨1, func F.snd fun x => var (Sum.inr 0)⟩)

Proof state:
case refine_1
L : Language
α : Type u'
⊢ (Cardinal.sum fun i => #(L.Term (α ⊕ Fin i))) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)

Tactic:
refine (sum_le_iSup_lift _).trans ?_

Result:
case refine_1
L : Language
α : Type u'
⊢ lift.{max u u', 0} #ℕ * ⨆ i, #(L.Term (α ⊕ Fin i)) ≤ ℵ₀ ⊔ #(α ⊕ (i : ℕ) × L.Functions i)