How to prove this equality?

Stream: new members

[Antoine Chambert-Loir]

I'm stuck on this…

example {ι : Type*} [decidable_eq ι] (p : α → ι) (s : finset ι)
  (f : Π (i : ι), i ∈ s → equiv.perm ↥{a : α | p a = i})
  (i j : ι) (hi : i ∈ s) (hj : j ∈ s) (h : i = j) :
  equiv.perm.of_subtype (f j hj) = equiv.perm.of_subtype (f i hi) :=

Because rw h does not work, even if one can rw hi and prove that it equal hj…

[Ruben Van de Velde]

Did you try subst?

[Antoine Chambert-Loir]

No, I even didn't know about it…
— and it works, thanks!

[Kevin Buzzard]

subst is a version of rw which avoids "motive is not type correct" issues but only works if one side of the equality is a "bare" term, e.g. you cannot subst h if h : a + b = c + d.

[Kevin Buzzard]

import tactic

variables (α : Type)

example {ι : Type*} [decidable_eq ι] (p : α → ι) (s : finset ι)
  (f : Π (i : ι), i ∈ s → equiv.perm ↥{a : α | p a = i})
  (i j : ι) (hi : i ∈ s) (hj : j ∈ s) (h : i = j) :
  equiv.perm.of_subtype (f j hj) = equiv.perm.of_subtype (f i hi) :=
begin
  revert hi,
  rw h,
  intro hi,
  refl,
end

works, because then all of the i's which need to be changed to j's to make the motive type-correct are present in the goal. This may or may not be what subst is doing under the hood.

[Riccardo Brasca]

You can also try conv.