From e068a857aca4245975a1989c9fd4e65540fa66e0 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Fri, 25 Aug 2023 14:55:34 +0200
Subject: [PATCH 01/11] feat: migrate List lemmas from mathlib

---
 Std/Data/List/Lemmas.lean | 282 +++++++++++++++++++++++++++++++++++++-
 1 file changed, 281 insertions(+), 1 deletion(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 22efaafba1..6456186ae4 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -28,6 +28,9 @@ theorem tail_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : t₁ = t₂ := (c
 theorem cons_inj (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' :=
   ⟨tail_eq_of_cons_eq, congrArg _⟩
 
+theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' :=
+  ⟨List.cons.inj, fun h => h.1 ▸ h.2 ▸ rfl⟩
+
 theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b L, l = b :: L
   | c :: l', _ => ⟨c, l', rfl⟩
 
@@ -44,6 +47,17 @@ theorem exists_mem_of_length_pos : ∀ {l : List α}, 0 < length l → ∃ a, a
 theorem length_pos_iff_exists_mem {l : List α} : 0 < length l ↔ ∃ a, a ∈ l :=
   ⟨exists_mem_of_length_pos, fun ⟨_, h⟩ => length_pos_of_mem h⟩
 
+theorem exists_cons_of_length_pos : ∀ {l : List α}, 0 < l.length → ∃ h t, l = h :: t
+  | h::t, _ => ⟨h, t, rfl⟩
+
+theorem length_pos_iff_exists_cons :
+    ∀ {l : List α}, 0 < l.length ↔ ∃ h t, l = h :: t :=
+  ⟨exists_cons_of_length_pos, fun ⟨_, _, eq⟩ => eq ▸ Nat.succ_pos _⟩
+
+theorem exists_cons_of_length_succ :
+    ∀ {l : List α}, l.length = n + 1 → ∃ h t, l = h :: t
+  | h::t, _ => ⟨h, t, rfl⟩
+
 theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
   Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero)
 
@@ -53,6 +67,12 @@ theorem exists_mem_of_ne_nil (l : List α) (h : l ≠ []) : ∃ x, x ∈ l :=
 theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
+theorem length_eq_two {l : List α} : l.length = 2 ↔ ∃ a b, l = [a, b] :=
+  ⟨fun _ => let [a, b] := l; ⟨a, b, rfl⟩, fun ⟨_, _, e⟩ => e ▸ rfl⟩
+
+theorem length_eq_three {l : List α} : l.length = 3 ↔ ∃ a b c, l = [a, b, c] :=
+  ⟨fun _ => let [a, b, c] := l; ⟨a, b, c, rfl⟩, fun ⟨_, _, _, e⟩ => e ▸ rfl⟩
+
 /-! ### mem -/
 
 @[simp] theorem not_mem_nil (a : α) : ¬ a ∈ [] := fun.
@@ -152,6 +172,30 @@ theorem mem_append_right {a : α} (l₁ : List α) {l₂ : List α} (h : a ∈ l
 theorem mem_iff_append {a : α} {l : List α} : a ∈ l ↔ ∃ s t : List α, l = s ++ a :: t :=
   ⟨append_of_mem, fun ⟨s, t, e⟩ => e ▸ by simp⟩
 
+/-! ### concat -/
+
+theorem concat_nil (a : α) : concat [] a = [a] :=
+  rfl
+
+theorem concat_cons (a b : α) (l : List α) : concat (a :: l) b = a :: concat l b :=
+  rfl
+
+theorem init_eq_of_concat_eq {a : α} {l₁ l₂ : List α} : concat l₁ a = concat l₂ a → l₁ = l₂ := by
+  intro h
+  rw [concat_eq_append, concat_eq_append] at h
+  apply append_left_inj [a] |>.mp h
+
+theorem last_eq_of_concat_eq {a b : α} {l : List α} : concat l a = concat l b → a = b := by
+  intro h
+  rw [concat_eq_append, concat_eq_append] at h
+  exact head_eq_of_cons_eq (append_right_inj l |>.mp h)
+
+theorem concat_ne_nil (a : α) (l : List α) : concat l a ≠ [] := by simp
+
+theorem concat_append (a : α) (l₁ l₂ : List α) : concat l₁ a ++ l₂ = l₁ ++ a :: l₂ := by simp
+
+theorem append_concat (a : α) (l₁ l₂ : List α) : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a := by simp
+
 /-! ### map -/
 
 theorem map_singleton (f : α → β) (a : α) : map f [a] = [f a] := rfl
@@ -207,6 +251,11 @@ theorem bind_map (f : β → γ) (g : α → List β) :
   | [] => rfl
   | a::l => by simp only [cons_bind, map_append, bind_map _ _ l]
 
+theorem map_bind (g : β → List γ) (f : α → β) :
+    ∀ l : List α, (List.map f l).bind g = l.bind fun a => g (f a)
+  | [] => rfl
+  | a :: l => by simp only [cons_bind, map_cons, map_bind _ _ l]
+
 /-! ### set-theoretic notation of Lists -/
 
 @[simp] theorem empty_eq : (∅ : List α) = [] := rfl
@@ -284,12 +333,20 @@ theorem map_subset {l₁ l₂ : List α} (f : α → β) (H : l₁ ⊆ l₂) : m
 
 theorem replicate_succ (a : α) (n) : replicate (n+1) a = a :: replicate n a := rfl
 
+@[simp] theorem replicate_zero (a : α) : replicate 0 a = [] := by rfl
+
+theorem replicate_one (a : α) : replicate 1 a = [a] := rfl
+
 theorem mem_replicate {a b : α} : ∀ {n}, b ∈ replicate n a ↔ n ≠ 0 ∧ b = a
   | 0 => by simp
   | n+1 => by simp [mem_replicate, Nat.succ_ne_zero]
 
 theorem eq_of_mem_replicate {a b : α} {n} (h : b ∈ replicate n a) : b = a := (mem_replicate.1 h).2
 
+theorem eq_replicate_length {a : α} : ∀ {l : List α}, l = replicate l.length a ↔ ∀ b ∈ l, b = a
+  | [] => by simp
+  | (b :: l) => by simp [eq_replicate_length]
+
 theorem eq_replicate_of_mem {a : α} :
     ∀ {l : List α}, (∀ b ∈ l, b = a) → l = replicate l.length a
   | [], _ => rfl
@@ -302,15 +359,61 @@ theorem eq_replicate {a : α} {n} {l : List α} :
   ⟨fun h => h ▸ ⟨length_replicate .., fun _ => eq_of_mem_replicate⟩,
    fun ⟨e, al⟩ => e ▸ eq_replicate_of_mem al⟩
 
+theorem replicate_add (m n) (a : α) : replicate (m + n) a = replicate m a ++ replicate n a := by
+  induction m <;> simp [*, succ_add]
+
+theorem replicate_succ' (n) (a : α) : replicate (n + 1) a = replicate n a ++ [a] :=
+  replicate_add n 1 a
+
+theorem replicate_subset_singleton (n) (a : α) : replicate n a ⊆ [a] := fun _ h =>
+  mem_singleton.2 (eq_of_mem_replicate h)
+
+theorem subset_singleton_iff {a : α} {L : List α} : L ⊆ [a] ↔ ∃ n, L = replicate n a := by
+  simp only [eq_replicate, subset_def, mem_singleton, exists_eq_left']
+
+@[simp] theorem map_replicate (f : α → β) (n) (a : α) :
+    map f (replicate n a) = replicate n (f a) := by
+  induction n <;> [rfl; simp only [*, replicate, map]]
+
+@[simp] theorem tail_replicate (a : α) (n) :
+    tail (replicate n a) = replicate (n - 1) a := by cases n <;> rfl
+
+@[simp] theorem join_replicate_nil (n : Nat) : join (replicate n []) = @nil α := by
+  induction n <;> [rfl; simp only [*, replicate, join, append_nil]]
+
+/-! ### pure -/
+
+-- Porting note: simp can prove this
+-- @[simp]
+theorem bind_singleton (f : α → List β) (x : α) : [x].bind f = f x :=
+  append_nil $ f x
+
+@[simp] theorem bind_singleton' (l : List α) : (l.bind fun x => [x]) = l := by
+  induction l <;> simp [*]
+
+theorem map_eq_bind {α β} (f : α → β) (l : List α) : map f l = l.bind fun x => [f x] := by
+  simp only [←map_singleton]
+  rw [← bind_singleton' l, bind_map, bind_singleton']
+
+theorem bind_assoc {α β} (l : List α) (f : α → List β) (g : β → List γ) :
+    (l.bind f).bind g = l.bind fun x => (f x).bind g := by induction l <;> simp [*]
+
 /-! ### getLast -/
 
+@[simp]
+theorem getLast_cons {a : α} {l : List α} :
+    ∀ h : l ≠ nil, getLast (a :: l) (cons_ne_nil a l) = getLast l h := by
+  induction l <;> intros
+  · contradiction
+  · rfl
+
 theorem getLast_cons' {a : α} {l : List α} : ∀ (h₁ : a :: l ≠ nil) (h₂ : l ≠ nil),
   getLast (a :: l) h₁ = getLast l h₂ := by
   induction l <;> intros; {contradiction}; rfl
 
 @[simp] theorem getLast_append {a : α} : ∀ (l : List α) h, getLast (l ++ [a]) h = a
   | [], _ => rfl
-  | a::t, h => by
+  | a::t, _ => by
     simp [getLast_cons' _ fun H => cons_ne_nil _ _ (append_eq_nil.1 H).2, getLast_append t]
 
 theorem getLast_concat : (h : concat l a ≠ []) → getLast (concat l a) h = a :=
@@ -322,6 +425,48 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = L ++ [b]
     | _, .inl rfl => .inr ⟨[], a, rfl⟩
     | _, .inr ⟨L, b, rfl⟩ => .inr ⟨a::L, b, rfl⟩
 
+theorem getLast_append_singleton {a : α} (l : List α) :
+    getLast (l ++ [a]) (append_ne_nil_of_ne_nil_right l _ (cons_ne_nil a _)) = a := by
+  simp only [getLast_append]
+
+-- Porting note: name should be fixed upstream
+theorem getLast_append' (l₁ l₂ : List α) (h : l₂ ≠ []) :
+    getLast (l₁ ++ l₂) (append_ne_nil_of_ne_nil_right l₁ l₂ h) = getLast l₂ h := by
+  induction l₁
+  · simp
+  case cons _ _ ih =>
+    simp only [cons_append]
+    rw [List.getLast_cons]
+    exact ih
+
+theorem getLast_concat' {a : α} (l : List α) : getLast (concat l a) (concat_ne_nil a l) = a :=
+  getLast_concat ..
+
+@[simp]
+theorem getLast_singleton' (a : α) : getLast [a] (cons_ne_nil a []) = a := rfl
+
+-- Porting note: simp can prove this
+-- @[simp]
+theorem getLast_cons_cons (a₁ a₂ : α) (l : List α) :
+    getLast (a₁ :: a₂ :: l) (cons_ne_nil _ _) = getLast (a₂ :: l) (cons_ne_nil a₂ l) :=
+  rfl
+
+theorem getLast_congr {l₁ l₂ : List α} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) (h₃ : l₁ = l₂) :
+    getLast l₁ h₁ = getLast l₂ h₂ := by subst l₁; rfl
+
+theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
+  | [], h => absurd rfl h
+  | [a], _ => by simp only [getLast, mem_singleton]
+  | a :: b :: l, h =>
+    List.mem_cons.2 <| Or.inr <| by
+        rw [getLast_cons_cons]
+        exact getLast_mem (cons_ne_nil b l)
+
+theorem getLast_replicate_succ (m : Nat) (a : α) :
+    (replicate (m + 1) a).getLast (ne_nil_of_length_eq_succ (length_replicate _ _)) = a := by
+  simp only [replicate_succ']
+  exact getLast_append_singleton _
+
 /-! ### sublists -/
 
 @[simp] theorem nil_sublist : ∀ l : List α, [] <+ l
@@ -472,6 +617,25 @@ theorem isSublist_iff_sublist [DecidableEq α] {l₁ l₂ : List α} : l₁.isSu
 instance [DecidableEq α] (l₁ l₂ : List α) : Decidable (l₁ <+ l₂) :=
   decidable_of_iff (l₁.isSublist l₂) isSublist_iff_sublist
 
+theorem Sublist.cons_cons {l₁ l₂ : List α} (a : α) (s : l₁ <+ l₂) : a :: l₁ <+ a :: l₂ :=
+  Sublist.cons₂ _ s
+
+theorem sublist_cons_of_sublist (a : α) {l₁ l₂ : List α} : l₁ <+ l₂ → l₁ <+ a :: l₂ :=
+  Sublist.cons _
+
+theorem sublist_of_cons_sublist_cons {l₁ l₂ : List α} : ∀ {a : α}, a :: l₁ <+ a :: l₂ → l₁ <+ l₂
+  | _, Sublist.cons _ s => sublist_of_cons_sublist s
+  | _, Sublist.cons₂ _ s => s
+
+theorem cons_sublist_cons_iff {l₁ l₂ : List α} {a : α} : a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂ :=
+  ⟨sublist_of_cons_sublist_cons, Sublist.cons_cons _⟩
+
+theorem eq_nil_of_sublist_nil {l : List α} (s : l <+ []) : l = [] :=
+  subset_nil.mp <| s.subset
+
+theorem Sublist.antisymm (s₁ : l₁ <+ l₂) (s₂ : l₂ <+ l₁) : l₁ = l₂ :=
+  s₁.eq_of_length_le s₂.length_le
+
 /-! ### head -/
 
 theorem head!_of_head? [Inhabited α] : ∀ {l : List α}, head? l = some a → head! l = a
@@ -481,6 +645,52 @@ theorem head?_eq_head : ∀ l h, @head? α l = some (head l h)
   | [], h => nomatch h rfl
   | _::_, _ => rfl
 
+theorem eq_cons_of_mem_head? {x : α} : ∀ {l : List α}, x ∈ l.head? → l = x :: tail l
+  | [], h => (Option.not_mem_none _ h).elim
+  | a :: l, h => by
+    simp only [head?, Option.mem_def, Option.some_inj] at h
+    exact h ▸ rfl
+
+theorem mem_of_mem_head? {x : α} {l : List α} (h : x ∈ l.head?) : x ∈ l :=
+  (eq_cons_of_mem_head? h).symm ▸ mem_cons_self _ _
+
+@[simp] theorem head!_cons [Inhabited α] (a : α) (l : List α) : head! (a :: l) = a := rfl
+
+@[simp] theorem head!_append [Inhabited α] (t : List α) {s : List α} (h : s ≠ []) :
+    head! (s ++ t) = head! s := by
+  induction s; contradiction; rfl
+
+theorem head?_append {s t : List α} {x : α} (h : x ∈ s.head?) : x ∈ (s ++ t).head? := by
+  cases s; contradiction; exact h
+
+theorem head?_append_of_ne_nil :
+    ∀ (l₁ : List α) {l₂ : List α} (_ : l₁ ≠ []), head? (l₁ ++ l₂) = head? l₁
+  | _ :: _, _, _ => rfl
+
+theorem cons_head?_tail : ∀ {l : List α} {a : α}, a ∈ head? l → a :: tail l = l
+  | [], a, h => by contradiction
+  | b :: l, a, h => by
+    simp at h
+    simp [h]
+
+theorem head!_mem_head? [Inhabited α] : ∀ {l : List α}, l ≠ [] → head! l ∈ head? l
+  | [], h => by contradiction
+  | a :: l, _ => rfl
+
+theorem cons_head!_tail [Inhabited α] {l : List α} (h : l ≠ []) : head! l :: tail l = l :=
+  cons_head?_tail (head!_mem_head? h)
+
+theorem head!_mem_self [Inhabited α] {l : List α} (h : l ≠ nil) : l.head! ∈ l := by
+  have h' := mem_cons_self l.head! l.tail
+  rwa [cons_head!_tail h] at h'
+
+@[simp] theorem head?_map (f : α → β) (l) : head? (map f l) = (head? l).map f := by
+  cases l <;> rfl
+
+@[simp 1100]
+theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
+    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp
+
 /-! ### tail -/
 
 @[simp] theorem tailD_eq_tail? (l l' : List α) : tailD l l' = (tail? l).getD l' := by
@@ -490,6 +700,17 @@ theorem tail_eq_tailD (l) : @tail α l = tailD l [] := by cases l <;> rfl
 
 theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_tailD]
 
+theorem tail_append_singleton_of_ne_nil {a : α} {l : List α} (h : l ≠ nil) :
+    tail (l ++ [a]) = tail l ++ [a] := by
+  induction l
+  · contradiction
+  · rw [tail, cons_append, tail]
+
+theorem tail_append_of_ne_nil (l l' : List α) (h : l ≠ []) : (l ++ l').tail = l.tail ++ l' := by
+  cases l
+  · contradiction
+  · simp
+
 /-! ### next? -/
 
 @[simp] theorem next?_nil : @next? α [] = none := rfl
@@ -519,6 +740,65 @@ theorem getLast?_eq_getLast : ∀ l h, @getLast? α l = some (getLast l h)
   | [], h => nomatch h rfl
   | _::_, _ => rfl
 
+@[simp] theorem getLast?_singleton (a : α) :
+    getLast? [a] = a := rfl
+
+@[simp] theorem getLast?_cons_cons (a b : α) (l : List α) :
+    getLast? (a :: b :: l) = getLast? (b :: l) := rfl
+
+@[simp] theorem getLast?_isNone : ∀ {l : List α}, (getLast? l).isNone ↔ l = []
+  | [] => by simp
+  | [a] => by simp
+  | a :: b :: l => by simp [getLast?_isNone (l := b :: l)]
+
+@[simp] theorem getLast?_isSome : ∀ {l : List α}, l.getLast?.isSome ↔ l ≠ []
+  | [] => by simp
+  | [a] => by simp
+  | a :: b :: l => by simp [getLast?_isSome (l := b :: l)]
+
+theorem mem_getLast?_eq_getLast : ∀ {l : List α} {x : α}, x ∈ l.getLast? → ∃ h, x = getLast l h
+  | [], x, hx => False.elim <| by simp at hx
+  | [a], x, hx =>
+    have : a = x := by simpa using hx
+    this ▸ ⟨cons_ne_nil a [], rfl⟩
+  | a :: b :: l, x, hx => by
+    rw [getLast?_cons_cons] at hx
+    rcases mem_getLast?_eq_getLast hx with ⟨_, h₂⟩
+    refine ⟨cons_ne_nil _ _, ?_⟩
+    assumption
+
+theorem getLast?_eq_getLast_of_ne_nil : ∀ {l : List α} (h : l ≠ []), l.getLast? = some (l.getLast h)
+  | [], h => (h rfl).elim
+  | [_], _ => rfl
+  | _ :: b :: l, _ => getLast?_eq_getLast_of_ne_nil (l := b :: l) (cons_ne_nil _ _)
+
+theorem mem_getLast?_cons {x y : α} : ∀ {l : List α}, x ∈ l.getLast? → x ∈ (y :: l).getLast?
+  | [], _ => by contradiction
+  | _ :: _, h => h
+
+theorem mem_of_mem_getLast? {l : List α} {a : α} (ha : a ∈ l.getLast?) : a ∈ l :=
+  let ⟨_, h₂⟩ := mem_getLast?_eq_getLast ha
+  h₂.symm ▸ getLast_mem _
+
+@[simp] theorem getLast?_append_cons :
+    ∀ (l₁ : List α) (a : α) (l₂ : List α), getLast? (l₁ ++ a :: l₂) = getLast? (a :: l₂)
+  | [], a, l₂ => rfl
+  | [b], a, l₂ => rfl
+  | b :: c :: l₁, a, l₂ => by
+    rw [cons_append, cons_append, getLast?_cons_cons, ←cons_append, getLast?_append_cons (c::l₁)]
+
+theorem getLast?_append_of_ne_nil (l₁ : List α) :
+    ∀ {l₂ : List α} (_ : l₂ ≠ []), getLast? (l₁ ++ l₂) = getLast? l₂
+  | [], hl₂ => by contradiction
+  | b :: l₂, _ => getLast?_append_cons l₁ b l₂
+
+theorem getLast?_append {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.getLast?) :
+    x ∈ (l₁ ++ l₂).getLast? := by
+  cases l₂
+  · contradiction
+  · rw [List.getLast?_append_cons]
+    exact h
+
 /-! ### dropLast -/
 
 @[simp] theorem dropLast_nil : @dropLast α [] = [] := rfl

From dba1c694852784900c211a3134a8a572784b5e5f Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Fri, 25 Aug 2023 15:08:18 +0200
Subject: [PATCH 02/11] chore: make linter happy

---
 Std/Data/List/Lemmas.lean | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 6456186ae4..7eac8de562 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -687,9 +687,26 @@ theorem head!_mem_self [Inhabited α] {l : List α} (h : l ≠ nil) : l.head! 
 @[simp] theorem head?_map (f : α → β) (l) : head? (map f l) = (head? l).map f := by
   cases l <;> rfl
 
-@[simp 1100]
+-- List.modifyHead_modifyHead.{u_1} Left-hand side simplifies from
+--   List.modifyHead g (List.modifyHead f l)
+-- to
+--   match
+--   match l with
+--   | [] => []
+--   | a :: l => f a :: l with
+-- | [] => []
+-- | a :: l => g a :: l
+-- using
+--   simp only [@List.modifyHead]
+-- Try to change the left-hand side to the simplified term!
+--
+-- @[simp 1100]
 theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
-    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp
+    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by
+  cases l
+  · simp only [modifyHead]
+  · simp only [modifyHead]
+    rfl
 
 /-! ### tail -/
 
@@ -970,7 +987,9 @@ theorem getLast?_eq_get? : ∀ (l : List α), getLast? l = l.get? (l.length - 1)
   | [], a => rfl
   | b :: l, a => by rw [cons_append, length_cons]; simp only [get?, get?_concat_length]
 
-@[simp] theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
+-- simp can prove this
+-- @[simp]
+theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
   simp [getLast?_eq_get?]
 
 @[simp] theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by

From aa5141044186c967b5a3412ca628951559fece2d Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Fri, 25 Aug 2023 16:17:17 +0200
Subject: [PATCH 03/11] chore: de-simp List.modifyHead

---
 Std/Data/List/Basic.lean    |  6 +++---
 Std/Data/List/Lemmas.lean   | 21 +++------------------
 Std/Data/String/Lemmas.lean |  4 ++--
 3 files changed, 8 insertions(+), 23 deletions(-)

diff --git a/Std/Data/List/Basic.lean b/Std/Data/List/Basic.lean
index 7ba041b852..4f1c66d4b4 100644
--- a/Std/Data/List/Basic.lean
+++ b/Std/Data/List/Basic.lean
@@ -531,7 +531,7 @@ modifyNthTail f 2 [a, b, c] = [a, b] ++ f [c]
   | n+1, a :: l => a :: modifyNthTail f n l
 
 /-- Apply `f` to the head of the list, if it exists. -/
-@[simp, inline] def modifyHead (f : α → α) : List α → List α
+@[inline] def modifyHead (f : α → α) : List α → List α
   | [] => []
   | a :: l => f a :: l
 
@@ -548,8 +548,8 @@ def modifyNthTR (f : α → α) (n : Nat) (l : List α) : List α := go l n #[]
   | a :: l, n+1, acc => go l n (acc.push a)
 
 theorem modifyNthTR_go_eq : ∀ l n, modifyNthTR.go f l n acc = acc.data ++ modifyNth f n l
-  | [], n => by cases n <;> simp [modifyNthTR.go, modifyNth]
-  | a :: l, 0 => by simp [modifyNthTR.go, modifyNth]
+  | [], n => by cases n <;> simp [modifyHead, modifyNthTR.go, modifyNth]
+  | a :: l, 0 => by simp [modifyHead, modifyNthTR.go, modifyNth]
   | a :: l, n+1 => by simp [modifyNthTR.go, modifyNth, modifyNthTR_go_eq l]
 
 @[csimp] theorem modifyNth_eq_modifyNthTR : @modifyNth = @modifyNthTR := by
diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 7eac8de562..e5a1463927 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -687,26 +687,11 @@ theorem head!_mem_self [Inhabited α] {l : List α} (h : l ≠ nil) : l.head! 
 @[simp] theorem head?_map (f : α → β) (l) : head? (map f l) = (head? l).map f := by
   cases l <;> rfl
 
--- List.modifyHead_modifyHead.{u_1} Left-hand side simplifies from
---   List.modifyHead g (List.modifyHead f l)
--- to
---   match
---   match l with
---   | [] => []
---   | a :: l => f a :: l with
--- | [] => []
--- | a :: l => g a :: l
--- using
---   simp only [@List.modifyHead]
--- Try to change the left-hand side to the simplified term!
---
--- @[simp 1100]
+@[simp]
 theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
     (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by
-  cases l
-  · simp only [modifyHead]
-  · simp only [modifyHead]
-    rfl
+  cases l <;> simp only [modifyHead]
+  rfl
 
 /-! ### tail -/
 
diff --git a/Std/Data/String/Lemmas.lean b/Std/Data/String/Lemmas.lean
index c96032bd85..d72cb51db8 100644
--- a/Std/Data/String/Lemmas.lean
+++ b/Std/Data/String/Lemmas.lean
@@ -237,7 +237,7 @@ theorem utf8SetAux_of_valid (c' : Char) (cs cs' : List Char) {i p : Nat} (hp : i
     utf8SetAux c' (cs ++ cs') ⟨i⟩ ⟨p⟩ = cs ++ cs'.modifyHead fun _ => c' := by
   match cs, cs' with
   | [], [] => rfl
-  | [], c::cs' => simp [← hp, utf8SetAux]
+  | [], c::cs' => simp [List.modifyHead, ← hp, utf8SetAux]
   | c::cs, cs' =>
     simp [utf8SetAux]; rw [if_neg]
     case hnc => simp [← hp, Pos.ext_iff]; exact ne_self_add_add_csize
@@ -740,7 +740,7 @@ theorem mapAux_of_valid (f : Char → Char) : ∀ l r, mapAux f ⟨utf8Len l⟩
   | l, c::r => by
     unfold mapAux
     rw [dif_neg (by rw [atEnd_of_valid]; simp)]
-    simp [set_of_valid l (c::r), get_of_valid l (c::r), next_of_valid l (f c) r]
+    simp [List.modifyHead, set_of_valid l (c::r), get_of_valid l (c::r), next_of_valid l (f c) r]
     simpa using mapAux_of_valid f (l++[f c]) r
 
 theorem map_eq (f : Char → Char) (s) : map f s = ⟨s.1.map f⟩ := by

From 1867caf88b392bafbef690e13d786c6588c36e7c Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Tue, 5 Sep 2023 15:42:08 +0200
Subject: [PATCH 04/11] chore: remove pure/map/bind List lemmas from the PR

---
 Std/Data/List/Lemmas.lean | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index e5a1463927..1288cbbfdd 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -381,23 +381,6 @@ theorem subset_singleton_iff {a : α} {L : List α} : L ⊆ [a] ↔ ∃ n, L = r
 @[simp] theorem join_replicate_nil (n : Nat) : join (replicate n []) = @nil α := by
   induction n <;> [rfl; simp only [*, replicate, join, append_nil]]
 
-/-! ### pure -/
-
--- Porting note: simp can prove this
--- @[simp]
-theorem bind_singleton (f : α → List β) (x : α) : [x].bind f = f x :=
-  append_nil $ f x
-
-@[simp] theorem bind_singleton' (l : List α) : (l.bind fun x => [x]) = l := by
-  induction l <;> simp [*]
-
-theorem map_eq_bind {α β} (f : α → β) (l : List α) : map f l = l.bind fun x => [f x] := by
-  simp only [←map_singleton]
-  rw [← bind_singleton' l, bind_map, bind_singleton']
-
-theorem bind_assoc {α β} (l : List α) (f : α → List β) (g : β → List γ) :
-    (l.bind f).bind g = l.bind fun x => (f x).bind g := by induction l <;> simp [*]
-
 /-! ### getLast -/
 
 @[simp]

From 3d7df73c42bf1830386695e6a2e6f61d1399f306 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Tue, 5 Sep 2023 16:15:22 +0200
Subject: [PATCH 05/11] chore: apply @fgdorais modifications

---
 Std/Data/List/Lemmas.lean | 49 +++++++++++++--------------------------
 1 file changed, 16 insertions(+), 33 deletions(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 1288cbbfdd..7b92b2ca3f 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -67,12 +67,6 @@ theorem exists_mem_of_ne_nil (l : List α) (h : l ≠ []) : ∃ x, x ∈ l :=
 theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
-theorem length_eq_two {l : List α} : l.length = 2 ↔ ∃ a b, l = [a, b] :=
-  ⟨fun _ => let [a, b] := l; ⟨a, b, rfl⟩, fun ⟨_, _, e⟩ => e ▸ rfl⟩
-
-theorem length_eq_three {l : List α} : l.length = 3 ↔ ∃ a b c, l = [a, b, c] :=
-  ⟨fun _ => let [a, b, c] := l; ⟨a, b, c, rfl⟩, fun ⟨_, _, _, e⟩ => e ▸ rfl⟩
-
 /-! ### mem -/
 
 @[simp] theorem not_mem_nil (a : α) : ¬ a ∈ [] := fun.
@@ -182,13 +176,13 @@ theorem concat_cons (a b : α) (l : List α) : concat (a :: l) b = a :: concat l
 
 theorem init_eq_of_concat_eq {a : α} {l₁ l₂ : List α} : concat l₁ a = concat l₂ a → l₁ = l₂ := by
   intro h
-  rw [concat_eq_append, concat_eq_append] at h
-  apply append_left_inj [a] |>.mp h
+  simp at h
+  assumption
 
 theorem last_eq_of_concat_eq {a b : α} {l : List α} : concat l a = concat l b → a = b := by
   intro h
-  rw [concat_eq_append, concat_eq_append] at h
-  exact head_eq_of_cons_eq (append_right_inj l |>.mp h)
+  simp at h
+  assumption
 
 theorem concat_ne_nil (a : α) (l : List α) : concat l a ≠ [] := by simp
 
@@ -333,7 +327,7 @@ theorem map_subset {l₁ l₂ : List α} (f : α → β) (H : l₁ ⊆ l₂) : m
 
 theorem replicate_succ (a : α) (n) : replicate (n+1) a = a :: replicate n a := rfl
 
-@[simp] theorem replicate_zero (a : α) : replicate 0 a = [] := by rfl
+@[simp] theorem replicate_zero (a : α) : replicate 0 a = [] := rfl
 
 theorem replicate_one (a : α) : replicate 1 a = [a] := rfl
 
@@ -360,7 +354,7 @@ theorem eq_replicate {a : α} {n} {l : List α} :
    fun ⟨e, al⟩ => e ▸ eq_replicate_of_mem al⟩
 
 theorem replicate_add (m n) (a : α) : replicate (m + n) a = replicate m a ++ replicate n a := by
-  induction m <;> simp [*, succ_add]
+  induction m with simp [succ_add] | succ _ ih => exact ih
 
 theorem replicate_succ' (n) (a : α) : replicate (n + 1) a = replicate n a ++ [a] :=
   replicate_add n 1 a
@@ -399,8 +393,8 @@ theorem getLast_cons' {a : α} {l : List α} : ∀ (h₁ : a :: l ≠ nil) (h₂
   | a::t, _ => by
     simp [getLast_cons' _ fun H => cons_ne_nil _ _ (append_eq_nil.1 H).2, getLast_append t]
 
-theorem getLast_concat : (h : concat l a ≠ []) → getLast (concat l a) h = a :=
-  concat_eq_append .. ▸ getLast_append _
+theorem getLast_concat {h : concat l a ≠ []} : getLast (concat l a) h = a :=
+  by simp
 
 theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = L ++ [b]
   | [] => .inl rfl
@@ -422,28 +416,17 @@ theorem getLast_append' (l₁ l₂ : List α) (h : l₂ ≠ []) :
     rw [List.getLast_cons]
     exact ih
 
-theorem getLast_concat' {a : α} (l : List α) : getLast (concat l a) (concat_ne_nil a l) = a :=
-  getLast_concat ..
-
 @[simp]
 theorem getLast_singleton' (a : α) : getLast [a] (cons_ne_nil a []) = a := rfl
 
--- Porting note: simp can prove this
--- @[simp]
-theorem getLast_cons_cons (a₁ a₂ : α) (l : List α) :
-    getLast (a₁ :: a₂ :: l) (cons_ne_nil _ _) = getLast (a₂ :: l) (cons_ne_nil a₂ l) :=
-  rfl
-
-theorem getLast_congr {l₁ l₂ : List α} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) (h₃ : l₁ = l₂) :
-    getLast l₁ h₁ = getLast l₂ h₂ := by subst l₁; rfl
-
-theorem getLast_mem : ∀ {l : List α} (h : l ≠ []), getLast l h ∈ l
-  | [], h => absurd rfl h
-  | [a], _ => by simp only [getLast, mem_singleton]
-  | a :: b :: l, h =>
-    List.mem_cons.2 <| Or.inr <| by
-        rw [getLast_cons_cons]
-        exact getLast_mem (cons_ne_nil b l)
+theorem getLast_mem {l : List α} (h : l ≠ []) : getLast l h ∈ l := by
+  induction l with try contradiction
+  | cons _ l ih =>
+    match l with
+    | nil => exact mem_singleton_self ..
+    | cons _ _ =>
+      rw [getLast_cons]
+      apply mem_cons_of_mem _ <| ih (cons_ne_nil _ _)
 
 theorem getLast_replicate_succ (m : Nat) (a : α) :
     (replicate (m + 1) a).getLast (ne_nil_of_length_eq_succ (length_replicate _ _)) = a := by

From d8c7c26a6a52b0111cd683b1890819c125ddba32 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Tue, 5 Sep 2023 16:35:41 +0200
Subject: [PATCH 06/11] chore: more @fgdorais suggestions

---
 Std/Data/List/Lemmas.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 7b92b2ca3f..2c48bb7702 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -369,10 +369,10 @@ theorem subset_singleton_iff {a : α} {L : List α} : L ⊆ [a] ↔ ∃ n, L = r
     map f (replicate n a) = replicate n (f a) := by
   induction n <;> [rfl; simp only [*, replicate, map]]
 
-@[simp] theorem tail_replicate (a : α) (n) :
+theorem tail_replicate (a : α) (n) :
     tail (replicate n a) = replicate (n - 1) a := by cases n <;> rfl
 
-@[simp] theorem join_replicate_nil (n : Nat) : join (replicate n []) = @nil α := by
+theorem join_replicate_nil (n : Nat) : join (replicate n []) = @nil α := by
   induction n <;> [rfl; simp only [*, replicate, join, append_nil]]
 
 /-! ### getLast -/
@@ -426,7 +426,7 @@ theorem getLast_mem {l : List α} (h : l ≠ []) : getLast l h ∈ l := by
     | nil => exact mem_singleton_self ..
     | cons _ _ =>
       rw [getLast_cons]
-      apply mem_cons_of_mem _ <| ih (cons_ne_nil _ _)
+      apply mem_cons_of_mem _ <| ih $ cons_ne_nil _ _
 
 theorem getLast_replicate_succ (m : Nat) (a : α) :
     (replicate (m + 1) a).getLast (ne_nil_of_length_eq_succ (length_replicate _ _)) = a := by

From df9cac79f8beb2e45102c535dc1256b9604e61f4 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Wed, 6 Sep 2023 12:37:11 +0200
Subject: [PATCH 07/11] chore: more @fgdorais suggestions

---
 Std/Data/List/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 2c48bb7702..0b004d6017 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -404,7 +404,7 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = L ++ [b]
 
 theorem getLast_append_singleton {a : α} (l : List α) :
     getLast (l ++ [a]) (append_ne_nil_of_ne_nil_right l _ (cons_ne_nil a _)) = a := by
-  simp only [getLast_append]
+  simp
 
 -- Porting note: name should be fixed upstream
 theorem getLast_append' (l₁ l₂ : List α) (h : l₂ ≠ []) :

From 827f0a5ed3e0a2f5a20b09e1d2258d433828ba2c Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Mon, 11 Sep 2023 15:31:42 +0200
Subject: [PATCH 08/11] chore: fix
 `List.getLast_append`/`List.getLast_singleton` problem

---
 Std/Data/List/Lemmas.lean | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 0b004d6017..9d9a8293b8 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -388,10 +388,14 @@ theorem getLast_cons' {a : α} {l : List α} : ∀ (h₁ : a :: l ≠ nil) (h₂
   getLast (a :: l) h₁ = getLast l h₂ := by
   induction l <;> intros; {contradiction}; rfl
 
-@[simp] theorem getLast_append {a : α} : ∀ (l : List α) h, getLast (l ++ [a]) h = a
-  | [], _ => rfl
-  | a::t, _ => by
-    simp [getLast_cons' _ fun H => cons_ne_nil _ _ (append_eq_nil.1 H).2, getLast_append t]
+@[simp] theorem getLast_append_singleton {a : α} :
+  ∀ (l : List α),
+    getLast (l ++ [a]) (append_ne_nil_of_ne_nil_right l _ (cons_ne_nil a _)) = a
+  | [] => rfl
+  | a::t => by
+    simp [
+      getLast_cons' _ fun H => cons_ne_nil _ _ (append_eq_nil.1 H).2,
+      getLast_append_singleton t]
 
 theorem getLast_concat {h : concat l a ≠ []} : getLast (concat l a) h = a :=
   by simp
@@ -402,12 +406,7 @@ theorem eq_nil_or_concat : ∀ l : List α, l = [] ∨ ∃ L b, l = L ++ [b]
     | _, .inl rfl => .inr ⟨[], a, rfl⟩
     | _, .inr ⟨L, b, rfl⟩ => .inr ⟨a::L, b, rfl⟩
 
-theorem getLast_append_singleton {a : α} (l : List α) :
-    getLast (l ++ [a]) (append_ne_nil_of_ne_nil_right l _ (cons_ne_nil a _)) = a := by
-  simp
-
--- Porting note: name should be fixed upstream
-theorem getLast_append' (l₁ l₂ : List α) (h : l₂ ≠ []) :
+theorem getLast_append (l₁ l₂ : List α) (h : l₂ ≠ []) :
     getLast (l₁ ++ l₂) (append_ne_nil_of_ne_nil_right l₁ l₂ h) = getLast l₂ h := by
   induction l₁
   · simp

From 20de13eaad1995a9809f06d9dfd05bd42e2d12b3 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Sun, 24 Sep 2023 10:22:06 +0200
Subject: [PATCH 09/11] chore: fix confusing function applications

---
 Std/Data/List/Lemmas.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 9d9a8293b8..3a8f7290fd 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -425,7 +425,7 @@ theorem getLast_mem {l : List α} (h : l ≠ []) : getLast l h ∈ l := by
     | nil => exact mem_singleton_self ..
     | cons _ _ =>
       rw [getLast_cons]
-      apply mem_cons_of_mem _ <| ih $ cons_ne_nil _ _
+      apply mem_cons_of_mem _ <| ih (cons_ne_nil _ _)
 
 theorem getLast_replicate_succ (m : Nat) (a : α) :
     (replicate (m + 1) a).getLast (ne_nil_of_length_eq_succ (length_replicate _ _)) = a := by

From 386071697e3da3fd51f7ab32fa607b4c2279fd7d Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Mon, 6 Nov 2023 12:12:09 +0100
Subject: [PATCH 10/11] Apply suggestions from code review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

All suggestions from @fgdorais

Co-authored-by: François G. Dorais <fgdorais@gmail.com>
---
 Std/Data/List/Lemmas.lean | 81 ++++++++++++---------------------------
 1 file changed, 25 insertions(+), 56 deletions(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index 3a8f7290fd..b6ece51e35 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -29,7 +29,7 @@ theorem cons_inj (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' :=
   ⟨tail_eq_of_cons_eq, congrArg _⟩
 
 theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' :=
-  ⟨List.cons.inj, fun h => h.1 ▸ h.2 ▸ rfl⟩
+  List.cons.injEq .. ▸ .rfl
 
 theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b L, l = b :: L
   | c :: l', _ => ⟨c, l', rfl⟩
@@ -48,7 +48,7 @@ theorem length_pos_iff_exists_mem {l : List α} : 0 < length l ↔ ∃ a, a ∈
   ⟨exists_mem_of_length_pos, fun ⟨_, h⟩ => length_pos_of_mem h⟩
 
 theorem exists_cons_of_length_pos : ∀ {l : List α}, 0 < l.length → ∃ h t, l = h :: t
-  | h::t, _ => ⟨h, t, rfl⟩
+  | _::_, _ => ⟨_, _, rfl⟩
 
 theorem length_pos_iff_exists_cons :
     ∀ {l : List α}, 0 < l.length ↔ ∃ h t, l = h :: t :=
@@ -56,7 +56,7 @@ theorem length_pos_iff_exists_cons :
 
 theorem exists_cons_of_length_succ :
     ∀ {l : List α}, l.length = n + 1 → ∃ h t, l = h :: t
-  | h::t, _ => ⟨h, t, rfl⟩
+  | _::_, _ => ⟨_, _, rfl⟩
 
 theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
   Nat.pos_iff_ne_zero.trans (not_congr length_eq_zero)
@@ -175,14 +175,10 @@ theorem concat_cons (a b : α) (l : List α) : concat (a :: l) b = a :: concat l
   rfl
 
 theorem init_eq_of_concat_eq {a : α} {l₁ l₂ : List α} : concat l₁ a = concat l₂ a → l₁ = l₂ := by
-  intro h
-  simp at h
-  assumption
+  simp
 
 theorem last_eq_of_concat_eq {a b : α} {l : List α} : concat l a = concat l b → a = b := by
-  intro h
-  simp at h
-  assumption
+  simp
 
 theorem concat_ne_nil (a : α) (l : List α) : concat l a ≠ [] := by simp
 
@@ -378,11 +374,8 @@ theorem join_replicate_nil (n : Nat) : join (replicate n []) = @nil α := by
 /-! ### getLast -/
 
 @[simp]
-theorem getLast_cons {a : α} {l : List α} :
-    ∀ h : l ≠ nil, getLast (a :: l) (cons_ne_nil a l) = getLast l h := by
-  induction l <;> intros
-  · contradiction
-  · rfl
+theorem getLast_cons {a : α} : ∀ {l} (h : l ≠ nil), getLast (a :: l) (cons_ne_nil a l) = getLast l h
+  | _::_, _ => rfl
 
 theorem getLast_cons' {a : α} {l : List α} : ∀ (h₁ : a :: l ≠ nil) (h₂ : l ≠ nil),
   getLast (a :: l) h₁ = getLast l h₂ := by
@@ -611,43 +604,34 @@ theorem head?_eq_head : ∀ l h, @head? α l = some (head l h)
   | _::_, _ => rfl
 
 theorem eq_cons_of_mem_head? {x : α} : ∀ {l : List α}, x ∈ l.head? → l = x :: tail l
-  | [], h => (Option.not_mem_none _ h).elim
-  | a :: l, h => by
-    simp only [head?, Option.mem_def, Option.some_inj] at h
-    exact h ▸ rfl
+  | _ :: _, rfl => rfl
 
 theorem mem_of_mem_head? {x : α} {l : List α} (h : x ∈ l.head?) : x ∈ l :=
   (eq_cons_of_mem_head? h).symm ▸ mem_cons_self _ _
 
 @[simp] theorem head!_cons [Inhabited α] (a : α) (l : List α) : head! (a :: l) = a := rfl
 
-@[simp] theorem head!_append [Inhabited α] (t : List α) {s : List α} (h : s ≠ []) :
-    head! (s ++ t) = head! s := by
-  induction s; contradiction; rfl
+@[simp] theorem head!_append [Inhabited α] (t : List α) : ∀ {s}, s ≠ [] → head! (s ++ t) = head! s
+  | _::_, _ => rfl
 
-theorem head?_append {s t : List α} {x : α} (h : x ∈ s.head?) : x ∈ (s ++ t).head? := by
-  cases s; contradiction; exact h
+theorem head?_append : ∀ {s t : List α} {x}, x ∈ s.head? → x ∈ (s ++ t).head?
+  | _::_, _, _, rfl => rfl
 
 theorem head?_append_of_ne_nil :
     ∀ (l₁ : List α) {l₂ : List α} (_ : l₁ ≠ []), head? (l₁ ++ l₂) = head? l₁
   | _ :: _, _, _ => rfl
 
 theorem cons_head?_tail : ∀ {l : List α} {a : α}, a ∈ head? l → a :: tail l = l
-  | [], a, h => by contradiction
-  | b :: l, a, h => by
-    simp at h
-    simp [h]
+  | _ :: _, _, rfl => rfl
 
 theorem head!_mem_head? [Inhabited α] : ∀ {l : List α}, l ≠ [] → head! l ∈ head? l
-  | [], h => by contradiction
-  | a :: l, _ => rfl
+  | _ :: _, _ => rfl
 
-theorem cons_head!_tail [Inhabited α] {l : List α} (h : l ≠ []) : head! l :: tail l = l :=
-  cons_head?_tail (head!_mem_head? h)
+theorem cons_head!_tail [Inhabited α] : ∀ {l : List α}, l ≠ [] → head! l :: tail l = l
+  | _::_, _ => rfl
 
-theorem head!_mem_self [Inhabited α] {l : List α} (h : l ≠ nil) : l.head! ∈ l := by
-  have h' := mem_cons_self l.head! l.tail
-  rwa [cons_head!_tail h] at h'
+theorem head!_mem_self [Inhabited α] : ∀ {l : List α}, l ≠ [] → l.head! ∈ l 
+  | _::_, _ => mem_cons_self ..
 
 @[simp] theorem head?_map (f : α → β) (l) : head? (map f l) = (head? l).map f := by
   cases l <;> rfl
@@ -667,16 +651,11 @@ theorem tail_eq_tailD (l) : @tail α l = tailD l [] := by cases l <;> rfl
 
 theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_tailD]
 
-theorem tail_append_singleton_of_ne_nil {a : α} {l : List α} (h : l ≠ nil) :
-    tail (l ++ [a]) = tail l ++ [a] := by
-  induction l
-  · contradiction
-  · rw [tail, cons_append, tail]
+theorem tail_append_singleton_of_ne_nil {a : α} : ∀ {l}, l ≠ [] → tail (l ++ [a]) = tail l ++ [a]
+  | _::_, _ => rfl
 
-theorem tail_append_of_ne_nil (l l' : List α) (h : l ≠ []) : (l ++ l').tail = l.tail ++ l' := by
-  cases l
-  · contradiction
-  · simp
+theorem tail_append_of_ne_nil : ∀ (l l' : List α), l ≠ [] → (l ++ l').tail = l.tail ++ l' 
+  | _::_, _, _ => rfl
 
 /-! ### next? -/
 
@@ -724,7 +703,6 @@ theorem getLast?_eq_getLast : ∀ l h, @getLast? α l = some (getLast l h)
   | a :: b :: l => by simp [getLast?_isSome (l := b :: l)]
 
 theorem mem_getLast?_eq_getLast : ∀ {l : List α} {x : α}, x ∈ l.getLast? → ∃ h, x = getLast l h
-  | [], x, hx => False.elim <| by simp at hx
   | [a], x, hx =>
     have : a = x := by simpa using hx
     this ▸ ⟨cons_ne_nil a [], rfl⟩
@@ -735,12 +713,10 @@ theorem mem_getLast?_eq_getLast : ∀ {l : List α} {x : α}, x ∈ l.getLast? 
     assumption
 
 theorem getLast?_eq_getLast_of_ne_nil : ∀ {l : List α} (h : l ≠ []), l.getLast? = some (l.getLast h)
-  | [], h => (h rfl).elim
   | [_], _ => rfl
   | _ :: b :: l, _ => getLast?_eq_getLast_of_ne_nil (l := b :: l) (cons_ne_nil _ _)
 
 theorem mem_getLast?_cons {x y : α} : ∀ {l : List α}, x ∈ l.getLast? → x ∈ (y :: l).getLast?
-  | [], _ => by contradiction
   | _ :: _, h => h
 
 theorem mem_of_mem_getLast? {l : List α} {a : α} (ha : a ∈ l.getLast?) : a ∈ l :=
@@ -756,15 +732,10 @@ theorem mem_of_mem_getLast? {l : List α} {a : α} (ha : a ∈ l.getLast?) : a 
 
 theorem getLast?_append_of_ne_nil (l₁ : List α) :
     ∀ {l₂ : List α} (_ : l₂ ≠ []), getLast? (l₁ ++ l₂) = getLast? l₂
-  | [], hl₂ => by contradiction
   | b :: l₂, _ => getLast?_append_cons l₁ b l₂
 
-theorem getLast?_append {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.getLast?) :
-    x ∈ (l₁ ++ l₂).getLast? := by
-  cases l₂
-  · contradiction
-  · rw [List.getLast?_append_cons]
-    exact h
+theorem getLast?_append : ∀ {l₁ l₂ : List α}, x ∈ l₂.getLast? → x ∈ (l₁ ++ l₂).getLast?
+  | _, _::_, h => getLast?_append_cons .. ▸ h
 
 /-! ### dropLast -/
 
@@ -937,10 +908,8 @@ theorem getLast?_eq_get? : ∀ (l : List α), getLast? l = l.get? (l.length - 1)
   | [], a => rfl
   | b :: l, a => by rw [cons_append, length_cons]; simp only [get?, get?_concat_length]
 
--- simp can prove this
--- @[simp]
 theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
-  simp [getLast?_eq_get?]
+  simp
 
 @[simp] theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
   rw [getLastD_eq_getLast?, getLast?_concat]; rfl

From 686f52a94f14fff5ea344fb334b5e77a0c2b1227 Mon Sep 17 00:00:00 2001
From: Adrien Champion <AdrienChampion@users.noreply.github.com>
Date: Mon, 6 Nov 2023 12:26:02 +0100
Subject: [PATCH 11/11] chore: remove trailing whitespaces

---
 Std/Data/List/Lemmas.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Std/Data/List/Lemmas.lean b/Std/Data/List/Lemmas.lean
index b6ece51e35..e78af42ea6 100644
--- a/Std/Data/List/Lemmas.lean
+++ b/Std/Data/List/Lemmas.lean
@@ -630,7 +630,7 @@ theorem head!_mem_head? [Inhabited α] : ∀ {l : List α}, l ≠ [] → head! l
 theorem cons_head!_tail [Inhabited α] : ∀ {l : List α}, l ≠ [] → head! l :: tail l = l
   | _::_, _ => rfl
 
-theorem head!_mem_self [Inhabited α] : ∀ {l : List α}, l ≠ [] → l.head! ∈ l 
+theorem head!_mem_self [Inhabited α] : ∀ {l : List α}, l ≠ [] → l.head! ∈ l
   | _::_, _ => mem_cons_self ..
 
 @[simp] theorem head?_map (f : α → β) (l) : head? (map f l) = (head? l).map f := by
@@ -654,7 +654,7 @@ theorem tail_eq_tail? (l) : @tail α l = (tail? l).getD [] := by simp [tail_eq_t
 theorem tail_append_singleton_of_ne_nil {a : α} : ∀ {l}, l ≠ [] → tail (l ++ [a]) = tail l ++ [a]
   | _::_, _ => rfl
 
-theorem tail_append_of_ne_nil : ∀ (l l' : List α), l ≠ [] → (l ++ l').tail = l.tail ++ l' 
+theorem tail_append_of_ne_nil : ∀ (l l' : List α), l ≠ [] → (l ++ l').tail = l.tail ++ l'
   | _::_, _, _ => rfl
 
 /-! ### next? -/