Theorem: LO.FirstOrder.Arith.eval_memRel (Arithmetization/ISigmaOne/Bit.lean)

State before:
ξ : Type u_1
n : ?m.134755
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y r : M
⊢ memRelOpr.val ![r, x, y] ↔ ⟪x, y⟫ ∈ r
Tactic:
unfold Semiformula.Operator.val
State after:
ξ : Type u_1
n : ?m.134755
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y r : M
⊢ (Semiformula.Eval (standardModel M) ![r, x, y] Empty.elim) memRelOpr.sentence ↔ ⟪x, y⟫ ∈ r

State before:
ξ : Type u_1
n : ?m.134755
M : Type u_2
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
x y r : M
⊢ (Semiformula.Eval (standardModel M) ![r, x, y] Empty.elim) memRelOpr.sentence ↔ ⟪x, y⟫ ∈ r
Tactic:
simp [memRelOpr, pair_defined.df.iff, memRel_defined.df.iff]
State after:
no goals