no goals
α : Sort u_1
β : Sort u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : α → Sort u_3
e : α ≃ β
f : (b : β) → P (↑e.symm b)
b : β
x : P (↑e.symm b)
⊢ ↑(Equiv.piCongrLeft' P e).symm (update f b x) = update (↑(Equiv.piCongrLeft' P e).symm f) (↑e.symm b) x
simp [(e.piCongrLeft' P).symm_apply_eq, piCongrLeft'_update]