-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Basic (goal)
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
⊢ P₁ = P₂
have 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₂
Tactic: obtain ⟨p₁⟩ := P₁
Cleared hypotheses: P₁, he, hr, hc, hp, this