Tactic to eliminate `ite`

Stream: general

[Adam Kurkiewicz]

Is there a tactic I can use to eliminate ite, which is used in Mathlib in e.g. Nat.add_div?

More concretely, how can I fill in the sorry?

import Mathlib.Tactic

theorem magic (H : (4 + 6)/2 = 4/2 + 6/2 + if 2 ≤ 4 % 2 + 6 % 2 then 1 else 0) : (4 + 6)/2 = 4/2 + 6/2 := by
  have : ¬ (2 ≤ 4 % 2 + 6 % 2) := by
    intro H
    rw[show 2%2 = 0 by ring] at H
    contradiction
  sorry

#check Nat.add_div

[llllvvuu]

split_ifs at H with h

[Adam Kurkiewicz]

Thank you! I was going nuts here. I'll try to add this to the docs.

[llllvvuu]

More concretely, how can I fill in the sorry?

theorem magic (H : (4 + 6)/2 = 4/2 + 6/2 + if 2 ≤ 4 % 2 + 6 % 2 then 1 else 0) : (4 + 6)/2 = 4/2 + 6/2 :=
  rfl

[Edward van de Meent]

also, lemmas like docs#if_pos and docs#if_neg exist, which are useful if you already have a proof of the condition or its negation

[Adam Kurkiewicz]

Thank you @Edward van de Meent , super helpful!