Theorem: LO.Semantics.satisfiableSet_iff_models_nonempty (Logic/Logic/Semantics.lean)

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
⊢ Satisfiable M T → (models M T).Nonempty
Tactic:
rintro ⟨𝓜, h𝓜⟩
State after:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
𝓜 : M
h𝓜 : 𝓜 ⊧* T
⊢ (models M T).Nonempty

State before:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
𝓜 : M
h𝓜 : 𝓜 ⊧* T
⊢ (models M T).Nonempty
Tactic:
exact ⟨𝓜, h𝓜⟩
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
⊢ (models M T).Nonempty → Satisfiable M T
Tactic:
rintro ⟨𝓜, h𝓜⟩
State after:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
𝓜 : M
h𝓜 : 𝓜 ∈ models M T
⊢ Satisfiable M T

State before:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
𝓜 : M
h𝓜 : 𝓜 ∈ models M T
⊢ Satisfiable M T
Tactic:
exact ⟨𝓜, h𝓜⟩
State after:
no goals