∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (R : Type u_10) (W : Type u_11) [inst_7 : Ring R]
  [inst_8 : AddCommGroup W] [inst_9 : Module k W] [inst_10 : Module R W] [inst_11 : SMulCommClass k R W]
  (e : P₁ ≃ᵃ[k] P₂) (f : P₂ →ᵃ[k] W) (x : P₁), ((AffineEquiv.congrLeftₗ R W e).symm f) x = f (e x)