L : Language
L' : Language
M : Type w
N : Type ?u.6618
P : Type ?u.6621
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 2
t₁ t₂ : Term L α
v : α → M
⊢ (funMap f fun i => realize v (Matrix.vecCons t₁ ![t₂] i)) = funMap f ![realize v t₁, realize v t₂]
L : Language
L' : Language
M : Type w
N : Type ?u.6618
P : Type ?u.6621
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 2
t₁ t₂ : Term L α
v : α → M
⊢ realize v (Functions.apply₂ f t₁ t₂) = funMap f ![realize v t₁, realize v t₂]
rw [Functions.apply₂, Term.realize]
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.6618
P : Type ?u.6621
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 2
t₁ t₂ : Term L α
v : α → M
⊢ realize v (Matrix.vecCons t₁ ![t₂] 0) = Matrix.vecCons (realize v t₁) ![realize v t₂] 0

case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.6618
P : Type ?u.6621
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 2
t₁ t₂ : Term L α
v : α → M
⊢ ∀ (i : Fin 1), realize v (Matrix.vecCons t₁ ![t₂] (succ i)) = Matrix.vecCons (realize v t₁) ![realize v t₂] (succ i)
L : Language
L' : Language
M : Type w
N : Type ?u.6618
P : Type ?u.6621
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 2
t₁ t₂ : Term L α
v : α → M
⊢ (funMap f fun i => realize v (Matrix.vecCons t₁ ![t₂] i)) = funMap f ![realize v t₁, realize v t₂]
refine' congr rfl (funext (Fin.cases _ _))
no goals
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.6618
P : Type ?u.6621
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 2
t₁ t₂ : Term L α
v : α → M
⊢ realize v (Matrix.vecCons t₁ ![t₂] 0) = Matrix.vecCons (realize v t₁) ![realize v t₂] 0
simp only [Matrix.cons_val_zero]
no goals
case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.6618
P : Type ?u.6621
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
f : Functions L 2
t₁ t₂ : Term L α
v : α → M
⊢ ∀ (i : Fin 1), realize v (Matrix.vecCons t₁ ![t₂] (succ i)) = Matrix.vecCons (realize v t₁) ![realize v t₂] (succ i)
simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]