awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
hk₂ :
  (e i ^ n).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
hki : k ≠ -(↑i : ι)
hij :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
l : ↥b.support
⊢ (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inl l) = 0 (Sum.inl l)

Tactic:
simp [e, -indexNeg_neg, hki]

Premises used: RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
hk₂ :
  (e i ^ n).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
hki : k ≠ -(↑i : ι)
hij :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
l : ι
contra :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)
rw :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
        (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))
⊢ (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))

Tactic:
rw [contra, hk₁]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
hk₂ :
  (e i ^ n).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
hki : k ≠ -(↑i : ι)
hij :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
l : ι
contra :
  (P.root : (a : ι) → M) l =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)
⊢ HAdd.hAdd (α := M) ((P.root : (a : ι) → M) (↑i : ι) : M)
      (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
        (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))) =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M))

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
hk₂ :
  (e i ^ n).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
hki : k ≠ -(↑i : ι)
hij :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∉
    range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)
l : ι
⊢ (P.root : (a : ι) → M) l ≠
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)

Tactic:
replace hij : P.root l ≠ P.root i + P.root k :=
          fun contra ↦ hij ⟨l, by rw [contra, hk₁]; module⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -(↑i : ι)
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
hk₂ :
  (e i ^ n).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
hki : k ≠ -(↑i : ι)
l : ι
hij :
  (P.root : (a : ι) → M) l ≠
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M)
⊢ (x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1) (Sum.inr l) = 0 (Sum.inr l)

Tactic:
simp [e, -indexNeg_neg, hij]

Premises used: RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this : Module.IsReflexive R M
⊢ IsAddTorsionFree M

Tactic:
have : IsAddTorsionFree M := .of_isTorsionFree R M
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
rw : ∀ (i_1 : ↥b.support ⊕ ι), ∃ (n : ℕ), (e i ^ n).col i_1 = 0
⊢ IsNilpotent (e i)

Tactic:
rw [Matrix.isNilpotent_iff_forall_col]

Premises used: Matrix.isNilpotent_iff_forall_col
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
h : ∀ (k : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) (Sum.inl k) = 0 (Sum.inl k)
h₁ : ∀ (k : ι), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) (Sum.inr k) = 0 (Sum.inr k)
⊢ (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0

Tactic:
ext (k | k)
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j k : ↥b.support
⊢ (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) (Sum.inl k) = 0 (Sum.inl k)

Tactic:
simp [e, sq, ne_neg P i, -indexNeg_neg]

Premises used: sq, RootPairing.ne_neg, RootPairing.indexNeg_neg, Subtype.val, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this_3 : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
this : (P.root : (a : ι) → M) k ≠ HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      ¬(x = (↑i : ι) ∧
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))

Tactic:
simpa [two_smul]

Premises used: two_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
suffices : (P.root : (a : ι) → M) k ≠ HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      ¬(x = (↑i : ι) ∧
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))

Tactic:
suffices P.root k ≠ (2 : ℕ) • P.root i by simpa [two_smul]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
⊢ (P.root : (a : ι) → M) k ≠ HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
fun contra ↦ P.nsmul_notMem_range_root (n := 2) (i := i) ⟨k, contra⟩

Premises used: Exists.intro, RootPairing.nsmul_notMem_range_root, Not
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
⊢ (P.root : (a : ι) → M) k ≠ HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
exact fun contra ↦ P.nsmul_notMem_range_root (n := 2) (i := i) ⟨k, contra⟩

Premises used: Exists.intro, RootPairing.nsmul_notMem_range_root
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
⊢ ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      ¬(x = (↑i : ι) ∧
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))

Tactic:
have aux : ∀ x : ι, x ∈ Finset.univ → ¬ (x = i ∧ P.root k = P.root i + P.root x) := by
        suffices P.root k ≠ (2 : ℕ) • P.root i by simpa [two_smul]
        exact fun contra ↦ P.nsmul_notMem_range_root (n := 2) (i := i) ⟨k, contra⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
j : ↥b.support
k : ι
aux :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      ¬(x = (↑i : ι) ∧
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M))
⊢ (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) (Sum.inr k) = 0 (Sum.inr k)

Tactic:
simp [e, sq, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux]

Premises used: sq, Finset.sum_ite_of_false, ite_and, RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
⊢ ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0

Tactic:
have case_inl (j : b.support) : (e i ^ 2).col (Sum.inl j) = 0 := by
    ext (k | k)
    · simp [e, sq, ne_neg P i, -indexNeg_neg]
    · have aux : ∀ x : ι, x ∈ Finset.univ → ¬ (x = i ∧ P.root k = P.root i + P.root x) := by
        suffices P.root k ≠ (2 : ℕ) • P.root i by simpa [two_smul]
        exact fun contra ↦ P.nsmul_notMem_range_root (n := 2) (i := i) ⟨k, contra⟩
      simp [e, sq, -indexNeg_neg, ← ite_and, Finset.sum_ite_of_false aux]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0
j : ↥b.support
⊢ ∃ (n : ℕ), (e i ^ n).col (Sum.inl j) = 0

Tactic:
⟨2, case_inl j⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0
j : ↥b.support
⊢ ∃ (n : ℕ), (e i ^ n).col (Sum.inl j) = 0

Tactic:
exact ⟨2, case_inl j⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0
j : ι
pos : ∀ (hij : j = -(↑i : ι)), ∃ (n : ℕ), (e i ^ n).col (Sum.inr j) = 0
neg : ∀ (hij : ¬j = -(↑i : ι)), ∃ (n : ℕ), (e i ^ n).col (Sum.inr j) = 0
⊢ ∃ (n : ℕ), (e i ^ n).col (Sum.inr j) = 0

Tactic:
by_cases hij : j = -i
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0
j : ι
hij : j = -(↑i : ι)
h : (e i ^ HAdd.hAdd (α := ℕ) 2 1).col (Sum.inr j) = 0
⊢ ∃ (n : ℕ), (e i ^ n).col (Sum.inr j) = 0

Tactic:
use 2 + 1
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0
j : ι
hij : j = -(↑i : ι)
h : ∀ (k : ↥b.support), (e i).col (Sum.inr j) (Sum.inl k) = u i (Sum.inl k)
h₁ : ∀ (k : ι), (e i).col (Sum.inr j) (Sum.inr k) = u i (Sum.inr k)
⊢ (e i).col (Sum.inr j) = u i

Tactic:
ext (k | k)
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0
j : ι
hij : j = -(↑i : ι)
k : ↥b.support
⊢ (e i).col (Sum.inr j) (Sum.inl k) = u i (Sum.inl k)

Tactic:
simp [e, -indexNeg_neg, Pi.single_apply, hij]

Premises used: Pi.single_apply, RootPairing.indexNeg_neg, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0
j : ι
hij : j = -(↑i : ι)
k : ι
⊢ (P.root : (a : ι) → M) k ≠
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) j : M)

Tactic:
simp [hij, P.ne_zero k]

Premises used: RootPairing.ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : IsDomain R
inst_2 : CharZero R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : P.IsCrystallographic
inst_8 : P.IsReduced
b : P.Base
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
this_1 : Module.IsReflexive R M
this_2 : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0
j : ι
hij : j = -(↑i : ι)
k : ι
⊢ (P.root : (a : ι) → M) k ≠
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) j : M)

Tactic:
have hk : P.root k ≠ P.root i + P.root j := by simp [hij, P.ne_zero k]