L : Language
L' : Language
M : Type w
N : Type ?u.237419
P : Type ?u.237422
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
R : Relations L 2
t₁ t₂ : Term L α
⊢ (RelMap R fun i => Term.realize v (Matrix.vecCons t₁ ![t₂] i)) = RelMap R ![Term.realize v t₁, Term.realize v t₂]
L : Language
L' : Language
M : Type w
N : Type ?u.237419
P : Type ?u.237422
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
R : Relations L 2
t₁ t₂ : Term L α
⊢ Realize (Relations.formula₂ R t₁ t₂) v ↔ RelMap R ![Term.realize v t₁, Term.realize v t₂]
rw [Relations.formula₂, realize_rel, iff_eq_eq]
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.237419
P : Type ?u.237422
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
R : Relations L 2
t₁ t₂ : Term L α
⊢ Term.realize v (Matrix.vecCons t₁ ![t₂] 0) = Matrix.vecCons (Term.realize v t₁) ![Term.realize v t₂] 0

case refine'_2
L : Language
L' : Language
M : Type w
N : Type ?u.237419
P : Type ?u.237422
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
R : Relations L 2
t₁ t₂ : Term L α
⊢ ∀ (i : Fin 1),
    Term.realize v (Matrix.vecCons t₁ ![t₂] (succ i)) = Matrix.vecCons (Term.realize v t₁) ![Term.realize v t₂] (succ i)
L : Language
L' : Language
M : Type w
N : Type ?u.237419
P : Type ?u.237422
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
R : Relations L 2
t₁ t₂ : Term L α
⊢ (RelMap R fun i => Term.realize v (Matrix.vecCons t₁ ![t₂] i)) = RelMap R ![Term.realize v t₁, Term.realize v t₂]
refine' congr rfl (funext (Fin.cases _ _))
no goals
case refine'_1
L : Language
L' : Language
M : Type w
N : Type ?u.237419
P : Type ?u.237422
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
R : Relations L 2
t₁ t₂ : Term L α
⊢ Term.realize v (Matrix.vecCons t₁ ![t₂] 0) = Matrix.vecCons (Term.realize v t₁) ![Term.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.237419
P : Type ?u.237422
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
R : Relations L 2
t₁ t₂ : Term L α
⊢ ∀ (i : Fin 1),
    Term.realize v (Matrix.vecCons t₁ ![t₂] (succ i)) = Matrix.vecCons (Term.realize v t₁) ![Term.realize v t₂] (succ i)
simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]