awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
haveI : (this : Language.empty.Structure ℕ) → Language.empty.infiniteTheory.ModelType
⊢ Language.empty.infiniteTheory.ModelType

Tactic:
haveI : Language.empty.Structure ℕ := emptyStructure
-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
this : Language.empty.Structure ℕ
⊢ Language.empty.infiniteTheory.ModelType

Tactic:
exact ((model_infiniteTheory_iff Language.empty).2 (inferInstance : Infinite ℕ)).bundled

Premises used: Iff.mpr, FirstOrder.Language.empty, FirstOrder.Language.model_infiniteTheory_iff, inferInstance, FirstOrder.Language.Theory.Model.bundled
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
k : α
⊢ realize.{u, v, w, u'} (L := L) v (var k) = v k

Tactic:
rfl

Premises used: FirstOrder.Language.Term.realize, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
v : α → M
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
⊢ realize v (func f ts) = funMap f fun (i : Fin n) ↦ realize v (ts i)

Tactic:
rfl

Premises used: FirstOrder.Language.Term.realize, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
n : ℕ
v : Fin n → M
f : L.Functions n
⊢ realize v f.term = funMap f v

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
g : α → β
v : β → M
a : α
⊢ realize.{u, v, w, v'} (L := L) v (relabel g (var a)) = realize.{u, v, w, u'} (L := L) (v ∘ g) (var a)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
g : α → β
v : β → M
l : ℕ
f : L.Functions l
ts : Fin l → L.Term α
ih : ∀ (a : Fin l), realize v (relabel g (ts a)) = realize (v ∘ g) (ts a)
⊢ realize v (relabel g (func f ts)) = realize (v ∘ g) (func f ts)

Tactic:
simp [ih]
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
g : α → β
v : β → M
var :
  ∀ (a : α),
    realize.{u, v, w, v'} (L := L) v (relabel g (Language.var a)) =
      realize.{u, v, w, u'} (L := L) (v ∘ g) (Language.var a)
func :
  ∀ {l : ℕ} (f : L.Functions l) (ts : Fin l → L.Term α)
    (ih : ∀ (a : Fin l), realize v (relabel g (ts a)) = realize (v ∘ g) (ts a)),
    realize v (relabel g (Language.func f ts)) = realize (v ∘ g) (Language.func f ts)
⊢ realize v (relabel g t) = realize (v ∘ g) t

Tactic:
induction t with
  | var => rfl
  | func f ts ih => simp [ih]

Premises used: FirstOrder.Language.Term.func, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
n n' m : ℕ
t : Term.{u, v, u'} L (α ⊕ Fin n)
v : α ⊕ Fin (n + n') → M
⊢ realize v (liftAt n' m t) =
    realize (v ∘ Sum.map id fun (i : Fin n) ↦ if (↑i : ℕ) < m then castAdd n' i else i.addNat n') t

Tactic:
realize_relabel

Premises used: FirstOrder.Language.Term.realize_relabel, FirstOrder.Language.Term.liftAt
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
c : L.Constants
v : α → M
⊢ realize v c.term = (↑c : M)

Tactic:
funMap_eq_coe_constants

Premises used: FirstOrder.Language.funMap_eq_coe_constants, FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
rw : (funMap f fun (i : Fin 1) ↦ realize v (![t] i)) = funMap f ![realize v t]
⊢ realize v (f.apply₁ t) = funMap f ![realize v t]

Tactic:
rw [Functions.apply₁, Term.realize]

Premises used: FirstOrder.Language.Functions.apply₁, FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
⊢ (funMap f fun (i : Fin 1) ↦ realize v (![t] i)) = funMap f ![realize v t]

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

Premises used: funext, congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
refine : ∀ (i : Fin 1), realize v (![t] i) = ![realize v t] i
⊢ (funMap f fun (i : Fin 1) ↦ realize v (![t] i)) = funMap f ![realize v t]

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

Premises used: funext, congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
f : L.Functions 1
t : L.Term α
v : α → M
i : Fin 1
⊢ realize v (![t] i) = ![realize v t] i

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'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
rw : (funMap f fun (i : Fin 2) ↦ realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, realize v t₂]
⊢ realize v (f.apply₂ t₁ t₂) = funMap f ![realize v t₁, realize v t₂]

Tactic:
rw [Functions.apply₂, Term.realize]

Premises used: FirstOrder.Language.Functions.apply₂, FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ (funMap f fun (i : Fin 2) ↦ realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, 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'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
refine_1 : realize v (![t₁, t₂] 0) = ![realize v t₁, realize v t₂] 0
refine_2 : ∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, realize v t₂] i.succ
⊢ (funMap f fun (i : Fin 2) ↦ realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, 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'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ realize v (![t₁, t₂] 0) = ![realize v t₁, 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'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ ∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, 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'
A : Set M
a : (↑A : Type w)
v : α → M
⊢ realize v (L.con a).term = (↑a : M)

Tactic:
rfl

Premises used: FirstOrder.Language.Term.realize, rfl, Sum.elim
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
tf : α → L.Term β
v : β → M
a : α
⊢ realize v (subst (var a) tf) = realize.{u, v, w, u'} (L := L) (fun (a : α) ↦ realize v (tf a)) (var a)

Tactic:
rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
tf : α → L.Term β
v : β → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
ih : ∀ (a : Fin l), realize v ((_ts a).subst tf) = realize (fun (a : α) ↦ realize v (tf a)) (_ts a)
⊢ realize v ((func _f _ts).subst tf) = realize (fun (a : α) ↦ realize v (tf a)) (func _f _ts)

Tactic:
simp [ih]
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
t : L.Term α
tf : α → L.Term β
v : β → M
var :
  ∀ (a : α),
    realize v (subst (Language.var a) tf) =
      realize.{u, v, w, u'} (L := L) (fun (a : α) ↦ realize v (tf a)) (Language.var a)
func :
  ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α)
    (ih : ∀ (a : Fin l), realize v ((_ts a).subst tf) = realize (fun (a : α) ↦ realize v (tf a)) (_ts a)),
    realize v ((Language.func _f _ts).subst tf) = realize (fun (a : α) ↦ realize v (tf a)) (Language.func _f _ts)
⊢ realize v (t.subst tf) = realize (fun (a : α) ↦ realize v (tf a)) t

Tactic:
induction t with
  | var => rfl
  | func _ _ ih => simp [ih]

Premises used: FirstOrder.Language.Term.func, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
β : Type v'
inst_1 : L'.Structure M
c : {n : ℕ} → L.Functions n → L'.Term (Fin n)
hc : ∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M), realize y g.term = realize y (c g)
v : β → M
a : β
⊢ realize.{u_4, u_5, w, v'} (L := L') v (substFunc.{u, v, v', u_4, u_5} (L := L) (var a) fun {n : ℕ} ↦ c) =
    realize.{u, v, w, v'} (L := L) v (var a)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
β : Type v'
inst_1 : L'.Structure M
c : {n : ℕ} → L.Functions n → L'.Term (Fin n)
hc : ∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M), realize y g.term = realize y (c g)
v : β → M
l : ℕ
f : L.Functions l
ts : Fin l → L.Term β
ih : ∀ (a : Fin l), realize.{u_4, u_5, w, v'} (L := L') v ((ts a).substFunc fun {n : ℕ} ↦ c) = realize v (ts a)
⊢ realize.{u_4, u_5, w, v'} (L := L') v ((func f ts).substFunc fun {n : ℕ} ↦ c) = realize v (func f ts)

Tactic:
simp [← ih, ← hc]
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
β : Type v'
inst_1 : L'.Structure M
c : {n : ℕ} → L.Functions n → L'.Term (Fin n)
hc : ∀ {n : ℕ} (g : L.Functions n) (y : Fin n → M), realize y g.term = realize y (c g)
v : β → M
x : L.Term β
var :
  ∀ (a : β),
    realize.{u_4, u_5, w, v'} (L := L') v (substFunc.{u, v, v', u_4, u_5} (L := L) (Language.var a) fun {n : ℕ} ↦ c) =
      realize.{u, v, w, v'} (L := L) v (Language.var a)
func :
  ∀ {l : ℕ} (f : L.Functions l) (ts : Fin l → L.Term β)
    (ih : ∀ (a : Fin l), realize.{u_4, u_5, w, v'} (L := L') v ((ts a).substFunc fun {n : ℕ} ↦ c) = realize v (ts a)),
    realize.{u_4, u_5, w, v'} (L := L') v ((Language.func f ts).substFunc fun {n : ℕ} ↦ c) =
      realize v (Language.func f ts)
⊢ realize.{u_4, u_5, w, v'} (L := L') v (x.substFunc fun {n : ℕ} ↦ c) = realize v x

Tactic:
induction x with
  | var => simp
  | func f ts ih => simp [← ih, ← hc]

Premises used: FirstOrder.Language.Term.func, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
v : β → M
v' : α → M
a : α
f : ↥(varFinset.{u, v, u'} (L := L) (var a)) → β
hv' : ∀ (a_1 : ↥(varFinset.{u, v, u'} (L := L) (var a))), v (f a_1) = v' (↑a_1 : α)
⊢ realize v (restrictVar (var a) f) = realize.{u, v, w, u'} (L := L) v' (var a)

Tactic:
simp [restrictVar, hv']

Premises used: FirstOrder.Language.Term.restrictVar
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
v : β → M
v' : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
ih :
  ∀ (a : Fin l) {f : ↥(_ts a).varFinset → β} (hv' : ∀ (a_1 : ↥(_ts a).varFinset), v (f a_1) = v' (↑a_1 : α)),
    realize v ((_ts a).restrictVar f) = realize v' (_ts a)
f : ↥(func _f _ts).varFinset → β
hv' : ∀ (a : ↥(func _f _ts).varFinset), v (f a) = v' (↑a : α)
i : Fin l
⊢ ∀ (a : ↥(_ts i).varFinset),
    v ((f ∘ Set.inclusion (s := (↑(_ts i).varFinset : Set α)) (t := (↑(func _f _ts).varFinset : Set α)) ⋯) a) =
      v' (↑a : α)

Tactic:
simp [Function.comp_apply, hv']

Premises used: Function.comp_apply
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
v : β → M
v' : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term α
ih :
  ∀ (a : Fin l) {f : ↥(_ts a).varFinset → β} (hv' : ∀ (a_1 : ↥(_ts a).varFinset), v (f a_1) = v' (↑a_1 : α)),
    realize v ((_ts a).restrictVar f) = realize v' (_ts a)
f : ↥(func _f _ts).varFinset → β
hv' : ∀ (a : ↥(func _f _ts).varFinset), v (f a) = v' (↑a : α)
⊢ realize v ((func _f _ts).restrictVar f) = realize v' (func _f _ts)

Tactic:
exact congr rfl (funext fun i => ih i ((by simp [Function.comp_apply, hv'])))

Premises used: funext, congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
t : L.Term α
f : ↥t.varFinset → β
v : β → M
v' : α → M
hv' : ∀ (a : ↥t.varFinset), v (f a) = v' (↑a : α)
var :
  ∀ (a : α) {f : ↥(varFinset.{u, v, u'} (L := L) (Language.var a)) → β}
    (hv' : ∀ (a_1 : ↥(varFinset.{u, v, u'} (L := L) (Language.var a))), v (f a_1) = v' (↑a_1 : α)),
    realize v (restrictVar (Language.var a) f) = realize.{u, v, w, u'} (L := L) v' (Language.var a)
func :
  ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α)
    (ih :
      ∀ (a : Fin l) {f : ↥(_ts a).varFinset → β} (hv' : ∀ (a_1 : ↥(_ts a).varFinset), v (f a_1) = v' (↑a_1 : α)),
        realize v ((_ts a).restrictVar f) = realize v' (_ts a))
    {f : ↥(Language.func _f _ts).varFinset → β}
    (hv' : ∀ (a : ↥(Language.func _f _ts).varFinset), v (f a) = v' (↑a : α)),
    realize v ((Language.func _f _ts).restrictVar f) = realize v' (Language.func _f _ts)
⊢ realize v (t.restrictVar f) = realize v' t

Tactic:
induction t with
  | var => simp [restrictVar, hv']
  | func _ _ ih =>
    exact congr rfl (funext fun i => ih i ((by simp [Function.comp_apply, hv'])))

Premises used: FirstOrder.Language.Term.restrictVar, FirstOrder.Language.Term.func, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : DecidableEq α
t : L.Term α
s : Set α
h : (↑t.varFinset : Set α) ⊆ s
v : α → M
⊢ ∀ (a : ↥t.varFinset),
    (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Set.inclusion (s := (↑t.varFinset : Set α)) (t := s) h a) = v (↑a : α)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
a : α ⊕ γ
f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var a)) → β
hxs' : ∀ (a_1 : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var a))), xs (Sum.inl (f a_1)) = xs' (↑a_1 : α)
var :
  ∀ (val : α) {f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (β := γ) (Language.var (Sum.inl val))) → β}
    (hxs' :
      ∀ (a : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (β := γ) (Language.var (Sum.inl val)))),
        xs (Sum.inl (f a)) = xs' (↑a : α)),
    realize xs (restrictVarLeft (Language.var (Sum.inl val)) f) =
      realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (Language.var (Sum.inl val))
var₁ :
  ∀ (val : γ) {f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var (Sum.inr val))) → β}
    (hxs' :
      ∀ (a : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var (Sum.inr val)))),
        xs (Sum.inl (f a)) = xs' (↑a : α)),
    realize xs (restrictVarLeft (Language.var (Sum.inr val)) f) =
      realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (Language.var (Sum.inr val))
⊢ realize xs (restrictVarLeft (Language.var a) f) = realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (Language.var a)

Tactic:
cases a
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
val : α
f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (β := γ) (var (Sum.inl val))) → β
hxs' : ∀ (a : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (β := γ) (var (Sum.inl val)))), xs (Sum.inl (f a)) = xs' (↑a : α)
⊢ realize xs (restrictVarLeft (var (Sum.inl val)) f) =
    realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (var (Sum.inl val))

Tactic:
simp [restrictVarLeft, hxs']

Premises used: FirstOrder.Language.Term.restrictVarLeft
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
val : γ
f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (var (Sum.inr val))) → β
hxs' : ∀ (a : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (var (Sum.inr val)))), xs (Sum.inl (f a)) = xs' (↑a : α)
⊢ realize xs (restrictVarLeft (var (Sum.inr val)) f) =
    realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (var (Sum.inr val))

Tactic:
simp [restrictVarLeft, hxs']

Premises used: FirstOrder.Language.Term.restrictVarLeft
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term (α ⊕ γ)
ih :
  ∀ (a : Fin l) {f : ↥(_ts a).varFinsetLeft → β}
    (hxs' : ∀ (a_1 : ↥(_ts a).varFinsetLeft), xs (Sum.inl (f a_1)) = xs' (↑a_1 : α)),
    realize xs ((_ts a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (_ts a)
f : ↥(func _f _ts).varFinsetLeft → β
hxs' : ∀ (a : ↥(func _f _ts).varFinsetLeft), xs (Sum.inl (f a)) = xs' (↑a : α)
i : Fin l
⊢ ∀ (a : ↥(_ts i).varFinsetLeft),
    xs
        (Sum.inl
          ((f ∘ Set.inclusion (s := (↑(_ts i).varFinsetLeft : Set α)) (t := (↑(func _f _ts).varFinsetLeft : Set α)) ⋯)
            a)) =
      xs' (↑a : α)

Tactic:
simp [hxs']
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
γ : Type u_4
xs : β ⊕ γ → M
xs' : α → M
l : ℕ
_f : L.Functions l
_ts : Fin l → L.Term (α ⊕ γ)
ih :
  ∀ (a : Fin l) {f : ↥(_ts a).varFinsetLeft → β}
    (hxs' : ∀ (a_1 : ↥(_ts a).varFinsetLeft), xs (Sum.inl (f a_1)) = xs' (↑a_1 : α)),
    realize xs ((_ts a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (_ts a)
f : ↥(func _f _ts).varFinsetLeft → β
hxs' : ∀ (a : ↥(func _f _ts).varFinsetLeft), xs (Sum.inl (f a)) = xs' (↑a : α)
⊢ realize xs ((func _f _ts).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (func _f _ts)

Tactic:
exact congr rfl (funext fun i => ih i (by simp [hxs']))

Premises used: funext, congr, rfl
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : DecidableEq α
γ : Type u_4
t : L.Term (α ⊕ γ)
f : ↥t.varFinsetLeft → β
xs : β ⊕ γ → M
xs' : α → M
hxs' : ∀ (a : ↥t.varFinsetLeft), xs (Sum.inl (f a)) = xs' (↑a : α)
var :
  ∀ (a : α ⊕ γ) {f : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var a)) → β}
    (hxs' :
      ∀ (a_1 : ↥(varFinsetLeft.{u, v, u', u_4} (L := L) (Language.var a))), xs (Sum.inl (f a_1)) = xs' (↑a_1 : α)),
    realize xs (restrictVarLeft (Language.var a) f) = realize (L := L) (Sum.elim xs' (xs ∘ Sum.inr)) (Language.var a)
func :
  ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term (α ⊕ γ))
    (ih :
      ∀ (a : Fin l) {f : ↥(_ts a).varFinsetLeft → β}
        (hxs' : ∀ (a_1 : ↥(_ts a).varFinsetLeft), xs (Sum.inl (f a_1)) = xs' (↑a_1 : α)),
        realize xs ((_ts a).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (_ts a))
    {f : ↥(Language.func _f _ts).varFinsetLeft → β}
    (hxs' : ∀ (a : ↥(Language.func _f _ts).varFinsetLeft), xs (Sum.inl (f a)) = xs' (↑a : α)),
    realize xs ((Language.func _f _ts).restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) (Language.func _f _ts)
⊢ realize xs (t.restrictVarLeft f) = realize (Sum.elim xs' (xs ∘ Sum.inr)) t

Tactic:
induction t with
  | var a => cases a <;> simp [restrictVarLeft, hxs']
  | func _ _ ih =>
    exact congr rfl (funext fun i => ih i (by simp [hxs']))

Premises used: FirstOrder.Language.Term.restrictVarLeft, FirstOrder.Language.Term.func, FirstOrder.Language.Term.var
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
inst_1 : DecidableEq α
γ : Type u_4
t : L.Term (α ⊕ γ)
s : Set α
h : (↑t.varFinsetLeft : Set α) ⊆ s
v : α → M
xs : γ → M
⊢ ∀ (a : ↥t.varFinsetLeft),
    Sum.elim (v ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) xs
        (Sum.inl (Set.inclusion (s := (↑t.varFinsetLeft : Set α)) (t := s) h a)) =
      v (↑a : α)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
a : β
⊢ realize (L := L) (α := α ⊕ β) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (constantsToVars (var a)) =
    realize (L := L[[α]]) v (var a)

Tactic:
simp
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n : ℕ
f : L[[α]].Functions n
ts : Fin n → L[[α]].Term β
ih : ∀ (a : Fin n), realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)
func :
  ∀ (f : L[[α]].Functions 0) (ts : Fin 0 → L[[α]].Term β)
    (ih :
      ∀ (a : Fin 0), realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)),
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts).constantsToVars =
      realize v (Language.func f ts)
func₁ :
  ∀ (n : ℕ) (f : L[[α]].Functions (n + 1)) (ts : Fin (n + 1) → L[[α]].Term β)
    (ih :
      ∀ (a : Fin (n + 1)),
        realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)),
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts).constantsToVars =
      realize v (Language.func f ts)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts).constantsToVars =
    realize v (Language.func f ts)

Tactic:
cases n
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
f : L[[α]].Functions 0
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)
func :
  ∀ (val : L.Functions 0),
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func (Sum.inl val) ts).constantsToVars =
      realize v (Language.func (Sum.inl val) ts)
func₁ :
  ∀ (val : (constantsOn α).Functions 0),
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func (Sum.inr val) ts).constantsToVars =
      realize v (Language.func (Sum.inr val) ts)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts).constantsToVars =
    realize v (Language.func f ts)

Tactic:
cases f
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)
val : L.Functions 0
func :
  Eq.{w + 1} (α := M) (funMap val fun (i : Fin 0) ↦ realize v (ts i))
    (funMap (L := L[[α]]) (n := 0) (Sum.inl val) fun (i : Fin 0) ↦ realize v (ts i))
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func (Sum.inl val) ts).constantsToVars =
    realize v (Language.func (Sum.inl val) ts)

Tactic:
simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]

Premises used: FirstOrder.Language.constantsOnFunc, FirstOrder.Language.constantsOn, FirstOrder.Language.Term.constantsToVars, FirstOrder.Language.Term.realize
-- Module: Mathlib.ModelTheory.Semantics
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u'
β : Type v'
inst_1 : L[[α]].Structure M
inst_2 : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a).constantsToVars = realize v (ts a)
val : L.Functions 0
func func₁ :
  Eq.{w + 1} (α := M) (funMap val fun (i : Fin 0) ↦ realize v (ts i)) (funMap val fun (i : Fin 0) ↦ realize v (ts i))
⊢ Eq.{w + 1} (α := M) (funMap val fun (i : Fin 0) ↦ realize v (ts i))
    (funMap (L := L[[α]]) (n := 0) (Sum.inl val) fun (i : Fin 0) ↦ realize v (ts i))

Tactic:
rw [withConstants_funMap_sumInl]

Premises used: FirstOrder.Language.withConstants_funMap_sumInl