obtain to massage syntactic equality

Stream: mathlib4

[Heather Macbeth]

One feature of mathlib3 obtain was that it could change the type of a term to something defeq, using a type annotation:

import tactic.rcases
import init.data.nat.lemmas

example {a : nat} : false :=
begin
  obtain ha1 | ha2 : a ≤ 2 ∨ 3 ≤ a := le_or_lt a 2,
  { sorry },
  { -- `ha2` has type `3 ≤ a`
    sorry }
end

It seems that std4 obtain has lost this:

import Std.Tactic.RCases
import Mathlib.Init.Data.Nat.Lemmas

example {a : Nat} : False := by
  obtain ha1 | ha2 : a ≤ 2 ∨ 3 ≤ a := le_or_lt a 2
  · sorry
  · -- `ha2` has type `2 < a`
    sorry

Would it be difficult to port this useful feature?

[Mario Carneiro]

Hm, this std MWE does not show the same behavior:

import Std.Tactic.RCases
import Std.Data.Nat.Lemmas

example {a : Nat} : False := by
  obtain ha1 | ha2 : a ≤ 2 ∨ 3 ≤ a := Decidable.or_iff_not_imp_left.2 (@Nat.not_le a 2).1

case inl
a: Nat
ha1: a ≤ 2
⊢ False
case inr
a: Nat
ha2: 3 ≤ a
⊢ False

[Mario Carneiro]

FTR this is already supposed to be implemented

[Mario Carneiro]

fixed on master