Theorem: LO.FirstOrder.Structure.Eq.QuotEq.rel_eq (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 : QuotEq H
⊢ op(=).val ![a, b] ↔ a = b
Tactic:
induction' a using Quotient.ind with a
State after:
case a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
b : QuotEq H
a : M
⊢ op(=).val ![⟦a⟧, b] ↔ ⟦a⟧ = b

State before:
case a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
b : QuotEq H
a : M
⊢ op(=).val ![⟦a⟧, b] ↔ ⟦a⟧ = b
Tactic:
induction' b using Quotient.ind with b
State after:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ op(=).val ![⟦a⟧, ⟦b⟧] ↔ ⟦a⟧ = ⟦b⟧

State before:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ op(=).val ![⟦a⟧, ⟦b⟧] ↔ ⟦a⟧ = ⟦b⟧
Tactic:
rw[of_eq_of]
State after:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ op(=).val ![⟦a⟧, ⟦b⟧] ↔ eqv L a b

State before:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ op(=).val ![⟦a⟧, ⟦b⟧] ↔ eqv L a b
Tactic:
simp [eqv, Semiformula.Operator.val]
State after:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ (Eval struc ![⟦a⟧, ⟦b⟧] Empty.elim) op(=).sentence ↔ (Eval inst✝ ![a, b] Empty.elim) op(=).sentence

State before:
case a.a
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
a b : M
⊢ (Eval struc ![⟦a⟧, ⟦b⟧] Empty.elim) op(=).sentence ↔ (Eval inst✝ ![a, b] Empty.elim) op(=).sentence
Tactic:
simpa [Evalm, Matrix.fun_eq_vec₂, Empty.eq_elim] using
  eval_mk (H := H) (e := ![a, b]) (ε := Empty.elim) (p := Semiformula.Operator.Eq.eq.sentence)
State after:
no goals