rcases can't use rfl on 0 = a in some circumstances.

[kim-em]

import Std.Tactic.RCases

variable {α : Type _} [LT α] (a : α)

theorem lt_trichotomy (a b : α) : a < b ∨ a = b ∨ b < a := sorry

example : True := by
  rcases lt_trichotomy 0 a with (ha | rfl | ha)

Fails with
tactic 'subst' failed, 'a' occurs at 0

This breaks a proof from Algebra.Order.Ring.Defs, leanprover-community/mathlib4#905.

[digama0]

This should be fixed in subst; both versions of rcases are just calling the subst tactic so probably you can make a repro that uses only that.

[kim-em]

I guess this is a repro:

theorem foo [OfNat α 0] (a : α) : a = 0 := sorry

example (a : α) [OfNat α 0] : True := by
  let t := @foo _ ?_ a
  subst t -- fails with `'a' occurs at 0`
  
example (a : α) [OfNat α 0] : True := by
  let t := foo a
  subst t  

[kim-em]

The problem here is that substCore calls exprDependsOn, which is conservative, and looks for any metavariables which could possibly result in a dependency.

[kim-em]

I think https://github.com/leanprover/lean4/compare/master...semorrison:lean4:subst_less_conservative?expand=1 would solve the problem.

[kim-em]

Per mathlib porting meeting discussion, it seems rcases should be synthesizing instances here.

[fgdorais]

Is this still an issue?