-- 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₂ : 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
⊢ { 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₂
have 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 }
Tactic: obtain ⟨p₂⟩ := P₂
Cleared hypotheses: P₂, he, hr, hc, hp, this