-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
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 : ι
n : ℕ
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)
zero :
  (HPow.hPow (β := ℕ) (e i) 0).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (α := ℕ) (β := M) 0 ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (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 k) 1)
⊢ (e i ^ n).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (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)
have succ : ∀ (n : ℕ)
  (ih :
    (e i ^ n).col (Sum.inr j) = 0 ∨
      ∃ (k : ι) (x : ℕ),
        (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
              (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
          (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)),
  (e i ^ (n + 1)).col (Sum.inr j) = 0 ∨
    ∃ (k : ι) (x : ℕ),
      (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) ((P.root : (a : ι) → M) j : M)
            (HSMul.hSMul (β := M) (n + 1) ((P.root : (a : ι) → M) (↑i : ι) : M)) ∧
        (e i ^ (n + 1)).col (Sum.inr j) =
          HSMul.hSMul (β := (j : ↥b.support ⊕ ι) → R) x (Pi.single (M := fun (a : ↥b.support ⊕ ι) ↦ R) (Sum.inr k) 1)
Tactic: induction n with
  | zero => exact Or.inr ⟨j, 1, by simp, by ext; simp [Pi.single_apply]⟩
  | succ n ih =>
    rcases ih with hn | ⟨k, x, hk₁, hk₂⟩
    · left; simp [aux, hn]
    rw [aux, hk₂, Matrix.mulVec_smul]
    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₁⟩
    by_cases hij : P.root j + (n + 1) • P.root i ∈ range P.root
    · obtain ⟨l, hl⟩ := hij
      right
      refine ⟨l, x * (P.chainBotCoeff i k + 1), hl, ?_⟩
      ext (m | m)
      · simp [e, -indexNeg_neg, hki]
      · rcases eq_or_ne m l with rfl | hml
        · replace hl : P.root m = P.root i + P.root k := by rw [hl, hk₁]; module
          simp [e, -indexNeg_neg, hl, mul_add]
        · replace hl : P.root m ≠ P.root i + P.root k :=
            fun contra ↦ hml (P.root.injective <| by rw [hl, contra, hk₁]; module)
          simp [e, -indexNeg_neg, hml, hl]
    · left
      ext (l | l)
      · simp [e, -indexNeg_neg, hki]
      · replace hij : P.root l ≠ P.root i + P.root k :=
          fun contra ↦ hij ⟨l, by rw [contra, hk₁]; module⟩
        simp [e, -indexNeg_neg, hij]
Cleared hypotheses: n