L : Language
L' : Language
M : Type w
N : Type ?u.246639
P : Type ?u.246642
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
f : Functions L n
x : Fin n → M
y : M
⊢ (y = funMap f fun i => x i) ↔ funMap f x = y
L : Language
L' : Language
M : Type w
N : Type ?u.246639
P : Type ?u.246642
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
f : Functions L n
x : Fin n → M
y : M
⊢ Realize (graph f) (cons y x) ↔ funMap f x = y
simp only [Formula.graph, Term.realize, realize_equal, Fin.cons_zero, Fin.cons_succ]
no goals
L : Language
L' : Language
M : Type w
N : Type ?u.246639
P : Type ?u.246642
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
φ ψ : Formula L α
v : α → M
f : Functions L n
x : Fin n → M
y : M
⊢ (y = funMap f fun i => x i) ↔ funMap f x = y
rw [eq_comm]