no goals
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.653346
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
g : M ≃[L] N
φ : Formula L α
v : α → M
⊢ Formula.Realize φ (↑g ∘ v) ↔ Formula.Realize φ v
rw [Formula.Realize, Formula.Realize, ← g.realize_boundedFormula φ, iff_eq_eq,
  Unique.eq_default (g ∘ default)]