[NFC] Chore: Clean up "BitStream.lean" for Style (#533)

Non-functional Change. This change does not change any behavior or
funcitonality. It just cleans up the file "BitStream.lean" to use better
style.

Here are the specific stylistic changes made:
1) prefer "where" over "{}" in structure instances
2)  use "induction' with" over "induction rename_i"

---------

Co-authored-by: Atticus Kuhn <[email protected]>

SSA/Experimental/Bits/Fast/BitStream.lean

@@ -374,68 +374,70 @@ variable {w : Nat} {x y : BitVec w} {a b a' b' : BitStream}
 local infix:20 " ≈ʷ " => EqualUpTo w
 
 -- TODO: These sorries are difficult, and will be proven in a later Pull Request.
-@[simp] theorem ofBitVec_sub : ofBitVec (x - y) ≈ʷ (ofBitVec x) - (ofBitVec y)  := by
+theorem ofBitVec_sub : ofBitVec (x - y) ≈ʷ (ofBitVec x) - (ofBitVec y)  := by
   sorry
 
-@[simp] theorem ofBitVec_add : ofBitVec (x + y) ≈ʷ (ofBitVec x) + (ofBitVec y)  := by
-  sorry
-
-@[simp] theorem ofBitVec_neg : ofBitVec (- x) ≈ʷ  - (ofBitVec x) := by
+theorem ofBitVec_add : ofBitVec (x + y) ≈ʷ (ofBitVec x) + (ofBitVec y)  := by
   sorry
 
+@[refl]
 theorem equal_up_to_refl : a ≈ʷ a := by
-  intros  j _
+  intros _ _
   rfl
 
+@[symm]
 theorem equal_up_to_symm (e : a ≈ʷ b) : b ≈ʷ a := by
   intros j h
   symm
   exact e j h
 
+@[trans]
 theorem equal_up_to_trans (e1 : a ≈ʷ b) (e2 : b ≈ʷ c) : a ≈ʷ c := by
   intros j h
   trans b j
   exact e1 j h
   exact e2 j h
 
-instance congr_equiv : Equivalence (EqualUpTo w) := {
-  refl := fun _ => equal_up_to_refl,
-  symm := equal_up_to_symm,
+instance congr_trans : Trans (EqualUpTo w) (EqualUpTo w) (EqualUpTo w) where
   trans := equal_up_to_trans
-}
 
-theorem sub_congr (e1 : a ≈ʷ b) (e2 : c  ≈ʷ d) : (a - c) ≈ʷ (b - d) := by
-  intros n h
-  have sub_congr_lemma : a.subAux c n = b.subAux d n := by
-    induction n
-    <;> simp only [subAux, Prod.mk.injEq, e1 _ h, e2 _ h, and_self]
-    rename_i _ ih
-    simp only [ih (by omega), and_self]
-  simp only [HSub.hSub, Sub.sub, BitStream.sub, sub_congr_lemma]
+instance congr_equiv : Equivalence (EqualUpTo w) where
+  refl := fun _ => equal_up_to_refl
+  symm := equal_up_to_symm
+  trans := equal_up_to_trans
 
-theorem add_congr (e1 : a ≈ʷ b) (e2 : c  ≈ʷ d) : (a + c) ≈ʷ (b + d) := by
+theorem add_congr (e1 : a ≈ʷ b) (e2 : c ≈ʷ d) : (a + c) ≈ʷ (b + d) := by
   intros n h
   have add_congr_lemma : a.addAux c n = b.addAux d n := by
-    induction n
+    induction' n with _ ih
     <;> simp only [addAux, Prod.mk.injEq, e1 _ h, e2 _ h]
-    rename_i _ ih
     simp only [ih (by omega), Bool.bne_right_inj]
   simp only [HAdd.hAdd, Add.add, BitStream.add, add_congr_lemma]
 
+theorem not_congr (e1 : a ≈ʷ b) : (~~~a) ≈ʷ ~~~b := by
+  intros g h
+  simp only [not_eq, e1 g h]
+
+theorem ofBitVec_neg : ofBitVec (- x) ≈ʷ - (ofBitVec x) := by
+  sorry
+
+theorem sub_congr (e1 : a ≈ʷ b) (e2 : c ≈ʷ d) : (a - c) ≈ʷ (b - d) := by
+  intros n h
+  have sub_congr_lemma : a.subAux c n = b.subAux d n := by
+    induction' n with _ ih
+    <;> simp only [subAux, Prod.mk.injEq, e1 _ h, e2 _ h, and_self]
+    simp only [ih (by omega), and_self]
+  simp only [HSub.hSub, Sub.sub, BitStream.sub, sub_congr_lemma]
+
 theorem neg_congr (e1 : a ≈ʷ b) : (-a) ≈ʷ -b := by
   intros n h
   have neg_congr_lemma : a.negAux n = b.negAux n := by
-    induction n
+    induction' n with _ ih
     <;> simp only [negAux, Prod.mk.injEq, (e1 _ h)]
-    rename_i _ ih
     simp only [ih (by omega), Bool.bne_right_inj, and_self]
   simp only [Neg.neg, BitStream.neg, neg_congr_lemma]
 
-theorem not_congr (e1 : a ≈ʷ b) : (~~~a) ≈ʷ ~~~b := by
-  intros g h
-  simp only [not_eq, e1 g h]
-
-theorem equal_trans  (e1 :  a ≈ʷ b) (e2 : c ≈ʷ d)  : (a ≈ʷ c) = (b ≈ʷ d) := by
+theorem equal_congr_congr  (e1 : a ≈ʷ b) (e2 : c ≈ʷ d) : (a ≈ʷ c) = (b ≈ʷ d) := by
   apply propext
   constructor
   <;> intros h

SSA/Experimental/Bits/Fast/Tactic.lean

@@ -180,7 +180,7 @@ simproc reduce_bitvec2 (BitStream.EqualUpTo (_ : Nat) _ _) := fun e => do
       return .done {
         expr := .app (.app (.app (.const ``BitStream.EqualUpTo []) w) lterm) rterm
         proof? :=
-        some (.app (.app (.app (.app (.app (.app (.app (.const ``BitStream.equal_trans []) w) l) lterm) r) rterm) lproof) rproof)
+        some (.app (.app (.app (.app (.app (.app (.app (.const ``BitStream.equal_congr_congr []) w) l) lterm) r) rterm) lproof) rproof)
       }
     | _ => throwError m!"Expression {e} is not of the expected form. Expected something of the form BitStream.EqualUpTo (w : Nat) (lhs : BitStream) (rhs : BitStream) : Prop"