L : Language
L' : Language
M : Type w
N : Type ?u.54593
P : Type ?u.54596
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
R : Relations L 1
t : Term L (α ⊕ Fin l)
⊢ (RelMap R fun i => realize (Sum.elim v xs) (Matrix.vecCons t ![] i)) = RelMap R ![realize (Sum.elim v xs) t]
L : Language
L' : Language
M : Type w
N : Type ?u.54593
P : Type ?u.54596
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
R : Relations L 1
t : Term L (α ⊕ Fin l)
⊢ Realize (Relations.boundedFormula₁ R t) v xs ↔ RelMap R ![realize (Sum.elim v xs) t]
rw [Relations.boundedFormula₁, realize_rel, iff_eq_eq]
L : Language
L' : Language
M : Type w
N : Type ?u.54593
P : Type ?u.54596
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
R : Relations L 1
t : Term L (α ⊕ Fin l)
x✝ : Fin 1
⊢ realize (Sum.elim v xs) (Matrix.vecCons t ![] x✝) = Matrix.vecCons (realize (Sum.elim v xs) t) ![] x✝
L : Language
L' : Language
M : Type w
N : Type ?u.54593
P : Type ?u.54596
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
R : Relations L 1
t : Term L (α ⊕ Fin l)
⊢ (RelMap R fun i => realize (Sum.elim v xs) (Matrix.vecCons t ![] i)) = RelMap R ![realize (Sum.elim v xs) t]
refine' congr rfl (funext fun _ => _)
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.54593
P : Type ?u.54596
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n l : ℕ
φ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
R : Relations L 1
t : Term L (α ⊕ Fin l)
x✝ : Fin 1
⊢ realize (Sum.elim v xs) (Matrix.vecCons t ![] x✝) = Matrix.vecCons (realize (Sum.elim v xs) t) ![] x✝
simp only [Matrix.cons_val_fin_one]