From b7a0bdb9c9ba6adade3650c560435031b5cdfa99 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 30 Jan 2021 11:58:56 -0800
Subject: [PATCH] fix: `Injection.lean`

---
 src/Lean/Meta/Tactic/Injection.lean | 12 +++++++++++-
 tests/lean/run/subtype_inj.lean     |  4 ++++
 2 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/subtype_inj.lean

diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean
index 32ae02f435..89f4fbdcb5 100644
--- a/src/Lean/Meta/Tactic/Injection.lean
+++ b/src/Lean/Meta/Tactic/Injection.lean
@@ -10,6 +10,14 @@ import Lean.Meta.Tactic.Intro
 
 namespace Lean.Meta
 
+def getCtorNumPropFields (ctorInfo : ConstructorVal) : MetaM Nat := do
+  forallTelescopeReducing ctorInfo.type fun xs _ => do
+    let mut numProps := 0
+    for i in [:ctorInfo.numFields] do
+      if (← isProp (← inferType xs[ctorInfo.numParams + i])) then
+        numProps := numProps + 1
+    return numProps
+
 inductive InjectionResultCore where
   | solved
   | subgoal (mvarId : MVarId) (numNewEqs : Nat)
@@ -42,7 +50,9 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor
             let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag
             assignExprMVar mvarId (mkApp val newMVar)
             let mvarId ← tryClear newMVar.mvarId! fvarId
-            pure $ InjectionResultCore.subgoal mvarId aCtor.numFields
+            /- Recall that `noConfusion` does not include equalities for propositions since they are trivial due to proof irrelevance. -/
+            let numPropFields ← getCtorNumPropFields aCtor
+            return InjectionResultCore.subgoal mvarId (aCtor.numFields - numPropFields)
           | _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction"
       | _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected"
 
diff --git a/tests/lean/run/subtype_inj.lean b/tests/lean/run/subtype_inj.lean
new file mode 100644
index 0000000000..28582904d8
--- /dev/null
+++ b/tests/lean/run/subtype_inj.lean
@@ -0,0 +1,4 @@
+theorem subtype_inj (A: Type) (p: A → Prop) (a b: A) (pa: p a) (pb: p b) : (⟨a, pa⟩: {a//p a}) = (⟨b, pb⟩: {b//p b}) → a = b := by
+  intro eq
+  injection eq
+  assumption