help with a cast

Stream: general

[Scott Morrison]

I used to be able to cope with problems like this, but not today apparently. Can anyone solve this one:

import data.equiv.basic

theorem equiv.Pi_congr_left'_symm_apply_symm {α β : Sort*} (P : α → Sort*) (e : α ≃ β) (f : Π b, P ((e.symm) b)) (b : β) :
  ((equiv.Pi_congr_left' P e).symm) f (e.symm b) = f b :=
begin
  sorry
end

[Adam Topaz]

Not the most elegant:

import data.equiv.basic

theorem equiv.Pi_congr_left'_symm_apply_symm {α β : Sort*} (P : α → Sort*) (e : α ≃ β)
  (f : Π b, P ((e.symm) b)) (b : β) :
  ((equiv.Pi_congr_left' P e).symm) f (e.symm b) = f b :=
begin
  let E := equiv.Pi_congr_left' P e,
  have : f = E (E.symm f), by simp,
  rw this,
  simp,
end

[Adam Topaz]

golfed a bit:

import data.equiv.basic

theorem equiv.Pi_congr_left'_symm_apply_symm {α β : Sort*} (P : α → Sort*) (e : α ≃ β)
  (f : Π b, P ((e.symm) b)) (b : β) :
  ((equiv.Pi_congr_left' P e).symm) f (e.symm b) = f b :=
begin
  rw [← (equiv.Pi_congr_left' P e).apply_symm_apply f],
  simp,
end