From 6bc5433b17ee269265aab3adad83dbdbbb80f198 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 Apr 2022 16:56:03 -0700
Subject: [PATCH] fix: add support for heterogeneous equality at
 `processGenDiseq`

---
 src/Lean/Meta/Tactic/Contradiction.lean |  7 +++++--
 tests/lean/run/matchEqnsHEqIssue.lean   | 24 ++++++++++++++++++++++++
 2 files changed, 29 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/matchEqnsHEqIssue.lean

diff --git a/src/Lean/Meta/Tactic/Contradiction.lean b/src/Lean/Meta/Tactic/Contradiction.lean
index b72a4ffbefd..9d7b1eb1d5c 100644
--- a/src/Lean/Meta/Tactic/Contradiction.lean
+++ b/src/Lean/Meta/Tactic/Contradiction.lean
@@ -87,7 +87,7 @@ private def elimEmptyInductive (mvarId : MVarId) (fvarId : FVarId) (fuel : Nat)
 /-- Return true if `e` is of the form `(x : α) → ... → s = t → ... → False` -/
 private def isGenDiseq (e : Expr) : Bool :=
   match e with
-  | Expr.forallE _ d b _ => (d.isEq || b.hasLooseBVar 0) && isGenDiseq b
+  | Expr.forallE _ d b _ => (d.isEq || d.isHEq || b.hasLooseBVar 0) && isGenDiseq b
   | _ => e.isConstOf ``False
 
 /--
@@ -101,7 +101,7 @@ private def mkGenDiseqMask (e : Expr) : Array Bool :=
 where
   go (e : Expr) (acc : Array Bool) : Array Bool :=
     match e with
-    | Expr.forallE _ d b _ => go b (acc.push (!b.hasLooseBVar 0 && d.isEq))
+    | Expr.forallE _ d b _ => go b (acc.push (!b.hasLooseBVar 0 && (d.isEq || d.isHEq)))
     | _ => acc
 
 /--
@@ -133,6 +133,9 @@ private def processGenDiseq (mvarId : MVarId) (localDecl : LocalDecl) : MetaM Bo
         if let some (_, lhs, _) ← matchEq? (← inferType arg) then
           unless (← isDefEq arg (← mkEqRefl lhs)) do
             return none
+        if let some (α, lhs, _,  _) ← matchHEq? (← inferType arg) then
+          unless (← isDefEq arg (← mkHEqRefl lhs)) do
+            return none
     let falseProof ← instantiateMVars (mkAppN localDecl.toExpr args)
     if (← hasAssignableMVar falseProof) then
       return none
diff --git a/tests/lean/run/matchEqnsHEqIssue.lean b/tests/lean/run/matchEqnsHEqIssue.lean
new file mode 100644
index 00000000000..603ff6aa746
--- /dev/null
+++ b/tests/lean/run/matchEqnsHEqIssue.lean
@@ -0,0 +1,24 @@
+inductive Ty :=
+| int: Ty
+| other: Ty
+
+inductive Tensor :=
+| int: Int -> Tensor
+| nested: List Tensor -> Tensor
+
+def hasBaseType: Tensor → Ty → Bool
+  | .int _, Ty.int      => true
+  | .int _, Ty.other    => true
+  | .nested _, _        => true
+
+def flatten (e: Tensor) (τ: Ty) (h: hasBaseType e τ): List Int :=
+  match e, τ with
+  | .int _, Ty.int     => []
+  | .int _, _          => []
+  | .nested [], _      => []
+  | .nested (_::_), _  => []
+
+theorem flatten_list (l: List Tensor) τ (h: hasBaseType (.nested l) τ):
+    flatten (.nested l) τ h = [] := by
+  simp [flatten]
+  repeat sorry