awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (constantsOn α).Functions 0
func : Eq.{w + 1} (α := M) (↑(L.con val) : M) (↑(Sum.inr val) : M)
⊢ 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)

Tactic:
simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]

Premises used: FirstOrder.Language.Term.constantsToVars, FirstOrder.Language.funMap_eq_coe_constants, FirstOrder.Language.Term.realize, Sum.elim_inl
-- 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 : (constantsOn α).Functions 0
⊢ Eq.{w + 1} (α := M) (↑(L.con val) : M) (↑(Sum.inr val) : M)

Tactic:
rfl
-- 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 + 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)
func :
  ∀ (val : L.Functions (n + 1)),
    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₁ :
  ∀ (f : (constantsOn α).Functions (n + 1)),
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func (Sum.inr f) ts).constantsToVars =
      realize v (Language.func (Sum.inr f) ts)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts).constantsToVars =
    realize v (Language.func f ts)

Tactic:
obtain - | f := 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
n : ℕ
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)
val : L.Functions (n + 1)
func :
  Eq.{w + 1} (α := M) (funMap val fun (i : Fin (n + 1)) ↦ realize v (ts i))
    (funMap (L := L[[α]]) (n := n + 1) (Sum.inl val) fun (i : Fin (n + 1)) ↦ 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
n : ℕ
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)
val : L.Functions (n + 1)
func func₁ :
  Eq.{w + 1} (α := M) (funMap val fun (i : Fin (n + 1)) ↦ realize v (ts i))
    (funMap val fun (i : Fin (n + 1)) ↦ realize v (ts i))
⊢ Eq.{w + 1} (α := M) (funMap val fun (i : Fin (n + 1)) ↦ realize v (ts i))
    (funMap (L := L[[α]]) (n := n + 1) (Sum.inl val) fun (i : Fin (n + 1)) ↦ realize v (ts i))

Tactic:
rw [withConstants_funMap_sumInl]

Premises used: FirstOrder.Language.withConstants_funMap_sumInl
-- 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 : ℕ
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)
f : (constantsOn α).Functions (n + 1)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func (Sum.inr f) ts).constantsToVars =
    realize v (func (Sum.inr f) ts)

Tactic:
isEmptyElim f

Premises used: isEmptyElim
-- 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 : ℕ
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)
f : (constantsOn α).Functions (n + 1)
⊢ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (func (Sum.inr f) ts).constantsToVars =
    realize v (func (Sum.inr f) ts)

Tactic:
exact isEmptyElim 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
t : L[[α]].Term β
v : β → M
var :
  ∀ (a : β),
    realize (L := L) (α := α ⊕ β) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (constantsToVars (Language.var a)) =
      realize (L := L[[α]]) v (Language.var a)
func :
  ∀ {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)),
    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) t.constantsToVars = realize v t

Tactic:
induction t with
  | var => simp
  | @func n f ts ih =>
    cases n
    · cases f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
        rfl
    · obtain - | f := f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · exact isEmptyElim f

Premises used: FirstOrder.Language.constantsOnFunc, FirstOrder.Language.Term.func, FirstOrder.Language.constantsOn, FirstOrder.Language.Term.constantsToVars, FirstOrder.Language.withConstants_funMap_sumInl, FirstOrder.Language.Term.var, FirstOrder.Language.funMap_eq_coe_constants, FirstOrder.Language.Term.realize, Sum.elim_inl
-- 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
ab : α ⊕ β
var :
  ∀ (a : α),
    realize (L := L[[α]]) v (varsToConstants (Language.var (Sum.inl a))) =
      realize (L := L) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.var (Sum.inl a))
var₁ :
  ∀ (b : β),
    realize (L := L[[α]]) v (varsToConstants (Language.var (Sum.inr b))) =
      realize (L := L) (α := α ⊕ β) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.var (Sum.inr b))
⊢ realize (L := L[[α]]) v (varsToConstants (Language.var ab)) =
    realize (L := L) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.var ab)

Tactic:
rcases ab with a | b
-- 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[[α]]) v (varsToConstants (var (Sum.inl a))) =
    realize (L := L) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (var (Sum.inl a))

Tactic:
simp [Language.con]

Premises used: FirstOrder.Language.con
-- 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
b : β
⊢ realize (L := L[[α]]) v (varsToConstants (var (Sum.inr b))) =
    realize (L := L) (α := α ⊕ β) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (var (Sum.inr b))

Tactic:
simp [Language.con]

