Theorem: LO.FirstOrder.Theory.modelsTheory_onTheory₁ (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
M : Type u
inst✝ : Nonempty M
s₂ : Structure L₂ M
T₁ : Theory L₁
⊢ M ⊧ₘ* lMap Φ T₁ ↔ M ⊧ₘ* T₁
Tactic:
simp [Semiformula.models_lMap, Theory.lMap, modelsTheory_iff, @modelsTheory_iff (T := T₁)]
State after:
no goals