awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 k : ι
x : ℕ
hk₁ :
  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) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j + 1)
        ((P.root : (a : ι) → M) (↑i : ι) : M)))
hij : (↑i : ι) = (P.reflectionPerm j : (a : ι) → ι) j
⊢ j = -(↑i : ι)
have rw : j = -(P.reflectionPerm j : (a : ι) → ι) j
Tactic: rw [hij, ← indexNeg_neg, neg_neg]
-- 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
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 k : ι
x : ℕ
hk₁ :
  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) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j + 1)
        ((P.root : (a : ι) → M) (↑i : ι) : M)))
hij : (↑i : ι) = (P.reflectionPerm j : (a : ι) → ι) j
rw : j = -(P.reflectionPerm j : (a : ι) → ι) j
⊢ j = -(↑i : ι)
have rw₁ : j = - -j
Tactic: rw [hij, ← indexNeg_neg, neg_neg]
-- 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
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 k : ι
x : ℕ
hk₁ :
  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) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j + 1)
        ((P.root : (a : ι) → M) (↑i : ι) : M)))
hij : (↑i : ι) = (P.reflectionPerm j : (a : ι) → ι) j
rw : j = -(P.reflectionPerm j : (a : ι) → ι) j
rw₁ : j = - -j
⊢ j = -(↑i : ι)
have rw₂ : j = j
Tactic: rw [hij, ← indexNeg_neg, neg_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
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 : ι
x : ℕ
hk₁ :
  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) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j + 1)
        ((P.root : (a : ι) → M) (↑i : ι) : M)))
⊢ False
have hij' : LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
  (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
Tactic: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
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 : ι
x : ℕ
hk₁ :
  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) (chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j + 1)
        ((P.root : (a : ι) → M) (↑i : ι) : M)))
hij' :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) (↑i : ι), (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
⊢ False
have hk₂ : chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j + 1 ≤
  chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j
Tactic: rw [root_add_nsmul_mem_range_iff_le_chainTopCoeff hij'] at hk₁
Cleared hypotheses: hk₁, hij'
-- 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
⊢ IsNilpotent (e i)
have have : ∀ (this : Module.IsReflexive R M), 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
-- 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
have have₁ have₂ : ∀ (this : Module.IsReflexive R M), IsNilpotent (e i)
⊢ IsNilpotent (e i)
have have₃ : ∀ (this : Module.IsReflexive R M) (this : IsAddTorsionFree M), 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
-- 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
have have₁ have₂ : ∀ (this : Module.IsReflexive R M), IsNilpotent (e i)
have₃ have₄ : ∀ (this : Module.IsReflexive R M) (this : IsAddTorsionFree M), IsNilpotent (e i)
⊢ IsNilpotent (e i)
have have₅ : ∀ (this : Module.IsReflexive R M) (this : IsAddTorsionFree M) (i_1 : ↥b.support ⊕ ι), ∃ (n : ℕ), (e i ^ n).col i_1 = 0
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
-- 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
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
⊢ IsNilpotent (e i)
have 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
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
-- 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
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
⊢ IsNilpotent (e i)
have 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
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
-- 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
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
⊢ IsNilpotent (e i)
have 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
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
-- 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
⊢ IsNilpotent (f i)
have obtain : ∀ (n : ℕ) (hn : e i ^ n = 0), IsNilpotent (f i)
Tactic: obtain ⟨n, hn⟩ := isNilpotent_e i
-- 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
n : ℕ
hn : e i ^ n = 0
⊢ IsNilpotent (f i)
have suffices : ω b * f i ^ n = 0
Tactic: suffices (ω b) * (f i ^ n) = 0 from ⟨n, by simpa [← mul_assoc] using congr_arg (ω b * ·) this⟩
-- 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
n : ℕ
hn : e i ^ n = 0
⊢ ω b * f i ^ n = 0
have suffices : ω b * f i ^ n = e i ^ n * ω b
Tactic: suffices (ω b) * (f i ^ n) = (e i ^ n) * (ω b) by simp [this, hn]