exact ⟨Finset.erase u (~f), by simp [ss],
  by simp; intro h; exact hu (Semantics.Satisfiable.of_subset h (by simp))⟩
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)
no goals