Apply suggestions from code review

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

src/Init/Data/Array/Perm.lean

@@ -68,15 +68,15 @@ theorem swap_perm {xs : Array α} {i j : Nat} (h₁ : i < xs.size) (h₂ : j < x
 namespace Perm
 
 set_option linter.indexVariables false in
-theorem extract {xs ys : Array α} (h : xs ~ ys) (lo hi : Nat)
+theorem extract {xs ys : Array α} (h : xs ~ ys) {lo hi : Nat}
     (wlo : ∀ i, i < lo → xs[i]? = ys[i]?) (whi : ∀ i, hi ≤ i → xs[i]? = ys[i]?) :
     (xs.extract lo (hi + 1)) ~ (ys.extract lo (hi + 1)) := by
   rcases xs with ⟨xs⟩
   rcases ys with ⟨ys⟩
   simp_all only [perm_toArray, List.getElem?_toArray, List.extract_toArray,
     List.extract_eq_drop_take]
-  apply List.Perm.take' (w := fun i h => by simpa using whi (lo + i) (by omega))
-  apply List.Perm.drop' (w := wlo)
+  apply List.Perm.take_of_getElem? (w := fun i h => by simpa using whi (lo + i) (by omega))
+  apply List.Perm.drop_of_getElem? (w := wlo)
   exact h
 
 end Perm

src/Init/Data/List/Nat/Perm.lean

@@ -57,16 +57,16 @@ theorem set_set_perm {as : List α} {i j : Nat} (h₁ : i < as.length) (h₂ : j
 namespace Perm
 
 /-- Variant of `List.Perm.take` specifying the the permutation is constant after `i` elementwise. -/
-theorem take' {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, i ≤ j → l₁[j]? = l₂[j]?) :
-    (l₁.take i) ~ (l₂.take i) := by
-  apply h.take
+theorem take_of_getElem? {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, i ≤ j → l₁[j]? = l₂[j]?) :
+    l₁.take i ~ l₂.take i := by
+  refine h.take (Perm.of_eq ?_)
   ext1 j
   simpa using w (i + j) (by omega)
 
 /-- Variant of `List.Perm.drop` specifying the the permutation is constant before `i` elementwise. -/
-theorem drop' {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, j < i → l₁[j]? = l₂[j]?) :
-    (l₁.drop i) ~ (l₂.drop i) := by
-  apply h.drop
+theorem drop_of_getElem? {l₁ l₂ : List α} (h : l₁ ~ l₂) {i : Nat} (w : ∀ j, j < i → l₁[j]? = l₂[j]?) :
+    l₁.drop i ~ l₂.drop i := by
+  refine h.drop (Perm.of_eq ?_)
   ext1
   simp only [getElem?_take]
   split <;> simp_all

src/Init/Data/List/Perm.lean

@@ -538,13 +538,19 @@ theorem perm_insertIdx {α} (x : α) (l : List α) {i} (h : i ≤ l.length) :
 
 namespace Perm
 
-theorem take {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.drop n = l₂.drop n) :
-    (l₁.take n) ~ (l₂.take n) := by
-  rwa [← List.take_append_drop n l₁, ← List.take_append_drop n l₂, w, perm_append_right_iff] at h
+theorem take {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.drop n ~ l₂.drop n) :
+    l₁.take n ~ l₂.take n := by
+  classical
+  rw [perm_iff_count] at h w ⊢
+  rw [← take_append_drop n l₁, ← take_append_drop n l₂] at h
+  simpa only [count_append, w, Nat.add_right_cancel_iff] using h
 
-theorem drop {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₂.take n = l₁.take n) :
-    (l₁.drop n) ~ (l₂.drop n) := by
-  rwa [← List.take_append_drop n l₁, ← List.take_append_drop n l₂, w, perm_append_left_iff] at h
+theorem drop {l₁ l₂ : List α} (h : l₁ ~ l₂) {n : Nat} (w : l₁.take n ~ l₂.take n) :
+    l₁.drop n ~ l₂.drop n := by
+  classical
+  rw [perm_iff_count] at h w ⊢
+  rw [← take_append_drop n l₁, ← take_append_drop n l₂] at h
+  simpa only [count_append, w, Nat.add_left_cancel_iff] using h
 
 end Perm