-- 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:
case mk
ι : 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₂ : RootPairing ι R M N
p₁ : PerfectPairing R M N
root✝ : ι ↪ M
coroot✝ : ι ↪ N
root_coroot_two✝ : ∀ (i : ι), (p₁.toLin (root✝ i)) (coroot✝ i) = 2
reflection_perm✝ : ι → ι ≃ ι
reflection_perm_root✝ : ∀ (i j : ι), root✝ j - (p₁ (root✝ j)) (coroot✝ i) • root✝ i = root✝ ((reflection_perm✝ i) j)
reflection_perm_coroot✝ :
  ∀ (i j : ι), coroot✝ j - (p₁ (root✝ i)) (coroot✝ j) • coroot✝ i = coroot✝ ((reflection_perm✝ i) j)
he :
  { toPerfectPairing := p₁, 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 =
    P₂.toPerfectPairing
hr :
  { toPerfectPairing := p₁, 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 =
    P₂.root
hc :
  range
      ⇑{ toPerfectPairing := p₁, 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 ⇑P₂.coroot
hp :
  { toPerfectPairing := p₁, 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 =
      P₂.coroot →
    { toPerfectPairing := p₁, 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 =
      P₂.reflection_perm
this :
  { toPerfectPairing := p₁, 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 =
    P₂.coroot
⊢ { toPerfectPairing := p₁, 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✝ } =
    P₂

Tactic:
obtain ⟨p₂⟩ := P₂

Result:
case mk.mk
ι : 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₁ : PerfectPairing R M N
root✝¹ : ι ↪ M
coroot✝¹ : ι ↪ N
root_coroot_two✝¹ : ∀ (i : ι), (p₁.toLin (root✝¹ i)) (coroot✝¹ i) = 2
reflection_perm✝¹ : ι → ι ≃ ι
reflection_perm_root✝¹ :
  ∀ (i j : ι), root✝¹ j - (p₁ (root✝¹ j)) (coroot✝¹ i) • root✝¹ i = root✝¹ ((reflection_perm✝¹ i) j)
reflection_perm_coroot✝¹ :
  ∀ (i j : ι), coroot✝¹ j - (p₁ (root✝¹ i)) (coroot✝¹ j) • coroot✝¹ i = coroot✝¹ ((reflection_perm✝¹ i) j)
p₂ : PerfectPairing R M N
root✝ : ι ↪ M
coroot✝ : ι ↪ N
root_coroot_two✝ : ∀ (i : ι), (p₂.toLin (root✝ i)) (coroot✝ i) = 2
reflection_perm✝ : ι → ι ≃ ι
reflection_perm_root✝ : ∀ (i j : ι), root✝ j - (p₂ (root✝ j)) (coroot✝ i) • root✝ i = root✝ ((reflection_perm✝ i) j)
reflection_perm_coroot✝ :
  ∀ (i j : ι), coroot✝ j - (p₂ (root✝ i)) (coroot✝ j) • coroot✝ i = coroot✝ ((reflection_perm✝ i) j)
he :
  { toPerfectPairing := p₁, 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 =
    { toPerfectPairing := p₂, 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 :
  { toPerfectPairing := p₁, 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 =
    { toPerfectPairing := p₂, 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
      ⇑{ toPerfectPairing := p₁, 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
      ⇑{ toPerfectPairing := p₂, 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 :
  { toPerfectPairing := p₁, 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 =
      { toPerfectPairing := p₂, 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 →
    { toPerfectPairing := p₁, 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 =
      { toPerfectPairing := p₂, 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 :
  { toPerfectPairing := p₁, 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 =
    { toPerfectPairing := p₂, 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
⊢ { toPerfectPairing := p₁, 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 := p₂, 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✝ }