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 x : ℕ
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 (-(↑i : ι))) 1)
hk₁ :
  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))) =
    0
rw :
  HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HAdd.hAdd (β := M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
        ((P.root : (a : ι) → M) (↑i : ι) : 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)
      (HAdd.hAdd (β := M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
        ((P.root : (a : ι) → M) (↑i : ι) : M)) =
    0

Tactic:
rw [← 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 x : ℕ
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 (-(↑i : ι))) 1)
hk₁ :
  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))) =
    0
⊢ HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HAdd.hAdd (β := M) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M))
        ((P.root : (a : ι) → M) (↑i : ι) : 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)))

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 x : ℕ
hk₁ :
  (P.root : (a : ι) → M) (-(↑i : ι)) =
    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 (-(↑i : ι))) 1)
⊢ (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)

Tactic:
replace hk₁ : P.root (-j) = (n + 1) • P.root i := by
        simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self, neg_eq_iff_add_eq_zero,
          add_smul, one_smul] at hk₁ ⊢
        rw [← 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 x : ℕ
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 (-(↑i : ι))) 1)
hk₁ : (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)
inl :
  ∀
    (hk₂ :
      (HPow.hPow (β := ℕ) (e i) 0).col (Sum.inr j) =
        HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x
          (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr (-(↑i : ι))) 1))
    (hk₁ :
      (P.root : (a : ι) → M) (-j) =
        HSMul.hSMul (β := M) (HAdd.hAdd (α := ℕ) 0 1) ((P.root : (a : ι) → M) (↑i : ι) : M)),
    False
inr : ∀ (hn : n > 0), False
⊢ False

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- 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)
x : ℕ
hk₂ :
  (HPow.hPow (β := ℕ) (e i) 0).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr (-(↑i : ι))) 1)
hk₁ : (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (HAdd.hAdd (α := ℕ) 0 1) ((P.root : (a : ι) → M) (↑i : ι) : M)
inl : j = -(↑i : ι)
⊢ False

Tactic:
apply h
-- 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)
x : ℕ
hk₂ :
  (HPow.hPow (β := ℕ) (e i) 0).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr (-(↑i : ι))) 1)
hk₁ : (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (HAdd.hAdd (α := ℕ) 0 1) ((P.root : (a : ι) → M) (↑i : ι) : M)
⊢ -j = (↑i : ι)

Tactic:
rw [zero_add, one_smul, EmbeddingLike.apply_eq_iff_eq] at hk₁

Premises used: EmbeddingLike.apply_eq_iff_eq, zero_add, one_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
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)
x : ℕ
hk₂ :
  (HPow.hPow (β := ℕ) (e i) 0).col (Sum.inr j) =
    HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x
      (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr (-(↑i : ι))) 1)
hk₁ : -j = (↑i : ι)
⊢ j = -(↑i : ι)

Tactic:
simp [← hk₁, -indexNeg_neg]

Premises used: RootPairing.indexNeg_neg
-- 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 x : ℕ
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 (-(↑i : ι))) 1)
hk₁ : (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)
hn : n > 0
⊢ 2 ≤ n + 1

Tactic:
lia
-- 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 x : ℕ
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 (-(↑i : ι))) 1)
hk₁ : (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)
hn : n > 0
⊢ (n + 1).AtLeastTwo

Tactic:
have _i : (n + 1).AtLeastTwo := ⟨by lia⟩
-- 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 x : ℕ
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 (-(↑i : ι))) 1)
hk₁ : (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)
hn : n > 0
_i : (n + 1).AtLeastTwo
⊢ False

Tactic:
P.nsmul_notMem_range_root (n := n + 1) (i := i) ⟨-j, hk₁⟩

Premises used: Exists.intro, RootPairing.nsmul_notMem_range_root, Neg.neg
-- 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 x : ℕ
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 (-(↑i : ι))) 1)
hk₁ : (P.root : (a : ι) → M) (-j) = HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)
hn : n > 0
_i : (n + 1).AtLeastTwo
⊢ False

Tactic:
exact P.nsmul_notMem_range_root (n := n + 1) (i := i) ⟨-j, hk₁⟩

Premises used: Exists.intro, RootPairing.nsmul_notMem_range_root, Neg.neg
-- 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)
⊢ k ≠ -(↑i : ι)

Tactic:
have hki : k ≠ -i := by
      rintro rfl
      replace hk₁ : P.root (-j) = (n + 1) • P.root i := by
        simp only [indexNeg_neg, root_reflectionPerm, reflection_apply_self, neg_eq_iff_add_eq_zero,
          add_smul, one_smul] at hk₁ ⊢
        rw [← hk₁]
        module
      rcases n.eq_zero_or_pos with rfl | hn
      · apply h
        rw [zero_add, one_smul, EmbeddingLike.apply_eq_iff_eq] at hk₁
        simp [← hk₁, -indexNeg_neg]
      · have _i : (n + 1).AtLeastTwo := ⟨by lia⟩
        exact P.nsmul_notMem_range_root (n := n + 1) (i := i) ⟨-j, 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 : ι)
pos :
  ∀
    (hij :
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
          (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)))),
    x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 = 0 ∨
      ∃ (k_1 : ι) (x_1 : ℕ),
        (P.root : (a : ι) → M) k_1 =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
          x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
            HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x_1
              (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k_1) 1)
neg :
  ∀
    (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)),
    x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 = 0 ∨
      ∃ (k_1 : ι) (x_1 : ℕ),
        (P.root : (a : ι) → M) k_1 =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
          x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
            HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x_1
              (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k_1) 1)
⊢ x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 = 0 ∨
    ∃ (k_1 : ι) (x_1 : ℕ),
      (P.root : (a : ι) → M) k_1 =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x_1
            (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k_1) 1)

Tactic:
by_cases hij : P.root j + (n + 1) • P.root i ∈ range P.root

Premises used: RootPairing.root, HAdd.hAdd, Set.range, OfNat.ofNat, Subtype.val, DFunLike.coe
-- 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 :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)))
pos :
  ∀ (l : ι)
    (hl :
      (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))),
    x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 = 0 ∨
      ∃ (k_1 : ι) (x_1 : ℕ),
        (P.root : (a : ι) → M) k_1 =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
          x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
            HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x_1
              (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k_1) 1)
⊢ x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 = 0 ∨
    ∃ (k_1 : ι) (x_1 : ℕ),
      (P.root : (a : ι) → M) k_1 =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x_1
            (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k_1) 1)

Tactic:
obtain ⟨l, hl⟩ := hij
-- 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 : ι
hl :
  (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))
pos :
  ∃ (k_1 : ι) (x_1 : ℕ),
    (P.root : (a : ι) → M) k_1 =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
          (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
      x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
        HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x_1 (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k_1) 1)
⊢ x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 = 0 ∨
    ∃ (k_1 : ι) (x_1 : ℕ),
      (P.root : (a : ι) → M) k_1 =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x_1
            (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k_1) 1)

Tactic:
right
-- 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 : ι
hl :
  (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))
⊢ ∃ (k_1 : ι) (x_1 : ℕ),
    (P.root : (a : ι) → M) k_1 =
        HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
          (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
      x • e i *ᵥ Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1 =
        HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x_1 (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k_1) 1)

Tactic:
⟨l, x * (P.chainBotCoeff i k + 1), hl, ?_⟩

Premises used: HMul.hMul, RootPairing.chainBotCoeff, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Subtype.val