Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: 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

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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

pp: 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

Tactic:
<;>

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