-- 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:
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₂

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
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) = ⊤
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 =
    { toRootPairing := P₂, span_root_eq_top := span_root_eq_top✝,
        span_coroot_eq_top := span_coroot_eq_top✝ }.toPerfectPairing
hr :
  { toRootPairing := P₁, span_root_eq_top := span_root_eq_top✝¹, span_coroot_eq_top := span_coroot_eq_top✝¹ }.root =
    { toRootPairing := P₂, span_root_eq_top := span_root_eq_top✝, span_coroot_eq_top := span_coroot_eq_top✝ }.root
h₁ :
  range
      ⇑{ toRootPairing := P₁, span_root_eq_top := span_root_eq_top✝¹,
            span_coroot_eq_top := span_coroot_eq_top✝¹ }.coroot ⊆
    range
      ⇑{ toRootPairing := P₂, span_root_eq_top := span_root_eq_top✝, span_coroot_eq_top := span_coroot_eq_top✝ }.coroot
h₂ :
  range
      ⇑{ toRootPairing := P₂, span_root_eq_top := span_root_eq_top✝,
            span_coroot_eq_top := span_coroot_eq_top✝ }.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✝¹ } =
    { toRootPairing := P₂, span_root_eq_top := span_root_eq_top✝, span_coroot_eq_top := span_coroot_eq_top✝ }

Proof state:
case intro
ι : 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₁.coroot i ∈ range ⇑P₂.coroot

Tactic:
use i

Result:
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₂ : RootSystem ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
i : ι
⊢ P₂.coroot i = P₁.coroot i

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
⊢ P₁ = P₂

Tactic:
suffices ∀ P₁ P₂ : RootSystem ι R M N, P₁.toPerfectPairing = P₂.toPerfectPairing →
    P₁.root = P₂.root → range P₁.coroot ⊆ range P₂.coroot by
  have h₁ := this P₁ P₂ he hr
  have h₂ := this P₂ P₁ he.symm hr.symm
  obtain ⟨P₁⟩ := P₁
  obtain ⟨P₂⟩ := P₂
  congr
  exact RootPairing.ext he hr (le_antisymm h₁ h₂)

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₂ : RootSystem ι R M N
he : P₁.toPerfectPairing = P₂.toPerfectPairing
hr : P₁.root = P₂.root
⊢ ∀ (P₁ P₂ : RootSystem ι R M N),
    P₁.toPerfectPairing = P₂.toPerfectPairing → P₁.root = P₂.root → range ⇑P₁.coroot ⊆ range ⇑P₂.coroot

Proof state:
case mk.mk.e_toRootPairing
ι : 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
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) = ⊤
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 =
    { toRootPairing := P₂, span_root_eq_top := span_root_eq_top✝,
        span_coroot_eq_top := span_coroot_eq_top✝ }.toPerfectPairing
hr :
  { toRootPairing := P₁, span_root_eq_top := span_root_eq_top✝¹, span_coroot_eq_top := span_coroot_eq_top✝¹ }.root =
    { toRootPairing := P₂, span_root_eq_top := span_root_eq_top✝, span_coroot_eq_top := span_coroot_eq_top✝ }.root
h₁ :
  range
      ⇑{ toRootPairing := P₁, span_root_eq_top := span_root_eq_top✝¹,
            span_coroot_eq_top := span_coroot_eq_top✝¹ }.coroot ⊆
    range
      ⇑{ toRootPairing := P₂, span_root_eq_top := span_root_eq_top✝, span_coroot_eq_top := span_coroot_eq_top✝ }.coroot
h₂ :
  range
      ⇑{ toRootPairing := P₂, span_root_eq_top := span_root_eq_top✝,
            span_coroot_eq_top := span_coroot_eq_top✝ }.coroot ⊆
    range
      ⇑{ toRootPairing := P₁, span_root_eq_top := span_root_eq_top✝¹,
            span_coroot_eq_top := span_coroot_eq_top✝¹ }.coroot
⊢ P₁ = P₂

Tactic:
exact RootPairing.ext he hr (le_antisymm h₁ h₂)

Result:
no goals