Theorem: LO.FirstOrder.Structure.Eq.eqv_relExt (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 ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v = rel r w
Tactic:
simp
State after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v ↔ rel r w

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v ↔ rel r w
Tactic:
constructor
State after:
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v → rel r w

case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r w → rel r v

State before:
case mp
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r v → rel r w
Tactic:
exact eqv_relExt_aux H r h
State after:
no goals

State before:
case mpr
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
r : L.Rel k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ rel r w → rel r v
Tactic:
exact eqv_relExt_aux H r (fun i => eqv_symm H (h i))
State after:
no goals