Zulip Chat Archive

Stream: lean4

Topic: Handling `ite`s


Marcus Rossel (Aug 24 2021 at 10:31):

How can I split on an ite in Lean 4?
I have an assumption h : if x then y else z and would like to split into two subgoals.

Scott Morrison (Aug 24 2021 at 11:15):

import Mathlib.Tactic.Basic

example (P : Prop) [Decidable P] : (if P then 0 else 0) = 0 := by
  by_cases P
  rw [if_pos h]
  rw [if_neg h]

Scott Morrison (Aug 24 2021 at 11:16):

(I'd like to port split_ifs soonish.)

Scott Morrison (Aug 24 2021 at 11:21):

You can rw [if_pos h] at w to resolve an if in a hypothesis, of course.


Last updated: Dec 20 2023 at 11:08 UTC