awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Semantics
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 : FunLike F M N
inst_3 : L.HomClass F M N
g : F
v : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
_ts_ih :
  ∀ (a : Fin l),
    Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts a) : N)
      ((g : (a : M) → N) (Term.realize v (_ts a)) : N)
⊢ Eq.{u_1 + 1} (α := N) (funMap _f fun (i : Fin l) ↦ Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts i))
    (funMap _f (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) fun (i : Fin l) ↦ Term.realize v (_ts i)))

Tactic:
congr rfl ?_

Premises used: congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
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 : FunLike F M N
inst_3 : L.HomClass F M N
g : F
v : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
_ts_ih :
  ∀ (a : Fin l),
    Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts a) : N)
      ((g : (a : M) → N) (Term.realize v (_ts a)) : N)
func :
  Eq.{u_1 + 1} (α := (i : Fin l) → N) (fun (i : Fin l) ↦ Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts i))
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) fun (i : Fin l) ↦ Term.realize v (_ts i))
⊢ Eq.{u_1 + 1} (α := N) (funMap _f fun (i : Fin l) ↦ Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts i))
    (funMap _f (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) fun (i : Fin l) ↦ Term.realize v (_ts i)))

Tactic:
refine congr rfl ?_

Premises used: congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
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 : FunLike F M N
inst_3 : L.HomClass F M N
g : F
v : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
_ts_ih :
  ∀ (a : Fin l),
    Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts a) : N)
      ((g : (a : M) → N) (Term.realize v (_ts a)) : N)
func :
  ∀ (x : Fin l),
    Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts x))
      (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) (fun (i : Fin l) ↦ Term.realize v (_ts i)) x)
⊢ Eq.{u_1 + 1} (α := (i : Fin l) → N) (fun (i : Fin l) ↦ Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts i))
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) fun (i : Fin l) ↦ Term.realize v (_ts i))

Tactic:
ext x
-- Module: Mathlib.ModelTheory.Semantics
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 : FunLike F M N
inst_3 : L.HomClass F M N
g : F
v : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
_ts_ih :
  ∀ (a : Fin l),
    Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts a) : N)
      ((g : (a : M) → N) (Term.realize v (_ts a)) : N)
x : Fin l
⊢ Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (_ts x))
    (Function.comp.{1, w + 1, u_1 + 1} (β := M) (⇑g : (a : M) → N) (fun (i : Fin l) ↦ Term.realize v (_ts i)) x)

Tactic:
simp [*]
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
⊢ Realize.{u, v, w, u'} (L := L) ⊥ v xs ↔ False

Tactic:
Iff.rfl

Premises used: Iff.rfl, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (∼φ).Realize v xs ↔ ¬φ.Realize v xs

Tactic:
Iff.rfl

Premises used: Iff.rfl, FirstOrder.Language.BoundedFormula.not, FirstOrder.Language.BoundedFormula.Realize, Not
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin l)
⊢ (t₁ =' t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ = realize (Sum.elim v xs) t₂

Tactic:
Iff.rfl

Premises used: Iff.rfl, FirstOrder.Language.Term.bdEqual, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
⊢ Realize.{u, v, w, u'} (L := L) ⊤ v xs ↔ True

Tactic:
simp [Top.top]

Premises used: Top.top
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⊓ ψ).Realize v xs ↔ φ.Realize v xs ∧ ψ.Realize v xs

Tactic:
simp [Realize]

Premises used: FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ []) v xs ↔
    ∀ (φ : L.BoundedFormula α n), Membership.mem (γ := List (L.BoundedFormula α n)) [] φ → φ.Realize v xs

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ l) v xs ↔
    ∀ φ ∈ l, φ.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ (φ :: l)) v xs ↔
    ∀ φ_1 ∈ φ :: l, φ_1.Realize v xs

Tactic:
simp [ih]
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
nil :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ []) v xs ↔
    ∀ (φ : L.BoundedFormula α n), Membership.mem (γ := List (L.BoundedFormula α n)) [] φ → φ.Realize v xs
cons :
  ∀ (φ : L.BoundedFormula α n) (l : List (L.BoundedFormula α n))
    (ih :
      Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ l) v xs ↔
        ∀ φ ∈ l, φ.Realize v xs),
    Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ (φ :: l)) v xs ↔
      ∀ φ_1 ∈ φ :: l, φ_1.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊓ x2) ⊤ l) v xs ↔
    ∀ φ ∈ l, φ.Realize v xs

Tactic:
induction l with
  | nil => simp
  | cons φ l ih => simp [ih]

Premises used: Fin.cons
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs

Tactic:
simp only [Realize]

