remaining suggestions

Author: hargoniX

src/Std/Sat/CNF/Basic.lean

@@ -53,7 +53,7 @@ theorem sat_def (a : α → Bool) (f : CNF α) : Sat a f ↔ (eval a f = true) :
 theorem unsat_def (f : CNF α) : Unsat f ↔ (∀ a, eval a f = false) := by rfl
 
 
-@[simp] theorem not_unsatisfiable_nil : ¬Unsat ([] : CNF α) :=
+@[simp] theorem not_unsat_nil : ¬Unsat ([] : CNF α) :=
   fun h => by simp [unsat_def] at h
 
 @[simp] theorem sat_nil {assign : α → Bool} : Sat assign ([] : CNF α) := by

src/Std/Sat/CNF/RelabelFin.lean

@@ -113,8 +113,7 @@ def relabelFin (f : CNF Nat) : CNF (Fin f.numLiterals) :=
   else
     List.replicate f.length []
 
-theorem unsat_relabelFin {f : CNF Nat} :
-    Unsat f.relabelFin ↔ Unsat f := by
+@[simp] theorem unsat_relabelFin {f : CNF Nat} : Unsat f.relabelFin ↔ Unsat f := by
   dsimp [relabelFin]
   split <;> rename_i h
   · apply unsat_relabel_iff