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

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) t.constantsToVars =
    realize (Sum.elim (fun a => ↑(L.con a)) (Sum.elim v xs)) t.constantsToVars

Tactic:
rcongr x

Result:
case e_v.h
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : α ⊕ β ⊕ Fin n
⊢ (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) x =
    Sum.elim (fun a => ↑(L.con a)) (Sum.elim v xs) x

Proof state:
case e_v.h
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : α ⊕ β ⊕ Fin n
⊢ (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) x =
    Sum.elim (fun a => ↑(L.con a)) (Sum.elim v xs) x

Tactic:
rcases x with (a | (b | i)) <;> 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
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs) (constantsVarsEquivLeft t) = realize (Sum.elim v xs) t

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

Result:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) t.constantsToVars =
    realize (Sum.elim v xs) t

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) t.constantsToVars =
    realize (Sum.elim v xs) t

Tactic:
refine _root_.trans ?_ realize_constantsToVars

Result:
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a => ↑(L.con a)) v) xs ∘ ⇑(Equiv.sumAssoc α β (Fin n)).symm) t.constantsToVars =
    realize (Sum.elim (fun a => ↑(L.con a)) (Sum.elim v xs)) t.constantsToVars