-- Module: Mathlib.LinearAlgebra.RootSystem.Basic
Goal:
ι : 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
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc :
  Eq.{u_4 + 1} (α := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P₁.coroot : (a : ι) → N))
    (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N))
hp : ∀ (hc' : P₁.coroot = P₂.coroot), P₁.reflectionPerm = P₂.reflectionPerm
this : P₁.coroot = P₂.coroot
obtain :
  ∀ (p₁ : M →ₗ[R] N →ₗ[R] R) [isPerfPair_toLinearMap : p₁.IsPerfPair] (root : ι ↪ M) (coroot : ι ↪ N)
    (root_coroot_two :
      ∀ (i : ι),
        Eq.{u_2 + 1} (α := R)
          ((((p₁ : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
              ((coroot : (a : ι) → N) i : N) :
            R)
          (2 : R))
    (reflectionPerm : ι → ι ≃ ι)
    (reflectionPerm_root :
      ∀ (i j : ι),
        HSub.hSub (α := M) ((root : (a : ι) → M) j : M)
            (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
              ((((p₁ : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
                  ((coroot : (a : ι) → N) i : N) :
                R)
              ((root : (a : ι) → M) i : M)) =
          (root : (a : ι) → M) ((reflectionPerm i : (a : ι) → ι) j : ι))
    (reflectionPerm_coroot :
      ∀ (i j : ι),
        HSub.hSub (α := N) ((coroot : (a : ι) → N) j : N)
            (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
              ((((p₁ : (a : M) → N →ₗ[R] R) ((root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
                  ((coroot : (a : ι) → N) j : N) :
                R)
              ((coroot : (a : ι) → N) i : N)) =
          (coroot : (a : ι) → N) ((reflectionPerm i : (a : ι) → ι) j : ι))
    (he :
      { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
            root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm,
            reflectionPerm_root := reflectionPerm_root, reflectionPerm_coroot := reflectionPerm_coroot :
            RootPairing ι R M N }.toLinearMap =
        P₂.toLinearMap)
    (hr :
      { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
            root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm,
            reflectionPerm_root := reflectionPerm_root, reflectionPerm_coroot := reflectionPerm_coroot :
            RootPairing ι R M N }.root =
        P₂.root)
    (hc :
      Eq.{u_4 + 1} (α := Set N)
        (range.{u_4, u_1 + 1} (ι := ι)
          (⇑{ toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
                  root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm,
                  reflectionPerm_root := reflectionPerm_root, reflectionPerm_coroot := reflectionPerm_coroot :
                  RootPairing ι R M N }.coroot :
            (a : ι) → N))
        (range.{u_4, u_1 + 1} (ι := ι) (⇑P₂.coroot : (a : ι) → N)))
    (hp :
      ∀
        (hc' :
          { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
                root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm,
                reflectionPerm_root := reflectionPerm_root, reflectionPerm_coroot := reflectionPerm_coroot :
                RootPairing ι R M N }.coroot =
            P₂.coroot),
        { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
              root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm,
              reflectionPerm_root := reflectionPerm_root, reflectionPerm_coroot := reflectionPerm_coroot :
              RootPairing ι R M N }.reflectionPerm =
          P₂.reflectionPerm)
    (this :
      { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
            root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm,
            reflectionPerm_root := reflectionPerm_root, reflectionPerm_coroot := reflectionPerm_coroot :
            RootPairing ι R M N }.coroot =
        P₂.coroot),
    { toLinearMap := p₁, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
        root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm,
        reflectionPerm_root := reflectionPerm_root, reflectionPerm_coroot := reflectionPerm_coroot :
        RootPairing ι R M N } =
      P₂
⊢ P₁ = P₂

Tactic:
obtain ⟨p₁⟩ := P₁