`isDefEq` causes maximum recursion depth has been reached when given type argument mismatched

Description

This bug only occurs when using big operator.

If S is given by axiom S : Finset ℕ rather than in the context, the bug disappears.
If P is defined not using ∏, the bug disappears.

Steps to Reproduce

import Mathlib

lemma card {a b : Finset α} : a = b → a.card = b.card := congrArg _

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

Expected behavior: No error or should have been caught.

Actual behavior: Error on card t.

Versions

• 4.9.0
• 4.11.0-rc2
• 4.16.0-rc1

Context

Code like card t above is generated (by meta-programming) to test whether lemmas like card can be applied to some term so we get new facts.
What we want is to recover if test fails, but unfortunately it crashes our meta-program.

This bug occurs only once in millions of such tests. No other similar case found yet, so it might be not vital.

Start by running the provided Mathlib reproducer on the listed Lean versions and trace the isDefEq call reached by card t, especially with the locally defined S and product P. Compare the behavior with the stated cases where S is an axiom or P does not use ∏; done means the mismatch no longer reaches maximum recursion depth and the generated meta-program can recover from the failed test.