awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
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} ℵ₀)) ≤
    max ℵ₀ (lift.{max (max u u') v, max (max u u') v} (lift.{max u v, u'} #α + lift.{u', max u v} L.card))
have simp : ℵ₀ + (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) + ℵ₀) ≤
  max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
Tactic: simp only [lift_add, lift_lift, lift_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
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) + ℵ₀) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
have rw : ℵ₀ + (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) +
    ℵ₀ ≤
  max ℵ₀ (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]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
rw :
  ℵ₀ + (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) +
      ℵ₀ ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
⊢ ℵ₀ + (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) + ℵ₀) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
have rw₁ : ℵ₀ +
    (ℵ₀ +
        (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)) ≤
  max ℵ₀ (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]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
rw :
  ℵ₀ + (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) +
      ℵ₀ ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₁ :
  ℵ₀ +
      (ℵ₀ +
          (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)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
⊢ ℵ₀ + (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) + ℵ₀) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
have rw₂ : ℵ₀ +
      (ℵ₀ +
        (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) ≤
  max ℵ₀ (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]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
rw :
  ℵ₀ + (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) +
      ℵ₀ ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₁ :
  ℵ₀ +
      (ℵ₀ +
          (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)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₂ :
  ℵ₀ +
        (ℵ₀ +
          (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
⊢ ℵ₀ + (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) + ℵ₀) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
have rw₃ : ℵ₀ + ℵ₀ +
      (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) ≤
  max ℵ₀ (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]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
rw :
  ℵ₀ + (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) +
      ℵ₀ ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₁ :
  ℵ₀ +
      (ℵ₀ +
          (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)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₂ :
  ℵ₀ +
        (ℵ₀ +
          (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₃ :
  ℵ₀ + ℵ₀ +
        (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
⊢ ℵ₀ + (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) + ℵ₀) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
have rw₄ : ℵ₀ + (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) ≤
  max ℵ₀ (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]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
rw :
  ℵ₀ + (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) +
      ℵ₀ ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₁ :
  ℵ₀ +
      (ℵ₀ +
          (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)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₂ :
  ℵ₀ +
        (ℵ₀ +
          (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₃ :
  ℵ₀ + ℵ₀ +
        (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₄ :
  ℵ₀ + (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
⊢ ℵ₀ + (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) + ℵ₀) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
have rw₅ : ℵ₀ +
    (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)) ≤
  max ℵ₀ (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]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
rw :
  ℵ₀ + (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) +
      ℵ₀ ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₁ :
  ℵ₀ +
      (ℵ₀ +
          (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)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₂ :
  ℵ₀ +
        (ℵ₀ +
          (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₃ :
  ℵ₀ + ℵ₀ +
        (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₄ :
  ℵ₀ + (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₅ :
  ℵ₀ +
      (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)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
⊢ ℵ₀ + (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) + ℵ₀) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
have rw₆ : max ℵ₀
    (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)) ≤
  max ℵ₀ (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]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
rw :
  ℵ₀ + (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) +
      ℵ₀ ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₁ :
  ℵ₀ +
      (ℵ₀ +
          (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)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₂ :
  ℵ₀ +
        (ℵ₀ +
          (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₃ :
  ℵ₀ + ℵ₀ +
        (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₄ :
  ℵ₀ + (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) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₅ :
  ℵ₀ +
      (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)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
rw₆ :
  max ℵ₀
      (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)) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
⊢ ℵ₀ + (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) + ℵ₀) ≤
    max ℵ₀ (lift.{max (max u v) (max u u') v, u'} #α + lift.{max u' (max u u') v, max u v} L.card)
have rw₇ : max ℵ₀
    (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))) ≤
  max ℵ₀ (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]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ Countable.{u' + 1} (constantsOn α).Symbols
have refine : #(constantsOn α).Symbols ≤ ℵ₀
Tactic: refine mk_le_aleph0_iff.mp ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ Countable L[[α]].Symbols
have simp : #L[[α]].Symbols ≤ ℵ₀
Tactic: simp only [← mk_le_aleph0_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ L[[α]].card ≤ ℵ₀
have simp : L.card ≤ ℵ₀ ∧ (constantsOn α).card ≤ ℵ₀
Tactic: simp only [withConstants, card_sum, add_le_aleph0, lift_le_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ L.card ≤ ℵ₀ ∧ (constantsOn α).card ≤ ℵ₀
have simp : Countable L.Symbols ∧ Countable.{u' + 1} (constantsOn α).Symbols
Tactic: simp only [card, mk_le_aleph0_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
left : Countable L.Symbols
⊢ Countable L.Symbols ∧ Countable.{u' + 1} (constantsOn α).Symbols
have right : Countable.{u' + 1} (constantsOn α).Symbols
Tactic: constructor
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ Countable ((n : ℕ) × L.BoundedFormula α n)
have refine : lift.{max u v, u'} #α + lift.{u', max u v} L.card ≤ ℵ₀
Tactic: refine Cardinal.mk_le_aleph0_iff.mp (BoundedFormula.card_le.trans (max_le (le_refl _) ?_))
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
inst : Countable α
inst_1 : Countable L.Symbols
⊢ lift.{max u v, u'} #α + lift.{u', max u v} L.card ≤ ℵ₀
have simp : Countable α ∧ Countable L.Symbols
Tactic: simp only [card, add_le_aleph0, lift_le_aleph0, mk_le_aleph0_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⟹ φ ⊔ ψ).Realize v xs
have simp : φ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
Tactic: simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (ψ ⟹ φ ⊔ ψ).Realize v xs
have simp : ψ.Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
Tactic: simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] θ
h₂ : ψ ⟹[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⊔ ψ ⟹ θ).Realize v xs
have simp : φ.Realize v xs ∨ ψ.Realize v xs → θ.Realize v xs
Tactic: simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⊓ ψ ⟹ φ).Realize v xs
have simp : φ.Realize v xs ∧ ψ.Realize v xs → φ.Realize v xs
Tactic: simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⊓ ψ ⟹ ψ).Realize v xs
have simp : φ.Realize v xs ∧ ψ.Realize v xs → ψ.Realize v xs
Tactic: simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] ψ
h₂ : φ ⟹[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⟹ ψ ⊓ θ).Realize v xs
have simp : φ.Realize v xs → ψ.Realize v xs ∧ θ.Realize v xs
Tactic: simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⇔ φ).Realize v xs
have rw : φ.Realize v xs ↔ φ.Realize v xs
Tactic: rw [BoundedFormula.realize_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
h : φ ⇔[T] ψ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (ψ ⇔ φ).Realize v xs
have rw : (φ ⇔ ψ).Realize v xs
Tactic: rw [BoundedFormula.realize_iff, Iff.comm, ← BoundedFormula.realize_iff]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (hypothesis)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
⊢ (φ ⇔ θ).Realize v xs
have h1' : (φ ⇔ ψ).Realize v xs
Tactic: have h1' := h1 M v xs
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (hypothesis)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
h1' : (φ ⇔ ψ).Realize v xs
⊢ (φ ⇔ θ).Realize v xs
have h2' : (ψ ⇔ θ).Realize v xs
Tactic: have h2' := h2 M v xs
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h1 : φ ⇔[T] ψ
h2 : ψ ⇔[T] θ
M : T.ModelType
v : α → (↑M : Type (max (max u v) w))
xs : Fin n → (↑M : Type (max (max u v) w))
h1' : (φ ⇔ ψ).Realize v xs
h2' : (ψ ⇔ θ).Realize v xs
⊢ (φ ⇔ θ).Realize v xs
have rw : ∀ (h1' : φ.Realize v xs ↔ ψ.Realize v xs) (h2' : ψ.Realize v xs ↔ θ.Realize v xs), φ.Realize v xs ↔ θ.Realize v xs
Tactic: rw [BoundedFormula.realize_iff] at *
Cleared hypotheses: h1', h2'
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∀' φ ⇔[T] ∀' ψ
have simp_rw : ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
  (∀ (a : (↑M : Type (max (max u v) w))),
      φ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)) ↔
    ∀ (a : (↑M : Type (max (max u v) w))),
      ψ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)
Tactic: simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
    BoundedFormula.realize_all]
-- Lean 4 proof step from Mathlib.ModelTheory.Equivalence (goal)
Goal:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α (n + 1)
h : φ ⇔[T] ψ
⊢ ∃' φ ⇔[T] ∃' ψ
have simp_rw : ∀ (M : T.ModelType) (v : α → (↑M : Type (max (max u v) w))) (xs : Fin n → (↑M : Type (max (max u v) w))),
  (∃ (a : (↑M : Type (max (max u v) w))),
      φ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)) ↔
    ∃ (a : (↑M : Type (max (max u v) w))),
      ψ.Realize v (Fin.snoc (α := fun (a : Fin n.succ) ↦ (↑M : Type (max (max u v) w))) xs a)
Tactic: simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff,
    BoundedFormula.realize_ex]