∀ (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ι → Type v₁) (M₂ : Type v₂) [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂] {ι' : Type u_1}
  (σ : ι ≃ ι') (f : MultilinearMap R M₁ M₂),
  (MultilinearMap.domDomCongrLinearEquiv' R S M₁ M₂ σ) f =
    { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ }