awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ : L.Formula α
v : α → M
⊢ φ.not.Realize v ↔ ¬φ.Realize v

Tactic:
Iff.rfl

Premises used: Iff.rfl, FirstOrder.Language.BoundedFormula.not, FirstOrder.Language.BoundedFormula.Realize, Not, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
⊢ Realize.{u, v, w, u'} (L := L) ⊥ v ↔ False

Tactic:
Iff.rfl

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

Tactic:
BoundedFormula.realize_top

Premises used: FirstOrder.Language.BoundedFormula.realize_top, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ ψ : L.Formula α
v : α → M
⊢ (φ ⊓ ψ).Realize v ↔ φ.Realize v ∧ ψ.Realize v

Tactic:
BoundedFormula.realize_inf

Premises used: FirstOrder.Language.BoundedFormula.realize_inf, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ ψ : L.Formula α
v : α → M
⊢ (φ.imp ψ).Realize v ↔ φ.Realize v → ψ.Realize v

Tactic:
BoundedFormula.realize_imp

Premises used: FirstOrder.Language.BoundedFormula.realize_imp, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
k : ℕ
R : L.Relations k
ts : Fin k → L.Term α
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin k) ↦
      Term.realize (α := α ⊕ Fin 0) (Sum.elim v default) (Term.relabel Sum.inl (ts i))) ↔
    RelMap.{u, v, w} (M := M) R fun (i : Fin k) ↦ Term.realize v (ts i)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
rw : (RelMap.{u, v, w} (M := M) R fun (i : Fin 1) ↦ Term.realize v (![t] i)) = RelMap R ![Term.realize v t]
⊢ (R.formula₁ t).Realize v ↔ RelMap R ![Term.realize v t]

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

