## Stream: general

### Topic: split_ifs weirdness

#### Reid Barton (Sep 28 2020 at 18:59):

Does anyone understand why split_ifs is producing two copies of 1 = 1 here?

import data.set.basic

open_locale classical

example {X Y : Type*} {f : X → Y} {s : set Y} {x : X} {t : set ℕ}
{k : x ∈ f ⁻¹' s} :
(if h : f x ∈ s then 1 else 0) ∈ t :=
begin
have : (if h : f x ∈ s then 1 else 0) = 1,
{ split_ifs,
refl, refl /- !! -/ },
sorry
end


#### Reid Barton (Sep 28 2020 at 19:00):

There are a couple behaviors I could understand... but this is not one of them

#### Reid Barton (Sep 28 2020 at 19:02):

With trace.simplify.rewrite I can see that dif_pos was applied twice

#### Reid Barton (Sep 28 2020 at 19:03):

while if the hypothesis k is removed then it applies dif_pos once and dif_neg once as expected, and the second goal is 0 = 1

#### Gabriel Ebner (Sep 29 2020 at 06:46):

Apparently split_if uses all assumptions to simplify the ifs. If you change k : x ∈ f ⁻¹' s to k : f x ∈ s then it would produce only a single goal.

Last updated: May 08 2021 at 09:11 UTC