From 36cc7c23b6ade3ef787c1adbf8e1b6dbb08884de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Nov 2022 06:14:19 -0800
Subject: [PATCH] fix: fixes #1886

---
 src/Lean/Elab/Tactic/Injection.lean             | 12 ++++++++++--
 tests/lean/run/1886.lean                        |  5 +++++
 tests/lean/run/autoboundIssues.lean             |  4 ++--
 tests/lean/run/concatElim.lean                  |  4 ++--
 tests/lean/run/inj1.lean                        | 17 +++++++----------
 tests/lean/run/inj2.lean                        | 10 ++++------
 tests/lean/run/injIssue.lean                    |  4 ++--
 tests/lean/run/injective.lean                   |  2 +-
 .../run/multiTargetCasesInductionIssue.lean     |  2 +-
 tests/lean/run/subtype_inj.lean                 |  1 -
 tests/lean/smartUnfolding.lean                  |  4 +---
 tests/lean/smartUnfolding.lean.expected.out     |  3 ---
 12 files changed, 35 insertions(+), 33 deletions(-)
 create mode 100644 tests/lean/run/1886.lean

diff --git a/src/Lean/Elab/Tactic/Injection.lean b/src/Lean/Elab/Tactic/Injection.lean
index eaaf69bd21..7f6fe14757 100644
--- a/src/Lean/Elab/Tactic/Injection.lean
+++ b/src/Lean/Elab/Tactic/Injection.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.Injection
+import Lean.Meta.Tactic.Assumption
 import Lean.Elab.Tactic.ElabTerm
 namespace Lean.Elab.Tactic
 
