chore: cleanup proof, use saner proof strategy

Author: bollu

src/Init/Data/BitVec/Lemmas.lean

@@ -1518,29 +1518,26 @@ theorem getLsb_replicate {n w : Nat} (x : BitVec w) :
     (x.replicate n).getLsb i =
     ((decide (i < w * n)) && (x.getLsb (i % w))) := by
   induction n generalizing x
-  case zero =>
-    simp
+  case zero => simp
   case succ n ih =>
     simp only [replicate_succ_eq, getLsb_cast, getLsb_append]
-    by_cases hi : i < w * n
-    · simp only [hi, decide_True, ih, Bool.true_and, cond_true, Bool.iff_and_self,
-      decide_eq_true_eq]
-      intros _
-      rw [Nat.mul_succ]
-      omega
-    · simp only [hi, decide_False, ih, Bool.false_and, cond_false]
-      by_cases hi' : i < w * (n + 1)
-      · simp only [hi', decide_True, Bool.true_and]
+    by_cases hi : i < w * (n + 1)
+    · simp only [hi, decide_True, Bool.true_and]
+      by_cases hi' : i < w * n
+      · simp [hi', ih]
+      · simp only [hi', decide_False, cond_false]
         congr
         rw [Nat.sub_eq_of_eq_add]
-        have hi : i / w = n := by
-          apply Nat.div_eq_of_lt_le (m := i) (k := n)
-            (by simp at hi; rw[Nat.mul_comm]; assumption)
-            (by rw [Nat.mul_comm]; assumption)
-        rw [← hi, Nat.add_comm, Nat.div_add_mod]
-      · simp only [hi', decide_False, Bool.false_and]
-        apply getLsb_ge
-        apply Nat.le_sub_of_add_le
-        simp only [Nat.mul_succ, Nat.not_lt] at hi'
-        omega
+        suffices i / w = n by
+          rw [← this, Nat.add_comm, Nat.div_add_mod]
+        apply Nat.div_eq_of_lt_le (m := i) (k := n)
+          (by simp only [Nat.not_lt] at hi'; rw[Nat.mul_comm]; omega)
+          (by rw [Nat.mul_comm]; omega)
+    · have hi' : ¬ (i < w * n) := by
+        simp [Nat.mul_succ] at hi; omega
+      simp only [hi', decide_False, cond_false, hi, Bool.false_and]
+      apply BitVec.getLsb_ge
+      apply Nat.le_sub_of_add_le
+      rw [Nat.mul_succ] at hi
+      omega
 end BitVec