simp[Semantics.realizeSet_iff]
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧* ⇑(Semiformula.lMap Φ) '' T
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
T : Theory L₁
M : Type u
i : Nonempty M
s : Structure L₁ M
hM : { Dom := M, nonempty := i, struc := s } ⊧* T
⊢ ∀ a ∈ T, { Dom := M, nonempty := i, struc := Structure.extendStructure Φ s } ⊧ (Semiformula.lMap Φ) a