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

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

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 3d1f9bda33..c2d345489d 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -315,7 +315,8 @@ theorem Iff.comm : (a ↔ b) ↔ (b ↔ a) :=
 
 theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop}
    (h₁ : Exists (fun x => p x)) (h₂ : ∀ (a : α), p a → b) : b :=
-  h₂ h₁.1 h₁.2
+  match h₁ with
+  | intro a h => h₂ a h
 
 /- Decidable -/