Premises used: FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
k : ℕ
l : List (L.BoundedFormula α k)
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
induction :
  (List.foldr imp f []).Realize v xs =
    ((∀ (i : L.BoundedFormula α k), Membership.mem (γ := List (L.BoundedFormula α k)) [] i → i.Realize v xs) →
      f.Realize v xs)
cons :
  ∀ (head : L.BoundedFormula α k) (tail : List (L.BoundedFormula α k)),
    (List.foldr imp f tail).Realize v xs = ((∀ i ∈ tail, i.Realize v xs) → f.Realize v xs) →
      (List.foldr imp f (head :: tail)).Realize v xs = ((∀ i ∈ head :: tail, i.Realize v xs) → f.Realize v xs)
⊢ (List.foldr imp f l).Realize v xs = ((∀ i ∈ l, i.Realize v xs) → f.Realize v xs)

Tactic:
induction l
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
⊢ (List.foldr imp f []).Realize v xs =
    ((∀ (i : L.BoundedFormula α k), Membership.mem (γ := List (L.BoundedFormula α k)) [] i → i.Realize v xs) →
      f.Realize v xs)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
⊢ (List.foldr imp f []).Realize v xs =
    ((∀ (i : L.BoundedFormula α k), Membership.mem (γ := List (L.BoundedFormula α k)) [] i → i.Realize v xs) →
      f.Realize v xs)

Tactic:
next => simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
f' : L.BoundedFormula α k
tail : List (L.BoundedFormula α k)
tail_ih : (List.foldr imp f tail).Realize v xs = ((∀ i ∈ tail, i.Realize v xs) → f.Realize v xs)
pos :
  f'.Realize v xs → (List.foldr imp f (f' :: tail)).Realize v xs = ((∀ i ∈ f' :: tail, i.Realize v xs) → f.Realize v xs)
neg :
  ¬f'.Realize v xs →
    (List.foldr imp f (f' :: tail)).Realize v xs = ((∀ i ∈ f' :: tail, i.Realize v xs) → f.Realize v xs)
⊢ (List.foldr imp f (f' :: tail)).Realize v xs = ((∀ i ∈ f' :: tail, i.Realize v xs) → f.Realize v xs)

Tactic:
by_cases f'.Realize v xs

Premises used: FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
f' : L.BoundedFormula α k
tail : List (L.BoundedFormula α k)
tail_ih : (List.foldr imp f tail).Realize v xs = ((∀ i ∈ tail, i.Realize v xs) → f.Realize v xs)
h : f'.Realize v xs
⊢ (List.foldr imp f (f' :: tail)).Realize v xs = ((∀ i ∈ f' :: tail, i.Realize v xs) → f.Realize v xs)

Tactic:
simp [*]
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
f' : L.BoundedFormula α k
tail : List (L.BoundedFormula α k)
tail_ih : (List.foldr imp f tail).Realize v xs = ((∀ i ∈ tail, i.Realize v xs) → f.Realize v xs)
h : ¬f'.Realize v xs
⊢ (List.foldr imp f (f' :: tail)).Realize v xs = ((∀ i ∈ f' :: tail, i.Realize v xs) → f.Realize v xs)

Tactic:
simp [*]
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
k : ℕ
R : L.Relations k
ts : Fin k → Term.{u, v, u'} L (α ⊕ Fin l)
⊢ (R.boundedFormula ts).Realize v xs ↔ RelMap.{u, v, w} (M := M) R fun (i : Fin k) ↦ realize (Sum.elim v xs) (ts i)

Tactic:
Iff.rfl

Premises used: Iff.rfl, FirstOrder.Language.Relations.boundedFormula, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : Term.{u, v, u'} L (α ⊕ Fin l)
rw :
  (RelMap.{u, v, w} (M := M) R fun (i : Fin 1) ↦ realize (Sum.elim v xs) (![t] i)) =
    RelMap R ![realize (Sum.elim v xs) t]
⊢ (R.boundedFormula₁ t).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t]

Tactic:
rw [Relations.boundedFormula₁, realize_rel, iff_eq_eq]

Premises used: FirstOrder.Language.Relations.boundedFormula₁, FirstOrder.Language.BoundedFormula.realize_rel, iff_eq_eq
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : Term.{u, v, u'} L (α ⊕ Fin l)
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 1) ↦ realize (Sum.elim v xs) (![t] i)) =
    RelMap R ![realize (Sum.elim v xs) t]

Tactic:
congr rfl (funext fun _ => ?_)

Premises used: funext, congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : Term.{u, v, u'} L (α ⊕ Fin l)
refine : ∀ (x : Fin 1), realize (Sum.elim v xs) (![t] x) = ![realize (Sum.elim v xs) t] x
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 1) ↦ realize (Sum.elim v xs) (![t] i)) =
    RelMap R ![realize (Sum.elim v xs) t]

Tactic:
refine congr rfl (funext fun _ => ?_)

Premises used: funext, congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 1
t : Term.{u, v, u'} L (α ⊕ Fin l)
x : Fin 1
⊢ realize (Sum.elim v xs) (![t] x) = ![realize (Sum.elim v xs) t] x

Tactic:
simp only [Matrix.cons_val_fin_one]

Premises used: Matrix.cons_val_fin_one
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin l)
rw :
  (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
⊢ (R.boundedFormula₂ t₁ t₂).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
rw [Relations.boundedFormula₂, realize_rel, iff_eq_eq]

Premises used: FirstOrder.Language.BoundedFormula.realize_rel, iff_eq_eq, FirstOrder.Language.Relations.boundedFormula₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin l)
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
congr rfl (funext (Fin.cases ?_ ?_))

Premises used: funext, congr, Fin.cases, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin l)
refine_1 : realize (Sum.elim v xs) (![t₁, t₂] 0) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] 0
refine_2 :
  ∀ (i : Fin 1),
    realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ realize (Sum.elim v xs) (![t₁, t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]

Tactic:
refine congr rfl (funext (Fin.cases ?_ ?_))

Premises used: funext, congr, Fin.cases, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin l)
⊢ realize (Sum.elim v xs) (![t₁, t₂] 0) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] 0

