-- 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₁ : 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 : ι)
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:
simp_all