Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : 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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
x : M
hx :
  x = longRoot P ∨
    x = -longRoot P ∨
      x = shortRoot P ∨
        x = -shortRoot P ∨
          x = shortAddLongRoot P ∨
            x = -shortAddLongRoot P ∨
              x = twoShortAddLongRoot P ∨
                x = -twoShortAddLongRoot P ∨
                  x = threeShortAddLongRoot P ∨
                    x = -threeShortAddLongRoot P ∨ x = threeShortAddTwoLongRoot P ∨ x = -threeShortAddTwoLongRoot P
⊢ x ∈ Set.range ⇑P.root

Tactic:
rcases hx with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl

Goal state after:
case 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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ longRoot P ∈ Set.range ⇑P.root

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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ -longRoot P ∈ Set.range ⇑P.root

case 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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ shortRoot P ∈ Set.range ⇑P.root

case inr.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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ -shortRoot P ∈ Set.range ⇑P.root

case inr.inr.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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ shortAddLongRoot P ∈ Set.range ⇑P.root

case inr.inr.inr.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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ -shortAddLongRoot P ∈ Set.range ⇑P.root

case inr.inr.inr.inr.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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ twoShortAddLongRoot P ∈ Set.range ⇑P.root

case inr.inr.inr.inr.inr.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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ -twoShortAddLongRoot P ∈ Set.range ⇑P.root

case inr.inr.inr.inr.inr.inr.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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ threeShortAddLongRoot P ∈ Set.range ⇑P.root

case inr.inr.inr.inr.inr.inr.inr.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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ -threeShortAddLongRoot P ∈ Set.range ⇑P.root

case inr.inr.inr.inr.inr.inr.inr.inr.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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ threeShortAddTwoLongRoot P ∈ Set.range ⇑P.root

case inr.inr.inr.inr.inr.inr.inr.inr.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✝¹ : P.EmbeddedG2
inst✝ : DecidableEq M
⊢ -threeShortAddTwoLongRoot P ∈ Set.range ⇑P.root