{ι : 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] →
                  {motive : RootPairing ι R M N → Sort u} →
                    (t : RootPairing ι R M N) →
                      ((toLinearMap : M →ₗ[R] N →ₗ[R] R) →
                          [isPerfPair_toLinearMap : toLinearMap.IsPerfPair] →
                            (root : ι ↪ M) →
                              (coroot : ι ↪ N) →
                                (root_coroot_two : ∀ (i : ι), (toLinearMap (root i)) (coroot i) = 2) →
                                  (reflectionPerm : ι → ι ≃ ι) →
                                    (reflectionPerm_root :
                                        ∀ (i j : ι),
                                          root j - (toLinearMap (root j)) (coroot i) • root i =
                                            root ((reflectionPerm i) j)) →
                                      (reflectionPerm_coroot :
                                          ∀ (i j : ι),
                                            coroot j - (toLinearMap (root i)) (coroot j) • coroot i =
                                              coroot ((reflectionPerm i) j)) →
                                        motive
                                          { toLinearMap := toLinearMap,
                                            isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root,
                                            coroot := coroot, root_coroot_two := root_coroot_two,
                                            reflectionPerm := reflectionPerm,
                                            reflectionPerm_root := reflectionPerm_root,
                                            reflectionPerm_coroot := reflectionPerm_coroot }) →
                        motive t