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

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ T ⊨[M] f ↔ ¬Satisfiable M (insert (~f) T)
Tactic:
simp [consequence_iff, Satisfiable]
State after:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f) ↔ ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f) ↔ ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
Tactic:
constructor
State after:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f) → ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T

case mpr
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ (x : M), ¬x ⊧ f → ¬x ⊧* T) → ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f

State before:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f) → ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
Tactic:
intro h 𝓜 hf hT
State after:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
𝓜 : M
hf : ¬𝓜 ⊧ f
hT : 𝓜 ⊧* T
⊢ False

State before:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
𝓜 : M
hf : ¬𝓜 ⊧ f
hT : 𝓜 ⊧* T
⊢ False
Tactic:
have : 𝓜 ⊧ f := h hT
State after:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
𝓜 : M
hf : ¬𝓜 ⊧ f
hT : 𝓜 ⊧* T
this : 𝓜 ⊧ f
⊢ False

State before:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
𝓜 : M
hf : ¬𝓜 ⊧ f
hT : 𝓜 ⊧* T
this : 𝓜 ⊧ f
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case mpr
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ (x : M), ¬x ⊧ f → ¬x ⊧* T) → ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
Tactic:
intro h 𝓜
State after:
case mpr
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
𝓜 : M
⊢ 𝓜 ⊧* T → 𝓜 ⊧ f

State before:
case mpr
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
𝓜 : M
⊢ 𝓜 ⊧* T → 𝓜 ⊧ f
Tactic:
contrapose
State after:
case mpr
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
𝓜 : M
⊢ ¬𝓜 ⊧ f → ¬𝓜 ⊧* T

State before:
case mpr
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
𝓜 : M
⊢ ¬𝓜 ⊧ f → ¬𝓜 ⊧* T
Tactic:
exact h 𝓜
State after:
no goals