using ite functions in a proof

Stream: new members

[Vivek Rajesh Joshi]

I want to expand the cases of a function defined in terms of a few nested if-then-else's. Is there a better way to do it than introducing a by_cases hypothesis for every if_else?

[Adam Topaz]

Here are some examples to get you started:

import Mathlib.Tactic

example (n : ℕ) (hn : n = 3) : (if n = 3 then 2 else 0) = 2 := by
  split <;> rfl

example (n : ℕ) (hn : n = 1) : (if n = 3 then 2 else 0) = 0 := by
  split <;> first | rfl | linarith

example (n : ℕ) (hn : n = 3) : (if n = 3 then 2 else 0) = 2 := by
  rw [if_pos hn]

example (n : ℕ) (hn : n = 1) : (if n = 3 then 2 else 0) = 0 := by
  rw [if_neg]
  linarith

[Vivek Rajesh Joshi]

Is there a way to name the hypothesis that comes out of a split?

[Yury G. Kudryashov]

split_ifs with h

[Vivek Rajesh Joshi]

Got it, thanks!

[Joachim Breitner]

I also use

split
next h =>  …
next h =>  …

especially if you are constrained to Lean core tactics.