`contradiction` tries to make use of constructor disjunction for proof equalities

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed
• Reduce the issue to a minimal, self-contained, reproducible test case.
• Test your test case against the latest nightly release.

Description

If there is an equality of proofs in context, where the proofs use different constructors, contradiction will try reasoning using noConfusion, leading to a kernel typechecking error.

Context

Reported on Zulip.

Steps to Reproduce

With the following:

example : False := by
  have : Or.inl trivial = Or.inr trivial := rfl
  contradiction

Expected behavior: contradiction should fail to find a contradiction

Actual behavior: contradiction succeeds, but then there is a "(kernel) unknown constant 'Or.noConfusion'" error.

Versions

Lean 4.16.0-nightly-2025-01-02
Target: x86_64-unknown-linux-gnu

Additional Information

Perhaps other "no-confusion-like" tactics should be audited for similar errors.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal example from the issue against the stated nightly version, then trace the contradiction tactic's handling of proof equalities and its noConfusion path. Done means the example fails to find a contradiction without producing a kernel unknown-constant error; consider whether related no-confusion-like paths show the same problem.