issue !4#11043: Porting note: was `decide!`

Stream: triage

[Random Issue Bot]

Today I chose issue 11043 for discussion!

Porting note: was decide!
Created by @Pietro Monticone (@pitmonticone) on 2024-02-28
Labels: porting-notes

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kyle Miller]

lean4#5999 should address this. It adds decide +revert to revert the free variables that the goal depends on, after cleaning up everything that the goal doesn't depend on. It leaves in propositional hypotheses that depend on these free variables. For example:

example (x : Nat) (h : x < 5) : x + 1 ≤ 5 := by decide +revert