[Usa2003Q1] some cleanup of Nat.digits_add'

MathPuzzles/Usa2003Q1.lean

@@ -29,29 +29,21 @@ theorem Nat.digits_add'
   induction ds with
   | nil =>
     intros x y hx1 hx2 hy
-    have hyy : y = 0 := Nat.digits_eq_nil_iff_eq_zero.mp hy.symm
-    rw[hyy]
-    simp
-    exact Nat.digits_of_lt b x hx2 hx1
+    simp[Nat.digits_eq_nil_iff_eq_zero.mp hy.symm, Nat.digits_of_lt b x hx2 hx1]
   | cons d ds ih =>
     intros x y hx1 hx2 hd
     rw[←hd, List.length_cons, Nat.pow_succ, List.cons_append]
     have hyp : 0 < y := by
        by_contra H
-       replace H : y = 0 := Nat.eq_zero_of_nonpos y H
-       rw[H] at hd
-       simp at hd
+       simp[Nat.eq_zero_of_nonpos y H] at hd
     have h3 := Nat.digits_def' hb hyp
-    have hdd := hd
-    rw[h3] at hdd
+    rw[h3] at hd
     have h4 : d = y % b := by aesop
     have h5 : ds = Nat.digits b (y/b) := by aesop
     have h2 := ih x (y/b) hx1 hx2 h5
     rw[←h5] at h2
     have h6 : 0 < x * (b ^ List.length ds * b) + y := by positivity
-    rw[Nat.digits_def' hb h6]
-    rw[←Nat.mul_assoc]
-
+    rw[Nat.digits_def' hb h6, ←Nat.mul_assoc]
     congr
     · rw[Nat.add_mod, Nat.mul_mod_left, zero_add, Nat.mod_mod]
       exact h4.symm