awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
φ : L.Formula α
v : α → M
rw : BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔ φ.Realize v
rw₁ :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔
    BoundedFormula.Realize φ v default
rw₂ :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v)
      (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) default)
⊢ Formula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ↔ φ.Realize v
have rw₃ : BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default =
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v)
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) default)
Tactic: rw [Formula.Realize, Formula.Realize, ← realize_boundedFormula g φ, iff_eq_eq,
    Unique.eq_default (g ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
α : Type u'
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
φ : L.Formula α
v : α → M
rw : BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔ φ.Realize v
rw₁ :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔
    BoundedFormula.Realize φ v default
rw₂ :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default ↔
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v)
      (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) default)
rw₃ :
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default =
    BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v)
      (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) default)
⊢ Formula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) ↔ φ.Realize v
have rw₄ : BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default =
  BoundedFormula.Realize.{u, v, u_1, u'} (M := N) φ ((⇑g : (a : M) → N) ∘ v) default
Tactic: rw [Formula.Realize, Formula.Realize, ← realize_boundedFormula g φ, iff_eq_eq,
    Unique.eq_default (g ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
φ : L.Sentence
⊢ M ⊨ φ ↔ N ⊨ φ
have rw : Formula.Realize.{u, v, w, 0} (M := M) φ default ↔ N ⊨ φ
Tactic: rw [Sentence.Realize, Sentence.Realize, ← realize_formula g,
    Unique.eq_default (g ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
φ : L.Sentence
rw : Formula.Realize.{u, v, w, 0} (M := M) φ default ↔ N ⊨ φ
⊢ M ⊨ φ ↔ N ⊨ φ
have rw₁ : Formula.Realize.{u, v, w, 0} (M := M) φ default ↔ Formula.Realize.{u, v, u_1, 0} (M := N) φ default
Tactic: rw [Sentence.Realize, Sentence.Realize, ← realize_formula g,
    Unique.eq_default (g ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
φ : L.Sentence
rw : Formula.Realize.{u, v, w, 0} (M := M) φ default ↔ N ⊨ φ
rw₁ : Formula.Realize.{u, v, w, 0} (M := M) φ default ↔ Formula.Realize.{u, v, u_1, 0} (M := N) φ default
⊢ M ⊨ φ ↔ N ⊨ φ
have rw₂ : Formula.Realize.{u, v, u_1, 0} (M := N) φ (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) default) ↔
  Formula.Realize.{u, v, u_1, 0} (M := N) φ default
Tactic: rw [Sentence.Realize, Sentence.Realize, ← realize_formula g,
    Unique.eq_default (g ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
F : Type u_4
inst_2 : EquivLike F M N
inst_3 : L.StrongHomClass F M N
g : F
φ : L.Sentence
rw : Formula.Realize.{u, v, w, 0} (M := M) φ default ↔ N ⊨ φ
rw₁ : Formula.Realize.{u, v, w, 0} (M := M) φ default ↔ Formula.Realize.{u, v, u_1, 0} (M := N) φ default
rw₂ :
  Formula.Realize.{u, v, u_1, 0} (M := N) φ (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) default) ↔
    Formula.Realize.{u, v, u_1, 0} (M := N) φ default
⊢ M ⊨ φ ↔ N ⊨ φ
have rw₃ : Formula.Realize.{u, v, u_1, 0} (M := N) φ default ↔ Formula.Realize.{u, v, u_1, 0} (M := N) φ default
Tactic: rw [Sentence.Realize, Sentence.Realize, ← realize_formula g,
    Unique.eq_default (g ∘ default)]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.reflexive ↔ Std.Refl fun (x y : M) ↦ RelMap r ![x, y]
have rw : M ⊨ r.reflexive ↔ ∀ ⦃a : M⦄, RelMap r ![a, a]
Tactic: rw [refl_def]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.irreflexive ↔ Std.Irrefl fun (x y : M) ↦ RelMap r ![x, y]
have rw : M ⊨ r.irreflexive ↔ ∀ ⦃a : M⦄, ¬RelMap r ![a, a]
Tactic: rw [irrefl_def]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.antisymmetric ↔ Std.Antisymm fun (x y : M) ↦ RelMap r ![x, y]
have rw : M ⊨ r.antisymmetric ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] → RelMap r ![b, a] → a = b
Tactic: rw [antisymm_def]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.transitive ↔ IsTrans M fun (x y : M) ↦ RelMap r ![x, y]
have rw : M ⊨ r.transitive ↔ ∀ ⦃a b c : M⦄, RelMap r ![a, b] → RelMap r ![b, c] → RelMap r ![a, c]
Tactic: rw [isTrans_def]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.total ↔ Std.Total fun (x y : M) ↦ RelMap r ![x, y]
have rw : M ⊨ r.total ↔ ∀ ⦃a b : M⦄, RelMap r ![a, b] ∨ RelMap r ![b, a]
Tactic: rw [total_def]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
⊢ M ⊨ Sentence.cardGe L n ↔ (↑n : Cardinal.{w}) ≤ #M
have rw : (∃ (xs : Fin n → M),
    BoundedFormula.Realize.{u, v, w, 0} (L := L) (α := Empty)
      (List.foldr (fun (x1 x2 : L.BoundedFormula Empty n) ↦ x1 ⊓ x2) ⊤
        (List.map (fun (ij : Fin n × Fin n) ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
          (List.filter (fun (ij : Fin n × Fin n) ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n))))
      default xs) ↔
  Nonempty.{max (w + 1) 1} (Fin n ↪ M)
Tactic: rw [← lift_mk_fin, ← lift_le.{0}, lift_lift, lift_mk_le, Sentence.cardGe, Sentence.Realize,
    BoundedFormula.realize_exs]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
⊢ (∃ (xs : Fin n → M),
      BoundedFormula.Realize.{u, v, w, 0} (L := L) (α := Empty)
        (List.foldr (fun (x1 x2 : L.BoundedFormula Empty n) ↦ x1 ⊓ x2) ⊤
          (List.map (fun (ij : Fin n × Fin n) ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
            (List.filter (fun (ij : Fin n × Fin n) ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n))))
        default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)
have simp_rw : (∃ (xs : Fin n → M),
    ∀ (φ : L.BoundedFormula Empty n),
      Membership.mem (γ := List (L.BoundedFormula Empty n))
          (List.map (fun (ij : Fin n × Fin n) ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
            (List.filter (fun (ij : Fin n × Fin n) ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))
          φ →
        φ.Realize default xs) ↔
  Nonempty.{max (w + 1) 1} (Fin n ↪ M)
Tactic: simp_rw [BoundedFormula.realize_foldr_inf]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
⊢ (∃ (xs : Fin n → M),
      ∀ (φ : L.BoundedFormula Empty n),
        Membership.mem (γ := List (L.BoundedFormula Empty n))
            (List.map (fun (ij : Fin n × Fin n) ↦ ∼((var ∘ Sum.inr) ij.1 =' (var ∘ Sum.inr) ij.2))
              (List.filter (fun (ij : Fin n × Fin n) ↦ decide (ij.1 ≠ ij.2)) (List.finRange n ×ˢ List.finRange n)))
            φ →
          φ.Realize default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)
have simp : (∃ (xs : Fin n → M),
    ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
      (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) ↔
  Nonempty.{max (w + 1) 1} (Fin n ↪ M)
Tactic: simp only [Function.comp_apply, List.mem_map, Prod.exists, Ne, List.mem_product,
    List.mem_finRange, forall_exists_index, and_imp, List.mem_filter, true_and]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
⊢ (∃ (xs : Fin n → M),
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)
have refine_1 : (∃ (xs : Fin n → M),
    ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
      (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) →
  Nonempty.{max (w + 1) 1} (Fin n ↪ M)
Tactic: refine ⟨?_, fun xs => ⟨xs.some, ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
refine_1 :
  (∃ (xs : Fin n → M),
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) →
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)
⊢ (∃ (xs : Fin n → M),
      ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
        (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs) ↔
    Nonempty.{max (w + 1) 1} (Fin n ↪ M)
have refine_2 : ∀ (xs : Nonempty.{max (w + 1) 1} (Fin n ↪ M)) (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
  (decide ¬x = x_1) = true →
    ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize (M := M) default (⇑xs.some : (a : Fin n) → M)
Tactic: refine ⟨?_, fun xs => ⟨xs.some, ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
⊢ Nonempty.{max (w + 1) 1} (Fin n ↪ M)
have refine_1 : ∀ (i j : Fin n) (ij : xs i = xs j), i = j
Tactic: refine ⟨⟨xs, fun i j ij => ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
xs : Fin n → M
h :
  ∀ (φ : L.BoundedFormula Empty n) (x x_1 : Fin n),
    (decide ¬x = x_1) = true → ∼(var (Sum.inr x) =' var (Sum.inr x_1)) = φ → φ.Realize default xs
i j : Fin n
ij : xs i = xs j
⊢ i = j
have refine_1 : ∀ (ij : i ≠ j), xs i ≠ xs j
Tactic: contrapose! ij
Cleared hypotheses: ij
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
⊢ M ⊨ L.distinctConstantsTheory s ↔ Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
have simp : (∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ) ↔
  Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
Tactic: simp only [distinctConstantsTheory, Theory.model_iff, Set.mem_image,
    Prod.exists, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
⊢ (∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ) ↔
    Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
have refine_1 : ∀
  (h :
    ∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ)
  (a : α) (as : a ∈ s) (b : α) (bs : b ∈ s)
  (ab : Eq.{w + 1} (α := M) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) a) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) b)),
  a = b
Tactic: refine ⟨fun h a as b bs ab => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
refine_1 :
  ∀
    (h :
      ∀ (φ : L[[α]].Sentence) (x x_1 : α),
        (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ)
    (a : α) (as : a ∈ s) (b : α) (bs : b ∈ s)
    (ab : Eq.{w + 1} (α := M) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) a) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) b)),
    a = b
⊢ (∀ (φ : L[[α]].Sentence) (x x_1 : α),
      (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ) ↔
    Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
have refine_2 : Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s →
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ
Tactic: refine ⟨fun h a as b bs ab => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : Eq.{w + 1} (α := M) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) a) ((fun (i : α) ↦ ((↑(L.con i) : M) : M)) b)
⊢ a = b
have refine_1 : ∀ (ab : a ≠ b), Ne.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)
Tactic: contrapose! ab
Cleared hypotheses: ab
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (hypothesis)
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
⊢ Ne.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)
have h' : M ⊨ Formula.not (Term.equal (L.con a).term (L.con b).term)
Tactic: have h' := h _ a b ⟨⟨as, bs⟩, ab⟩ rfl
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (hypothesis)
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
h :
  ∀ (φ : L[[α]].Sentence) (x x_1 : α),
    (x, x_1) ∈ s ×ˢ s ∩ (Set.diagonal α)ᶜ → Formula.not (Term.equal (L.con x).term (L.con x_1).term) = φ → M ⊨ φ
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : a ≠ b
h' : M ⊨ Formula.not (Term.equal (L.con a).term (L.con b).term)
⊢ Ne.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)
have h'₁ : ¬Eq.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)
Tactic: simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal,
      Term.realize_constants] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
α : Type u'
M : Type w
inst : L[[α]].Structure M
s : Set α
h : Set.InjOn.{u', w} (β := M) (fun (i : α) ↦ (↑(L.con i) : M)) s
a b : α
ab : (a, b) ∈ (Set.diagonal α)ᶜ
as : (a, b).1 ∈ s
bs : (a, b).2 ∈ s
⊢ M ⊨ Formula.not (Term.equal (L.con a).term (L.con b).term)
have refine_2 : ¬Eq.{w + 1} (α := M) (↑(L.con a) : M) (↑(L.con b) : M)
Tactic: simp only [Sentence.Realize, Formula.realize_not, Formula.realize_equal, Term.realize_constants]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
T : L.Theory
h : M ≅[L] N
⊢ M ⊨ T ↔ N ⊨ T
have rw : T ⊆ L.completeTheory M ↔ N ⊨ T
Tactic: rw [Theory.model_iff_subset_completeTheory, Theory.model_iff_subset_completeTheory,
    h.completeTheory_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
T : L.Theory
h : M ≅[L] N
rw : T ⊆ L.completeTheory M ↔ N ⊨ T
⊢ M ⊨ T ↔ N ⊨ T
have rw₁ : T ⊆ L.completeTheory M ↔ T ⊆ L.completeTheory N
Tactic: rw [Theory.model_iff_subset_completeTheory, Theory.model_iff_subset_completeTheory,
    h.completeTheory_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Semantics (goal)
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
T : L.Theory
h : M ≅[L] N
rw : T ⊆ L.completeTheory M ↔ N ⊨ T
rw₁ : T ⊆ L.completeTheory M ↔ T ⊆ L.completeTheory N
⊢ M ⊨ T ↔ N ⊨ T
have rw₂ : T ⊆ L.completeTheory N ↔ T ⊆ L.completeTheory N
Tactic: rw [Theory.model_iff_subset_completeTheory, Theory.model_iff_subset_completeTheory,
    h.completeTheory_eq]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
⊢ #((n : ℕ) × (L.sum L.skolem₁).Functions n) = #((n : ℕ) × L.BoundedFormula Empty (n + 1))
have simp : ((sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) +
    sum fun (i : ℕ) ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))) =
  sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
Tactic: simp only [card_functions_sum, skolem₁_Functions, mk_sigma, sum_add_distrib']
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
| (sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) +
    sum fun (i : ℕ) ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))
have h : ∀ (i : ℕ), lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))
Tactic: enter [2, 1, i]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
i : ℕ
| lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))
have h : #(L.BoundedFormula Empty (i + 1))
Tactic: rw [lift_id'.{u, v}]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
| (sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) +
    sum fun (i : ℕ) ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))