Premises used: FirstOrder.Language.Formula.realize_rel, FirstOrder.Language.Relations.formula₁, iff_eq_eq
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
R : L.Relations 1
t : L.Term α
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 1) ↦ Term.realize v (![t] i)) = RelMap R ![Term.realize v 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'
v : α → M
R : L.Relations 1
t : L.Term α
refine : ∀ (x : Fin 1), Term.realize v (![t] x) = ![Term.realize v t] x
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 1) ↦ Term.realize v (![t] i)) = RelMap R ![Term.realize v 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'
v : α → M
R : L.Relations 1
t : L.Term α
x : Fin 1
⊢ Term.realize v (![t] x) = ![Term.realize v 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'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
rw :
  (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ Term.realize v (![t₁, t₂] i)) =
    RelMap R ![Term.realize v t₁, Term.realize v t₂]
⊢ (R.formula₂ t₁ t₂).Realize v ↔ RelMap R ![Term.realize v t₁, Term.realize v t₂]

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

Premises used: FirstOrder.Language.Formula.realize_rel, iff_eq_eq, FirstOrder.Language.Relations.formula₂
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ Term.realize v (![t₁, t₂] i)) =
    RelMap R ![Term.realize v t₁, Term.realize v 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'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
refine_1 : Term.realize v (![t₁, t₂] 0) = ![Term.realize v t₁, Term.realize v t₂] 0
refine_2 : ∀ (i : Fin 1), Term.realize v (![t₁, t₂] i.succ) = ![Term.realize v t₁, Term.realize v t₂] i.succ
⊢ (RelMap.{u, v, w} (M := M) R fun (i : Fin 2) ↦ Term.realize v (![t₁, t₂] i)) =
    RelMap R ![Term.realize v t₁, Term.realize v 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'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ Term.realize v (![t₁, t₂] 0) = ![Term.realize v t₁, Term.realize v 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'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ ∀ (i : Fin 1), Term.realize v (![t₁, t₂] i.succ) = ![Term.realize v t₁, Term.realize v 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.Formula α
v : α → M
⊢ (φ ⊔ ψ).Realize v ↔ φ.Realize v ∨ ψ.Realize v

Tactic:
BoundedFormula.realize_sup

Premises used: FirstOrder.Language.BoundedFormula.realize_sup, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ ψ : L.Formula α
v : α → M
⊢ (φ.iff ψ).Realize v ↔ (φ.Realize v ↔ ψ.Realize v)

Tactic:
BoundedFormula.realize_iff

Premises used: FirstOrder.Language.BoundedFormula.realize_iff, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
rw :
  BoundedFormula.Realize φ (Function.comp (β := β ⊕ Fin 0) (Sum.elim v (default ∘ Fin.cast ⋯)) (Sum.inl ∘ g))
      (Function.comp (β := Fin (HAdd.hAdd (α := ℕ) 0 0)) default (natAdd 0)) =
    BoundedFormula.Realize φ (v ∘ g) default
⊢ (relabel g φ).Realize v ↔ φ.Realize (v ∘ g)

Tactic:
rw [Realize, Realize, relabel, BoundedFormula.realize_relabel, iff_eq_eq, Fin.castAdd_zero]

Premises used: Fin.castAdd_zero, FirstOrder.Language.BoundedFormula.realize_relabel, FirstOrder.Language.Formula.relabel, iff_eq_eq, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ BoundedFormula.Realize φ (Function.comp (β := β ⊕ Fin 0) (Sum.elim v (default ∘ Fin.cast ⋯)) (Sum.inl ∘ g))
      (Function.comp (β := Fin (HAdd.hAdd (α := ℕ) 0 0)) default (natAdd 0)) =
    BoundedFormula.Realize φ (v ∘ g) default

Tactic:
congr rfl (funext finZeroElim)

Premises used: finZeroElim, funext, congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
φ : L.Formula α
g : α → β
v : β → M
⊢ BoundedFormula.Realize φ (Function.comp (β := β ⊕ Fin 0) (Sum.elim v (default ∘ Fin.cast ⋯)) (Sum.inl ∘ g))
      (Function.comp (β := Fin (HAdd.hAdd (α := ℕ) 0 0)) default (natAdd 0)) =
    BoundedFormula.Realize φ (v ∘ g) default

Tactic:
exact congr rfl (funext finZeroElim)

Premises used: finZeroElim, funext, congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
φ : L.Formula (Fin n)
v : Empty → M
x : Fin n → M
rw : BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ φ.Realize x
rw₁ :
  BoundedFormula.Realize φ (Sum.elim v (x ∘ castAdd 0) ∘ Sum.inr) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₂ : BoundedFormula.Realize φ (x ∘ castAdd 0) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₃ : BoundedFormula.Realize φ (x ∘ Fin.cast ⋯) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₄ : BoundedFormula.Realize φ (x ∘ id) (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₅ : BoundedFormula.Realize φ x (x ∘ natAdd n) ↔ BoundedFormula.Realize φ x default
rw₆ rw₇ : BoundedFormula.Realize φ x default ↔ BoundedFormula.Realize φ x default
⊢ BoundedFormula.Realize (BoundedFormula.relabel Sum.inr φ) v x ↔ φ.Realize x

Tactic:
rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
    cast_refl, Function.comp_id,
    Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]

Premises used: Inhabited.default, Function.comp_id, Fin.natAdd, Sum.elim_comp_inr, Function.comp, Fin.castAdd_zero, FirstOrder.Language.BoundedFormula.realize_relabel, Subsingleton.elim, Fin.cast_refl, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
t₁ t₂ : L.Term α
x : α → M
⊢ (t₁.equal t₂).Realize x ↔ Term.realize x t₁ = Term.realize x t₂

Tactic:
simp [Term.equal, Realize]

Premises used: FirstOrder.Language.Term.equal, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
f : L.Functions n
x : Fin n → M
y : M
simp : (y = funMap f fun (i : Fin n) ↦ x i) ↔ funMap f x = y
⊢ Realize.{u, v, w, 0} (M := M) (graph f) (cons (α := fun (a : Fin (n + 1)) ↦ M) y x) ↔ funMap f x = y

Tactic:
simp only [Formula.graph, Term.realize, realize_equal, Fin.cons_zero, Fin.cons_succ]

Premises used: FirstOrder.Language.Formula.realize_equal, Fin.cons_succ, FirstOrder.Language.Term.realize, Fin.cons_zero, FirstOrder.Language.Formula.graph
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
f : L.Functions n
x : Fin n → M
y : M
rw rw₁ : (funMap f fun (i : Fin n) ↦ x i) = y ↔ funMap f x = y
⊢ (y = funMap f fun (i : Fin n) ↦ x i) ↔ funMap f x = y

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
rw : BoundedFormula.Realize φ x y = BoundedFormula.Realize φ x default
⊢ BoundedFormula.Realize φ x y ↔ φ.Realize x

Tactic:
rw [Formula.Realize, iff_iff_eq]

Premises used: iff_iff_eq, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
e__xs : y = default
⊢ BoundedFormula.Realize φ x y = BoundedFormula.Realize φ x default

Tactic:
congr
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
e__xs : ∀ (i : Fin 0), y i = default i
⊢ y = default

Tactic:
ext i
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
i : Fin 0
⊢ y i = default i

Tactic:
Fin.elim0 i

Premises used: Fin.elim0
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ : L.Formula α
x : α → M
y : Fin 0 → M
i : Fin 0
⊢ y i = default i

Tactic:
exact Fin.elim0 i

Premises used: Fin.elim0
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : L.Formula α
v : α → M
⊢ (φ.onFormula ψ).Realize v ↔ ψ.Realize v

Tactic:
φ.realize_onBoundedFormula ψ

Premises used: FirstOrder.Language.LHom.realize_onBoundedFormula, FirstOrder.Language.LHom.onFormula, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : L.Formula α
h :
  ∀ (x : α → M),
    Membership.mem (γ := Set (α → M)) (setOf (φ.onFormula ψ).Realize) x ↔
      Membership.mem (γ := Set (α → M)) (setOf ψ.Realize) x
⊢ Eq (α := Set (α → M)) (setOf (φ.onFormula ψ).Realize) (setOf ψ.Realize)

Tactic:
ext
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : L.Formula α
x : α → M
⊢ Membership.mem (γ := Set (α → M)) (setOf (φ.onFormula ψ).Realize) x ↔
    Membership.mem (γ := Set (α → M)) (setOf ψ.Realize) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
φ : L.Sentence
⊢ M ⊨ Formula.not φ ↔ ¬M ⊨ φ

Tactic:
Iff.rfl

Premises used: FirstOrder.Language.Sentence.Realize, Iff.rfl, FirstOrder.Language.BoundedFormula.not, FirstOrder.Language.BoundedFormula.Realize, Not, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
simp :
  BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default ↔
    M ⊨ φ
⊢ (Realize.{u, v, w, u'} (L := L) (M := M) ((_root_.Equiv.symm equivSentence : (a : L[[α]].Sentence) → L.Formula α) φ)
      fun (a : α) ↦ (↑(L.con a) : M)) ↔
    M ⊨ φ

Tactic:
simp only [equivSentence, _root_.Equiv.symm_symm, Equiv.coe_trans, Realize,
    BoundedFormula.realize_relabelEquiv, Function.comp]

Premises used: FirstOrder.Language.Formula.equivSentence, Function.comp, Equiv.symm_symm, FirstOrder.Language.BoundedFormula.realize_relabelEquiv, Equiv.coe_trans, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
⊢ BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default ↔
    M ⊨ φ

Tactic:
_root_.trans ?_ BoundedFormula.realize_constantsVarsEquiv

Premises used: trans, FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
refine :
  BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default ↔
    BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].BoundedFormula Empty 0) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default) default
⊢ BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default ↔
    M ⊨ φ

Tactic:
refine _root_.trans ?_ BoundedFormula.realize_constantsVarsEquiv

Premises used: trans, FirstOrder.Language.BoundedFormula.realize_constantsVarsEquiv
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
rw :
  BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default =
    BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].BoundedFormula Empty 0) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default) default
