Theorem: LO.FirstOrder.Semiformula.models_lMap (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ : Language
L₂ : Language
Φ : L₁ →ᵥ L₂
M : Type u
inst✝ : Nonempty M
s₂ : Structure L₂ M
n : ℕ
e : Fin n → M
ε : μ → M
σ : Sentence L₁
⊢ s₂.toStruc ⊧ (lMap Φ) σ ↔ (Structure.lMap Φ s₂).toStruc ⊧ σ
Tactic:
simp [Semantics.Realize, Evalf, eval_lMap]
State after:
no goals