case var
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
ab : α ⊕ β
⊢ realize v (varsToConstants (var ab)) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (var ab)

case func
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
n : ℕ
f : Functions L n
ts : Fin n → Term L (α ⊕ β)
ih : ∀ (a : Fin n), realize v (varsToConstants (ts a)) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (ts a)
⊢ realize v (varsToConstants (func f ts)) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (func f ts)
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
t : Term L (α ⊕ β)
v : β → M
⊢ realize v (varsToConstants t) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) t
induction' t with ab n f ts ih
case var.inl
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
a : α
⊢ realize v (varsToConstants (var (Sum.inl a))) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (var (Sum.inl a))

case var.inr
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
b : β
⊢ realize v (varsToConstants (var (Sum.inr b))) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (var (Sum.inr b))
case var
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
ab : α ⊕ β
⊢ realize v (varsToConstants (var ab)) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (var ab)
cases' ab with a b
case var.inr
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
b : β
⊢ realize v (varsToConstants (var (Sum.inr b))) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (var (Sum.inr b))
case var.inl
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
a : α
⊢ realize v (varsToConstants (var (Sum.inl a))) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (var (Sum.inl a))

case var.inr
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
b : β
⊢ realize v (varsToConstants (var (Sum.inr b))) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (var (Sum.inr b))
. simp [Language.con, realize, constantMap, funMap_eq_coe_constants]
no goals
case var.inr
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
b : β
⊢ realize v (varsToConstants (var (Sum.inr b))) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (var (Sum.inr b))
. simp [realize, constantMap]
no goals
case var.inl
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
a : α
⊢ realize v (varsToConstants (var (Sum.inl a))) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (var (Sum.inl a))
simp [Language.con, realize, constantMap, funMap_eq_coe_constants]
no goals
case var.inr
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
b : β
⊢ realize v (varsToConstants (var (Sum.inr b))) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (var (Sum.inr b))
simp [realize, constantMap]
case func
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
n : ℕ
f : Functions L n
ts : Fin n → Term L (α ⊕ β)
ih : ∀ (a : Fin n), realize v (varsToConstants (ts a)) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (ts a)
⊢ (funMap (Sum.inl f) fun i => realize (Sum.elim (fun a => ↑(Language.con L a)) v) (ts i)) =
    funMap f fun i => realize (Sum.elim (fun a => ↑(Language.con L a)) v) (ts i)
case func
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
n : ℕ
f : Functions L n
ts : Fin n → Term L (α ⊕ β)
ih : ∀ (a : Fin n), realize v (varsToConstants (ts a)) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (ts a)
⊢ realize v (varsToConstants (func f ts)) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (func f ts)
simp only [realize, constantsOn, mk₂_Functions, ih]
no goals
case func
L : Language
L' : Language
M : Type w
N : Type ?u.19079
P : Type ?u.19082
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
v : β → M
n : ℕ
f : Functions L n
ts : Fin n → Term L (α ⊕ β)
ih : ∀ (a : Fin n), realize v (varsToConstants (ts a)) = realize (Sum.elim (fun a => ↑(Language.con L a)) v) (ts a)
⊢ (funMap (Sum.inl f) fun i => realize (Sum.elim (fun a => ↑(Language.con L a)) v) (ts i)) =
    funMap f fun i => realize (Sum.elim (fun a => ↑(Language.con L a)) v) (ts i)
rw [withConstants_funMap_sum_inl]