-- 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 h
ι : 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
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ (span R (range ⇑P₁.root)).subtype.dualMap (P₁.toLin.flip (P₁.coroot i)) =
    (span R (range ⇑P₁.root)).subtype.dualMap (P₁.toLin.flip (P₂.coroot i))

Tactic:
apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)

Result:
case h.hx
ι : 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
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ ?m.36057 ∈ span R (range ⇑P₁.root)

case h.hf₁
ι : 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
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ (P₁.toLin.flip (P₁.coroot i)) ?m.36057 = 2

case h.hf₂
ι : 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
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ MapsTo (⇑(preReflection ?m.36057 (P₁.toLin.flip (P₁.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)

case h.hg₁
ι : 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
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ (P₁.toLin.flip (P₂.coroot i)) ?m.36057 = 2

case h.hg₂
ι : 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
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ MapsTo (⇑(preReflection ?m.36057 (P₁.toLin.flip (P₂.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)

ι : 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
this : NoZeroSMulDivisors ℤ M
i : ι
⊢ M