@@ -18,6 +19,13 @@ private def checkUnusedIds (tacticName : Name) (mvarId : MVarId) (unusedIds : Li
   unless unusedIds.isEmpty do
     Meta.throwTacticEx tacticName mvarId m!"too many identifiers provided, unused: {unusedIds}"
 
+-- TODO: move to a different place?
+private def tryAssumption (mvarId : MVarId) : MetaM (List MVarId) := do
+  if (← mvarId.assumptionCore) then
+    return []
+  else
+    return [mvarId]
+
 @[builtin_tactic «injection»] def evalInjection : Tactic := fun stx => do
   -- leading_parser nonReservedSymbol "injection " >> termParser >> withIds
   let fvarId ← elabAsFVar stx[1]
@@ -25,13 +33,13 @@ private def checkUnusedIds (tacticName : Name) (mvarId : MVarId) (unusedIds : Li
   liftMetaTactic fun mvarId => do
     match (← Meta.injection mvarId fvarId ids) with
     | .solved                      => checkUnusedIds `injection mvarId ids; return []
-    | .subgoal mvarId' _ unusedIds => checkUnusedIds `injection mvarId unusedIds; return [mvarId']
+    | .subgoal mvarId' _ unusedIds => checkUnusedIds `injection mvarId unusedIds; tryAssumption mvarId'
 
 @[builtin_tactic «injections»] def evalInjections : Tactic := fun stx => do
   let ids := stx[1].getArgs.toList.map getNameOfIdent'
   liftMetaTactic fun mvarId => do
     match (← Meta.injections mvarId ids) with
     | .solved                    => checkUnusedIds `injections mvarId ids; return []
-    | .subgoal mvarId' unusedIds => checkUnusedIds `injections mvarId unusedIds; return [mvarId']
+    | .subgoal mvarId' unusedIds => checkUnusedIds `injections mvarId unusedIds; tryAssumption mvarId'
 
 end Lean.Elab.Tactic
diff --git a/tests/lean/run/1886.lean b/tests/lean/run/1886.lean
new file mode 100644
index 0000000000..d26d74ed77
--- /dev/null
+++ b/tests/lean/run/1886.lean
@@ -0,0 +1,5 @@
+structure U (α : Type) where
+  a : α
+
+theorem mk_inj (w : U.mk a = U.mk b) : a = b := by
+  injection w
diff --git a/tests/lean/run/autoboundIssues.lean b/tests/lean/run/autoboundIssues.lean
index 1e88b98747..95d1233f96 100644
--- a/tests/lean/run/autoboundIssues.lean
+++ b/tests/lean/run/autoboundIssues.lean
@@ -1,8 +1,8 @@
 example : n.succ = 1 → n = 0 := by
-  intros h; injection h; assumption
+  intros h; injection h
 
 example (h : n.succ = 1) : n = 0 := by
-  injection h; assumption
+  injection h
 
 opaque T : Type
 opaque T.Pred : T → T → Prop
diff --git a/tests/lean/run/concatElim.lean b/tests/lean/run/concatElim.lean
index 2d135a8a7d..b04e39d0ee 100644
--- a/tests/lean/run/concatElim.lean
+++ b/tests/lean/run/concatElim.lean
@@ -35,7 +35,7 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro
   | [a]   =>
     intro n h
     have : 1 = n + 1 := h
-    have : 0 = n := by injection this; assumption
+    have : 0 = n := by injection this
     subst this
     rfl
   | x₁::x₂::xs =>
@@ -46,7 +46,7 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro
       injection h
     | succ n =>
       have : (x₁ :: x₂ :: xs).length = xs.length + 2 := by simp [lengthCons]
-      have : xs.length = n := by rw [this] at h; injection h with h; injection h with h; assumption
+      have : xs.length = n := by rw [this] at h; injection h with h; injection h
       simp [dropLast, lengthCons, dropLastLen (x₂::xs) xs.length (lengthCons ..), this]
 
 @[inline]
diff --git a/tests/lean/run/inj1.lean b/tests/lean/run/inj1.lean
index 413063df6a..f6799b1ac9 100644
--- a/tests/lean/run/inj1.lean
+++ b/tests/lean/run/inj1.lean
@@ -1,28 +1,25 @@
-
-
 theorem test1 {α} (a b : α) (as bs : List α) (h : a::as = b::bs) : a = b :=
 by {
-  injection h;
-  assumption;
+  injection h
 }
 
-theorem test2 {α} (a b : α) (as bs : List α) (h : a::as = b::bs) : a = b :=
+theorem test2 {α} (a b : α) (f : α → α) (as bs : List α) (h : a::as = b::bs) : f a = f b :=
 by {
   injection h with h1 h2;
-  exact h1
+  rw [h1]
 }
 
-theorem test3 {α} (a b : α) (as bs : List α) (h : (x : List α) → (y : List α) → x = y) : as = bs :=
+theorem test3 {α} (a b : α) (f : List α → List α) (as bs : List α) (h : (x : List α) → (y : List α) → x = y) : f as = f bs :=
 have : a::as = b::bs := h (a::as) (b::bs);
 by {
   injection this with h1 h2;
-  exact h2
+  rw [h2]
 }
 
-theorem test4 {α} (a b : α) (as bs : List α) (h : (x : List α) → (y : List α) → x = y) : as = bs :=
+theorem test4 {α} (a b : α) (f : List α → List α) (as bs : List α) (h : (x : List α) → (y : List α) → x = y) : f as = f bs :=
 by {
   injection h (a::as) (b::bs) with h1 h2;
-  exact h2
+  rw [h2]
 }
 
 theorem test5 {α} (a : α) (as : List α) (h : a::as = []) : 0 > 1 :=
diff --git a/tests/lean/run/inj2.lean b/tests/lean/run/inj2.lean
index 6359d09a2b..0c4e57d3bd 100644
--- a/tests/lean/run/inj2.lean
+++ b/tests/lean/run/inj2.lean
@@ -10,20 +10,18 @@ inductive Fin2 : Nat → Type
 
 theorem test1 {α β} {n} (a₁ a₂ : α) (b₁ b₂ : β) (v w : Vec2 α β n) (h : Vec2.cons a₁ b₁ v = Vec2.cons a₂ b₂ w) : a₁ = a₂ :=
 by {
-  injection h;
-  assumption
+  injection h
 }
 
 theorem test2 {α β} {n} (a₁ a₂ : α) (b₁ b₂ : β) (v w : Vec2 α β n) (h : Vec2.cons a₁ b₁ v = Vec2.cons a₂ b₂ w) : v = w :=
 by {
-  injection h with h1 h2 h3 h4;
-  assumption
+  injection h with h1 h2 h3 h4
 }
 
-theorem test3 {α β} {n} (a₁ a₂ : α) (b₁ b₂ : β) (v w : Vec2 α β n) (h : Vec2.cons a₁ b₁ v = Vec2.cons a₂ b₂ w) : v = w :=
+theorem test3 {α β} {n} (a₁ a₂ : α) (b₁ b₂ : β) (v w : Vec2 α β n) (f : Vec2 α β n → Nat) (h : Vec2.cons a₁ b₁ v = Vec2.cons a₂ b₂ w) : f v = f w :=
 by {
   injection h with _ _ _ h4;
-  exact h4
+  rw [h4]
 }
 
 theorem test4 {α} (v : Fin2 0) : α :=
diff --git a/tests/lean/run/injIssue.lean b/tests/lean/run/injIssue.lean
index ec0a95f0c7..f9cd6c2dfe 100644
--- a/tests/lean/run/injIssue.lean
+++ b/tests/lean/run/injIssue.lean
@@ -1,4 +1,4 @@
-theorem ex1 (n m : Nat) : some n = some m → n = m := by
+theorem ex1 (n m : Nat) (f : Nat → Nat) : some n = some m → f n = f m := by
   intro h
   injection h with h
-  exact h
+  rw [h]
diff --git a/tests/lean/run/injective.lean b/tests/lean/run/injective.lean
index cf04c92697..02c900cb78 100644
--- a/tests/lean/run/injective.lean
+++ b/tests/lean/run/injective.lean
@@ -6,7 +6,7 @@ structure InjectiveFunction (α : Type u) (β : Type v) where
 
 def add1 : InjectiveFunction Nat Nat where
   fn a      := a + 1
-  inj a b h := by injection h; assumption
+  inj a b h := by injection h
 
 instance : CoeFun (InjectiveFunction α β) (fun _ => α → β) where
   coe s := s.fn
diff --git a/tests/lean/run/multiTargetCasesInductionIssue.lean b/tests/lean/run/multiTargetCasesInductionIssue.lean
index 507d9919bc..a4a067bbd2 100644
--- a/tests/lean/run/multiTargetCasesInductionIssue.lean
+++ b/tests/lean/run/multiTargetCasesInductionIssue.lean
@@ -15,7 +15,7 @@ def Vec.casesOn
     match n, as, h with
     | 0,   [],    _ => nil
     | n+1, a::as, h =>
-      have : as.length = n := by injection h; assumption
+      have : as.length = n := by injection h
       have ih : motive n ⟨as, this⟩ := go n as this
       cons n a ⟨as, this⟩ ih
   match as with
diff --git a/tests/lean/run/subtype_inj.lean b/tests/lean/run/subtype_inj.lean
index 28582904d8..6971105d95 100644
--- a/tests/lean/run/subtype_inj.lean
+++ b/tests/lean/run/subtype_inj.lean
@@ -1,4 +1,3 @@
 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
diff --git a/tests/lean/smartUnfolding.lean b/tests/lean/smartUnfolding.lean
index 243a863d2d..0f8029133c 100644
--- a/tests/lean/smartUnfolding.lean
+++ b/tests/lean/smartUnfolding.lean
@@ -1,6 +1,4 @@
 theorem ex1 (x y : Nat) (h : x + 2 = y + 2) : x = y := by
   injection h with h
   trace_state -- without smart unfolding the state would be a mess
-  injection h with h
-  trace_state -- without smart unfolding the state would be a mess
-  assumption
+  injection h
diff --git a/tests/lean/smartUnfolding.lean.expected.out b/tests/lean/smartUnfolding.lean.expected.out
index f7e5657466..5f115edef9 100644
--- a/tests/lean/smartUnfolding.lean.expected.out
+++ b/tests/lean/smartUnfolding.lean.expected.out
@@ -1,6 +1,3 @@
 x y : Nat
 h : Nat.add x 1 = Nat.add y 1
 ⊢ x = y
-x y : Nat
-h : Nat.add x 0 = Nat.add y 0
-⊢ x = y