∀ {ι : Type u_7} {ι' : Type u_8} (R : ι → Type u_9) (e : ι ≃ ι') [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)]
  (f : (b : ι') → R (e.symm b)) (x : ι), (RingEquiv.piCongrLeft' R e).symm f x = ⋯ ▸ f (e x)