Module: Mathlib.LinearAlgebra.RootSystem.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toLinearMap = P₂.toLinearMap
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hp : P₁.coroot = P₂.coroot → P₁.reflectionPerm = P₂.reflectionPerm
this : P₁.coroot = P₂.coroot
⊢ P₁ = P₂

Tactic:
obtain ⟨p₁⟩ := P₁

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
inst✝ : 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 : ι), (p₁ (root✝ i)) (coroot✝ i) = 2
reflectionPerm✝ : ι → ι ≃ ι
reflectionPerm_root✝ : ∀ (i j : ι), root✝ j - (p₁ (root✝ j)) (coroot✝ i) • root✝ i = root✝ ((reflectionPerm✝ i) j)
reflectionPerm_coroot✝ :
  ∀ (i j : ι), coroot✝ j - (p₁ (root✝ i)) (coroot✝ j) • coroot✝ i = coroot✝ ((reflectionPerm✝ i) 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✝ }.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✝ }.root =
    P₂.root
hc :
  range
      ⇑{ 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✝ }.coroot =
    range ⇑P₂.coroot
hp :
  { 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✝ }.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✝ }.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✝ }.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✝ } =
    P₂