fix: avoid recursion in invariant side conditions

[n33levo]

Description

trivial tries apply_rfl, which treats ⊆ as a reflexive relation and checks whether its operands are definitionally equal. For a concrete namespace, that check unfolded nclose through Pos.flatten and CoPset.suffixesRaw until Lean reached its recursion limit.

This marks nclose irreducible after its root computation theorem, keeping that implementation detail out of automatic definitional equality while preserving explicit unfolding with simp [nclose]. The original side-condition tactic order remains unchanged.

The tests cover the direct apply_rfl fallback and the complete iinv flow with ofName `rnd.

Fixes #557

Verification

• cd Iris && lake build --wfail IrisTest
• cd Iris && lake build --wfail
• cd Iris && lake exe check-imports Iris
• cd Iris && lake exe dumpPortingData
• cd IrisMath && lake build --wfail
• cd IrisMath && lake exe check-imports IrisMath
• Porting staleness check: No stale entries.
• git diff --check

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[MackieLoeffel]

My hope was that we would be able to fix #557 by finding out what causes the recursion limit and then fixing the root cause instead of just reordering the tactics.

[n33levo]

My hope was that we would be able to fix #557 by finding out what causes the recursion limit and then fixing the root cause instead of just reordering the tactics.

that actually makes more sense, thanks for pointing out, anyway I think we can fix the root case by making nclose irreducible, it should avoid problematic unfolding now. Tested it locally with the initial tatic order, things are passing now

[MackieLoeffel]

Thanks for finding the root cause of this! I made a cleanup pass over the PR and used it as an opportunity to use iinv more often. This is ready to be merged now.

[markusdemedeiros]

Awesome! This also fixed a recursion error in #608