-- 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
have have₁ have₂ : ∀ (this : Module.IsReflexive R M), IsNilpotent (e i)
have₃ have₄ : ∀ (this : Module.IsReflexive R M) (this : IsAddTorsionFree M), IsNilpotent (e i)
have₅ :
  ∀ (this : Module.IsReflexive R M) (this : IsAddTorsionFree M) (i_1 : ↥b.support ⊕ ι), ∃ (n : ℕ), (e i ^ n).col i_1 = 0
have₆ :
  ∀ (this : Module.IsReflexive R M) (this : IsAddTorsionFree M)
    (case_inl : ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0) (i_1 : ↥b.support ⊕ ι),
    ∃ (n : ℕ), (e i ^ n).col i_1 = 0
inl :
  ∀ (this : Module.IsReflexive R M) (this : IsAddTorsionFree M)
    (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
inr inr₁ :
  ∀ (this : Module.IsReflexive R M) (this : IsAddTorsionFree M)
    (case_inl : ∀ (j : ↥b.support), (HPow.hPow (β := ℕ) (e i) 2).col (Sum.inl j) = 0) (j : ι),
    ∃ (n : ℕ), (e i ^ n).col (Sum.inr j) = 0
⊢ IsNilpotent (e i)

Tactic:
classical
  have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
  have : IsAddTorsionFree M := .of_isTorsionFree R M
  letI := P.indexNeg
  rw [Matrix.isNilpotent_iff_forall_col]
  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]
  rintro (j | j)
  · exact ⟨2, case_inl j⟩
  · by_cases hij : j = -i
    · use 2 + 1
      replace hij : (e i).col (Sum.inr j) = u i := by
        ext (k | k)
        · simp [e, -indexNeg_neg, Pi.single_apply, hij]
        · have hk : P.root k ≠ P.root i + P.root j := by simp [hij, P.ne_zero k]
          simp [e, -indexNeg_neg, hk]
      rw [pow_succ, ← Matrix.mulVec_single_one, ← Matrix.mulVec_mulVec]
      simp [hij, case_inl i]
    use P.chainTopCoeff i j + 1
    rcases isNilpotent_e_aux i (P.chainTopCoeff i j + 1) hij with this | ⟨k, x, hk₁, -⟩
    · assumption
    exfalso
    replace hk₁ : P.root j + (P.chainTopCoeff i j + 1) • P.root i ∈ range P.root := ⟨k, hk₁⟩
    have hij' : LinearIndependent R ![P.root i, P.root j] := by
      apply IsReduced.linearIndependent P ?_ ?_
      · rintro rfl
        apply P.nsmul_notMem_range_root (n := P.chainTopCoeff i i + 2) (i := i)
        convert! hk₁ using 1
        module
      · contrapose hij
        rw [root_eq_neg_iff] at hij
        rw [hij, ← indexNeg_neg, neg_neg]
    rw [root_add_nsmul_mem_range_iff_le_chainTopCoeff hij'] at hk₁
    lia

Premises used: Matrix.mulVec_single_one, pow_succ, Matrix.isNilpotent_iff_forall_col, Matrix.mulVec_mulVec