awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₂ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₃ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₄ :
  lift.{u, u'} (lift.{u', 0} #(Fin i) + lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₅ : lift.{u, u'} (lift.{u', 0} #(Fin i)) + lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
  ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₂ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₃ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₄ :
  lift.{u, u'} (lift.{u', 0} #(Fin i) + lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₅ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₆ : lift.{u, u'} (lift.{u', 0} #(Fin i)) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
  ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₂ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₃ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₄ :
  lift.{u, u'} (lift.{u', 0} #(Fin i) + lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₅ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₆ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₇ : lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
  ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₂ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₃ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₄ :
  lift.{u, u'} (lift.{u', 0} #(Fin i) + lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₅ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₆ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₇ :
  lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₈ : lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
  ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₂ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₃ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₄ :
  lift.{u, u'} (lift.{u', 0} #(Fin i) + lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₅ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₆ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₇ :
  lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₈ :
  lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₉ : lift.{max u' u, 0} (↑i : Cardinal.{0}) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
  ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₂ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₃ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₄ :
  lift.{u, u'} (lift.{u', 0} #(Fin i) + lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₅ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₆ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₇ :
  lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₈ :
  lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₉ :
  lift.{max u' u, 0} (↑i : Cardinal.{0}) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₁₀ : (↑i : Cardinal.{max u u'}) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
  ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₂ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₃ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₄ :
  lift.{u, u'} (lift.{u', 0} #(Fin i) + lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₅ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₆ :
  lift.{u, u'} (lift.{u', 0} #(Fin i)) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₇ :
  lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} (lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₈ :
  lift.{max u' u, 0} #(Fin i) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₉ :
  lift.{max u' u, 0} (↑i : Cardinal.{0}) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
refine_1₁₀ :
  (↑i : Cardinal.{max u u'}) + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₁₁ : ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i)) ≤
  ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ Ne (α := Cardinal.{max u u'}) (⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i))) 0
have refine_1 : LE.le (α := Cardinal.{max u u'}) 1 (⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)))
Tactic: rw [← Cardinal.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ LE.le (α := Cardinal.{max u u'}) 1 (⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)))
have refine_1 : 1 ≤ #(Term.{u, v, u'} L (α ⊕ Fin 1))
Tactic: refine _root_.trans ?_ (le_ciSup bddAbove_of_small 1)
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ 1 ≤ #(Term.{u, v, u'} L (α ⊕ Fin 1))
have refine_1 : Nonempty (Term.{u, v, u'} L (α ⊕ Fin 1))
Tactic: rw [Cardinal.one_le_iff_ne_zero, mk_ne_zero_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
have refine_2 : Infinite ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ∧
  #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
Tactic: rw [max_le_iff, ← infinite_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ Infinite ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ∧
    #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
have refine_2 : ∀ (i j : ℕ)
  (ij :
    Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
      ((fun (i : ℕ) ↦
          (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) (i + 1) (var (Sum.inr (last i))) :
            (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
        i)
      ((fun (i : ℕ) ↦
          (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) (i + 1) (var (Sum.inr (last i))) :
            (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
        j)),
  i = j
Tactic: refine ⟨Infinite.of_injective
        (fun i => ⟨i + 1, var (Sum.inr (last i))⟩) fun i j ij => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
refine_2 :
  ∀ (i j : ℕ)
    (ij :
      Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
        ((fun (i : ℕ) ↦
            (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) (i + 1) (var (Sum.inr (last i))) :
              (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
          i)
        ((fun (i : ℕ) ↦
            (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) (i + 1) (var (Sum.inr (last i))) :
              (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
          j)),
    i = j
⊢ Infinite ((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ∧
    #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
have refine_2₁ : #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
Tactic: refine ⟨Infinite.of_injective
        (fun i => ⟨i + 1, var (Sum.inr (last i))⟩) fun i j ij => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i j : ℕ
ij :
  Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
    ((fun (i : ℕ) ↦
        (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) (i + 1) (var (Sum.inr (last i))) :
          (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
      i)
    ((fun (i : ℕ) ↦
        (Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) (i + 1) (var (Sum.inr (last i))) :
          (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)))
      j)
⊢ i = j
have refine_2 : i = i
Tactic: cases ij
Cleared hypotheses: j, ij
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ Nonempty (Sum.{u', u} α ((i : ℕ) × L.Functions i) ↪ (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
have refine_2 : Function.Injective (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (β := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
  (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
    fun (F : (i : ℕ) × L.Functions i) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
      (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
        var (Sum.inr 0)))
Tactic: refine ⟨⟨Sum.elim (fun i => ⟨0, var (Sum.inl i)⟩)
        fun F => ⟨1, func F.2 fun _ => var (Sum.inr 0)⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (hypothesis)
Goal:
L : Language
α : Type u'
a b : α
h :
  Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inl a))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inl b))
⊢ Eq (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (Sum.inl a) (Sum.inl b)
have h₁ : a = b
Tactic: simp only [Sum.elim_inl, Sigma.mk.inj_iff, heq_eq_eq, var.injEq, Sum.inl.injEq, true_and]
          at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
a b : α
h : a = b
⊢ Eq (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (Sum.inl a) (Sum.inl b)
have refine_2 : Eq (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (Sum.inl b) (Sum.inl b)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (hypothesis)
Goal:
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  Eq (α := (n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inr a))
    (Sum.elim (fun (i : α) ↦ Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 0 (var (Sum.inl i)))
      (fun (F : (i : ℕ) × L.Functions i) ↦
        Sigma.mk (β := fun (n : ℕ) ↦ Term.{u, v, u'} L (α ⊕ Fin n)) 1
          (func (F.snd (β := fun (i : ℕ) ↦ L.Functions i)) fun (x : Fin (F.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦
            var (Sum.inr 0)))
      (Sum.inr b))
⊢ Eq (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (Sum.inr a) (Sum.inr b)
have h₁ : a.fst (β := fun (i : ℕ) ↦ L.Functions i) = b.fst (β := fun (i : ℕ) ↦ L.Functions i) ∧
  a.snd (β := fun (i : ℕ) ↦ L.Functions i) ≍ b.snd (β := fun (i : ℕ) ↦ L.Functions i) ∧
    HEq (α := Fin (a.fst (β := fun (i : ℕ) ↦ L.Functions i)) → Term.{u, v, u'} L (α ⊕ Fin 1))
      fun (x : Fin (a.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦ var (Sum.inr 0) (β :=
      Fin (b.fst (β := fun (i : ℕ) ↦ L.Functions i)) → Term.{u, v, u'} L (α ⊕ Fin 1))
      fun (x : Fin (b.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦ var (Sum.inr 0)
Tactic: simp only [Sum.elim_inr, Sigma.mk.inj_iff, heq_eq_eq, func.injEq, true_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
a b : (i : ℕ) × L.Functions i
h :
  a.fst (β := fun (i : ℕ) ↦ L.Functions i) = b.fst (β := fun (i : ℕ) ↦ L.Functions i) ∧
    a.snd (β := fun (i : ℕ) ↦ L.Functions i) ≍ b.snd (β := fun (i : ℕ) ↦ L.Functions i) ∧
      HEq (α := Fin (a.fst (β := fun (i : ℕ) ↦ L.Functions i)) → Term.{u, v, u'} L (α ⊕ Fin 1))
        fun (x : Fin (a.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦ var (Sum.inr 0) (β :=
        Fin (b.fst (β := fun (i : ℕ) ↦ L.Functions i)) → Term.{u, v, u'} L (α ⊕ Fin 1))
        fun (x : Fin (b.fst (β := fun (i : ℕ) ↦ L.Functions i))) ↦ var (Sum.inr 0)
⊢ Eq (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (Sum.inr a) (Sum.inr b)
have refine_2 : Eq (α := Sum.{u', u} α ((i : ℕ) × L.Functions i)) (Sum.inr b) (Sum.inr b)
Tactic: rw [Sigma.ext_iff.2 ⟨h.1, h.2.1⟩]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
inst : Encodable α
inst_1 : Encodable ((i : ℕ) × L.Functions i)
t : L.Term α
⊢ (Option.join do
      let a ← (listDecode t.listEncode).head?
      pure (some a)) =
    some t
have rw : (Option.join do
    let a ← [t].head?
    pure (some a)) =
  some t
Tactic: rw [← flatMap_singleton listEncode, listDecode_encode_list]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
h1 : Countable α
h2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
⊢ Countable (L.Term α)
have refine : ℵ₀ ≤ ℵ₀ ∧ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ ℵ₀
Tactic: refine mk_le_aleph0_iff.1 (card_le.trans (max_le_iff.2 ?_))
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
h1 : Countable α
h2 : Countable.{max (u + 1) 1} ((l : ℕ) × L.Functions l)
⊢ ℵ₀ ≤ ℵ₀ ∧ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ ℵ₀
have simp : #α ≤ ℵ₀ ∧ #((i : ℕ) × L.Functions i) ≤ ℵ₀
Tactic: simp only [le_refl, mk_sum, add_le_aleph0, lift_le_aleph0, true_and]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
m : ℕ
φ : L.BoundedFormula α m
n : ℕ
ψ : L.BoundedFormula α n
h : m = n
⊢ L.BoundedFormula α n = L.BoundedFormula α m
have rw : L.BoundedFormula α n = L.BoundedFormula α n
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
n₁ : ℕ
t₁ : Term.{u, v, u'} L (α ⊕ Fin n₁)
n₂ : ℕ
t₂ : Term.{u, v, u'} L (α ⊕ Fin n₂)
l : List ((k : ℕ) × Term.{u, v, u'} L (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h : n₁ = n₂
⊢ Term.{u, v, u'} L (α ⊕ Fin n₂) = Term.{u, v, u'} L (α ⊕ Fin n₁)
have rw : Term.{u, v, u'} L (α ⊕ Fin n₂) = Term.{u, v, u'} L (α ⊕ Fin n₂)
Tactic: rw [h]