Theorem: LO.FirstOrder.Structure.extendStructure.models_lMap (Logic/FirstOrder/Completeness/SubLanguage.lean)

State before:
μ : Sort ?u.144343
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
σ : Sentence L₁
⊢ (extendStructure Φ s₁).toStruc ⊧ (lMap Φ) σ ↔ s₁.toStruc ⊧ σ
Tactic:
simp[Semantics.Realize, Evalf, eval_lMap Φ injf injr]
State after:
no goals