refactor: simplify some nomatch with nofun (#3564)

and also don’t wrap `nomatch` with `False.elim`; it is not necessary, as
`nomatch` already inhabits any type.

src/Init/Data/List/Basic.lean

@@ -727,9 +727,9 @@ inductive lt [LT α] : List α → List α → Prop where
 instance [LT α] : LT (List α) := ⟨List.lt⟩
 
 instance hasDecidableLt [LT α] [h : DecidableRel (α:=α) (·<·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂)
-  | [],    []    => isFalse (fun h => nomatch h)
+  | [],    []    => isFalse nofun
   | [],    _::_  => isTrue (List.lt.nil _ _)
-  | _::_, []     => isFalse (fun h => nomatch h)
+  | _::_, []     => isFalse nofun
   | a::as, b::bs =>
     match h a b with
     | isTrue h₁  => isTrue (List.lt.head _ _ h₁)

src/Init/Prelude.lean

@@ -1635,8 +1635,8 @@ instance : LT Nat where
   lt := Nat.lt
 
 theorem Nat.not_succ_le_zero : ∀ (n : Nat), LE.le (succ n) 0 → False
-  | 0,      h => nomatch h
-  | succ _, h => nomatch h
+  | 0      => nofun
+  | succ _ => nofun
 
 theorem Nat.not_lt_zero (n : Nat) : Not (LT.lt n 0) :=
   not_succ_le_zero n

src/Lean/Data/PersistentHashMap.lean

@@ -84,14 +84,14 @@ partial def insertAtCollisionNodeAux [BEq α] : CollisionNode α β → Nat →
       else insertAtCollisionNodeAux n (i+1) k v
     else
       ⟨Node.collision (keys.push k) (vals.push v) (size_push heq k v), IsCollisionNode.mk _ _ _⟩
-  | ⟨Node.entries _, h⟩, _, _, _ => False.elim (nomatch h)
+  | ⟨Node.entries _, h⟩, _, _, _ => nomatch h
 
 def insertAtCollisionNode [BEq α] : CollisionNode α β → α → β → CollisionNode α β :=
   fun n k v => insertAtCollisionNodeAux n 0 k v
 
 def getCollisionNodeSize : CollisionNode α β → Nat
   | ⟨Node.collision keys _ _, _⟩ => keys.size
-  | ⟨Node.entries _, h⟩          => False.elim (nomatch h)
+  | ⟨Node.entries _, h⟩          => nomatch h
 
 def mkCollisionNode (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) : Node α β :=
   let ks : Array α := Array.mkEmpty maxCollisions
@@ -105,7 +105,7 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize
     let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v
     if depth >= maxDepth || getCollisionNodeSize newNode < maxCollisions then newNode.val
     else match newNode with
-      | ⟨Node.entries _, h⟩ => False.elim (nomatch h)
+      | ⟨Node.entries _, h⟩ => nomatch h
       | ⟨Node.collision keys vals heq, _⟩ =>
         let rec traverse (i : Nat) (entries : Node α β) : Node α β :=
           if h : i < keys.size then

src/Lean/Syntax.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Sebastian Ullrich, Leonardo de Moura
 -/
 prelude
-import Init.Data.Range 
+import Init.Data.Range
 import Init.Data.Hashable
 import Lean.Data.Name
 import Lean.Data.Format
@@ -37,9 +37,9 @@ inductive IsNode : Syntax → Prop where
 
 def SyntaxNode : Type := {s : Syntax // IsNode s }
 
-def unreachIsNodeMissing {β} (h : IsNode Syntax.missing) : β := False.elim (nomatch h)
-def unreachIsNodeAtom {β} {info val} (h : IsNode (Syntax.atom info val)) : β := False.elim (nomatch h)
-def unreachIsNodeIdent {β info rawVal val preresolved} (h : IsNode (Syntax.ident info rawVal val preresolved)) : β := False.elim (nomatch h)
+def unreachIsNodeMissing {β} : IsNode Syntax.missing → β := nofun
+def unreachIsNodeAtom {β} {info val} : IsNode (Syntax.atom info val) → β := nofun
+def unreachIsNodeIdent {β info rawVal val preresolved} : IsNode (Syntax.ident info rawVal val preresolved) → β := nofun
 
 def isLitKind (k : SyntaxNodeKind) : Bool :=
   k == strLitKind || k == numLitKind || k == charLitKind || k == nameLitKind || k == scientificLitKind