Tactic:
simp only [Matrix.cons_val_zero]

Premises used: Matrix.cons_val_zero
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
v : α → M
xs : Fin l → M
R : L.Relations 2
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin l)
⊢ ∀ (i : Fin 1),
    realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ

Tactic:
simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Premises used: Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
mp : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mpr : φ.Realize v xs ∨ ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mp₁ mp₂ : (∼φ ⟹ ψ).Realize v xs → φ.Realize v xs ∨ ψ.Realize v xs
mp₃ : (∼φ ⟹ ψ).Realize v xs → ¬φ.Realize v xs → ψ.Realize v xs
mpr₁ : φ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₂ : ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₃ : φ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₄ : ψ.Realize v xs → (∼φ ⟹ ψ).Realize v xs
mpr₅ : φ.Realize v xs → (∼φ).Realize v xs → ψ.Realize v xs
mpr₆ : ψ.Realize v xs → (∼φ).Realize v xs → ψ.Realize v xs
mp₄ mp₅ mp₆ : (∼φ ⟹ ψ).Realize v xs → ¬φ.Realize v xs → ψ.Realize v xs
mpr₇ : φ.Realize v xs → (∼φ).Realize v xs → ψ.Realize v xs
mp₇ mp₈ mp₉ mp₁₀ mp₁₁ : (∼φ ⟹ ψ).Realize v xs → ¬φ.Realize v xs → ψ.Realize v xs
⊢ (∼φ ⟹ ψ).Realize v xs ↔ φ.Realize v xs ∨ ψ.Realize v xs

Tactic:
tauto
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ []) v xs ↔
    ∃ (φ : L.BoundedFormula α n), Membership.mem (γ := List (L.BoundedFormula α n)) [] φ ∧ φ.Realize v xs

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
v : α → M
xs : Fin n → M
φ : L.BoundedFormula α n
l : List (L.BoundedFormula α n)
ih :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ ∈ l, φ.Realize v xs
cons :
  (φ ⊔ List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l).Realize v xs ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₁ :
  φ.Realize v xs ∨ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₂ : (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
cons₃ :
  (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔ ∃ (φ_1 : L.BoundedFormula α n), (φ_1 = φ ∨ φ_1 ∈ l) ∧ φ_1.Realize v xs
cons₄ :
  (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔
    ∃ (φ_1 : L.BoundedFormula α n), φ_1 = φ ∧ φ_1.Realize v xs ∨ φ_1 ∈ l ∧ φ_1.Realize v xs
cons₅ :
  (φ.Realize v xs ∨ ∃ φ ∈ l, φ.Realize v xs) ↔
    (∃ (x : L.BoundedFormula α n), x = φ ∧ x.Realize v xs) ∨ ∃ x ∈ l, x.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ (φ :: l)) v xs ↔
    ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs

Tactic:
simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]

Premises used: exists_or, List.foldr_cons, exists_eq_left, List.mem_cons, FirstOrder.Language.BoundedFormula.realize_sup, or_and_right
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
l : List (L.BoundedFormula α n)
v : α → M
xs : Fin n → M
nil :
  Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ []) v xs ↔
    ∃ (φ : L.BoundedFormula α n), Membership.mem (γ := List (L.BoundedFormula α n)) [] φ ∧ φ.Realize v xs
