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

State before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ T ⊨[Struc L] σ ↔
    ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Structure L M] [inst_2 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
Tactic:
simp [consequence_iff]
State after:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ) ↔
    ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ

State before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ) ↔
    ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
Tactic:
constructor
State after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ) →
    ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ

case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ) →
    ∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ

State before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ) →
    ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
Tactic:
intro h M x s _ hM
State after:
case mp
L : Language
μ : Type u_1
inst✝² : Semiformula.Operator.Eq L
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
inst✝ : Structure.Eq L M
hM : M ⊧ₘ* T
⊢ M ⊧ₘ σ

State before:
case mp
L : Language
μ : Type u_1
inst✝² : Semiformula.Operator.Eq L
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
inst✝ : Structure.Eq L M
hM : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Tactic:
exact h M x hM
State after:
no goals

State before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ) →
    ∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ
Tactic:
intro h M x s hM
State after:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
⊢ M ⊧ₘ σ

State before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Tactic:
haveI : Nonempty M := ⟨x⟩
State after:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
⊢ M ⊧ₘ σ

State before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
⊢ M ⊧ₘ σ
Tactic:
have H : M ⊧ₘ* (𝐄𝐐 : Theory L) := models_of_subtheory hM
State after:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
⊢ M ⊧ₘ σ

State before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
⊢ M ⊧ₘ σ
Tactic:
have e : Structure.Eq.QuotEq H ≡ₑ[L] M := Structure.Eq.QuotEq.elementaryEquiv H
State after:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
e : Structure.Eq.QuotEq H ≡ₑ[L] M
⊢ M ⊧ₘ σ

State before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
e : Structure.Eq.QuotEq H ≡ₑ[L] M
⊢ M ⊧ₘ σ
Tactic:
exact e.models.mp $ h (Structure.Eq.QuotEq H) ⟦x⟧ (e.modelsTheory.mpr hM)
State after:
no goals