fix: add support for heterogeneous equality at processGenDiseq

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

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