fixes

src/Init/Core.lean

@@ -1937,6 +1937,15 @@ instance : Subsingleton (Squash α) where
     apply Quot.sound
     trivial
 
+/-! # Relations -/
+
+/--
+`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
+-/
+class Antisymm {α : Sort u} (r : α → α → Prop) : Prop where
+  /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
+  antisymm {a b : α} : r a b → r b a → a = b
+
 namespace Lean
 /-! # Kernel reduction hints -/
 
@@ -2112,14 +2121,4 @@ instance : Commutative Or := ⟨fun _ _ => propext or_comm⟩
 instance : Commutative And := ⟨fun _ _ => propext and_comm⟩
 instance : Commutative Iff := ⟨fun _ _ => propext iff_comm⟩
 
-/--
-`Antisymm (·≤·)` says that `(·≤·)` is antisymmetric, that is, `a ≤ b → b ≤ a → a = b`.
--/
-class Antisymm (r : α → α → Prop) : Prop where
-  /-- An antisymmetric relation `(·≤·)` satisfies `a ≤ b → b ≤ a → a = b`. -/
-  antisymm {a b : α} : r a b → r b a → a = b
-
-@[deprecated Antisymm (since := "2024-10-16"), inherit_doc Antisymm]
-abbrev _root_.Antisymm (r : α → α → Prop) : Prop := Std.Antisymm r
-
 end Std

src/Init/Data/Array/Basic.lean

@@ -25,8 +25,6 @@ variable {α : Type u}
 
 namespace Array
 
-@[deprecated size (since := "2024-10-13")] abbrev data := @toList
-
 /-! ### Preliminary theorems -/
 
 @[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=

src/Init/Data/List/BasicAux.lean

@@ -232,8 +232,7 @@ theorem sizeOf_get [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.g
     apply Nat.lt_trans ih
     simp_arith
 
-theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : α → α → Prop)]
-    {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
+theorem le_antisymm [LT α] [s : Antisymm (¬ · < · : α → α → Prop)] {as bs : List α} (h₁ : as ≤ bs) (h₂ : bs ≤ as) : as = bs :=
   match as, bs with
   | [],    []    => rfl
   | [],    _::_ => False.elim <| h₂ (List.lt.nil ..)
@@ -249,8 +248,7 @@ theorem le_antisymm [LT α] [s : Std.Antisymm (¬ · < · : α → α → Prop)]
         have : a = b := s.antisymm hab hba
         simp [this, ih]
 
-instance [LT α] [Std.Antisymm (¬ · < · : α → α → Prop)] :
-    Std.Antisymm (· ≤ · : List α → List α → Prop) where
+instance [LT α] [Antisymm (¬ · < · : α → α → Prop)] : Antisymm (· ≤ · : List α → List α → Prop) where
   antisymm h₁ h₂ := le_antisymm h₁ h₂
 
 end List

src/Init/Data/List/MinMax.lean

@@ -75,7 +75,7 @@ theorem le_min?_iff [Min α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `min_eq_or`,
 -- and `le_min_iff`.
-theorem min?_eq_some_iff [Min α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
+theorem min?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
     (le_refl : ∀ a : α, a ≤ a)
     (min_eq_or : ∀ a b : α, min a b = a ∨ min a b = b)
     (le_min_iff : ∀ a b c : α, a ≤ min b c ↔ a ≤ b ∧ a ≤ c) {xs : List α} :
@@ -146,7 +146,7 @@ theorem max?_le_iff [Max α] [LE α]
 
 -- This could be refactored by designing appropriate typeclasses to replace `le_refl`, `max_eq_or`,
 -- and `le_min_iff`.
-theorem max?_eq_some_iff [Max α] [LE α] [anti : Std.Antisymm ((· : α) ≤ ·)]
+theorem max?_eq_some_iff [Max α] [LE α] [anti : Antisymm ((· : α) ≤ ·)]
     (le_refl : ∀ a : α, a ≤ a)
     (max_eq_or : ∀ a b : α, max a b = a ∨ max a b = b)
     (max_le_iff : ∀ a b c : α, max b c ≤ a ↔ b ≤ a ∧ c ≤ a) {xs : List α} :

src/Init/Data/Nat/Basic.lean

@@ -490,10 +490,10 @@ protected theorem le_antisymm_iff {a b : Nat} : a = b ↔ a ≤ b ∧ b ≤ a :=
             (fun ⟨hle, hge⟩ => Nat.le_antisymm hle hge)
 protected theorem eq_iff_le_and_ge : ∀{a b : Nat}, a = b ↔ a ≤ b ∧ b ≤ a := @Nat.le_antisymm_iff
 
-instance : Std.Antisymm ( . ≤ . : Nat → Nat → Prop) where
+instance : Antisymm ( . ≤ . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm h₁ h₂
 
-instance : Std.Antisymm (¬ . < . : Nat → Nat → Prop) where
+instance : Antisymm (¬ . < . : Nat → Nat → Prop) where
   antisymm h₁ h₂ := Nat.le_antisymm (Nat.ge_of_not_lt h₂) (Nat.ge_of_not_lt h₁)
 
 protected theorem add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m :=

src/Init/Data/String/Basic.lean

@@ -1148,23 +1148,23 @@ namespace String
 /--
 If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
 -/
-def dropPrefix? (s : String) (pre : String) : Option Substring :=
-  s.toSubstring.dropPrefix? pre.toSubstring
+def dropPrefix? (s : String) (pre : Substring) : Option Substring :=
+  s.toSubstring.dropPrefix? pre
 
 /--
 If `suff` is a suffix of `s`, i.e. `s = t ++ suff`, returns the remainder `t`.
 -/
-def dropSuffix? (s : String) (suff : String) : Option Substring :=
-  s.toSubstring.dropSuffix? suff.toSubstring
+def dropSuffix? (s : String) (suff : Substring) : Option Substring :=
+  s.toSubstring.dropSuffix? suff
 
 /-- `s.stripPrefix pre` will remove `pre` from the beginning of `s` if it occurs there,
 or otherwise return `s`. -/
-def stripPrefix (s : String) (pre : String) : String :=
+def stripPrefix (s : String) (pre : Substring) : String :=
   s.dropPrefix? pre |>.map Substring.toString |>.getD s
 
 /-- `s.stripSuffix suff` will remove `suff` from the end of `s` if it occurs there,
 or otherwise return `s`. -/
-def stripSuffix (s : String) (suff : String) : String :=
+def stripSuffix (s : String) (suff : Substring) : String :=
   s.dropSuffix? suff |>.map Substring.toString |>.getD s
 
 end String

src/Init/Data/Sum.lean

@@ -4,5 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yury G. Kudryashov
 -/
 prelude
-import Init.Data.Sum.Basic
-import Init.Data.Sum.Lemmas
+import Init.Core
+
+namespace Sum
+
+deriving instance DecidableEq for Sum
+deriving instance BEq for Sum
+
+/-- Check if a sum is `inl` and if so, retrieve its contents. -/
+def getLeft? : α ⊕ β → Option α
+  | inl a => some a
+  | inr _ => none
+
+/-- Check if a sum is `inr` and if so, retrieve its contents. -/
+def getRight? : α ⊕ β → Option β
+  | inr b => some b
+  | inl _ => none
+
+end Sum

src/Init/Data/Sum/Basic.lean

@@ -1,178 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Yury G. Kudryashov
--/
-prelude
-import Init.PropLemmas
-
-/-!
-# Disjoint union of types
-
-This file defines basic operations on the the sum type `α ⊕ β`.
-
-`α ⊕ β` is the type made of a copy of `α` and a copy of `β`. It is also called *disjoint union*.
-
-## Main declarations
-
-* `Sum.isLeft`: Returns whether `x : α ⊕ β` comes from the left component or not.
-* `Sum.isRight`: Returns whether `x : α ⊕ β` comes from the right component or not.
-* `Sum.getLeft`: Retrieves the left content of a `x : α ⊕ β` that is known to come from the left.
-* `Sum.getRight`: Retrieves the right content of `x : α ⊕ β` that is known to come from the right.
-* `Sum.getLeft?`: Retrieves the left content of `x : α ⊕ β` as an option type or returns `none`
-  if it's coming from the right.
-* `Sum.getRight?`: Retrieves the right content of `x : α ⊕ β` as an option type or returns `none`
-  if it's coming from the left.
-* `Sum.map`: Maps `α ⊕ β` to `γ ⊕ δ` component-wise.
-* `Sum.elim`: Nondependent eliminator/induction principle for `α ⊕ β`.
-* `Sum.swap`: Maps `α ⊕ β` to `β ⊕ α` by swapping components.
-* `Sum.LiftRel`: The disjoint union of two relations.
-* `Sum.Lex`: Lexicographic order on `α ⊕ β` induced by a relation on `α` and a relation on `β`.
-
-## Further material
-
-See `Batteries.Data.Sum.Lemmas` for theorems about these definitions.
-
-## Notes
-
-The definition of `Sum` takes values in `Type _`. This effectively forbids `Prop`- valued sum types.
-To this effect, we have `PSum`, which takes value in `Sort _` and carries a more complicated
-universe signature in consequence. The `Prop` version is `Or`.
--/
-
-namespace Sum
-
-deriving instance DecidableEq for Sum
-deriving instance BEq for Sum
-
-section get
-
-/-- Check if a sum is `inl`. -/
-def isLeft : α ⊕ β → Bool
-  | inl _ => true
-  | inr _ => false
-
-/-- Check if a sum is `inr`. -/
-def isRight : α ⊕ β → Bool
-  | inl _ => false
-  | inr _ => true
-
-/-- Retrieve the contents from a sum known to be `inl`.-/
-def getLeft : (ab : α ⊕ β) → ab.isLeft → α
-  | inl a, _ => a
-
-/-- Retrieve the contents from a sum known to be `inr`.-/
-def getRight : (ab : α ⊕ β) → ab.isRight → β
-  | inr b, _ => b
-
-/-- Check if a sum is `inl` and if so, retrieve its contents. -/
-def getLeft? : α ⊕ β → Option α
-  | inl a => some a
-  | inr _ => none
-
-/-- Check if a sum is `inr` and if so, retrieve its contents. -/
-def getRight? : α ⊕ β → Option β
-  | inr b => some b
-  | inl _ => none
-
-@[simp] theorem isLeft_inl : (inl x : α ⊕ β).isLeft = true := rfl
-@[simp] theorem isLeft_inr : (inr x : α ⊕ β).isLeft = false := rfl
-@[simp] theorem isRight_inl : (inl x : α ⊕ β).isRight = false := rfl
-@[simp] theorem isRight_inr : (inr x : α ⊕ β).isRight = true := rfl
-
-@[simp] theorem getLeft_inl (h : (inl x : α ⊕ β).isLeft) : (inl x).getLeft h = x := rfl
-@[simp] theorem getRight_inr (h : (inr x : α ⊕ β).isRight) : (inr x).getRight h = x := rfl
-
-@[simp] theorem getLeft?_inl : (inl x : α ⊕ β).getLeft? = some x := rfl
-@[simp] theorem getLeft?_inr : (inr x : α ⊕ β).getLeft? = none := rfl
-@[simp] theorem getRight?_inl : (inl x : α ⊕ β).getRight? = none := rfl
-@[simp] theorem getRight?_inr : (inr x : α ⊕ β).getRight? = some x := rfl
-
-end get
-
-/-- Define a function on `α ⊕ β` by giving separate definitions on `α` and `β`. -/
-protected def elim {α β γ} (f : α → γ) (g : β → γ) : α ⊕ β → γ :=
-  fun x => Sum.casesOn x f g
-
-@[simp] theorem elim_inl (f : α → γ) (g : β → γ) (x : α) :
-    Sum.elim f g (inl x) = f x := rfl
-
-@[simp] theorem elim_inr (f : α → γ) (g : β → γ) (x : β) :
-    Sum.elim f g (inr x) = g x := rfl
-
-/-- Map `α ⊕ β` to `α' ⊕ β'` sending `α` to `α'` and `β` to `β'`. -/
-protected def map (f : α → α') (g : β → β') : α ⊕ β → α' ⊕ β' :=
-  Sum.elim (inl ∘ f) (inr ∘ g)
-
-@[simp] theorem map_inl (f : α → α') (g : β → β') (x : α) : (inl x).map f g = inl (f x) := rfl
-
-@[simp] theorem map_inr (f : α → α') (g : β → β') (x : β) : (inr x).map f g = inr (g x) := rfl
-
-/-- Swap the factors of a sum type -/
-def swap : α ⊕ β → β ⊕ α := Sum.elim inr inl
-
-@[simp] theorem swap_inl : swap (inl x : α ⊕ β) = inr x := rfl
-
-@[simp] theorem swap_inr : swap (inr x : α ⊕ β) = inl x := rfl
-
-section LiftRel
-
-/-- Lifts pointwise two relations between `α` and `γ` and between `β` and `δ` to a relation between
-`α ⊕ β` and `γ ⊕ δ`. -/
-inductive LiftRel (r : α → γ → Prop) (s : β → δ → Prop) : α ⊕ β → γ ⊕ δ → Prop
-  /-- `inl a` and `inl c` are related via `LiftRel r s` if `a` and `c` are related via `r`. -/
-  | protected inl {a c} : r a c → LiftRel r s (inl a) (inl c)
-  /-- `inr b` and `inr d` are related via `LiftRel r s` if `b` and `d` are related via `s`. -/
-  | protected inr {b d} : s b d → LiftRel r s (inr b) (inr d)
-
-@[simp] theorem liftRel_inl_inl : LiftRel r s (inl a) (inl c) ↔ r a c :=
-  ⟨fun h => by cases h; assumption, LiftRel.inl⟩
-
-@[simp] theorem not_liftRel_inl_inr : ¬LiftRel r s (inl a) (inr d) := nofun
-
-@[simp] theorem not_liftRel_inr_inl : ¬LiftRel r s (inr b) (inl c) := nofun
-
-@[simp] theorem liftRel_inr_inr : LiftRel r s (inr b) (inr d) ↔ s b d :=
-  ⟨fun h => by cases h; assumption, LiftRel.inr⟩
-
-instance {r : α → γ → Prop} {s : β → δ → Prop}
-    [∀ a c, Decidable (r a c)] [∀ b d, Decidable (s b d)] :
-    ∀ (ab : α ⊕ β) (cd : γ ⊕ δ), Decidable (LiftRel r s ab cd)
-  | inl _, inl _ => decidable_of_iff' _ liftRel_inl_inl
-  | inl _, inr _ => Decidable.isFalse not_liftRel_inl_inr
-  | inr _, inl _ => Decidable.isFalse not_liftRel_inr_inl
-  | inr _, inr _ => decidable_of_iff' _ liftRel_inr_inr
-
-end LiftRel
-
-section Lex
-
-/-- Lexicographic order for sum. Sort all the `inl a` before the `inr b`, otherwise use the
-respective order on `α` or `β`. -/
-inductive Lex (r : α → α → Prop) (s : β → β → Prop) : α ⊕ β → α ⊕ β → Prop
-  /-- `inl a₁` and `inl a₂` are related via `Lex r s` if `a₁` and `a₂` are related via `r`. -/
-  | protected inl {a₁ a₂} (h : r a₁ a₂) : Lex r s (inl a₁) (inl a₂)
-  /-- `inr b₁` and `inr b₂` are related via `Lex r s` if `b₁` and `b₂` are related via `s`. -/
-  | protected inr {b₁ b₂} (h : s b₁ b₂) : Lex r s (inr b₁) (inr b₂)
-  /-- `inl a` and `inr b` are always related via `Lex r s`. -/
-  | sep (a b) : Lex r s (inl a) (inr b)
-
-attribute [simp] Lex.sep
-
-@[simp] theorem lex_inl_inl : Lex r s (inl a₁) (inl a₂) ↔ r a₁ a₂ :=
-  ⟨fun h => by cases h; assumption, Lex.inl⟩
-
-@[simp] theorem lex_inr_inr : Lex r s (inr b₁) (inr b₂) ↔ s b₁ b₂ :=
-  ⟨fun h => by cases h; assumption, Lex.inr⟩
-
-@[simp] theorem lex_inr_inl : ¬Lex r s (inr b) (inl a) := nofun
-
-instance instDecidableRelSumLex [DecidableRel r] [DecidableRel s] : DecidableRel (Lex r s)
-  | inl _, inl _ => decidable_of_iff' _ lex_inl_inl
-  | inl _, inr _ => Decidable.isTrue (Lex.sep _ _)
-  | inr _, inl _ => Decidable.isFalse lex_inr_inl
-  | inr _, inr _ => decidable_of_iff' _ lex_inr_inr
-
-end Lex
-
-end Sum

src/Init/Data/Sum/Lemmas.lean

@@ -1,251 +0,0 @@
-/-
-Copyright (c) 2017 Mario Carneiro. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Yury G. Kudryashov
--/
-prelude
-import Init.Data.Sum.Basic
-import Init.Ext
-
-/-!
-# Disjoint union of types
-
-Theorems about the definitions introduced in `Init.Data.Sum.Basic`.
--/
-
-open Function
-
-namespace Sum
-
-@[simp] protected theorem «forall» {p : α ⊕ β → Prop} :
-    (∀ x, p x) ↔ (∀ a, p (inl a)) ∧ ∀ b, p (inr b) :=
-  ⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨h₁, h₂⟩ => Sum.rec h₁ h₂⟩
-
-@[simp] protected theorem «exists» {p : α ⊕ β → Prop} :
-    (∃ x, p x) ↔ (∃ a, p (inl a)) ∨ ∃ b, p (inr b) :=
-  ⟨ fun
-    | ⟨inl a, h⟩ => Or.inl ⟨a, h⟩
-    | ⟨inr b, h⟩ => Or.inr ⟨b, h⟩,
-    fun
-    | Or.inl ⟨a, h⟩ => ⟨inl a, h⟩
-    | Or.inr ⟨b, h⟩ => ⟨inr b, h⟩⟩
-
-theorem forall_sum {γ : α ⊕ β → Sort _} (p : (∀ ab, γ ab) → Prop) :
-    (∀ fab, p fab) ↔ (∀ fa fb, p (Sum.rec fa fb)) := by
-  refine ⟨fun h fa fb => h _, fun h fab => ?_⟩
-  have h1 : fab = Sum.rec (fun a => fab (Sum.inl a)) (fun b => fab (Sum.inr b)) := by
-    apply funext
-    rintro (_ | _) <;> rfl
-  rw [h1]; exact h _ _
-
-section get
-
-@[simp] theorem inl_getLeft : ∀ (x : α ⊕ β) (h : x.isLeft), inl (x.getLeft h) = x
-  | inl _, _ => rfl
-@[simp] theorem inr_getRight : ∀ (x : α ⊕ β) (h : x.isRight), inr (x.getRight h) = x
-  | inr _, _ => rfl
-
-@[simp] theorem getLeft?_eq_none_iff {x : α ⊕ β} : x.getLeft? = none ↔ x.isRight := by
-  cases x <;> simp only [getLeft?, isRight, eq_self_iff_true, reduceCtorEq]
-
-@[simp] theorem getRight?_eq_none_iff {x : α ⊕ β} : x.getRight? = none ↔ x.isLeft := by
-  cases x <;> simp only [getRight?, isLeft, eq_self_iff_true, reduceCtorEq]
-
-theorem eq_left_getLeft_of_isLeft : ∀ {x : α ⊕ β} (h : x.isLeft), x = inl (x.getLeft h)
-  | inl _, _ => rfl
-
-@[simp] theorem getLeft_eq_iff (h : x.isLeft) : x.getLeft h = a ↔ x = inl a := by
-  cases x <;> simp at h ⊢
-
-theorem eq_right_getRight_of_isRight : ∀ {x : α ⊕ β} (h : x.isRight), x = inr (x.getRight h)
-  | inr _, _ => rfl
-
-@[simp] theorem getRight_eq_iff (h : x.isRight) : x.getRight h = b ↔ x = inr b := by
-  cases x <;> simp at h ⊢
-
-@[simp] theorem getLeft?_eq_some_iff : x.getLeft? = some a ↔ x = inl a := by
-  cases x <;> simp only [getLeft?, Option.some.injEq, inl.injEq, reduceCtorEq]
-
-@[simp] theorem getRight?_eq_some_iff : x.getRight? = some b ↔ x = inr b := by
-  cases x <;> simp only [getRight?, Option.some.injEq, inr.injEq, reduceCtorEq]
-
-@[simp] theorem bnot_isLeft (x : α ⊕ β) : !x.isLeft = x.isRight := by cases x <;> rfl
-
-@[simp] theorem isLeft_eq_false {x : α ⊕ β} : x.isLeft = false ↔ x.isRight := by cases x <;> simp
-
-theorem not_isLeft {x : α ⊕ β} : ¬x.isLeft ↔ x.isRight := by simp
-
-@[simp] theorem bnot_isRight (x : α ⊕ β) : !x.isRight = x.isLeft := by cases x <;> rfl
-
-@[simp] theorem isRight_eq_false {x : α ⊕ β} : x.isRight = false ↔ x.isLeft := by cases x <;> simp
-
-theorem not_isRight {x : α ⊕ β} : ¬x.isRight ↔ x.isLeft := by simp
-
-theorem isLeft_iff : x.isLeft ↔ ∃ y, x = Sum.inl y := by cases x <;> simp
-
-theorem isRight_iff : x.isRight ↔ ∃ y, x = Sum.inr y := by cases x <;> simp
-
-end get
-
-theorem inl.inj_iff : (inl a : α ⊕ β) = inl b ↔ a = b := ⟨inl.inj, congrArg _⟩
-
-theorem inr.inj_iff : (inr a : α ⊕ β) = inr b ↔ a = b := ⟨inr.inj, congrArg _⟩
-
-theorem inl_ne_inr : inl a ≠ inr b := nofun
-
-theorem inr_ne_inl : inr b ≠ inl a := nofun
-
-/-! ### `Sum.elim` -/
-
-@[simp] theorem elim_comp_inl (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inl = f :=
-  rfl
-
-@[simp] theorem elim_comp_inr (f : α → γ) (g : β → γ) : Sum.elim f g ∘ inr = g :=
-  rfl
-
-@[simp] theorem elim_inl_inr : @Sum.elim α β _ inl inr = id :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-theorem comp_elim (f : γ → δ) (g : α → γ) (h : β → γ) :
-    f ∘ Sum.elim g h = Sum.elim (f ∘ g) (f ∘ h) :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-@[simp] theorem elim_comp_inl_inr (f : α ⊕ β → γ) :
-    Sum.elim (f ∘ inl) (f ∘ inr) = f :=
-  funext fun x => Sum.casesOn x (fun _ => rfl) fun _ => rfl
-
-theorem elim_eq_iff {u u' : α → γ} {v v' : β → γ} :
-    Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v' := by
-  simp [funext_iff]
-
-/-! ### `Sum.map` -/
-
-@[simp] theorem map_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
-    ∀ x : Sum α β, (x.map f g).map f' g' = x.map (f' ∘ f) (g' ∘ g)
-  | inl _ => rfl
-  | inr _ => rfl
-
-@[simp] theorem map_comp_map (f' : α' → α'') (g' : β' → β'') (f : α → α') (g : β → β') :
-    Sum.map f' g' ∘ Sum.map f g = Sum.map (f' ∘ f) (g' ∘ g) :=
-  funext <| map_map f' g' f g
-
-@[simp] theorem map_id_id : Sum.map (@id α) (@id β) = id :=
-  funext fun x => Sum.recOn x (fun _ => rfl) fun _ => rfl
-
-theorem elim_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} {x} :
-    Sum.elim f₂ g₂ (Sum.map f₁ g₁ x) = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) x := by
-  cases x <;> rfl
-
-theorem elim_comp_map {f₁ : α → β} {f₂ : β → ε} {g₁ : γ → δ} {g₂ : δ → ε} :
-    Sum.elim f₂ g₂ ∘ Sum.map f₁ g₁ = Sum.elim (f₂ ∘ f₁) (g₂ ∘ g₁) :=
-  funext fun _ => elim_map
-
-@[simp] theorem isLeft_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    isLeft (x.map f g) = isLeft x := by
-  cases x <;> rfl
-
-@[simp] theorem isRight_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    isRight (x.map f g) = isRight x := by
-  cases x <;> rfl
-
-@[simp] theorem getLeft?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    (x.map f g).getLeft? = x.getLeft?.map f := by
-  cases x <;> rfl
-
-@[simp] theorem getRight?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
-    (x.map f g).getRight? = x.getRight?.map g := by cases x <;> rfl
-
-/-! ### `Sum.swap` -/
-
-@[simp] theorem swap_swap (x : α ⊕ β) : swap (swap x) = x := by cases x <;> rfl
-
-@[simp] theorem swap_swap_eq : swap ∘ swap = @id (α ⊕ β) := funext <| swap_swap
-
-@[simp] theorem isLeft_swap (x : α ⊕ β) : x.swap.isLeft = x.isRight := by cases x <;> rfl
-
-@[simp] theorem isRight_swap (x : α ⊕ β) : x.swap.isRight = x.isLeft := by cases x <;> rfl
-
-@[simp] theorem getLeft?_swap (x : α ⊕ β) : x.swap.getLeft? = x.getRight? := by cases x <;> rfl
-
-@[simp] theorem getRight?_swap (x : α ⊕ β) : x.swap.getRight? = x.getLeft? := by cases x <;> rfl
-
-section LiftRel
-
-theorem LiftRel.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b)
-  (h : LiftRel r₁ s₁ x y) : LiftRel r₂ s₂ x y := by
-  cases h
-  · exact LiftRel.inl (hr _ _ ‹_›)
-  · exact LiftRel.inr (hs _ _ ‹_›)
-
-theorem LiftRel.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : LiftRel r₁ s x y) :
-    LiftRel r₂ s x y :=
-  (h.mono hr) fun _ _ => id
-
-theorem LiftRel.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : LiftRel r s₁ x y) :
-    LiftRel r s₂ x y :=
-  h.mono (fun _ _ => id) hs
-
-protected theorem LiftRel.swap (h : LiftRel r s x y) : LiftRel s r x.swap y.swap := by
-  cases h
-  · exact LiftRel.inr ‹_›
-  · exact LiftRel.inl ‹_›
-
-@[simp] theorem liftRel_swap_iff : LiftRel s r x.swap y.swap ↔ LiftRel r s x y :=
-  ⟨fun h => by rw [← swap_swap x, ← swap_swap y]; exact h.swap, LiftRel.swap⟩
-
-end LiftRel
-
-section Lex
-
-protected theorem LiftRel.lex {a b : α ⊕ β} (h : LiftRel r s a b) : Lex r s a b := by
-  cases h
-  · exact Lex.inl ‹_›
-  · exact Lex.inr ‹_›
-
-theorem liftRel_subrelation_lex : Subrelation (LiftRel r s) (Lex r s) := LiftRel.lex
-
-theorem Lex.mono (hr : ∀ a b, r₁ a b → r₂ a b) (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r₁ s₁ x y) :
-    Lex r₂ s₂ x y := by
-  cases h
-  · exact Lex.inl (hr _ _ ‹_›)
-  · exact Lex.inr (hs _ _ ‹_›)
-  · exact Lex.sep _ _
-
-theorem Lex.mono_left (hr : ∀ a b, r₁ a b → r₂ a b) (h : Lex r₁ s x y) : Lex r₂ s x y :=
-  (h.mono hr) fun _ _ => id
-
-theorem Lex.mono_right (hs : ∀ a b, s₁ a b → s₂ a b) (h : Lex r s₁ x y) : Lex r s₂ x y :=
-  h.mono (fun _ _ => id) hs
-
-theorem lex_acc_inl (aca : Acc r a) : Acc (Lex r s) (inl a) := by
-  induction aca with
-  | intro _ _ IH =>
-    constructor
-    intro y h
-    cases h with
-    | inl h' => exact IH _ h'
-
-theorem lex_acc_inr (aca : ∀ a, Acc (Lex r s) (inl a)) {b} (acb : Acc s b) :
-    Acc (Lex r s) (inr b) := by
-  induction acb with
-  | intro _ _ IH =>
-    constructor
-    intro y h
-    cases h with
-    | inr h' => exact IH _ h'
-    | sep => exact aca _
-
-theorem lex_wf (ha : WellFounded r) (hb : WellFounded s) : WellFounded (Lex r s) :=
-  have aca : ∀ a, Acc (Lex r s) (inl a) := fun a => lex_acc_inl (ha.apply a)
-  ⟨fun x => Sum.recOn x aca fun b => lex_acc_inr aca (hb.apply b)⟩
-
-end Lex
-
-theorem elim_const_const (c : γ) :
-    Sum.elim (const _ c : α → γ) (const _ c : β → γ) = const _ c := by
-  apply funext
-  rintro (_ | _) <;> rfl
-
-@[simp] theorem elim_lam_const_lam_const (c : γ) :
-    Sum.elim (fun _ : α => c) (fun _ : β => c) = fun _ => c :=
-  Sum.elim_const_const c

src/Init/PropLemmas.lean

@@ -135,10 +135,6 @@ Both reduce to `b = false ∧ c = false` via `not_or`.
 
 theorem not_and_of_not_or_not (h : ¬a ∨ ¬b) : ¬(a ∧ b) := h.elim (mt (·.1)) (mt (·.2))
 
-/-! ## not equal -/
-
-theorem ne_of_apply_ne {α β : Sort _} (f : α → β) {x y : α} : f x ≠ f y → x ≠ y :=
-  mt <| congrArg _
 
 /-! ## Ite -/
 
@@ -388,17 +384,6 @@ theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' :
 
 end quantifiers
 
-/-! ## membership -/
-
-section Mem
-variable [Membership α β] {s t : β} {a b : α}
-
-theorem ne_of_mem_of_not_mem (h : a ∈ s) : b ∉ s → a ≠ b := mt fun e => e ▸ h
-
-theorem ne_of_mem_of_not_mem' (h : a ∈ s) : a ∉ t → s ≠ t := mt fun e => e ▸ h
-
-end Mem
-
 /-! ## Nonempty -/
 
 @[simp] theorem nonempty_prop {p : Prop} : Nonempty p ↔ p :=

tests/lean/run/nofun1.lean

@@ -1,10 +1,10 @@
-theorem Sum.inl_ne_inr' : inl a ≠ inr b := nofun
+theorem Sum.inl_ne_inr : inl a ≠ inr b := nofun
 
-theorem Sum.inr_ne_inl' : inr b ≠ inl a := nofun
+theorem Sum.inr_ne_inl : inr b ≠ inl a := nofun
 
-theorem Sum.inl_ne_inr'' : inl a ≠ inr b := by nofun
+theorem Sum.inl_ne_inr' : inl a ≠ inr b := by nofun
 
-theorem Sum.inr_ne_inl'' : inr b ≠ inl a := by nofun
+theorem Sum.inr_ne_inl' : inr b ≠ inl a := by nofun
 
 def f (a b : Bool) (_ : Sum.inr b ≠ Sum.inl a) : Nat := 0