mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : (e i).col (Sum.inr j) = u i
⊢ e i ^ 2 *ᵥ e i *ᵥ Pi.single (Sum.inr j) 1 = 0

Tactic:
]

Goal state after:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : (e i).col (Sum.inr j) = u i
⊢ e i ^ 2 *ᵥ e i *ᵥ Pi.single (Sum.inr j) 1 = 0
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✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
⊢ P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i = P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ ω b * (h j * f i - f i * h j) = ω b * (h j * f i - f i * h j)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -(h j * e i - e i * h j) * ω b = -(h j * e i - e i * h j) * ω b

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -(b.cartanMatrix i j • e i) * ω b = -(b.cartanMatrix i j • e i) * ω b

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_1
ι : 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✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (shortAddLong P) * (B.form (P.root (shortAddLong P))) (P.root (shortAddLong P)) =
    P.pairing i (shortAddLong P) * (B.form (P.root (shortAddLong P))) (P.root (shortAddLong P))

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_2
ι : 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✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ 2 * (B.form (P.root i)) (shortRoot P) + 2 * (B.form (P.root i)) (longRoot P) =
    2 * (B.form (P.root i)) (shortRoot P) + 2 * (B.form (P.root i)) (longRoot P)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

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✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₀ : 2 * x + -3 * y = -3 ∨ 2 * x + -3 * y = -1 ∨ 2 * x + -3 * y = 0 ∨ 2 * x + -3 * y = 1 ∨ 2 * x + -3 * y = 3
h₁ :
  2 * (x + 1) + -3 * y = -3 ∨
    2 * (x + 1) + -3 * y = -1 ∨ 2 * (x + 1) + -3 * y = 0 ∨ 2 * (x + 1) + -3 * y = 1 ∨ 2 * (x + 1) + -3 * y = 3
h₂ :
  2 * x + -3 * (y - 1) = -3 ∨
    2 * x + -3 * (y - 1) = -1 ∨ 2 * x + -3 * (y - 1) = 0 ∨ 2 * x + -3 * (y - 1) = 1 ∨ 2 * x + -3 * (y - 1) = 3
h₃ :
  2 * (x + 1) + -3 * (y - 1) = -3 ∨
    2 * (x + 1) + -3 * (y - 1) = -1 ∨
      2 * (x + 1) + -3 * (y - 1) = 0 ∨ 2 * (x + 1) + -3 * (y - 1) = 1 ∨ 2 * (x + 1) + -3 * (y - 1) = 3
hA : A = -3
⊢ False

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✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₀ : 2 * x + -3 * y = -3 ∨ 2 * x + -3 * y = -1 ∨ 2 * x + -3 * y = 0 ∨ 2 * x + -3 * y = 1 ∨ 2 * x + -3 * y = 3
h₁ :
  2 * (x + 1) + -3 * y = -3 ∨
    2 * (x + 1) + -3 * y = -1 ∨ 2 * (x + 1) + -3 * y = 0 ∨ 2 * (x + 1) + -3 * y = 1 ∨ 2 * (x + 1) + -3 * y = 3
h₂ :
  2 * x + -3 * (y - 1) = -3 ∨
    2 * x + -3 * (y - 1) = -1 ∨ 2 * x + -3 * (y - 1) = 0 ∨ 2 * x + -3 * (y - 1) = 1 ∨ 2 * x + -3 * (y - 1) = 3
h₃ :
  2 * (x + 1) + -3 * (y - 1) = -3 ∨
    2 * (x + 1) + -3 * (y - 1) = -1 ∨
      2 * (x + 1) + -3 * (y - 1) = 0 ∨ 2 * (x + 1) + -3 * (y - 1) = 1 ∨ 2 * (x + 1) + -3 * (y - 1) = 3
hA : A = -3
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j k : ι
x : ℕ
hk₁ : P.root j + (chainTopCoeff (↑i) j + 1) • P.root ↑i ∈ range ⇑P.root
hij : ↑i = (P.reflectionPerm j) j
⊢ j = -↑i

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j k : ι
x : ℕ
hk₁ : P.root j + (chainTopCoeff (↑i) j + 1) • P.root ↑i ∈ range ⇑P.root
hij : ↑i = (P.reflectionPerm j) j
⊢ j = -↑i
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_3
ι : 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✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (P.root (short P))) (P.root (short P)) +
      P.pairing i (long P) * (B.form (P.root (long P))) (P.root (long P)) =
    P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (B.form (longRoot P)) (longRoot P)

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j k : ι
x : ℕ
hk₁ : P.root j + (chainTopCoeff (↑i) j + 1) • P.root ↑i ∈ range ⇑P.root
hij : ↑i = (P.reflectionPerm j) j
⊢ j = j

