L : Language
L' : Language
M : Type w
N : Type ?u.22479
P : Type ?u.22482
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
n : ℕ
t : Term (L[[α]]) (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a => ↑(Language.con L a)) v) xs ∘ ↑(Equiv.sumAssoc α β (Fin n)).symm)
      (constantsToVars t) =
    realize (Sum.elim v xs) t
L : Language
L' : Language
M : Type w
N : Type ?u.22479
P : Type ?u.22482
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
n : ℕ
t : Term (L[[α]]) (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a => ↑(Language.con L a)) v) xs) (↑constantsVarsEquivLeft t) =
    realize (Sum.elim v xs) t
simp only [constantsVarsEquivLeft, realize_relabel, Equiv.coe_trans, Function.comp_apply,
  constantsVarsEquiv_apply, relabelEquiv_symm_apply]
L : Language
L' : Language
M : Type w
N : Type ?u.22479
P : Type ?u.22482
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
n : ℕ
t : Term (L[[α]]) (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a => ↑(Language.con L a)) v) xs ∘ ↑(Equiv.sumAssoc α β (Fin n)).symm)
      (constantsToVars t) =
    realize (Sum.elim (fun a => ↑(Language.con L a)) (Sum.elim v xs)) (constantsToVars t)
L : Language
L' : Language
M : Type w
N : Type ?u.22479
P : Type ?u.22482
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
n : ℕ
t : Term (L[[α]]) (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a => ↑(Language.con L a)) v) xs ∘ ↑(Equiv.sumAssoc α β (Fin n)).symm)
      (constantsToVars t) =
    realize (Sum.elim v xs) t
refine' _root_.trans _ realize_constantsToVars
case e_v.h
L : Language
L' : Language
M : Type w
N : Type ?u.22479
P : Type ?u.22482
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
n : ℕ
t : Term (L[[α]]) (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : α ⊕ β ⊕ Fin n
⊢ (Sum.elim (Sum.elim (fun a => ↑(Language.con L a)) v) xs ∘ ↑(Equiv.sumAssoc α β (Fin n)).symm) x =
    Sum.elim (fun a => ↑(Language.con L a)) (Sum.elim v xs) x
L : Language
L' : Language
M : Type w
N : Type ?u.22479
P : Type ?u.22482
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
n : ℕ
t : Term (L[[α]]) (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a => ↑(Language.con L a)) v) xs ∘ ↑(Equiv.sumAssoc α β (Fin n)).symm)
      (constantsToVars t) =
    realize (Sum.elim (fun a => ↑(Language.con L a)) (Sum.elim v xs)) (constantsToVars t)
rcongr x
no goals
case e_v.h
L : Language
L' : Language
M : Type w
N : Type ?u.22479
P : Type ?u.22482
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
inst✝¹ : Structure (L[[α]]) M
inst✝ : LHom.IsExpansionOn (lhomWithConstants L α) M
n : ℕ
t : Term (L[[α]]) (β ⊕ Fin n)
v : β → M
xs : Fin n → M
x : α ⊕ β ⊕ Fin n
⊢ (Sum.elim (Sum.elim (fun a => ↑(Language.con L a)) v) xs ∘ ↑(Equiv.sumAssoc α β (Fin n)).symm) x =
    Sum.elim (fun a => ↑(Language.con L a)) (Sum.elim v xs) x
rcases x with (a | (b | i)) <;> simp