-- Mathlib/ModelTheory/Semantics.lean
theorem realize_constantsToVars [L[[α]].Structure M] [(lhomWithConstants L α).IsExpansionOn M]
    {t : L[[α]].Term β} {v : β → M} :
    t.constantsToVars.realize (Sum.elim (fun a => ↑(L.con a)) v) = t.realize v

Proof state:
case var
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
a✝ : β
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (var a✝).constantsToVars = realize v (var a✝)

Tactic:
simp

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
t : L[[α]].Term β
v : β → M
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) t.constantsToVars = realize v t

Tactic:
induction' t with _ n f ts ih

Result:
case var
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
a✝ : β
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (var a✝).constantsToVars = realize v (var a✝)

case func
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (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)) v) (ts a).constantsToVars = realize v (ts a)
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

Proof state:
case func.succ.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (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)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions (n✝ + 1)
⊢ (funMap val✝ fun i => realize v (ts i)) = funMap (Sum.inl val✝) fun i => realize v (ts i)

Tactic:
rw [withConstants_funMap_sumInl]

Result:
no goals

Proof state:
case func.succ.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (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)) v) (ts a).constantsToVars = realize v (ts a)
f : (constantsOn α).Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (func (Sum.inr f) ts).constantsToVars = realize v (func (Sum.inr f) ts)

Tactic:
exact isEmptyElim f

Result:
no goals

Proof state:
case func.zero.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a => ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions 0
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)

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

Result:
case func.zero.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a => ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions 0
⊢ (funMap val✝ fun i => realize v (ts i)) = funMap (Sum.inl val✝) fun i => realize v (ts i)

Proof state:
case func.zero.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a => ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : (constantsOn α).Functions 0
⊢ ↑(L.con val✝) = ↑(Sum.inr val✝)

Tactic:
rfl

Result:
no goals

Proof state:
case func.succ
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (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)) v) (ts a).constantsToVars = realize v (ts a)
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

Tactic:
obtain - | f := f

Result:
case func.succ.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (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)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)

case func.succ.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (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)) v) (ts a).constantsToVars = realize v (ts a)
f : (constantsOn α).Functions (n✝ + 1)
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (func (Sum.inr f) ts).constantsToVars = realize v (func (Sum.inr f) ts)

Proof state:
case func.zero
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (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)) v) (ts a).constantsToVars = realize v (ts a)
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (func f ts).constantsToVars = realize v (func f ts)

Tactic:
cases f

Result:
case func.zero.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a => ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions 0
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (func (Sum.inl val✝) ts).constantsToVars =
    realize v (func (Sum.inl val✝) ts)

case func.zero.inr
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a => ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : (constantsOn α).Functions 0
⊢ realize (Sum.elim (fun a => ↑(L.con a)) v) (func (Sum.inr val✝) ts).constantsToVars =
    realize v (func (Sum.inr val✝) ts)

Proof state:
case func.zero.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a => ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions 0
⊢ (funMap val✝ fun i => realize v (ts i)) = funMap (Sum.inl val✝) fun i => realize v (ts i)

Tactic:
rw [withConstants_funMap_sumInl]

Result:
no goals