split_ifs weirdness

Stream: general

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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.