-- Mathlib/LinearAlgebra/RootSystem/Basic.lean
/-- In characteristic zero if there is no torsion, the correspondence between roots and coroots is
unique.

Formally, the point is that the hypothesis `hc` depends only on the range of the coroot mappings. -/
@[ext]
protected lemma ext [CharZero R] [NoZeroSMulDivisors R M]
    {P₁ P₂ : RootPairing ι R M N}
    (he : P₁.toPerfectPairing = P₂.toPerfectPairing)
    (hr : P₁.root = P₂.root)
    (hc : range P₁.coroot = range P₂.coroot) :
    P₁ = P₂

Proof state:
ι : 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✝ : NoZeroSMulDivisors R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
⊢ P₁ = P₂

Tactic:
have hp (hc' : P₁.coroot = P₂.coroot) : P₁.reflection_perm = P₂.reflection_perm := by
  ext i j
  refine P₁.root.injective ?_
  conv_rhs => rw [hr]
  simp only [root_reflection_perm, reflection_apply, coroot']
  simp only [hr, he, hc']

Result:
ι : 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✝ : NoZeroSMulDivisors R M
P₁ P₂ : RootPairing ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
hc : range ⇑P₁.coroot = range ⇑P₂.coroot
hp : P₁.coroot = P₂.coroot → P₁.reflection_perm = P₂.reflection_perm
⊢ P₁ = P₂

Proof state:
case mk.mk.mk.mk.e_reflection_perm
ι : 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✝ : NoZeroSMulDivisors R M
root✝¹ : ι ↪ M
coroot✝¹ : ι ↪ N
reflection_perm✝¹ : ι → ι ≃ ι
root✝ : ι ↪ M
coroot✝ : ι ↪ N
reflection_perm✝ : ι → ι ≃ ι
toLin✝¹ : M →ₗ[R] N →ₗ[R] R
bijectiveLeft✝¹ : Bijective ⇑toLin✝¹
bijectiveRight✝¹ : Bijective ⇑toLin✝¹.flip
root_coroot_two✝¹ :
  ∀ (i : ι),
    ({ toLin := toLin✝¹, bijectiveLeft := bijectiveLeft✝¹, bijectiveRight := bijectiveRight✝¹ }.toLin (root✝¹ i))
        (coroot✝¹ i) =
      2
reflection_perm_root✝¹ :
  ∀ (i j : ι),
    root✝¹ j -
        ({ toLin := toLin✝¹, bijectiveLeft := bijectiveLeft✝¹, bijectiveRight := bijectiveRight✝¹ } (root✝¹ j))
            (coroot✝¹ i) •
          root✝¹ i =
      root✝¹ ((reflection_perm✝¹ i) j)
reflection_perm_coroot✝¹ :
  ∀ (i j : ι),
    coroot✝¹ j -
        ({ toLin := toLin✝¹, bijectiveLeft := bijectiveLeft✝¹, bijectiveRight := bijectiveRight✝¹ } (root✝¹ i))
            (coroot✝¹ j) •
          coroot✝¹ i =
      coroot✝¹ ((reflection_perm✝¹ i) j)
toLin✝ : M →ₗ[R] N →ₗ[R] R
bijectiveLeft✝ : Bijective ⇑toLin✝
bijectiveRight✝ : Bijective ⇑toLin✝.flip
root_coroot_two✝ :
  ∀ (i : ι),
    ({ toLin := toLin✝, bijectiveLeft := bijectiveLeft✝, bijectiveRight := bijectiveRight✝ }.toLin (root✝ i))
        (coroot✝ i) =
      2
reflection_perm_root✝ :
  ∀ (i j : ι),
    root✝ j -
        ({ toLin := toLin✝, bijectiveLeft := bijectiveLeft✝, bijectiveRight := bijectiveRight✝ } (root✝ j))
            (coroot✝ i) •
          root✝ i =
      root✝ ((reflection_perm✝ i) j)
reflection_perm_coroot✝ :
  ∀ (i j : ι),
    coroot✝ j -
        ({ toLin := toLin✝, bijectiveLeft := bijectiveLeft✝, bijectiveRight := bijectiveRight✝ } (root✝ i))
            (coroot✝ j) •
          coroot✝ i =
      coroot✝ ((reflection_perm✝ i) j)
he :
  { toLin := toLin✝¹, bijectiveLeft := bijectiveLeft✝¹, bijectiveRight := bijectiveRight✝¹, root := root✝¹,
        coroot := coroot✝¹, root_coroot_two := root_coroot_two✝¹, reflection_perm := reflection_perm✝¹,
        reflection_perm_root := reflection_perm_root✝¹,
        reflection_perm_coroot := reflection_perm_coroot✝¹ }.toPerfectPairing =
    { toLin := toLin✝, bijectiveLeft := bijectiveLeft✝, bijectiveRight := bijectiveRight✝, root := root✝,
        coroot := coroot✝, root_coroot_two := root_coroot_two✝, reflection_perm := reflection_perm✝,
        reflection_perm_root := reflection_perm_root✝,
        reflection_perm_coroot := reflection_perm_coroot✝ }.toPerfectPairing
hr :
  { toLin := toLin✝¹, bijectiveLeft := bijectiveLeft✝¹, bijectiveRight := bijectiveRight✝¹, root := root✝¹,
        coroot := coroot✝¹, root_coroot_two := root_coroot_two✝¹, reflection_perm := reflection_perm✝¹,
        reflection_perm_root := reflection_perm_root✝¹, reflection_perm_coroot := reflection_perm_coroot✝¹ }.root =
    { toLin := toLin✝, bijectiveLeft := bijectiveLeft✝, bijectiveRight := bijectiveRight✝, root := root✝,
        coroot := coroot✝, root_coroot_two := root_coroot_two✝, reflection_perm := reflection_perm✝,
        reflection_perm_root := reflection_perm_root✝, reflection_perm_coroot := reflection_perm_coroot✝ }.root
hc :
  range
      ⇑{ toLin := toLin✝¹, bijectiveLeft := bijectiveLeft✝¹, bijectiveRight := bijectiveRight✝¹, root := root✝¹,
            coroot := coroot✝¹, root_coroot_two := root_coroot_two✝¹, reflection_perm := reflection_perm✝¹,
            reflection_perm_root := reflection_perm_root✝¹,
            reflection_perm_coroot := reflection_perm_coroot✝¹ }.coroot =
    range
      ⇑{ toLin := toLin✝, bijectiveLeft := bijectiveLeft✝, bijectiveRight := bijectiveRight✝, root := root✝,
            coroot := coroot✝, root_coroot_two := root_coroot_two✝, reflection_perm := reflection_perm✝,
            reflection_perm_root := reflection_perm_root✝, reflection_perm_coroot := reflection_perm_coroot✝ }.coroot
hp :
  { toLin := toLin✝¹, bijectiveLeft := bijectiveLeft✝¹, bijectiveRight := bijectiveRight✝¹, root := root✝¹,
          coroot := coroot✝¹, root_coroot_two := root_coroot_two✝¹, reflection_perm := reflection_perm✝¹,
          reflection_perm_root := reflection_perm_root✝¹, reflection_perm_coroot := reflection_perm_coroot✝¹ }.coroot =
      { toLin := toLin✝, bijectiveLeft := bijectiveLeft✝, bijectiveRight := bijectiveRight✝, root := root✝,
          coroot := coroot✝, root_coroot_two := root_coroot_two✝, reflection_perm := reflection_perm✝,
          reflection_perm_root := reflection_perm_root✝, reflection_perm_coroot := reflection_perm_coroot✝ }.coroot →
    { toLin := toLin✝¹, bijectiveLeft := bijectiveLeft✝¹, bijectiveRight := bijectiveRight✝¹, root := root✝¹,
          coroot := coroot✝¹, root_coroot_two := root_coroot_two✝¹, reflection_perm := reflection_perm✝¹,
          reflection_perm_root := reflection_perm_root✝¹,
          reflection_perm_coroot := reflection_perm_coroot✝¹ }.reflection_perm =
      { toLin := toLin✝, bijectiveLeft := bijectiveLeft✝, bijectiveRight := bijectiveRight✝, root := root✝,
          coroot := coroot✝, root_coroot_two := root_coroot_two✝, reflection_perm := reflection_perm✝,
          reflection_perm_root := reflection_perm_root✝,
          reflection_perm_coroot := reflection_perm_coroot✝ }.reflection_perm
this :
  { toLin := toLin✝¹, bijectiveLeft := bijectiveLeft✝¹, bijectiveRight := bijectiveRight✝¹, root := root✝¹,
        coroot := coroot✝¹, root_coroot_two := root_coroot_two✝¹, reflection_perm := reflection_perm✝¹,
        reflection_perm_root := reflection_perm_root✝¹, reflection_perm_coroot := reflection_perm_coroot✝¹ }.coroot =
    { toLin := toLin✝, bijectiveLeft := bijectiveLeft✝, bijectiveRight := bijectiveRight✝, root := root✝,
        coroot := coroot✝, root_coroot_two := root_coroot_two✝, reflection_perm := reflection_perm✝,
        reflection_perm_root := reflection_perm_root✝, reflection_perm_coroot := reflection_perm_coroot✝ }.coroot
⊢ reflection_perm✝¹ = reflection_perm✝

Tactic:
exact hp this

Result:
no goals