Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas

Goal state before:
pp: case 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
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root i')) (P.root i')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root i')) (P.root i')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

pp: case 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
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root i')) (P.root i')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root j')) (P.root j')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

pp: case 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
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root j')) (P.root j')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root i')) (P.root i')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

pp: case 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
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root j')) (P.root j')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root j')) (P.root j')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

Tactic:
<;>

Goal state after:
case 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
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root i')) (P.root i')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root i')) (P.root i')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

case 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
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root i')) (P.root i')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root j')) (P.root j')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

case 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
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root j')) (P.root j')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root i')) (P.root i')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

case 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
i j : ι
inst✝² : IsDomain R
inst✝¹ : P.IsReduced
B : P.InvariantForm
inst✝ : P.IsIrreducible
h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)
k : ι
this : Nonempty ι
i' j' : ι
h' :
  (B.form (P.root k)) (P.root k) = (B.form (P.root i')) (P.root i') ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j')) (P.root j')
hi : (B.form (P.root i)) (P.root i) = (B.form (P.root j')) (P.root j')
hj : (B.form (P.root j)) (P.root j) = (B.form (P.root j')) (P.root j')
⊢ (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨
    (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)