Tactic:
]

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: case calc_4
ι : 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✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (3 * (B.form (shortRoot P)) (shortRoot P)) =
    (P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (shortRoot P)) (shortRoot P)

Tactic:
]

Goal state after:
case calc_4
ι : 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✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
this : Fintype ι
B : P.InvariantForm
⊢ P.pairing i (short P) * (B.form (shortRoot P)) (shortRoot P) +
      P.pairing i (long P) * (3 * (B.form (shortRoot P)) (shortRoot P)) =
    (P.pairing i (short P) + 3 * P.pairing i (long P)) * (B.form (shortRoot P)) (shortRoot P)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₀ : 2 * x + -1 * y = -3 ∨ 2 * x + -1 * y = -1 ∨ 2 * x + -1 * y = 0 ∨ 2 * x + -1 * y = 1 ∨ 2 * x + -1 * y = 3
h₁ :
  2 * (x + 1) + -1 * y = -3 ∨
    2 * (x + 1) + -1 * y = -1 ∨ 2 * (x + 1) + -1 * y = 0 ∨ 2 * (x + 1) + -1 * y = 1 ∨ 2 * (x + 1) + -1 * y = 3
h₂ :
  2 * x + -1 * (y - 1) = -3 ∨
    2 * x + -1 * (y - 1) = -1 ∨ 2 * x + -1 * (y - 1) = 0 ∨ 2 * x + -1 * (y - 1) = 1 ∨ 2 * x + -1 * (y - 1) = 3
h₃ :
  2 * (x + 1) + -1 * (y - 1) = -3 ∨
    2 * (x + 1) + -1 * (y - 1) = -1 ∨
      2 * (x + 1) + -1 * (y - 1) = 0 ∨ 2 * (x + 1) + -1 * (y - 1) = 1 ∨ 2 * (x + 1) + -1 * (y - 1) = 3
hA : A = -1
⊢ False

Tactic:
]

Goal state after:
case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₀ : 2 * x + -1 * y = -3 ∨ 2 * x + -1 * y = -1 ∨ 2 * x + -1 * y = 0 ∨ 2 * x + -1 * y = 1 ∨ 2 * x + -1 * y = 3
h₁ :
  2 * (x + 1) + -1 * y = -3 ∨
    2 * (x + 1) + -1 * y = -1 ∨ 2 * (x + 1) + -1 * y = 0 ∨ 2 * (x + 1) + -1 * y = 1 ∨ 2 * (x + 1) + -1 * y = 3
h₂ :
  2 * x + -1 * (y - 1) = -3 ∨
    2 * x + -1 * (y - 1) = -1 ∨ 2 * x + -1 * (y - 1) = 0 ∨ 2 * x + -1 * (y - 1) = 1 ∨ 2 * x + -1 * (y - 1) = 3
h₃ :
  2 * (x + 1) + -1 * (y - 1) = -3 ∨
    2 * (x + 1) + -1 * (y - 1) = -1 ∨
      2 * (x + 1) + -1 * (y - 1) = 0 ∨ 2 * (x + 1) + -1 * (y - 1) = 1 ∨ 2 * (x + 1) + -1 * (y - 1) = 3
hA : A = -1
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case calc_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -(h j * (e i * ω b)) - -(e i * (h j * ω b)) = e i * (h j * ω b) - h j * (e i * ω b)

Tactic:
]

Goal state after:
case calc_1
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -(h j * (e i * ω b)) - -(e i * (h j * ω b)) = e i * (h j * ω b) - h j * (e i * ω b)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case h.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : ¬j = -↑i
k : ι
x : ℕ
hk₁ : chainTopCoeff (↑i) j + 1 ≤ chainTopCoeff (↑i) j
hij' : LinearIndependent R ![P.root ↑i, P.root j]
⊢ False

Tactic:
]

