Applying hypotheses to if then else

Stream: mathlib4

[Connor Gordon]

I have (perhaps unwisely) defined certain functions via if-then-else, and am now trying to prove things about them. The split tactic has been useful at times, but sometimes it unpacks too much. More specifically, if I have something of the form if p then q else r and a hypothesis that states that p is true, is there a way to simplify this to just q (or similarly, if I have that p is false, can I simplify to r?)

You can see the relevant part in MWE.lean. I am also open to suggestions for better ways to write what I am trying to define here (namely, I have a series of covers indexed by sets, where two sets in particular are special and need to be handled individually).

[Yaël Dillies]

Yes, there is the lemma docs#if_pos (or docs#dif_pos if it's dependent)

[Connor Gordon]

That works! Or well, it mostly works, for whatever reason I am now having a rw[if_neg] that is timing out. Any idea why that might be? Here's a new MWE.lean

[Kyle Miller]

You can usually do simp [h] if h : p is your hypothesis. (And you can use simp? [h] to see what lemma it's invoking.)

This is how you can pass in additional hypotheses to dispatch side conditions for simp lemmas.

[Joachim Breitner]

You can also try

 simp only [h, ↓reduceIte]

(On the phone right now).

I wonder if there should be a tactic for “very careful evaluating” for cleaning up after if and case splits like these, and possibly have such tactics run them implicitly.

[Kevin Buzzard]

Connor Gordon said:

That works! Or well, it mostly works, for whatever reason I am now having a rw[if_neg] that is timing out. Any idea why that might be? Here's a new MWE.lean

There's no timeout for me. Are you on an old mathlib?