have h : ∀ (i : ℕ), #(L.BoundedFormula Empty (i + 1))
Tactic: enter [2, 1, i]; rw [lift_id'.{u, v}]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
⊢ ((sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) +
      sum fun (i : ℕ) ↦ lift.{u, max u v} #(L.BoundedFormula Empty (i + 1))) =
    sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
have conv_lhs : ((sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) + sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))) =
  sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
Tactic: conv_lhs => enter [2, 1, i]; rw [lift_id'.{u, v}]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
⊢ ((sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) + sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))) =
    sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
have rw : (sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) ≤ sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
Tactic: rw [add_comm, add_eq_max, max_eq_left]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
rw : (sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) ≤ sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
⊢ ((sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) + sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))) =
    sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
have rw₁ : ℵ₀ ≤ sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
Tactic: rw [add_comm, add_eq_max, max_eq_left]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
⊢ (sum fun (i : ℕ) ↦ lift.{max u v, u} #(L.Functions i)) ≤ sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
have H : ∀ (n : ℕ), lift.{max u v, u} #(L.Functions n) ≤ #(L.BoundedFormula Empty (n + 1))
Tactic: gcongr with n
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
n : ℕ
⊢ lift.{max u v, u} #(L.Functions n) ≤ #(L.BoundedFormula Empty (n + 1))
have H : Nonempty (L.Functions n ↪ L.BoundedFormula Empty (n + 1))
Tactic: rw [← lift_le.{_, max u v}, lift_lift, lift_mk_le.{v}]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
n : ℕ
⊢ Nonempty (L.Functions n ↪ L.BoundedFormula Empty (n + 1))
have H : ∀ (f g : L.Functions n)
  (h :
    Eq (α := L.BoundedFormula Empty (n + 1))
      ((fun (f : L.Functions n) ↦ (func f default =' func f default : L.BoundedFormula Empty (n + 1))) f)
      ((fun (f : L.Functions n) ↦ (func f default =' func f default : L.BoundedFormula Empty (n + 1))) g)),
  f = g
Tactic: refine ⟨⟨fun f => (func f default).bdEqual (func f default), fun f g h => ?_⟩⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
n : ℕ
f g : L.Functions n
h :
  Eq (α := L.BoundedFormula Empty (n + 1))
    ((fun (f : L.Functions n) ↦ (func f default =' func f default : L.BoundedFormula Empty (n + 1))) f)
    ((fun (f : L.Functions n) ↦ (func f default =' func f default : L.BoundedFormula Empty (n + 1))) g)
⊢ f = g
have H : f = f
Tactic: rcases h with ⟨rfl, ⟨rfl⟩⟩
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
⊢ ℵ₀ ≤ sum fun (i : ℕ) ↦ #(L.BoundedFormula Empty (i + 1))
have rw : ℵ₀ ≤ #((i : ℕ) × L.BoundedFormula Empty (i + 1))
Tactic: rw [← mk_sigma]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
⊢ #((n : ℕ) × (L.sum L.skolem₁).Functions n) ≤ max ℵ₀ L.card
have rw : #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ max ℵ₀ L.card
Tactic: rw [card_functions_sum_skolem₁]
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ max ℵ₀ L.card
have trans : #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ #((n : ℕ) × L.BoundedFormula Empty n)
Tactic: trans #(Σ n, L.BoundedFormula Empty n)
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
trans : #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ #((n : ℕ) × L.BoundedFormula Empty n)
⊢ #((n : ℕ) × L.BoundedFormula Empty (n + 1)) ≤ max ℵ₀ L.card
have trans₁ : #((n : ℕ) × L.BoundedFormula Empty n) ≤ max ℵ₀ L.card
Tactic: trans #(Σ n, L.BoundedFormula Empty n)
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
⊢ #((n : ℕ) × L.BoundedFormula Empty n) ≤ max ℵ₀ L.card
have refine : lift.{max u v, max u v} (max ℵ₀ (lift.{max u v, 0} #Empty + lift.{0, max u v} L.card)) ≤
  lift.{max u v, max u v} (max ℵ₀ L.card)
Tactic: refine _root_.trans BoundedFormula.card_le (lift_le.{max u v}.1 ?_)
-- Lean 4 proof step from Mathlib.ModelTheory.Skolem (goal)
Goal:
L : Language
⊢ lift.{max u v, max u v} (max ℵ₀ (lift.{max u v, 0} #Empty + lift.{0, max u v} L.card)) ≤
    lift.{max u v, max u v} (max ℵ₀ L.card)
have simp : lift.{max u v, max u v} (max ℵ₀ L.card) ≤ lift.{max u v, max u v} (max ℵ₀ L.card)
Tactic: simp only [mk_empty, lift_zero, lift_uzero, zero_add]