Theorem: LO.FirstOrder.Structure.Eq.eqv_symm (Logic/FirstOrder/Basic/Eq.lean)

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ eqv L a b → eqv L b a
Tactic:
have : M ⊧ₘ “∀ x y, x = y → y = x” := H.realize (Theory.eqAxiom.symm (L := L))
State after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
this : M ⊧ₘ (“∀' ∀' (#1 = #0 → #0 = #1)”)
⊢ eqv L a b → eqv L b a

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
this : M ⊧ₘ (“∀' ∀' (#1 = #0 → #0 = #1)”)
⊢ eqv L a b → eqv L b a
Tactic:
simp [models_def] at this
State after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
this : ∀ (x x_1 : M), op(=).val ![x, x_1] → op(=).val ![x_1, x]
⊢ eqv L a b → eqv L b a

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
this : ∀ (x x_1 : M), op(=).val ![x, x_1] → op(=).val ![x_1, x]
⊢ eqv L a b → eqv L b a
Tactic:
exact this a b
State after:
no goals