refactor: final refactor of CachedLemmas

LeanSAT/AIG/CachedLemmas.lean

@@ -48,8 +48,8 @@ The AIG produced by `AIG.mkAtomCached` agrees with the input AIG on all indices
 both.
 -/
 theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size}
-    {hbound}
-    : (aig.mkAtomCached var).aig.decls[idx]'hbound = aig.decls[idx] := by
+    {hbound} :
+    (aig.mkAtomCached var).aig.decls[idx]'hbound = aig.decls[idx] := by
   match hcache:aig.cache.get? (.atom var) with
   | some gate =>
     have := mkAtomCached_hit_aig aig hcache
@@ -64,8 +64,8 @@ theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < ai
 /--
 `AIG.mkAtomCached` never shrinks the underlying AIG.
 -/
-theorem mkAtomCached_le_size (aig : AIG α) (var : α)
-    : aig.decls.size ≤ (aig.mkAtomCached var).aig.decls.size := by
+theorem mkAtomCached_le_size (aig : AIG α) (var : α) :
+    aig.decls.size ≤ (aig.mkAtomCached var).aig.decls.size := by
   dsimp [mkAtomCached]
   split
   . simp
@@ -79,8 +79,8 @@ instance : LawfulOperator α (fun _ => α) mkAtomCached where
 The central equality theorem between `mkAtomCached` and `mkAtom`.
 -/
 @[simp]
-theorem mkAtomCached_eval_eq_mkAtom_eval {aig : AIG α}
-    : ⟦aig.mkAtomCached var, assign⟧ = ⟦aig.mkAtom var, assign⟧ := by
+theorem mkAtomCached_eval_eq_mkAtom_eval {aig : AIG α} :
+    ⟦aig.mkAtomCached var, assign⟧ = ⟦aig.mkAtom var, assign⟧ := by
   simp only [mkAtomCached]
   split
   . next heq1 =>
@@ -103,8 +103,9 @@ theorem denote_mkConst_cached {aig : AIG α} {hit} :
 /--
 `mkConstCached` does not modify the input AIG upon a cache hit.
 -/
-theorem mkConstCached_hit_aig (aig : AIG α) {hit} (hcache : aig.cache.get? (.const val) = some hit)
-    : (aig.mkConstCached val).aig = aig := by
+theorem mkConstCached_hit_aig (aig : AIG α) {hit}
+    (hcache : aig.cache.get? (.const val) = some hit) :
+    (aig.mkConstCached val).aig = aig := by
   simp only [mkConstCached]
   split <;> simp_all
 
@@ -117,11 +118,12 @@ theorem mkConstCached_miss_aig (aig : AIG α) (hcache : aig.cache.get? (.const v
   split <;> simp_all
 
 /--
-The AIG produced by `AIG.mkConstCached` agrees with the input AIG on all indices that are valid for both.
+The AIG produced by `AIG.mkConstCached` agrees with the input AIG on all indices that are valid for
+both.
 -/
 theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size}
-    {hbound}
-    : (aig.mkConstCached val).aig.decls[idx]'hbound = aig.decls[idx] := by
+    {hbound} :
+    (aig.mkConstCached val).aig.decls[idx]'hbound = aig.decls[idx] := by
   match hcache:aig.cache.get? (.const val) with
   | some gate =>
     have := mkConstCached_hit_aig aig hcache
@@ -136,8 +138,8 @@ theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx <
 /--
 `AIG.mkConstCached` never shrinks the underlying AIG.
 -/
-theorem mkConstCached_le_size (aig : AIG α) (val : Bool)
-    : aig.decls.size ≤ (aig.mkConstCached val).aig.decls.size := by
+theorem mkConstCached_le_size (aig : AIG α) (val : Bool) :
+    aig.decls.size ≤ (aig.mkConstCached val).aig.decls.size := by
   dsimp [mkConstCached]
   split
   . simp
@@ -153,8 +155,8 @@ instance : LawfulOperator α (fun _ => Bool) mkConstCached where
 The central equality theorem between `mkConstCached` and `mkConst`.
 -/
 @[simp]
-theorem mkConstCached_eval_eq_mkConst_eval {aig : AIG α}
-    : ⟦aig.mkConstCached val, assign⟧ = ⟦aig.mkConst val, assign⟧ := by
+theorem mkConstCached_eval_eq_mkConst_eval {aig : AIG α} :
+    ⟦aig.mkConstCached val, assign⟧ = ⟦aig.mkConst val, assign⟧ := by
   simp only [mkConstCached]
   split
   . next heq1 =>
@@ -164,8 +166,7 @@ theorem mkConstCached_eval_eq_mkConst_eval {aig : AIG α}
 /--
 If we find a cached gate declaration in the AIG, denoting it is equivalent to denoting `AIG.mkGate`.
 -/
-theorem denote_mkGate_cached {aig : AIG α} {input} {hit}
-      :
+theorem denote_mkGate_cached {aig : AIG α} {input} {hit} :
     aig.cache.get? (.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
       →
     ⟦⟨aig, hit.idx, hit.hbound⟩, assign⟧
@@ -179,8 +180,8 @@ theorem denote_mkGate_cached {aig : AIG α} {input} {hit}
     unfold denote denote.go
   split <;> simp_all[denote]
 
-theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig)
-    : aig.decls.size ≤ (go aig input).aig.decls.size := by
+theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) :
+    aig.decls.size ≤ (go aig input).aig.decls.size := by
   dsimp [go]
   split
   . simp
@@ -208,8 +209,7 @@ theorem mkGateCached_le_size (aig : AIG α) (input : GateInput aig)
   . apply mkGateCached.go_le_size
 
 theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
-    ∀ (idx : Nat) (h1) (h2),
-      (go aig input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
+    ∀ (idx : Nat) (h1) (h2), (go aig input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
     generalize hres : go aig input = res
     unfold go at hres
     dsimp at hres
@@ -261,8 +261,7 @@ The AIG produced by `AIG.mkGateCached` agrees with the input AIG on all indices
 both.
 -/
 theorem mkGateCached_decl_eq (aig : AIG α) (input : GateInput aig) :
-    ∀ (idx : Nat) (h1) (h2),
-      (aig.mkGateCached input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
+    ∀ (idx : Nat) (h1) (h2), (aig.mkGateCached input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
     generalize hres : mkGateCached aig input = res
     unfold mkGateCached at hres
     dsimp at hres