cons :
  ∀ (φ : L.BoundedFormula α n) (l : List (L.BoundedFormula α n))
    (ih :
      Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
        ∃ φ ∈ l, φ.Realize v xs),
    Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ (φ :: l)) v xs ↔
      ∃ φ_1 ∈ φ :: l, φ_1.Realize v xs
⊢ Realize.{u, v, w, u'} (L := L) (List.foldr (fun (x1 x2 : L.BoundedFormula α n) ↦ x1 ⊔ x2) ⊥ l) v xs ↔
    ∃ φ ∈ l, φ.Realize v xs

Tactic:
induction l with
  | nil => simp
  | cons φ l ih =>
    simp_rw [List.foldr_cons, realize_sup, ih, List.mem_cons, or_and_right, exists_or,
      exists_eq_left]

Premises used: exists_or, List.foldr_cons, Fin.cons, exists_eq_left, List.mem_cons, FirstOrder.Language.BoundedFormula.realize_sup, or_and_right
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∀' θ).Realize v xs ↔ ∀ (a : M), θ.Realize v (snoc (α := fun (a : Fin l.succ) ↦ M) xs a)

Tactic:
Iff.rfl

Premises used: Iff.rfl, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
rw :
  (∃ (x : M), ¬(∼θ).Realize v (snoc (α := fun (a : Fin l.succ) ↦ M) xs x)) ↔
    ∃ (a : M), θ.Realize v (snoc (α := fun (a : Fin l.succ) ↦ M) xs a)
⊢ (∃' θ).Realize v xs ↔ ∃ (a : M), θ.Realize v (snoc (α := fun (a : Fin l.succ) ↦ M) xs a)

Tactic:
rw [BoundedFormula.ex, realize_not, realize_all, not_forall]

Premises used: FirstOrder.Language.BoundedFormula.realize_not, FirstOrder.Language.BoundedFormula.realize_all, FirstOrder.Language.BoundedFormula.ex, Classical.not_forall
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
l : ℕ
φ ψ : L.BoundedFormula α l
v : α → M
xs : Fin l → M
⊢ (φ ⇔ ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Realize v xs)

Tactic:
simp only [BoundedFormula.iff, realize_inf, realize_imp, ← iff_def]

Premises used: FirstOrder.Language.BoundedFormula.realize_inf, FirstOrder.Language.BoundedFormula.iff, iff_def, FirstOrder.Language.BoundedFormula.realize_imp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
m n : ℕ
h : m = n
h' : m ≤ n
φ : L.BoundedFormula α m
v : α → M
xs : Fin n → M
subst : ∀ {h' : m ≤ m} {xs : Fin m → M}, (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast ⋯)
⊢ (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)

Tactic:
subst h
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
m : ℕ
φ : L.BoundedFormula α m
v : α → M
h' : m ≤ m
xs : Fin m → M
⊢ (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast ⋯)

Tactic:
simp only [castLE_rfl, cast_refl, Function.comp_id]

Premises used: Function.comp_id, FirstOrder.Language.BoundedFormula.castLE_rfl, Fin.cast_refl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L'.Structure M
ft : (n : ℕ) → Term.{u, v, u'} L (α ⊕ Fin n) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin n)) (xs : Fin n → M),
    realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n_1 : ℕ
xs : Fin n_1 → M
⊢ Realize (mapTermRel ft fr fun (x : ℕ) ↦ id (n := n_1) falsum) v' xs ↔ Realize.{u, v, w, u'} (L := L) falsum v xs

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L'.Structure M
ft : (n : ℕ) → Term.{u, v, u'} L (α ⊕ Fin n) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin n)) (xs : Fin n → M),
    realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n_1 : ℕ
t₁ t₂ : Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin n_1 → M
⊢ (mapTermRel ft fr (fun (x : ℕ) ↦ id) (equal t₁ t₂)).Realize v' xs ↔ (equal t₁ t₂).Realize v xs

Tactic:
simp [mapTermRel, Realize, h1]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L'.Structure M
ft : (n : ℕ) → Term.{u, v, u'} L (α ⊕ Fin n) → Term.{u_4, u_5, v'} L' (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 :
  ∀ (n : ℕ) (t : Term.{u, v, u'} L (α ⊕ Fin n)) (xs : Fin n → M),
    realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n_1 l : ℕ
R : L.Relations l
ts : Fin l → Term.{u, v, u'} L (α ⊕ Fin n_1)
xs : Fin n_1 → M
⊢ (mapTermRel ft fr (fun (x : ℕ) ↦ id) (rel R ts)).Realize v' xs ↔ (rel R ts).Realize v xs

Tactic:
simp [mapTermRel, Realize, h1, h2]

Premises used: FirstOrder.Language.BoundedFormula.mapTermRel, FirstOrder.Language.BoundedFormula.Realize