feat(data/equiv): pi_congr

[semorrison]

Provides

def Pi_congr_left' (P : α → Sort w) (e : α ≃ β) : (Π a, P a) ≃ (Π b, P (e.symm b)) := ...
def Pi_congr_left (P : β → Sort w) (e : α ≃ β) : (Π a, P (e a)) ≃ (Π b, P b) :=

and deduces the "general case"

def Pi_congr (W : α → Sort w) (Z : β → Sort z) (h₁ : α ≃ β) (h₂ : Π a : α, (W a ≃ Z (h₁ a))) : (Π a, W a) ≃ (Π b, Z b) := ...

Thanks @urkud and @digama0 for explaining the method(s) of proof!

These constructions prove useful in my equiv_rw tactic, which is coming along nicely.

[robertylewis]

Do you really want all of these arguments explicit?

[semorrison]

I've made {W Z}, but left h₁ explicit.