∀ {ι : Type u_2} {R : Type u_3} {M : Type u_1} {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] (p : M →ₗ[R] N →ₗ[R] R) (root : ι ↪ M)
  (coroot : ι ↪ N) (hp : ∀ (i : ι), (p (root i)) (coroot i) = 2)
  (hr :
    ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root))
  (i j : ι), root j - (p (root j)) (coroot i) • root i = root ((RootPairing.equiv_of_mapsTo p root coroot i hr hp) j)