Theorem: LO.Complete.inconsistent_of_unsatisfiable (Logic/Logic/System.lean)

State before:
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
inst✝¹ : ∀ (𝓜 : M), Semantics.Meaningful 𝓜
𝓢 : S
T : Set F
inst✝ : Complete 𝓢 (Semantics.models M T)
⊢ ¬Semantics.Satisfiable M T → System.Inconsistent 𝓢
Tactic:
contrapose
State after:
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
inst✝¹ : ∀ (𝓜 : M), Semantics.Meaningful 𝓜
𝓢 : S
T : Set F
inst✝ : Complete 𝓢 (Semantics.models M T)
⊢ ¬System.Inconsistent 𝓢 → ¬¬Semantics.Satisfiable M T

State before:
S : Type u_1
F : Type u_2
inst✝⁴ : LogicalConnective F
inst✝³ : System F S
M : Type u_3
inst✝² : Semantics F M
inst✝¹ : ∀ (𝓜 : M), Semantics.Meaningful 𝓜
𝓢 : S
T : Set F
inst✝ : Complete 𝓢 (Semantics.models M T)
⊢ ¬System.Inconsistent 𝓢 → ¬¬Semantics.Satisfiable M T
Tactic:
simpa [←System.not_consistent_iff_inconsistent] using satisfiable_of_consistent
State after:
no goals