L : Language
M : Type u_3
N : Type u_4
P : Type ?u.308452
Q : Type ?u.308455
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
h :
  Formula.Realize (Formula.graph f) (↑φ ∘ Fin.cons (funMap f x) x) ↔
    Formula.Realize (Formula.graph f) (Fin.cons (funMap f x) x)
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.308452
Q : Type ?u.308455
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
have h := φ.map_formula (Formula.graph f) (Fin.cons (funMap f x) x)
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.308452
Q : Type ?u.308455
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
h : funMap f (↑φ ∘ x) = ↑φ (funMap f x) ↔ funMap f x = funMap f x
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.308452
Q : Type ?u.308455
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
h :
  Formula.Realize (Formula.graph f) (↑φ ∘ Fin.cons (funMap f x) x) ↔
    Formula.Realize (Formula.graph f) (Fin.cons (funMap f x) x)
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
rw [Formula.realize_graph, Fin.comp_cons, Formula.realize_graph] at h
no goals
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.308452
Q : Type ?u.308455
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
φ : M ↪ₑ[L] N
n : ℕ
f : Functions L n
x : Fin n → M
h : funMap f (↑φ ∘ x) = ↑φ (funMap f x) ↔ funMap f x = funMap f x
⊢ ↑φ (funMap f x) = funMap f (↑φ ∘ x)
rw [eq_comm, h]