Goal state after:
case h.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : IsDomain R
inst✝⁸ : CharZero R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.IsCrystallographic
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : ¬j = -↑i
k : ι
x : ℕ
hk₁ : chainTopCoeff (↑i) j + 1 ≤ chainTopCoeff (↑i) j
hij' : LinearIndependent R ![P.root ↑i, P.root j]
⊢ False
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✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
⊢ 2 • P.pairingIn ℤ (short P) i + 1 • P.pairingIn ℤ (long P) i =
    2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

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✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
⊢ P.root (twoShortAddLong P) = 2 • P.root (short P) + 1 • P.root (long P)

Tactic:
]

Goal state after:
ι : 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✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
⊢ 2 • P.pairingIn ℤ (short P) i + 1 • P.pairingIn ℤ (long P) i =
    2 * P.pairingIn ℤ (short P) i + P.pairingIn ℤ (long P) i

ι : 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✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
⊢ P.root (twoShortAddLong P) = 2 • P.root (short P) + 1 • P.root (long P)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case calc_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -(b.cartanMatrix i j • e i) * ω b = -b.cartanMatrix i j • (e i * ω b)

Tactic:
]

Goal state after:
case calc_2
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
⊢ -(b.cartanMatrix i j • e i) * ω b = -b.cartanMatrix i j • (e i * ω b)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₀ : 2 * x + 0 * y = -3 ∨ 2 * x + 0 * y = -1 ∨ 2 * x + 0 * y = 0 ∨ 2 * x + 0 * y = 1 ∨ 2 * x + 0 * y = 3
h₁ :
  2 * (x + 1) + 0 * y = -3 ∨
    2 * (x + 1) + 0 * y = -1 ∨ 2 * (x + 1) + 0 * y = 0 ∨ 2 * (x + 1) + 0 * y = 1 ∨ 2 * (x + 1) + 0 * y = 3
h₂ :
  2 * x + 0 * (y - 1) = -3 ∨
    2 * x + 0 * (y - 1) = -1 ∨ 2 * x + 0 * (y - 1) = 0 ∨ 2 * x + 0 * (y - 1) = 1 ∨ 2 * x + 0 * (y - 1) = 3
h₃ :
  2 * (x + 1) + 0 * (y - 1) = -3 ∨
    2 * (x + 1) + 0 * (y - 1) = -1 ∨
      2 * (x + 1) + 0 * (y - 1) = 0 ∨ 2 * (x + 1) + 0 * (y - 1) = 1 ∨ 2 * (x + 1) + 0 * (y - 1) = 3
hA : A = 0
⊢ False

Tactic:
]

Goal state after:
case inr.inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra : P.IsG2
n : ι
x y : ℤ
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
hmi' : P.root m ≠ -P.root i
hni : P.root n ≠ P.root i
hni' : P.root n ≠ -P.root i
h₀ : 2 * x + 0 * y = -3 ∨ 2 * x + 0 * y = -1 ∨ 2 * x + 0 * y = 0 ∨ 2 * x + 0 * y = 1 ∨ 2 * x + 0 * y = 3
h₁ :
  2 * (x + 1) + 0 * y = -3 ∨
    2 * (x + 1) + 0 * y = -1 ∨ 2 * (x + 1) + 0 * y = 0 ∨ 2 * (x + 1) + 0 * y = 1 ∨ 2 * (x + 1) + 0 * y = 3
h₂ :
  2 * x + 0 * (y - 1) = -3 ∨
    2 * x + 0 * (y - 1) = -1 ∨ 2 * x + 0 * (y - 1) = 0 ∨ 2 * x + 0 * (y - 1) = 1 ∨ 2 * x + 0 * (y - 1) = 3
h₃ :
  2 * (x + 1) + 0 * (y - 1) = -3 ∨
    2 * (x + 1) + 0 * (y - 1) = -1 ∨
      2 * (x + 1) + 0 * (y - 1) = 0 ∨ 2 * (x + 1) + 0 * (y - 1) = 1 ∨ 2 * (x + 1) + 0 * (y - 1) = 3
hA : A = 0
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
⊢ k ≠ ↑i ∧ P.root k ≠ -P.root ↑i

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
⊢ k ≠ ↑i ∧ P.root k ≠ -P.root ↑i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
⊢ ¬k = (P.reflectionPerm ↑i) ↑i

Tactic:
]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
⊢ ¬k = (P.reflectionPerm ↑i) ↑i