Zulip Chat Archive
Stream: new members
Topic: using ite functions in a proof
Vivek Rajesh Joshi (May 13 2024 at 17:47):
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 (May 13 2024 at 17:51):
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 (May 13 2024 at 17:58):
Is there a way to name the hypothesis that comes out of a split
?
Yury G. Kudryashov (May 13 2024 at 17:58):
split_ifs with h
Vivek Rajesh Joshi (May 13 2024 at 17:58):
Got it, thanks!
Joachim Breitner (May 13 2024 at 18:00):
I also use
split
next h => …
next h => …
especially if you are constrained to Lean core tactics.
Last updated: May 02 2025 at 03:31 UTC