chore: bump dependencies (#4012)

This just bumps the Std dependency, to get access to Mario's new "Try this:" implementation.



Co-authored-by: Bulhwi Cha <chabulhwi@semmalgil.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: 5 people

Mathlib/Data/Char.lean

@@ -27,8 +27,6 @@ theorem Char.utf8Size_pos (c : Char) : 0 < c.utf8Size := by
   repeat (split; decide)
   decide
 
-theorem String.csize_pos : (c : Char) → 0 < String.csize c := Char.utf8Size_pos
-
 /--
 Provides a `LinearOrder` instance on `Char`. `Char` is the type of Unicode scalar values.
 -/

Mathlib/Data/List/Infix.lean

@@ -43,56 +43,17 @@ variable {l l₁ l₂ l₃ : List α} {a b : α} {m n : ℕ}
 
 section Fix
 
-@[simp]
-theorem prefix_append (l₁ l₂ : List α) : l₁ <+: l₁ ++ l₂ :=
-  ⟨l₂, rfl⟩
 #align list.prefix_append List.prefix_append
-
-@[simp]
-theorem suffix_append (l₁ l₂ : List α) : l₂ <:+ l₁ ++ l₂ :=
-  ⟨l₁, rfl⟩
 #align list.suffix_append List.suffix_append
-
-theorem infix_append (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ l₂ ++ l₃ :=
-  ⟨l₁, l₃, rfl⟩
 #align list.infix_append List.infix_append
-
-@[simp]
-theorem infix_append' (l₁ l₂ l₃ : List α) : l₂ <:+: l₁ ++ (l₂ ++ l₃) := by
-  rw [← List.append_assoc]; apply infix_append
 #align list.infix_append' List.infix_append'
-
-theorem isPrefix.isInfix : l₁ <+: l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨[], t, h⟩
 #align list.is_prefix.is_infix List.isPrefix.isInfix
-
-theorem isSuffix.isInfix : l₁ <:+ l₂ → l₁ <:+: l₂ := fun ⟨t, h⟩ => ⟨t, [], by rw [h, append_nil]⟩
 #align list.is_suffix.is_infix List.isSuffix.isInfix
-
-theorem nil_prefix (l : List α) : [] <+: l :=
-  ⟨l, rfl⟩
 #align list.nil_prefix List.nil_prefix
-
-theorem nil_suffix (l : List α) : [] <:+ l :=
-  ⟨l, append_nil _⟩
 #align list.nil_suffix List.nil_suffix
-
-theorem nil_infix (l : List α) : [] <:+: l :=
-  (nil_prefix _).isInfix
 #align list.nil_infix List.nil_infix
-
-@[refl]
-theorem prefix_refl (l : List α) : l <+: l :=
-  ⟨[], append_nil _⟩
 #align list.prefix_refl List.prefix_refl
-
-@[refl]
-theorem suffix_refl (l : List α) : l <:+ l :=
-  ⟨[], rfl⟩
 #align list.suffix_refl List.suffix_refl
-
-@[refl]
-theorem infix_refl (l : List α) : l <:+: l :=
-  (prefix_refl l).isInfix
 #align list.infix_refl List.infix_refl
 
 theorem prefix_rfl : l <+: l :=
@@ -107,80 +68,24 @@ theorem infix_rfl : l <:+: l :=
   infix_refl _
 #align list.infix_rfl List.infix_rfl
 
-@[simp]
-theorem suffix_cons (a : α) : ∀ l, l <:+ a :: l :=
-  suffix_append [a]
 #align list.suffix_cons List.suffix_cons
 
 theorem prefix_concat (a : α) (l) : l <+: concat l a := by simp
 #align list.prefix_concat List.prefix_concat
 
-theorem infix_cons : l₁ <:+: l₂ → l₁ <:+: a :: l₂ := fun ⟨L₁, L₂, h⟩ => ⟨a :: L₁, L₂, h ▸ rfl⟩
 #align list.infix_cons List.infix_cons
-
-theorem infix_concat : l₁ <:+: l₂ → l₁ <:+: concat l₂ a := fun ⟨L₁, L₂, h⟩ =>
-  ⟨L₁, concat L₂ a, by simp_rw [← h, concat_eq_append, append_assoc]⟩
 #align list.infix_concat List.infix_concat
-
-@[trans]
-theorem isPrefix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <+: l₂ → l₂ <+: l₃ → l₁ <+: l₃
-  | _, _, _, ⟨r₁, rfl⟩, ⟨r₂, rfl⟩ => ⟨r₁ ++ r₂, (append_assoc _ _ _).symm⟩
 #align list.is_prefix.trans List.isPrefix.trans
-
-@[trans]
-theorem isSuffix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
-  | _, _, _, ⟨l₁, rfl⟩, ⟨l₂, rfl⟩ => ⟨l₂ ++ l₁, append_assoc _ _ _⟩
 #align list.is_suffix.trans List.isSuffix.trans
-
-@[trans]
-theorem isInfix.trans : ∀ {l₁ l₂ l₃ : List α}, l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
-  | l, _, _, ⟨l₁, r₁, rfl⟩, ⟨l₂, r₂, rfl⟩ => ⟨l₂ ++ l₁, r₁ ++ r₂, by simp only [append_assoc]⟩
 #align list.is_infix.trans List.isInfix.trans
-
-protected theorem isInfix.sublist : l₁ <:+: l₂ → l₁ <+ l₂ := fun ⟨s, t, h⟩ => by
-  rw [← h]
-  exact (sublist_append_right _ _).trans (sublist_append_left _ _)
 #align list.is_infix.sublist List.isInfix.sublist
-
-protected theorem isInfix.subset (hl : l₁ <:+: l₂) : l₁ ⊆ l₂ :=
-  hl.sublist.subset
 #align list.is_infix.subset List.isInfix.subset
-
-protected theorem isPrefix.sublist (h : l₁ <+: l₂) : l₁ <+ l₂ :=
-  h.isInfix.sublist
 #align list.is_prefix.sublist List.isPrefix.sublist
-
-protected theorem isPrefix.subset (hl : l₁ <+: l₂) : l₁ ⊆ l₂ :=
-  hl.sublist.subset
 #align list.is_prefix.subset List.isPrefix.subset
-
-protected theorem isSuffix.sublist (h : l₁ <:+ l₂) : l₁ <+ l₂ :=
-  h.isInfix.sublist
 #align list.is_suffix.sublist List.isSuffix.sublist
-
-protected theorem isSuffix.subset (hl : l₁ <:+ l₂) : l₁ ⊆ l₂ :=
-  hl.sublist.subset
 #align list.is_suffix.subset List.isSuffix.subset
-
-@[simp]
-theorem reverse_suffix : reverse l₁ <:+ reverse l₂ ↔ l₁ <+: l₂ :=
-  ⟨fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_reverse l₁, ← reverse_append, e, reverse_reverse]⟩,
-    fun ⟨r, e⟩ => ⟨reverse r, by rw [← reverse_append, e]⟩⟩
 #align list.reverse_suffix List.reverse_suffix
-
-@[simp]
-theorem reverse_prefix : reverse l₁ <+: reverse l₂ ↔ l₁ <:+ l₂ := by
-  rw [← reverse_suffix]; simp only [reverse_reverse]
 #align list.reverse_prefix List.reverse_prefix
-
-@[simp]
-theorem reverse_infix : reverse l₁ <:+: reverse l₂ ↔ l₁ <:+: l₂ :=
-  ⟨fun ⟨s, t, e⟩ =>
-    ⟨reverse t, reverse s, by
-      rw [← reverse_reverse l₁, append_assoc, ← reverse_append, ← reverse_append, e,
-        reverse_reverse]⟩,
-    fun ⟨s, t, e⟩ =>
-    ⟨reverse t, reverse s, by rw [append_assoc, ← reverse_append, ← reverse_append, e]⟩⟩
 #align list.reverse_infix List.reverse_infix
 
 alias reverse_prefix ↔ _ isSuffix.reverse
@@ -192,46 +97,22 @@ alias reverse_suffix ↔ _ isPrefix.reverse
 alias reverse_infix ↔ _ isInfix.reverse
 #align list.is_infix.reverse List.isInfix.reverse
 
-theorem isInfix.length_le (h : l₁ <:+: l₂) : l₁.length ≤ l₂.length :=
-  h.sublist.length_le
 #align list.is_infix.length_le List.isInfix.length_le
-
-theorem isPrefix.length_le (h : l₁ <+: l₂) : l₁.length ≤ l₂.length :=
-  h.sublist.length_le
 #align list.is_prefix.length_le List.isPrefix.length_le
-
-theorem isSuffix.length_le (h : l₁ <:+ l₂) : l₁.length ≤ l₂.length :=
-  h.sublist.length_le
 #align list.is_suffix.length_le List.isSuffix.length_le
+#align list.infix_nil_iff List.infix_nil
+#align list.prefix_nil_iff List.prefix_nil
+#align list.suffix_nil_iff List.suffix_nil
 
-theorem eq_nil_of_infix_nil (h : l <:+: []) : l = [] :=
-  eq_nil_of_sublist_nil h.sublist
+alias infix_nil ↔ eq_nil_of_infix_nil _
 #align list.eq_nil_of_infix_nil List.eq_nil_of_infix_nil
 
-@[simp]
-theorem infix_nil_iff : l <:+: [] ↔ l = [] :=
-  ⟨fun h => eq_nil_of_sublist_nil h.sublist, fun h => h ▸ infix_rfl⟩
-#align list.infix_nil_iff List.infix_nil_iff
-
-@[simp]
-theorem prefix_nil_iff : l <+: [] ↔ l = [] :=
-  ⟨fun h => eq_nil_of_infix_nil h.isInfix, fun h => h ▸ prefix_rfl⟩
-#align list.prefix_nil_iff List.prefix_nil_iff
-
-@[simp]
-theorem suffix_nil_iff : l <:+ [] ↔ l = [] :=
-  ⟨fun h => eq_nil_of_infix_nil h.isInfix, fun h => h ▸ suffix_rfl⟩
-#align list.suffix_nil_iff List.suffix_nil_iff
-
-alias prefix_nil_iff ↔ eq_nil_of_prefix_nil _
+alias prefix_nil ↔ eq_nil_of_prefix_nil _
 #align list.eq_nil_of_prefix_nil List.eq_nil_of_prefix_nil
 
-alias suffix_nil_iff ↔ eq_nil_of_suffix_nil _
+alias suffix_nil ↔ eq_nil_of_suffix_nil _
 #align list.eq_nil_of_suffix_nil List.eq_nil_of_suffix_nil
 
-theorem infix_iff_prefix_suffix (l₁ l₂ : List α) : l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂ :=
-  ⟨fun ⟨s, t, e⟩ => ⟨l₁ ++ t, ⟨_, rfl⟩, by rw [← e, append_assoc]; exact ⟨_, rfl⟩⟩,
-    fun ⟨_, ⟨t, rfl⟩, s, e⟩ => ⟨s, t, by rw [append_assoc]; exact e⟩⟩
 #align list.infix_iff_prefix_suffix List.infix_iff_prefix_suffix
 
 theorem eq_of_infix_of_length_eq (h : l₁ <:+: l₂) : l₁.length = l₂.length → l₁ = l₂ :=
@@ -246,101 +127,22 @@ theorem eq_of_suffix_of_length_eq (h : l₁ <:+ l₂) : l₁.length = l₂.lengt
   h.sublist.eq_of_length
 #align list.eq_of_suffix_of_length_eq List.eq_of_suffix_of_length_eq
 
-theorem prefix_of_prefix_length_le : ∀ { l₁ l₂ l₃ : List α } ,
-  l₁ <+: l₃ → l₂ <+: l₃ → length l₁ ≤ length l₂ → l₁ <+: l₂
-| [] , l₂ , _, _, _, _ => nil_prefix _
-| a :: l₁ , b :: l₂ , _ , ⟨ r₁ , rfl ⟩ , ⟨ r₂ , e ⟩ , ll => by
-  injection e with _ e'
-  subst b
-  rcases prefix_of_prefix_length_le ⟨ _ , rfl ⟩ ⟨ _ , e' ⟩
-    (le_of_succ_le_succ ll) with ⟨ r₃ , rfl ⟩
-  exact ⟨ r₃ , rfl ⟩
 #align list.prefix_of_prefix_length_le List.prefix_of_prefix_length_le
-
-theorem prefix_or_prefix_of_prefix (h₁ : l₁ <+: l₃) (h₂ : l₂ <+: l₃) : l₁ <+: l₂ ∨ l₂ <+: l₁ :=
-  (le_total (length l₁) (length l₂)).imp (prefix_of_prefix_length_le h₁ h₂)
-    (prefix_of_prefix_length_le h₂ h₁)
 #align list.prefix_or_prefix_of_prefix List.prefix_or_prefix_of_prefix
-
-theorem suffix_of_suffix_length_le (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) (ll : length l₁ ≤ length l₂) :
-    l₁ <:+ l₂ :=
-  reverse_prefix.1 <|
-    prefix_of_prefix_length_le (reverse_prefix.2 h₁) (reverse_prefix.2 h₂) (by simp [ll])
 #align list.suffix_of_suffix_length_le List.suffix_of_suffix_length_le
-
-theorem suffix_or_suffix_of_suffix (h₁ : l₁ <:+ l₃) (h₂ : l₂ <:+ l₃) : l₁ <:+ l₂ ∨ l₂ <:+ l₁ :=
-  (prefix_or_prefix_of_prefix (reverse_prefix.2 h₁) (reverse_prefix.2 h₂)).imp reverse_prefix.1
-    reverse_prefix.1
 #align list.suffix_or_suffix_of_suffix List.suffix_or_suffix_of_suffix
-
-theorem suffix_cons_iff : l₁ <:+ a :: l₂ ↔ l₁ = a :: l₂ ∨ l₁ <:+ l₂ := by
-  constructor
-  · rintro ⟨⟨hd, tl⟩, hl₃⟩
-    · exact Or.inl hl₃
-    · simp only [cons_append] at hl₃
-      injection hl₃ with _ hl₄
-      exact Or.inr ⟨_, hl₄⟩
-  · rintro (rfl | hl₁)
-    · exact (a :: l₂).suffix_refl
-    · exact hl₁.trans (l₂.suffix_cons _)
 #align list.suffix_cons_iff List.suffix_cons_iff
-
-theorem infix_cons_iff : l₁ <:+: a :: l₂ ↔ l₁ <+: a :: l₂ ∨ l₁ <:+: l₂ := by
-  constructor
-  · rintro ⟨⟨hd, tl⟩, t, hl₃⟩
-    · exact Or.inl ⟨t, hl₃⟩
-    · simp only [cons_append] at hl₃
-      injection hl₃ with _ hl₄
-      exact Or.inr ⟨_, t, hl₄⟩
-  · rintro (h | hl₁)
-    · exact h.isInfix
-    · exact infix_cons hl₁
 #align list.infix_cons_iff List.infix_cons_iff
-
-theorem infix_of_mem_join : ∀ {L : List (List α)}, l ∈ L → l <:+: join L
-  | l' :: _, h =>
-    match h with
-    | List.Mem.head .. => infix_append [] _ _
-    | List.Mem.tail _ hlMemL =>
-      isInfix.trans (infix_of_mem_join hlMemL) <| (suffix_append _ _).isInfix
 #align list.infix_of_mem_join List.infix_of_mem_join
-
-theorem prefix_append_right_inj (l) : l ++ l₁ <+: l ++ l₂ ↔ l₁ <+: l₂ :=
-  exists_congr fun r => by rw [append_assoc, append_right_inj]
 #align list.prefix_append_right_inj List.prefix_append_right_inj
-
-theorem prefix_cons_inj (a) : a :: l₁ <+: a :: l₂ ↔ l₁ <+: l₂ :=
-  prefix_append_right_inj [a]
 #align list.prefix_cons_inj List.prefix_cons_inj
-
-theorem take_prefix (n) (l : List α) : take n l <+: l :=
-  ⟨_, take_append_drop _ _⟩
 #align list.take_prefix List.take_prefix
-
-theorem drop_suffix (n) (l : List α) : drop n l <:+ l :=
-  ⟨_, take_append_drop _ _⟩
 #align list.drop_suffix List.drop_suffix
-
-theorem take_sublist (n) (l : List α) : take n l <+ l :=
-  (take_prefix n l).sublist
 #align list.take_sublist List.take_sublist
-
-theorem drop_sublist (n) (l : List α) : drop n l <+ l :=
-  (drop_suffix n l).sublist
 #align list.drop_sublist List.drop_sublist
-
-theorem take_subset (n) (l : List α) : take n l ⊆ l :=
-  (take_sublist n l).subset
 #align list.take_subset List.take_subset
-
-theorem drop_subset (n) (l : List α) : drop n l ⊆ l :=
-  (drop_sublist n l).subset
 #align list.drop_subset List.drop_subset
-
-theorem mem_of_mem_take (h : a ∈ l.take n) : a ∈ l :=
-  take_subset n l h
 #align list.mem_of_mem_take List.mem_of_mem_take
-
 #align list.mem_of_mem_drop List.mem_of_mem_drop
 
 lemma dropSlice_sublist (n m : ℕ) (l : List α) : l.dropSlice n m <+ l :=
@@ -505,25 +307,8 @@ theorem isPrefix.reduceOption {l₁ l₂ : List (Option α)} (h : l₁ <+: l₂)
   h.filter_map id
 #align list.is_prefix.reduce_option List.isPrefix.reduceOption
 
-theorem isPrefix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <+: l₂) :
-    l₁.filter p <+: l₂.filter p := by
-  obtain ⟨xs, rfl⟩ := h
-  rw [filter_append]
-  exact prefix_append _ _
 #align list.is_prefix.filter List.isPrefix.filter
