-- Mathlib/LinearAlgebra/RootSystem/Basic.lean
/-- In characteristic zero if there is no torsion, a finite root system is determined entirely by
its roots. -/
@[ext]
protected lemma ext [CharZero R] [NoZeroSMulDivisors R M]
    {P₁ P₂ : RootSystem ι R M N}
    (he : P₁.toPerfectPairing = P₂.toPerfectPairing)
    (hr : P₁.root = P₂.root) :
    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₂ : RootSystem ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
this :
  ∀ (P₁ P₂ : RootSystem ι R M N),
    P₁.toPerfectPairing = P₂.toPerfectPairing → P₁.root = P₂.root → range ⇑P₁.coroot ⊆ range ⇑P₂.coroot
h₁ : range ⇑P₁.coroot ⊆ range ⇑P₂.coroot
h₂ : range ⇑P₂.coroot ⊆ range ⇑P₁.coroot
⊢ P₁ = P₂

Tactic:
obtain ⟨P₁⟩ := P₁

Result:
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₂ : RootSystem ι R M N
this :
  ∀ (P₁ P₂ : RootSystem ι R M N),
    P₁.toPerfectPairing = P₂.toPerfectPairing → P₁.root = P₂.root → range ⇑P₁.coroot ⊆ range ⇑P₂.coroot
P₁ : RootPairing ι R M N
span_root_eq_top✝ : span R (range ⇑P₁.root) = ⊤
span_coroot_eq_top✝ : span R (range ⇑P₁.coroot) = ⊤
he :
  { toRootPairing := P₁, span_root_eq_top := span_root_eq_top✝,
        span_coroot_eq_top := span_coroot_eq_top✝ }.toPerfectPairing =
    P₂.toPerfectPairing
hr :
  { toRootPairing := P₁, span_root_eq_top := span_root_eq_top✝, span_coroot_eq_top := span_coroot_eq_top✝ }.root =
    P₂.root
h₁ :
  range
      ⇑{ toRootPairing := P₁, span_root_eq_top := span_root_eq_top✝,
            span_coroot_eq_top := span_coroot_eq_top✝ }.coroot ⊆
    range ⇑P₂.coroot
h₂ :
  range ⇑P₂.coroot ⊆
    range
      ⇑{ toRootPairing := P₁, span_root_eq_top := span_root_eq_top✝, span_coroot_eq_top := span_coroot_eq_top✝ }.coroot
⊢ { toRootPairing := P₁, span_root_eq_top := span_root_eq_top✝, span_coroot_eq_top := span_coroot_eq_top✝ } = P₂

Proof state:
case h.a
ι : 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₂ : RootSystem ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
i : ι
⊢ P₁.toLin.flip (P₂.coroot i) = P₁.toLin.flip (P₁.coroot i)

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

Result:
case h.a.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₂ : RootSystem ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
i : ι
⊢ (P₁.toLin.flip (P₂.coroot i)) ?m.95757 = 2

case h.a.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₂ : RootSystem ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
i : ι
⊢ MapsTo (⇑(preReflection ?m.95757 (P₁.toLin.flip (P₂.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)

case h.a.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₂ : RootSystem ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
i : ι
⊢ (P₁.toLin.flip (P₁.coroot i)) ?m.95757 = 2

case h.a.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₂ : RootSystem ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
i : ι
⊢ MapsTo (⇑(preReflection ?m.95757 (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₂ : RootSystem ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
i : ι
⊢ M