-- 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₂ : RootPairing ι R M N
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
obtain :
  ∀ (p₂ : M →ₗ[R] N →ₗ[R] R) [isPerfPair_toLinearMap_1 : p₂.IsPerfPair] (root_1 : ι ↪ M) (coroot_1 : ι ↪ N)
    (root_coroot_two_1 :
      ∀ (i : ι),
        Eq.{u_2 + 1} (α := R)
          ((((p₂ : (a : M) → N →ₗ[R] R) ((root_1 : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
              ((coroot_1 : (a : ι) → N) i : N) :
            R)
          (2 : R))
    (reflectionPerm_1 : ι → ι ≃ ι)
    (reflectionPerm_root_1 :
      ∀ (i j : ι),
        HSub.hSub (α := M) ((root_1 : (a : ι) → M) j : M)
            (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
              ((((p₂ : (a : M) → N →ₗ[R] R) ((root_1 : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
                  ((coroot_1 : (a : ι) → N) i : N) :
                R)
              ((root_1 : (a : ι) → M) i : M)) =
          (root_1 : (a : ι) → M) ((reflectionPerm_1 i : (a : ι) → ι) j : ι))
    (reflectionPerm_coroot_1 :
      ∀ (i j : ι),
        HSub.hSub (α := N) ((coroot_1 : (a : ι) → N) j : N)
            (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
              ((((p₂ : (a : M) → N →ₗ[R] R) ((root_1 : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
                  ((coroot_1 : (a : ι) → N) j : N) :
                R)
              ((coroot_1 : (a : ι) → N) i : N)) =
          (coroot_1 : (a : ι) → N) ((reflectionPerm_1 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 =
        { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap_1, root := root_1, coroot := coroot_1,
            root_coroot_two := root_coroot_two_1, reflectionPerm := reflectionPerm_1,
            reflectionPerm_root := reflectionPerm_root_1, reflectionPerm_coroot := reflectionPerm_coroot_1 :
            RootPairing ι R M N }.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 =
        { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap_1, root := root_1, coroot := coroot_1,
            root_coroot_two := root_coroot_two_1, reflectionPerm := reflectionPerm_1,
            reflectionPerm_root := reflectionPerm_root_1, reflectionPerm_coroot := reflectionPerm_coroot_1 :
            RootPairing ι R M N }.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} (ι := ι)
          (⇑{ toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap_1, root := root_1, coroot := coroot_1,
                  root_coroot_two := root_coroot_two_1, reflectionPerm := reflectionPerm_1,
                  reflectionPerm_root := reflectionPerm_root_1, reflectionPerm_coroot := reflectionPerm_coroot_1 :
                  RootPairing ι R M N }.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 =
            { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap_1, root := root_1, coroot := coroot_1,
                root_coroot_two := root_coroot_two_1, reflectionPerm := reflectionPerm_1,
                reflectionPerm_root := reflectionPerm_root_1, reflectionPerm_coroot := reflectionPerm_coroot_1 :
                RootPairing ι R M N }.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 =
          { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap_1, root := root_1, coroot := coroot_1,
              root_coroot_two := root_coroot_two_1, reflectionPerm := reflectionPerm_1,
              reflectionPerm_root := reflectionPerm_root_1, reflectionPerm_coroot := reflectionPerm_coroot_1 :
              RootPairing ι R M N }.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 =
        { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap_1, root := root_1, coroot := coroot_1,
            root_coroot_two := root_coroot_two_1, reflectionPerm := reflectionPerm_1,
            reflectionPerm_root := reflectionPerm_root_1, reflectionPerm_coroot := reflectionPerm_coroot_1 :
            RootPairing ι R M N }.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 } =
      { toLinearMap := p₂, isPerfPair_toLinearMap := isPerfPair_toLinearMap_1, root := root_1, coroot := coroot_1,
        root_coroot_two := root_coroot_two_1, reflectionPerm := reflectionPerm_1,
        reflectionPerm_root := reflectionPerm_root_1, reflectionPerm_coroot := reflectionPerm_coroot_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 } =
    P₂

Tactic:
obtain ⟨p₂⟩ := P₂