L : Language
L' : Language
M : Type w
N : Type ?u.5630
P : Type ?u.5633
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 1
t : Term L α
v : α → M
⊢ (funMap f fun i => realize v (Matrix.vecCons t ![] i)) = funMap f ![realize v t]
L : Language
L' : Language
M : Type w
N : Type ?u.5630
P : Type ?u.5633
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 1
t : Term L α
v : α → M
⊢ realize v (Functions.apply₁ f t) = funMap f ![realize v t]
rw [Functions.apply₁, Term.realize]
L : Language
L' : Language
M : Type w
N : Type ?u.5630
P : Type ?u.5633
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 1
t : Term L α
v : α → M
i : Fin 1
⊢ realize v (Matrix.vecCons t ![] i) = Matrix.vecCons (realize v t) ![] i
L : Language
L' : Language
M : Type w
N : Type ?u.5630
P : Type ?u.5633
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 1
t : Term L α
v : α → M
⊢ (funMap f fun i => realize v (Matrix.vecCons t ![] i)) = funMap f ![realize v t]
refine' congr rfl (funext fun i => _)
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.5630
P : Type ?u.5633
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 1
t : Term L α
v : α → M
i : Fin 1
⊢ realize v (Matrix.vecCons t ![] i) = Matrix.vecCons (realize v t) ![] i
simp only [Matrix.cons_val_fin_one]