⊢ BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default ↔
    BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].BoundedFormula Empty 0) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default) default

Tactic:
rw [iff_iff_eq]

Premises used: iff_iff_eq
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
e__v :
  ∀ (val : α),
    Eq.{w + 1} (α := M)
      (Function.comp (α := α ⊕ Empty) (fun (a : α) ↦ (↑(L.con a) : M)) (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)
        (Sum.inl val))
      (Sum.elim (β := Empty) (fun (a : α) ↦ (↑(L.con a) : M)) default (Sum.inl val))
e__v₁ :
  ∀ (a : Empty),
    Eq.{w + 1} (α := M)
      (Function.comp (α := α ⊕ Empty) (fun (a : α) ↦ (↑(L.con a) : M)) (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)
        (Sum.inr a))
      (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default (Sum.inr a))
⊢ BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].Sentence) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      ((fun (a : α) ↦ (↑(L.con a) : M)) ∘ (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)) default =
    BoundedFormula.Realize.{u, v, w, u'} (L := L) (M := M) (α := α ⊕ Empty) (l := 0)
      ((BoundedFormula.constantsVarsEquiv : (a : L[[α]].BoundedFormula Empty 0) → L.BoundedFormula (α ⊕ Empty) 0) φ)
      (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default) default

Tactic:
congr 1 with (_ | a)
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
val : α
⊢ Eq.{w + 1} (α := M)
    (Function.comp (α := α ⊕ Empty) (fun (a : α) ↦ (↑(L.con a) : M)) (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)
      (Sum.inl val))
    (Sum.elim (β := Empty) (fun (a : α) ↦ (↑(L.con a) : M)) default (Sum.inl val))

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L[[α]].Sentence
a : Empty
⊢ Eq.{w + 1} (α := M)
    (Function.comp (α := α ⊕ Empty) (fun (a : α) ↦ (↑(L.con a) : M)) (⇑(Equiv.sumEmpty α Empty) : (a : α ⊕ Empty) → α)
      (Sum.inr a))
    (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) default (Sum.inr a))

