squeeze_simp and simp only disagreeing

Stream: general

[Yakov Pechersky]

Is there something I don't understand about simplifying in a dite conditional? Why do the first two examples work, but the third one doesn't?

import data.fin

variables {n : ℕ}

open fin

@[simp] lemma succ_above_lt_iff (p : fin (n + 1)) (i : fin n) : p.succ_above i < p ↔ i.cast_succ < p :=
begin
  refine iff.intro _ _,
  { intro h,
    cases succ_above_lt_ge p i with H H,
    { exact H },
    { rw succ_above_above _ _ H at h,
      exact lt_trans (cast_succ_lt_succ i) h } },
  { intro h,
    rw succ_above_below _ _ h,
    exact h }
end

example (p : fin (n + 1)) (i : fin n) :
  p.pred_above (p.succ_above i) (succ_above_ne _ _) = i :=
begin
  rw pred_above,
  simp, -- it's able to simp in the dite condition
  /-
n : ℕ,
p : fin (n + 1),
i : fin n
⊢ dite (i.cast_succ < p) (λ (h : i.cast_succ < p), (p.succ_above i).cast_lt _)
      (λ (h : ¬i.cast_succ < p), (p.succ_above i).pred _) =
    i
-/
  sorry
end

example (p : fin (n + 1)) (i : fin n) :
  p.pred_above (p.succ_above i) (succ_above_ne _ _) = i :=
begin
  rw pred_above,
  squeeze_simp, -- still able to simp in the dite condition, suggests succ_above_lt_iff
  sorry
end

example (p : fin (n + 1)) (i : fin n) :
  p.pred_above (p.succ_above i) (succ_above_ne _ _) = i :=
begin
  rw pred_above,
  simp only [succ_above_lt_iff], -- simplify tactic failed to simplify
  sorry
end

[Johan Commelin]

Yes, this is really annoying. I don't understand the details, but it's a known issue. And I think people have ideas on how to improve this.