Premises used: FirstOrder.Language.con
-- 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
l : ℕ
f : L.Functions l
ts : Fin l → L.Term (α ⊕ β)
ih : ∀ (a : Fin l), realize v (ts a).varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a)
func :
  Eq.{w + 1} (α := M)
    (funMap (L := L[[α]]) (n := l) (Sum.inl f) fun (i : Fin l) ↦
      realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
    (funMap f fun (i : Fin l) ↦ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
⊢ realize v (Language.func f ts).varsToConstants =
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts)

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

Premises used: FirstOrder.Language.constantsOnFunc, FirstOrder.Language.constantsOn, FirstOrder.Language.Term.varsToConstants, 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
l : ℕ
f : L.Functions l
ts : Fin l → L.Term (α ⊕ β)
ih : ∀ (a : Fin l), realize v (ts a).varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a)
func func₁ :
  Eq.{w + 1} (α := M) (funMap f fun (i : Fin l) ↦ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
    (funMap f fun (i : Fin l) ↦ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
⊢ Eq.{w + 1} (α := M)
    (funMap (L := L[[α]]) (n := l) (Sum.inl f) fun (i : Fin l) ↦
      realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))
    (funMap f fun (i : Fin l) ↦ realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts i))

Tactic:
rw [withConstants_funMap_sumInl]

Premises used: FirstOrder.Language.withConstants_funMap_sumInl
-- 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
t : L.Term (α ⊕ β)
v : β → M
var :
  ∀ (ab : α ⊕ β),
    realize (L := L[[α]]) v (varsToConstants (Language.var ab)) =
      realize (L := L) (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.var ab)
func :
  ∀ {l : ℕ} (f : L.Functions l) (ts : Fin l → L.Term (α ⊕ β))
    (ih :
      ∀ (a : Fin l), realize v (ts a).varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (ts a)),
    realize v (Language.func f ts).varsToConstants =
      realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) (Language.func f ts)
⊢ realize v t.varsToConstants = realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) t

Tactic:
induction t with
  | var ab => rcases ab with a | b <;> simp [Language.con]
  | func f ts ih =>
    simp only [realize, constantsOn, constantsOnFunc, ih, varsToConstants]
    -- Porting note: below lemma does not work with simp for some reason
    rw [withConstants_funMap_sumInl]

Premises used: FirstOrder.Language.constantsOnFunc, FirstOrder.Language.Term.func, FirstOrder.Language.constantsOn, FirstOrder.Language.withConstants_funMap_sumInl, FirstOrder.Language.con, FirstOrder.Language.Term.var, FirstOrder.Language.Term.varsToConstants, 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
simp :
  realize
      (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
      t.constantsToVars =
    realize (Sum.elim v xs) t
⊢ realize (L := L) (α := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      ((constantsVarsEquivLeft : (a : L[[α]].Term (β ⊕ Fin n)) → L.Term ((α ⊕ β) ⊕ Fin n)) t) =
    realize (Sum.elim v xs) t

Tactic:
simp only [constantsVarsEquivLeft, realize_relabel, Equiv.coe_trans, Function.comp_apply,
    constantsVarsEquiv_apply, relabelEquiv_symm_apply]

Premises used: FirstOrder.Language.Term.constantsVarsEquivLeft, FirstOrder.Language.Term.realize_relabel, FirstOrder.Language.Term.constantsVarsEquiv_apply, FirstOrder.Language.Term.relabelEquiv_symm_apply, Function.comp_apply, Equiv.coe_trans
-- 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize
      (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
      t.constantsToVars =
    realize (Sum.elim v xs) t

Tactic:
_root_.trans ?_ realize_constantsToVars

Premises used: trans, FirstOrder.Language.Term.realize_constantsToVars
-- 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
refine :
  realize
      (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
      t.constantsToVars =
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs)) t.constantsToVars
⊢ realize
      (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
      t.constantsToVars =
    realize (Sum.elim v xs) t

Tactic:
refine _root_.trans ?_ realize_constantsToVars

Premises used: trans, FirstOrder.Language.Term.realize_constantsToVars
-- 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
e_v :
  Eq (α := Sum.{u', v'} α (β ⊕ Fin n) → M)
    (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
    (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs))
⊢ realize
      (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
      t.constantsToVars =
    realize (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs)) t.constantsToVars

Tactic:
congr 1
-- 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
e_v :
  ∀ (x : Sum.{u', v'} α (β ⊕ Fin n)),
    Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) x =
      Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) x
⊢ Eq (α := Sum.{u', v'} α (β ⊕ Fin n) → M)
    (Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n))
    (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs))

Tactic:
funext x
-- 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : Sum.{u', v'} α (β ⊕ Fin n)
e_v :
  ∀ (a : α),
    Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
        (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) (Sum.inl a) =
      Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inl a)
