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

State before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ Semantics.Satisfiable (Struc L) T ↔ ∃ M, ∃ (x : Nonempty M), ∃ x_1, ∃ (_ : Structure.Eq L M), M ⊧ₘ* T
Tactic:
simp [satisfiable_iff]
State after:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, M ⊧ₘ* T) ↔ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T

State before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, M ⊧ₘ* T) ↔ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
constructor
State after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, M ⊧ₘ* T) → ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T

case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T) → ∃ M a x, M ⊧ₘ* T

State before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, M ⊧ₘ* T) → ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
intro ⟨M, x, s, hM⟩
State after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T

State before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
haveI : Nonempty M := ⟨x⟩
State after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T

State before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
have H : M ⊧ₘ* (𝐄𝐐 : Theory L) := models_of_subtheory hM
State after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T

State before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
have e : Structure.Eq.QuotEq H ≡ₑ[L] M := Structure.Eq.QuotEq.elementaryEquiv H
State after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
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 a x, Structure.Eq L M ∧ M ⊧ₘ* T

State before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
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 a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
exact ⟨Structure.Eq.QuotEq H, ⟦x⟧, inferInstance, inferInstance, e.modelsTheory.mpr hM⟩
State after:
no goals

State before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T) → ∃ M a x, M ⊧ₘ* T
Tactic:
intro ⟨M, i, s, _, hM⟩
State after:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
i : M
s : Structure L M
left✝ : Structure.Eq L M
hM : M ⊧ₘ* T
⊢ ∃ M a x, M ⊧ₘ* T

State before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
i : M
s : Structure L M
left✝ : Structure.Eq L M
hM : M ⊧ₘ* T
⊢ ∃ M a x, M ⊧ₘ* T
Tactic:
exact ⟨M, i, s, hM⟩
State after:
no goals