Tactic:
cases a
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
φ : L.Formula α
rw :
  (Realize.{u, v, w, u'} (L := L) (M := M)
      ((_root_.Equiv.symm equivSentence : (a : L[[α]].Sentence) → L.Formula α)
        ((equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ))
      fun (a : α) ↦ (↑(L.con a) : M)) ↔
    Realize.{u, v, w, u'} (M := M) φ fun (a : α) ↦ (↑(L.con a) : M)
rw₁ rw₂ :
  (Realize.{u, v, w, u'} (M := M) φ fun (a : α) ↦ (↑(L.con a) : M)) ↔
    Realize.{u, v, w, u'} (M := M) φ fun (a : α) ↦ (↑(L.con a) : M)
⊢ Sentence.Realize (L := L[[α]]) M ((equivSentence : (a : L.Formula α) → L[[α]].Sentence) φ) ↔
    Realize.{u, v, w, u'} (M := M) φ fun (a : α) ↦ (↑(L.con a) : M)

Tactic:
rw [← realize_equivSentence_symm_con M (equivSentence φ), _root_.Equiv.symm_apply_apply]

Premises used: FirstOrder.Language.Formula.equivSentence, Equiv.symm_apply_apply, FirstOrder.Language.Formula.realize_equivSentence_symm_con, DFunLike.coe
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
φ : L[[α]].Sentence
v : α → M
⊢ Realize.{u, v, w, u'} (L := L) ((_root_.Equiv.symm equivSentence : (a : L[[α]].Sentence) → L.Formula α) φ) v ↔ M ⊨ φ

Tactic:
letI := constantsOn.structure v
  realize_equivSentence_symm_con M φ

Premises used: FirstOrder.Language.Formula.realize_equivSentence_symm_con, FirstOrder.Language.constantMap, Sum.elim
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
ψ : L.Sentence
⊢ M ⊨ φ.onSentence ψ ↔ M ⊨ ψ

Tactic:
φ.realize_onFormula ψ

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.LHom.realize_onFormula, FirstOrder.Language.LHom.onSentence
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
φ : L.Sentence
⊢ φ ∈ L.completeTheory M ↔ M ⊨ φ

Tactic:
Iff.rfl

Premises used: FirstOrder.Language.Sentence.Realize, FirstOrder.Language.completeTheory, Set.Mem, Iff.rfl, setOf, FirstOrder.Language.Formula.Realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
N : Type u_1
inst : L.Structure M
inst_1 : L.Structure N
⊢ M ≅[L] N ↔ ∀ (φ : L.Sentence), M ⊨ φ ↔ N ⊨ φ

Tactic:
simp only [ElementarilyEquivalent, Set.ext_iff, completeTheory, Set.mem_setOf_eq]

Premises used: FirstOrder.Language.completeTheory, FirstOrder.Language.ElementarilyEquivalent, Set.mem_setOf_eq, Set.ext_iff
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
⊢ M ⊨ T ↔ ∀ φ ∈ T, M ⊨ φ

Tactic:
⟨fun h => h.realize_of_mem, fun h => ⟨h⟩⟩

Premises used: FirstOrder.Language.Theory.Model.realize_of_mem, FirstOrder.Language.Theory.Model.mk, Iff.intro
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
T : L.Theory
inst_1 : M ⊨ T
φ : L.Sentence
h : φ ∈ T
⊢ M ⊨ φ

Tactic:
Theory.Model.realize_of_mem φ h

Premises used: FirstOrder.Language.Theory.Model.realize_of_mem
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
inst_1 : L'.Structure M
φ : L →ᴸ L'
inst_2 : φ.IsExpansionOn M
T : L.Theory
⊢ M ⊨ φ.onTheory T ↔ M ⊨ T

Tactic:
simp [Theory.model_iff, LHom.onTheory]

Premises used: FirstOrder.Language.Theory.model_iff, FirstOrder.Language.LHom.onTheory
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type u_2
inst : L.Structure M
inst_1 : L.Structure N
inst_2 : L.Structure P
α : Type u'
β : Type v'
γ : Type u_3
n : ℕ
T : L.Theory
⊢ Theory.Model.{u, v, w} (L := L) M ∅

Tactic:
⟨fun φ hφ => (Set.notMem_empty φ hφ).elim⟩

Premises used: False.elim, FirstOrder.Language.Theory.Model.mk, Set.notMem_empty
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
T T' : L.Theory
_h : M ⊨ T'
hs : T ⊆ T'
⊢ M ⊨ T

Tactic:
⟨fun _φ hφ => T'.realize_sentence_of_mem (hs hφ)⟩

Premises used: FirstOrder.Language.Theory.Model.mk, FirstOrder.Language.Theory.realize_sentence_of_mem
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
T T' : L.Theory
h : M ⊨ T
h' : M ⊨ T'
simp : ∀ (h : ∀ φ ∈ T, M ⊨ φ) (h' : ∀ φ ∈ T', M ⊨ φ) (φ : L.Sentence), φ ∈ T ∨ φ ∈ T' → M ⊨ φ
⊢ M ⊨ T ∪ T'

Tactic:
simp only [model_iff, Set.mem_union] at *

Premises used: Set.mem_union, FirstOrder.Language.Theory.model_iff