-- 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 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 (P₁.root i) (P₁.toLin.flip (P₂.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)

Tactic:
exact hr ▸ he ▸ P₂.mapsTo_reflection_root i

Result:
no goals

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

Tactic:
exact hr ▸ he ▸ P₂.coroot_root_two i

Result:
no goals

Proof state:
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)) (P₁.root i) = 2

Tactic:
exact P₁.coroot_root_two i

Result:
no goals

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

Tactic:
have h₂ := this P₂ P₁ he.symm hr.symm

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

Proof state:
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 (P₁.root i) (P₁.toLin.flip (P₁.coroot i)))) (range ⇑P₁.root) (range ⇑P₁.root)

Tactic:
exact P₁.mapsTo_reflection_root i

Result:
no goals

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

Tactic:
clear! P₁ P₂

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

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

Tactic:
apply P₁.bijectiveRight.injective

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

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

Tactic:
have h₁ := this P₁ P₂ he hr

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