-- 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),
    P₁.toPerfectPairing = P₂.toPerfectPairing → P₁.root = P₂.root → range ⇑P₁.coroot ⊆ range ⇑P₂.coroot

Tactic:
rintro P₁ P₂ he hr - ⟨i, rfl⟩

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

Proof state:
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✝ }

Tactic:
congr

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