Theorem: LO.FirstOrder.satisfiable_iff (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
T U : Theory L
⊢ Semantics.Satisfiable (Struc L) T → ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* T
Tactic:
rintro ⟨s, hs⟩
State after:
case intro
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝ : Nonempty M
s✝ : Structure L M
T U : Theory L
s : Struc L
hs : s ⊧* T
⊢ ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* T

State before:
case intro
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝ : Nonempty M
s✝ : Structure L M
T U : Theory L
s : Struc L
hs : s ⊧* T
⊢ ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* T
Tactic:
exact ⟨s.Dom, s.nonempty, s.struc, hs⟩
State after:
no goals

State before:
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M : Type u_1
inst✝ : Nonempty M
s : Structure L M
T U : Theory L
⊢ (∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* T) → Semantics.Satisfiable (Struc L) T
Tactic:
rintro ⟨M, i, s, hT⟩
State after:
case intro.intro.intro
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M✝ : Type u_1
inst✝ : Nonempty M✝
s✝ : Structure L M✝
T U : Theory L
M : Type v
i : Nonempty M
s : Structure L M
hT : M ⊧ₘ* T
⊢ Semantics.Satisfiable (Struc L) T

State before:
case intro.intro.intro
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
M✝ : Type u_1
inst✝ : Nonempty M✝
s✝ : Structure L M✝
T U : Theory L
M : Type v
i : Nonempty M
s : Structure L M
hT : M ⊧ₘ* T
⊢ Semantics.Satisfiable (Struc L) T
Tactic:
exact ⟨s.toStruc, hT⟩
State after:
no goals