simpa hygiene issue

Stream: general

[Yakov Pechersky]

simpa substitutes in this over existing this. Expected?

import group_theory.perm.cycles

variables {α : Type*} [decidable_eq α] {x y : α}

open list equiv equiv.perm

def list.form_perm (l : list α) : equiv.perm α :=
(list.zip_with equiv.swap l l.tail).prod

example (h : x ≠ y) : [x, y].erase_dup.form_perm.is_cycle :=
begin
  have : nodup [x, y] := by simpa,
  simpa [erase_dup_eq_self.mpr this, form_perm] using is_cycle.swap h
  -- what is the hyp used for ^^? it is the is_cycle.swap h, not what we want
end

[Yakov Pechersky]

Of course, I can prove it using

simpa [←erase_dup_eq_self, h, form_perm] using is_cycle.swap h

but just wanted to flag