isDefEq causes maximum recursion depth has been reached

[Qiu233]

Description

This bug extremely rarely arises when working with metaprogramming.
The following is the only case it's encountered.

Though mathlib is involved, I don't think it can ever fix a function from standard library, so I put the issue here.

Steps to Reproduce

import Mathlib

example := by
  let S := Finset.range 10000
  let P := ∏ a ∈ S, a
  have t : P = (∏ a ∈ S, a) := by rfl
  have : (?a : Finset ℕ) = ?b := by
    exact t

example := by
  let S := Finset.range 10000
  let P := ∏ a ∈ S, a
  have t : P = (∏ a ∈ S, a) := by rfl
  have : @Eq (Finset ℕ) ?a ?b := by
    exact t

Expected behavior: No error.

Actual behavior: Error maximum recursion depth has been reached throws on the exacts.

Versions

• 4.9.0
• 4.11.0-rc2
• latest version test now going on