style: format CNF

LeanSAT/CNF/Relabel.lean

@@ -69,7 +69,8 @@ theorem relabel_congr {x : CNF α} {f g : α → β} (w : ∀ a, mem a x → f a
 theorem sat_relabel {x : CNF α} (h : (g ∘ f) ⊨ x) : g ⊨ (relabel f x) := by
   simp_all [(· ⊨ ·)]
 
-theorem unsat_relabel {x : CNF α} (f : α → β) (h : unsatisfiable α x) : unsatisfiable β (relabel f x) := by
+theorem unsat_relabel {x : CNF α} (f : α → β) (h : unsatisfiable α x)
+    : unsatisfiable β (relabel f x) := by
   simp_all [unsatisfiable, (· ⊨ ·)]
 
 theorem nonempty_or_impossible (x : CNF α) : Nonempty α ∨ ∃ n, x = List.replicate n [] := by

LeanSAT/CNF/RelabelFin.lean

@@ -14,15 +14,17 @@ def Clause.maxLiteral (c : Clause Nat) : Option Nat := (c.map (·.1)) |>.maximum
 theorem Clause.of_maxLiteral_eq_some (c : Clause Nat) (h : c.maxLiteral = some maxLit) :
     ∀ lit, mem lit c → lit ≤ maxLit := by
   intro lit hlit
-  simp only [maxLiteral, List.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h
+  simp only [maxLiteral, List.maximum?_eq_some_iff', List.mem_map, forall_exists_index, and_imp,
+    forall_apply_eq_imp_iff₂] at h
   simp only [mem] at hlit
   rcases h with ⟨_, hbar⟩
   cases hlit
   all_goals
     have := hbar (lit, _) (by assumption)
     omega
 
-theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : mem l c) : ∃ maxLit, c.maxLiteral = some maxLit := by
+theorem Clause.maxLiteral_eq_some_of_mem (c : Clause Nat) (h : mem l c)
+    : ∃ maxLit, c.maxLiteral = some maxLit := by
   dsimp[mem] at h
   cases h <;> rename_i h
   all_goals