no goals
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.238691
Q : Type ?u.238694
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
α : Type u_5
φ : Formula L α
x : α → M
⊢ Formula.Realize φ (↑f ∘ x) ↔ Formula.Realize φ x
rw [Formula.Realize, Formula.Realize, ← f.map_boundedFormula, Unique.eq_default (f ∘ default)]