From 1ae5d8eb463a38468e4b2e65fb3f6ab995dcd4a1 Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Mon, 13 Feb 2023 21:33:33 -0500
Subject: [PATCH] simplify left-pad a touch

---
 SizedArray.lean | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/SizedArray.lean b/SizedArray.lean
index d85e1fc..2b7069d 100644
--- a/SizedArray.lean
+++ b/SizedArray.lean
@@ -498,10 +498,12 @@ def left_pad' (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n)
   : SizedArray α to := by
     let pad_amt := to - n
     let (h₂ : pad_amt = to - n) := rfl
+
     let padding := replicate pad_amt with'
     let padded := append padding xs
-    rw [h₂] at padded
-    rw [Nat.sub_add_cancel] at padded
+
+    rw [h₂, Nat.sub_add_cancel] at padded
+
     exact padded
     exact h
 
@@ -510,18 +512,19 @@ def left_pad (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n)
     cases hle : (decide (to ≤ n)) with
     | true  => 
       rw [max, Nat.instMaxNat, maxOfLe]
-      simp
       let hle : to ≤ n := of_decide_eq_true hle
       simp [hle]
       exact xs
     | false => 
       let hle : ¬to ≤ n := of_decide_eq_false hle
+
+      rw [max, Nat.instMaxNat, maxOfLe]
+      simp [hle]
+
       let hnle := hle
       rw [Nat.not_le_eq, ← Nat.succ_eq_add_one] at hnle
       let hnle := Nat.le_of_succ_le hnle
-
-      rw [max, Nat.instMaxNat, maxOfLe]
-      simp
-      simp [hle]
       
       exact left_pad' to with' xs hnle
+
+#eval left_pad 10 413 (from_list [1,2,3,4,5,6,7])