Theorem: LO.Compact.conseq_compact (Logic/Logic/Semantics.lean)

State before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ T ⊨[M] f ↔ ∃ u, ↑u ⊆ T ∧ ↑u ⊨[M] f
Tactic:
simp [Semantics.consequence_iff_not_satisfiable, compact (T := insert (~f) T)]
State after:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x) ↔ ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)

State before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x) ↔ ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Tactic:
constructor
State after:
case mp
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x) → ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)

case mpr
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)) → ∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x

State before:
case mp
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x) → ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Tactic:
intro ⟨u, ss, hu⟩
State after:
case mp
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)

State before:
case mp
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Tactic:
exact ⟨Finset.erase u (~f), by simp [ss],
  by simp; intro h; exact hu (Semantics.Satisfiable.of_subset h (by simp))⟩
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ↑(u.erase (~f)) ⊆ T
Tactic:
simp [ss]
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ¬Semantics.Satisfiable M (insert (~f) ↑(u.erase (~f)))
Tactic:
simp
State after:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ¬Semantics.Satisfiable M (insert (~f) ↑u)

State before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Tactic:
intro h
State after:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
h : Semantics.Satisfiable M (insert (~f) ↑u)
⊢ False

State before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
h : Semantics.Satisfiable M (insert (~f) ↑u)
⊢ False
Tactic:
exact hu (Semantics.Satisfiable.of_subset h (by simp))
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
h : Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ↑u ⊆ insert (~f) ↑u
Tactic:
simp
State after:
no goals

State before:
case mpr
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)) → ∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x
Tactic:
intro ⟨u, ss, hu⟩
State after:
case mpr
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ T
hu : ¬Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x

State before:
case mpr
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ T
hu : ¬Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x
Tactic:
exact ⟨insert (~f) u,
  by simpa using Set.insert_subset_insert ss, by simpa using hu⟩
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ T
hu : ¬Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ↑(insert (~f) u) ⊆ insert (~f) T
Tactic:
simpa using Set.insert_subset_insert ss
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ T
hu : ¬Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ¬Semantics.Satisfiable M ↑(insert (~f) u)
Tactic:
simpa using hu
State after:
no goals