how do you make ite/dite compute in tactic mode

Stream: general

[Slavomir Kaslev]

Suppose the context is

a b x : ℕ,
h : x < a
⊢ dite (x < a) (λ (h : x < a), sum.inl ⟨x, h⟩) (λ (h_1 : ¬x < a), sum.inr ⟨x - a, _⟩) = sum.inl ⟨x, h⟩

since we know x < a is true (h), how does one make dite reduce to its "then" value sum.inl ⟨x, h⟩?

[Reid Barton]

The lemma you need is dif_pos.

[Scott Morrison]

(and you can find this by typing library_search)

[Slavomir Kaslev]

That's exactly it. Thank you so much, Reid!

[Yury G. Kudryashov]

If you don't have x < a in the environment, then you can also use split_ifs tactic that will run by_cases on relevant conditions, then simplify using if_pos, if_neg, dif_pos, dif_neg.