-
-theorem isSuffix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+ l₂) :
-    l₁.filter p <:+ l₂.filter p := by
-  obtain ⟨xs, rfl⟩ := h
-  rw [filter_append]
-  exact suffix_append _ _
 #align list.is_suffix.filter List.isSuffix.filter
-
-theorem isInfix.filter (p : α → Bool) ⦃l₁ l₂ : List α⦄ (h : l₁ <:+: l₂) :
-    l₁.filter p <:+: l₂.filter p := by
-  obtain ⟨xs, ys, rfl⟩ := h
-  rw [filter_append, filter_append]
-  exact infix_append _ _ _
 #align list.is_infix.filter List.isInfix.filter
 
 instance : IsPartialOrder (List α) (· <+: ·) where
@@ -569,8 +354,7 @@ theorem mem_inits : ∀ s t : List α, s ∈ inits t ↔ s <+: t
 @[simp]
 theorem mem_tails : ∀ s t : List α, s ∈ tails t ↔ s <:+ t
   | s, [] => by
-    simp only [tails, mem_singleton]
-    exact ⟨fun h => by rw [h], eq_nil_of_suffix_nil⟩
+    simp only [tails, mem_singleton, suffix_nil]
   | s, a :: t => by
     simp only [tails, mem_cons, mem_tails s t];
     exact

Mathlib/Data/Nat/Order/Basic.lean

@@ -175,17 +175,7 @@ theorem lt_one_iff {n : ℕ} : n < 1 ↔ n = 0 :=
 
 /-! ### `add` -/
 
-
-theorem add_pos_left {m : ℕ} (h : 0 < m) (n : ℕ) : 0 < m + n :=
-  calc
-    m + n > 0 + n := Nat.add_lt_add_right h n
-    _ = n := Nat.zero_add n
-    _ ≥ 0 := zero_le n
 #align nat.add_pos_left Nat.add_pos_left
-
-theorem add_pos_right (m : ℕ) {n : ℕ} (h : 0 < n) : 0 < m + n := by
-  rw [add_comm]
-  exact add_pos_left h m
 #align nat.add_pos_right Nat.add_pos_right
 
 theorem add_pos_iff_pos_or_pos (m n : ℕ) : 0 < m + n ↔ 0 < m ∨ 0 < n :=