L : Language
L' : Language
M : Type w
N : Type ?u.55232
P : Type ?u.55235
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 2
t₁ t₂ : Term L (α ⊕ Fin l)
⊢ (RelMap R fun i => realize (Sum.elim v xs) (Matrix.vecCons t₁ ![t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
L : Language
L' : Language
M : Type w
N : Type ?u.55232
P : Type ?u.55235
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 2
t₁ t₂ : Term L (α ⊕ Fin l)
⊢ Realize (Relations.boundedFormula₂ R t₁ t₂) v xs ↔ RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
rw [Relations.boundedFormula₂, realize_rel, iff_eq_eq]
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.55232
P : Type ?u.55235
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 2
t₁ t₂ : Term L (α ⊕ Fin l)
⊢ realize (Sum.elim v xs) (Matrix.vecCons t₁ ![t₂] 0) =
    Matrix.vecCons (realize (Sum.elim v xs) t₁) ![realize (Sum.elim v xs) t₂] 0

case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.55232
P : Type ?u.55235
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 2
t₁ t₂ : Term L (α ⊕ Fin l)
⊢ ∀ (i : Fin 1),
    realize (Sum.elim v xs) (Matrix.vecCons t₁ ![t₂] (succ i)) =
      Matrix.vecCons (realize (Sum.elim v xs) t₁) ![realize (Sum.elim v xs) t₂] (succ i)
L : Language
L' : Language
M : Type w
N : Type ?u.55232
P : Type ?u.55235
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 2
t₁ t₂ : Term L (α ⊕ Fin l)
⊢ (RelMap R fun i => realize (Sum.elim v xs) (Matrix.vecCons t₁ ![t₂] i)) =
    RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
refine' congr rfl (funext (Fin.cases _ _))
no goals
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.55232
P : Type ?u.55235
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 2
t₁ t₂ : Term L (α ⊕ Fin l)
⊢ realize (Sum.elim v xs) (Matrix.vecCons t₁ ![t₂] 0) =
    Matrix.vecCons (realize (Sum.elim v xs) t₁) ![realize (Sum.elim v xs) t₂] 0
simp only [Matrix.cons_val_zero]
no goals
case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.55232
P : Type ?u.55235
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 2
t₁ t₂ : Term L (α ⊕ Fin l)
⊢ ∀ (i : Fin 1),
    realize (Sum.elim v xs) (Matrix.vecCons t₁ ![t₂] (succ i)) =
      Matrix.vecCons (realize (Sum.elim v xs) t₁) ![realize (Sum.elim v xs) t₂] (succ i)
simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]