From e08d35cea1893fac25c684036fead96b5ae47b10 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 15 Dec 2024 01:21:15 +0100
Subject: [PATCH] fix: type incorrect term produced by `contradiction` (#6387)

This PR fixes a type error in the proof generated by the `contradiction`
tactic.

closes #4851
---
 src/Lean/Meta/Tactic/Contradiction.lean | 3 ++-
 tests/lean/run/4851.lean                | 2 ++
 2 files changed, 4 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/4851.lean

diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean
index 4ccbfcba91..534c7a0cb8 100644
--- a/src/Lean/Meta/Tactic/Contradiction.lean
+++ b/src/Lean/Meta/Tactic/Contradiction.lean
@@ -160,7 +160,8 @@ def _root_.Lean.MVarId.contradictionCore (mvarId : MVarId) (config : Contradicti
         -- (h : ¬ p) (h' : p)
         if let some p ← matchNot? localDecl.type then
           if let some pFVarId ← findLocalDeclWithType? p then
-            mvarId.assign (← mkAbsurd (← mvarId.getType) (mkFVar pFVarId) localDecl.toExpr)
+            -- We use `False.elim` because `p`'s type may be Type
+            mvarId.assign (← mkFalseElim (← mvarId.getType) (mkApp localDecl.toExpr (mkFVar pFVarId)))
             return true
         -- (h : x ≠ x)
         if let some (_, lhs, rhs) ← matchNe? localDecl.type then
diff --git a/tests/lean/run/4851.lean b/tests/lean/run/4851.lean
new file mode 100644
index 0000000000..033b794092
--- /dev/null
+++ b/tests/lean/run/4851.lean
@@ -0,0 +1,2 @@
+theorem T0 (α : Type) (x : α) (H: α → False) : False := by
+  contradiction