Theorem: LO.FirstOrder.Arith.eval_lMap_oringEmb (Logic/FirstOrder/Arith/Model.lean)

State before:
n : ℕ
ξ : Type u_2
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
L : Language
inst✝⁶ : L.ORing
s : Structure L M
inst✝⁵ : Structure.Zero L M
inst✝⁴ : Structure.One L M
inst✝³ : Structure.Add L M
inst✝² : Structure.Mul L M
inst✝¹ : Structure.Eq L M
inst✝ : Structure.LT L M
e : Fin n → M
ε : ξ → M
p : Semiformula ℒₒᵣ ξ n
⊢ (Semiformula.Evalm M e ε) ((Semiformula.lMap oringEmb) p) ↔ (Semiformula.Evalm M e ε) p
Tactic:
simp [Semiformula.eval_lMap, standardModel_lMap_oringEmb_eq_standardModel]
State after:
no goals