Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case neg.inl
ι : 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
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this✝ : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
this : li = 2 * lj ∨ lj = 2 * li
k₁ k₂ : ι
hk : P.pairing k₂ k₁ * (B.form (P.root k₁)) (P.root k₁) = P.pairing k₁ k₂ * (B.form (P.root k₂)) (P.root k₂)
⊢ 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:
rcases this with h₀ | h₀ <;> rcases key k₁ with h₁ | h₁ <;> rcases key k₂ with h₂ | h₂ <;>
    simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk

Goal state after:
case neg.inl.inl.inl.inl
ι : 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
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : li = 2 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
hk : 2 * P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂ ∨ lj = 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₂

case neg.inl.inl.inl.inr
ι : 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
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : li = 2 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
hk : 2 * P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ lj = 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₂

case neg.inl.inl.inr.inl
ι : 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
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : li = 2 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = li
hk : P.pairing k₂ k₁ = 2 * P.pairing k₁ k₂ ∨ lj = 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₂

case neg.inl.inl.inr.inr
ι : 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
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : li = 2 * lj
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = lj
hk : P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ lj = 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₂

case neg.inl.inr.inl.inl
ι : 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
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : lj = 2 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = 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₂

case neg.inl.inr.inl.inr
ι : 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
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : lj = 2 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = li
h₂ : (B.form (P.root k₂)) (P.root k₂) = 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₂

case neg.inl.inr.inr.inl
ι : 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
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : lj = 2 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = 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₂

case neg.inl.inr.inr.inr
ι : 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
P : RootPairing ι R M N
inst✝⁵ : Finite ι
inst✝⁴ : CharZero R
inst✝³ : P.IsCrystallographic
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : R := (B.form (P.root i)) (P.root i)
lj : R := (B.form (P.root j)) (P.root j)
hij : li ≠ lj
key : ∀ (k : ι), (B.form (P.root k)) (P.root k) = li ∨ (B.form (P.root k)) (P.root k) = lj
k₁ k₂ : ι
h₀ : lj = 2 * li
h₁ : (B.form (P.root k₁)) (P.root k₁) = lj
h₂ : (B.form (P.root k₂)) (P.root k₂) = 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₂