e_v₁ :
  ∀ (b : β),
    Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
        (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n)
        (Sum.inr (Sum.inl b)) =
      Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inr (Sum.inl b))
e_v₂ :
  ∀ (i : Fin n),
    Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
        (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
        (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n)
        (Sum.inr (Sum.inr i)) =
      Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inr (Sum.inr i))
⊢ Function.comp (β := (α ⊕ β) ⊕ Fin n) (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) x =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) x

Tactic:
rcases x with (a | (b | i))
-- 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
a : α
⊢ Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
      (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n) (Sum.inl a) =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inl 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
b : β
⊢ Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
      (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n)
      (Sum.inr (Sum.inl b)) =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inr (Sum.inl b))

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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
i : Fin n
⊢ Function.comp (α := Sum.{u', v'} α (β ⊕ Fin n)) (β := (α ⊕ β) ⊕ Fin n)
      (Sum.elim (Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) v) xs)
      (⇑(_root_.Equiv.symm (Equiv.sumAssoc α β (Fin n))) : (a : α ⊕ β ⊕ Fin n) → (α ⊕ β) ⊕ Fin n)
      (Sum.inr (Sum.inr i)) =
    Sum.elim (fun (a : α) ↦ (↑(L.con a) : M)) (Sum.elim v xs) (Sum.inr (Sum.inr i))

Tactic:
simp
-- 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
v : α → M
a : α
⊢ Term.realize v (φ.onTerm (var a)) = Term.realize.{u, v, w, u'} (L := L) v (var a)

Tactic:
rfl
-- 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
v : α → M
l : ℕ
f : L.Functions l
ts : Fin l → L.Term α
ih : ∀ (a : Fin l), Term.realize v (φ.onTerm (ts a)) = Term.realize v (ts a)
⊢ Term.realize v (φ.onTerm (func f ts)) = Term.realize v (func f ts)

Tactic:
simp only [Term.realize, LHom.onTerm, LHom.map_onFunction, ih]

Premises used: FirstOrder.Language.LHom.onTerm, FirstOrder.Language.LHom.map_onFunction, FirstOrder.Language.Term.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
t : L.Term α
v : α → M
var : ∀ (a : α), Term.realize v (φ.onTerm (Language.var a)) = Term.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), Term.realize v (φ.onTerm (ts a)) = Term.realize v (ts a)),
    Term.realize v (φ.onTerm (Language.func f ts)) = Term.realize v (Language.func f ts)
⊢ Term.realize v (φ.onTerm t) = Term.realize v t

Tactic:
induction t with
  | var => rfl
  | func f ts ih => simp only [Term.realize, LHom.onTerm, LHom.map_onFunction, ih]

Premises used: FirstOrder.Language.LHom.onTerm, FirstOrder.Language.LHom.map_onFunction, FirstOrder.Language.Term.func, FirstOrder.Language.Term.var, FirstOrder.Language.Term.realize
-- 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
t : L.Term α
v : α → M
var :
  ∀ (a : α),
    Eq.{u_1 + 1} (α := N) (Term.realize.{u, v, u_1, u'} (L := L) ((⇑g : (a : M) → N) ∘ v) (Language.var a) : N)
      ((g : (a : M) → N) (Term.realize.{u, v, w, u'} (L := L) v (Language.var a)) : N)
func :
  ∀ {l : ℕ} (_f : L.Functions l) (_ts : Fin l → L.Term α),
    (∀ (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) (Term.realize ((⇑g : (a : M) → N) ∘ v) (Language.func _f _ts) : N)
        ((g : (a : M) → N) (Term.realize v (Language.func _f _ts)) : N)
⊢ Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) t : N) ((g : (a : M) → N) (Term.realize v t) : N)

Tactic:
induction t
-- 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
a : α
⊢ Eq.{u_1 + 1} (α := N) (Term.realize.{u, v, u_1, u'} (L := L) ((⇑g : (a : M) → N) ∘ v) (var a) : N)
    ((g : (a : M) → N) (Term.realize.{u, v, w, u'} (L := L) v (var a)) : N)

Tactic:
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} (α := 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)))
⊢ Eq.{u_1 + 1} (α := N) (Term.realize ((⇑g : (a : M) → N) ∘ v) (Language.func _f _ts) : N)
    ((g : (a : M) → N) (Term.realize v (Language.func _f _ts)) : N)

Tactic:
rw [Term.realize, Term.realize, HomClass.map_fun]

Premises used: FirstOrder.Language.Term.realize, FirstOrder.Language.HomClass.map_fun