awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
h₀ : lj = 2 * li
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    li
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    li
hk : P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ li = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 2 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
h₀ : lj = 2 * li
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    li
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    lj
hk : P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂ ∨ li = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 2 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
h₀ : lj = 2 * li
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    lj
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    li
hk : 2 * P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ li = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 2 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
h₀ : lj = 2 * li
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    lj
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    lj
hk : 2 * P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂ ∨ li = 0
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 2 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this_1 : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
this : li = 3 * lj ∨ lj = 3 * li
⊢ (∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 2 * P.pairing j i ∨ P.pairing j i = 2 * P.pairing i j) ∨
    ∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 3 * P.pairing j i ∨ P.pairing j i = 3 * P.pairing i j

Tactic:
Or.inr fun k₁ k₂ ↦ ?_

Premises used: Or.inr
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this_1 : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
this : li = 3 * lj ∨ lj = 3 * li
neg :
  ∀ (k₁ k₂ : ι),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
⊢ (∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 2 * P.pairing j i ∨ P.pairing j i = 2 * P.pairing i j) ∨
    ∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 3 * P.pairing j i ∨ P.pairing j i = 3 * P.pairing i j

Tactic:
refine Or.inr fun k₁ k₂ ↦ ?_

Premises used: Or.inr
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this_1 : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
this : li = 3 * lj ∨ lj = 3 * li
k₁ k₂ : ι
⊢ HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)

Tactic:
have hk := B.pairing_mul_eq_pairing_mul_swap k₁ k₂
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this_1 : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
this : li = 3 * lj ∨ lj = 3 * li
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
neg :
  ∀ (h₀ : li = 3 * lj),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
neg₁ :
  ∀ (h₀ : lj = 3 * li),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
rcases this with h₀ | h₀
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : li = 3 * lj
neg :
  ∀
    (h₁ :
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) =
        li),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
neg₁ :
  ∀
    (h₁ :
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) =
        lj),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
rcases key k₁ with h₁ | h₁
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : lj = 3 * li
neg :
  ∀
    (h₁ :
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) =
        li),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
neg₁ :
  ∀
    (h₁ :
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) =
        lj),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
rcases key k₁ with h₁ | h₁
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : li = 3 * lj
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    li
neg :
  ∀
    (h₂ :
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) =
        li),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
neg₁ :
  ∀
    (h₂ :
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) =
        lj),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
rcases key k₂ with h₂ | h₂
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : li = 3 * lj
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    lj
neg :
  ∀
    (h₂ :
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) =
        li),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
neg₁ :
  ∀
    (h₂ :
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) =
        lj),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
rcases key k₂ with h₂ | h₂
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
inst_8 : IsDomain R
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) i : M)
lj : R :=
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((P.root : (a : ι) → M) j : M)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : lj = 3 * li
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    li
neg :
  ∀
    (h₂ :
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) =
        li),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
neg₁ :
  ∀
    (h₂ :
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) =
        lj),
    P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂

Tactic:
rcases key k₂ with h₂ | h₂