{ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (toLinearMap : M →ₗ[R] N →ₗ[R] R) →
                    [isPerfPair_toLinearMap : toLinearMap.IsPerfPair] →
                      (root : ι ↪ M) →
                        (coroot : ι ↪ N) →
                          (∀ (i : ι), (toLinearMap (root i)) (coroot i) = 2) →
                            (reflectionPerm : ι → ι ≃ ι) →
                              (∀ (i j : ι),
                                  root j - (toLinearMap (root j)) (coroot i) • root i = root ((reflectionPerm i) j)) →
                                (∀ (i j : ι),
                                    coroot j - (toLinearMap (root i)) (coroot j) • coroot i =
                                      coroot ((reflectionPerm i) j)) →
                                  RootPairing ι R M N