From c9471ea029a683ccf4dedd92ab37dcb10496dcbb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Feb 2022 07:17:31 -0800
Subject: [PATCH] fix: invalid proof

---
 src/Init/Prelude.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index e8a529dda3..a5b97170c1 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -204,7 +204,8 @@ class inductive Nonempty (α : Sort u) : Prop where
 axiom Classical.choice {α : Sort u} : Nonempty α → α
 
 protected def Nonempty.elim {α : Sort u} {p : Prop} (h₁ : Nonempty α) (h₂ : α → p) : p :=
-  h₂ h₁.1
+  match h₁ with
+  | intro a => h₂ a
 
 instance {α : Sort u} [Inhabited α] : Nonempty α :=
   ⟨default⟩