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
obtain : ∀ (n : ℕ) (hn : e i ^ n = 0), IsNilpotent (f i)
⊢ IsNilpotent (f i)

Tactic:
obtain ⟨n, hn⟩ := isNilpotent_e i

Premises used: RootPairing.GeckConstruction.isNilpotent_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
n : ℕ
hn : e i ^ n = 0
this : ω b * f i ^ n = 0
⊢ f i ^ n = 0

Tactic:
simpa [← mul_assoc] using congr_arg (ω b * ·) this

Premises used: HMul.hMul, RootPairing.GeckConstruction.ω, mul_assoc, congr_arg
-- 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
n : ℕ
hn : e i ^ n = 0
suffices : ω b * f i ^ n = 0
⊢ IsNilpotent (f i)

Tactic:
suffices (ω b) * (f i ^ n) = 0 from ⟨n, by simpa [← mul_assoc] using congr_arg (ω b * ·) this⟩
-- 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
n : ℕ
hn : e i ^ n = 0
this : ω b * f i ^ n = e i ^ n * ω b
⊢ ω b * f i ^ n = 0

Tactic:
simp [this, hn]
-- 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
n : ℕ
hn : e i ^ n = 0
suffices : ω b * f i ^ n = e i ^ n * ω b
⊢ ω b * f i ^ n = 0

Tactic:
suffices (ω b) * (f i ^ n) = (e i ^ n) * (ω b) by simp [this, hn]
-- 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
⊢ ω b * HPow.hPow (β := ℕ) (f i) 0 = HPow.hPow (β := ℕ) (e i) 0 * ω b

Tactic:
simp
-- 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
n : ℕ
ih : ω b * f i ^ n = e i ^ n * ω b
succ : ω b * (f i ^ n * f i) = e i ^ (n + 1) * ω b
succ₁ : ω b * (f i ^ n * f i) = e i ^ n * e i * ω b
succ₂ : ω b * f i ^ n * f i = e i ^ n * e i * ω b
succ₃ : e i ^ n * ω b * f i = e i ^ n * e i * ω b
succ₄ : e i ^ n * (ω b * f i) = e i ^ n * e i * ω b
succ₅ : e i ^ n * (e i * ω b) = e i ^ n * e i * ω b
succ₆ succ₇ : e i ^ n * e i * ω b = e i ^ n * e i * ω b
⊢ ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b

Tactic:
rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]

Premises used: pow_succ, mul_assoc, RootPairing.GeckConstruction.ω_mul_f
-- 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
n : ℕ
zero : ω b * HPow.hPow (β := ℕ) (f i) 0 = HPow.hPow (β := ℕ) (e i) 0 * ω b
succ : ∀ (n : ℕ) (ih : ω b * f i ^ n = e i ^ n * ω b), ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b
⊢ ω b * f i ^ n = e i ^ n * ω b

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]

Premises used: pow_succ, mul_assoc, RootPairing.GeckConstruction.ω_mul_f, Submodule.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 : CharZero R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsCrystallographic
b : P.Base
inst_7 : Fintype ι
i : ↥b.support
_i : InvolutiveNeg ι := P.indexNeg
this : Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ j (↑i : ι)) 0
simp : Eq.{u_2 + 1} (α := R) (∑ x : ι, (↑(P.pairingIn ℤ x (↑i : ι)) : R)) 0
⊢ (h i).trace = 0

Tactic:
simp only [h_eq_diagonal, Matrix.trace_diagonal, Fintype.sum_sum_type, Finset.univ_eq_attach,
      Sum.elim_inl, Pi.zero_apply, Finset.sum_const_zero, Sum.elim_inr, zero_add]

Premises used: Fintype.sum_sum_type, Matrix.trace_diagonal, Pi.zero_apply, zero_add, Finset.sum_const_zero, Sum.elim_inr, Finset.univ_eq_attach, Sum.elim_inl, RootPairing.GeckConstruction.h_eq_diagonal
-- 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 : CharZero R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsCrystallographic
b : P.Base
inst_7 : Fintype ι
i : ↥b.support
_i : InvolutiveNeg ι := P.indexNeg
this : Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ j (↑i : ι)) 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : Eq (α := ℤ) (∑ x : ι, P.pairingIn ℤ x (↑i : ι)) 0
⊢ Eq.{u_2 + 1} (α := R) (∑ x : ι, (↑(P.pairingIn ℤ x (↑i : ι)) : R)) 0

Tactic:
norm_cast
-- 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 : CharZero R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsCrystallographic
b : P.Base
inst_7 : Fintype ι
i : ↥b.support
_i : InvolutiveNeg ι := P.indexNeg
suffices : Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ j (↑i : ι)) 0
⊢ (h i).trace = 0

Tactic:
suffices ∑ j, P.pairingIn ℤ j i = 0 by
    simp only [h_eq_diagonal, Matrix.trace_diagonal, Fintype.sum_sum_type, Finset.univ_eq_attach,
      Sum.elim_inl, Pi.zero_apply, Finset.sum_const_zero, Sum.elim_inr, zero_add]
    norm_cast
-- 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 : CharZero R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsCrystallographic
b : P.Base
inst_7 : Fintype ι
i : ↥b.support
_i : InvolutiveNeg ι := P.indexNeg
this : Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ (-j) (↑i : ι)) (∑ j : ι, P.pairingIn ℤ j (↑i : ι))
⊢ Eq (α := ℤ) (-∑ j : ι, P.pairingIn ℤ j (↑i : ι)) (∑ j : ι, P.pairingIn ℤ j (↑i : ι))

Tactic:
simpa using this
-- 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 : CharZero R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsCrystallographic
b : P.Base
inst_7 : Fintype ι
i : ↥b.support
_i : InvolutiveNeg ι := P.indexNeg
suffices : Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ (-j) (↑i : ι)) (∑ j : ι, P.pairingIn ℤ j (↑i : ι))
⊢ Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ j (↑i : ι)) 0

Tactic:
suffices ∑ j, P.pairingIn ℤ (-j) i = ∑ j, P.pairingIn ℤ j i from
    eq_zero_of_neg_eq <| by simpa using this
-- 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 : CharZero R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsCrystallographic
b : P.Base
inst_7 : Fintype ι
i : ↥b.support
_i : InvolutiveNeg ι := P.indexNeg
σ : ι ≃ ι := Involutive.toPerm Neg.neg ⋯
⊢ Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ (-j) (↑i : ι)) (∑ j : ι, P.pairingIn ℤ j (↑i : ι))

Tactic:
σ.sum_comp (P.pairingIn ℤ · i)

Premises used: Equiv.sum_comp, RootPairing.pairingIn, Int, Subtype.val
-- 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 : CharZero R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsCrystallographic
b : P.Base
inst_7 : Fintype ι
i : ↥b.support
_i : InvolutiveNeg ι := P.indexNeg
σ : ι ≃ ι := Involutive.toPerm Neg.neg ⋯
⊢ Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ (-j) (↑i : ι)) (∑ j : ι, P.pairingIn ℤ j (↑i : ι))

Tactic:
exact σ.sum_comp (P.pairingIn ℤ · i)

Premises used: Equiv.sum_comp, RootPairing.pairingIn, Int, Subtype.val
-- 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 : CharZero R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsCrystallographic
b : P.Base
inst_7 : Fintype ι
i : ↥b.support
letI letI₁ letI₂ : (h i).trace = 0
letI₃ : Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ j (↑i : ι)) 0
letI₄ :
  let _i := P.indexNeg;
  Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ (-j) (↑i : ι)) (∑ j : ι, P.pairingIn ℤ j (↑i : ι))
letI₅ :
  let _i := P.indexNeg;
  Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ (-j) (↑i : ι)) (∑ j : ι, P.pairingIn ℤ j (↑i : ι))
⊢ (h i).trace = 0

Tactic:
classical
  letI _i := P.indexNeg
  suffices ∑ j, P.pairingIn ℤ j i = 0 by
    simp only [h_eq_diagonal, Matrix.trace_diagonal, Fintype.sum_sum_type, Finset.univ_eq_attach,
      Sum.elim_inl, Pi.zero_apply, Finset.sum_const_zero, Sum.elim_inr, zero_add]
    norm_cast
  suffices ∑ j, P.pairingIn ℤ (-j) i = ∑ j, P.pairingIn ℤ j i from
    eq_zero_of_neg_eq <| by simpa using this
  let σ : ι ≃ ι := Function.Involutive.toPerm _ neg_involutive
  exact σ.sum_comp (P.pairingIn ℤ · 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 ι
x : ↥(lieAlgebra b)
obtain :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (hx :
      Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
        x),
    Eq.{u_2 + 1} (α := R)
      ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
          (((toEnd R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R) : ↥(lieAlgebra b) →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
                (a : ↥(lieAlgebra b)) → Module.End R (↥b.support ⊕ ι → R))
              (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
                Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
                  (lieAlgebra b) x)
                x hx) :
            Module.End R (↥b.support ⊕ ι → R)) :
        R)
      (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
        (((toEnd R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R) : ↥(lieAlgebra b) →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
              (a : ↥(lieAlgebra b)) → Module.End R (↥b.support ⊕ ι → R))
            x :
          Module.End R (↥b.support ⊕ ι → R)) :
      R)
    (0 : R)

Tactic:
obtain ⟨x, hx⟩ := x
-- 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 ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
this :
  Eq.{u_2 + 1} (α := R)
    ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
        ((Matrix.toLin' :
              (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R)
            x :
          (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) :
      R)
    (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
        (((toEnd R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R) : ↥(lieAlgebra b) →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
              (a : ↥(lieAlgebra b)) → Module.End R (↥b.support ⊕ ι → R))
            (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
              Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
                (lieAlgebra b) x)
              x hx) :
          Module.End R (↥b.support ⊕ ι → R)) :
      R)
    (0 : R)

Tactic:
simpa
-- 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 ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
suffices :
  Eq.{u_2 + 1} (α := R)
    ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
        ((Matrix.toLin' :
              (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R)
            x :
          (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) :
      R)
    (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
        (((toEnd R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R) : ↥(lieAlgebra b) →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
              (a : ↥(lieAlgebra b)) → Module.End R (↥b.support ⊕ ι → R))
            (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
              Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
                (lieAlgebra b) x)
              x hx) :
          Module.End R (↥b.support ⊕ ι → R)) :
      R)
    (0 : R)

Tactic:
suffices trace R _ x.toLin' = 0 by simpa
-- 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 ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
        ((Matrix.toLin' :
              (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R)
            x :
          (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) :
      R)
    (0 : R)

Tactic:
LieAlgebra.trace_toEnd_eq_zero ?_ hx

Premises used: LieAlgebra.trace_toEnd_eq_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 ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
refine :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
    Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
        (Set.range h ∪ Set.range e ∪ Set.range f) x →
      Eq.{u_2 + 1} (α := R)
        ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
            (((toEnd R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (↥b.support ⊕ ι → R) :
                    Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R →ₗ⁅R⁆
                      Module.End R (↥b.support ⊕ ι → R)) :
                  (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Module.End R (↥b.support ⊕ ι → R))
                x :
              Module.End R (↥b.support ⊕ ι → R)) :
          R)
        (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
        ((Matrix.toLin' :
              (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R)
            x :
          (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) :
      R)
    (0 : R)

Tactic:
refine LieAlgebra.trace_toEnd_eq_zero ?_ hx

Premises used: LieAlgebra.trace_toEnd_eq_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 ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
i : ↥b.support
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
        (((toEnd R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (↥b.support ⊕ ι → R) :
                Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
              (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Module.End R (↥b.support ⊕ ι → R))
            (h i) :
          Module.End R (↥b.support ⊕ ι → R)) :
      R)
    (0 : R)

Tactic:
simp
-- 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 ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
i : ↥b.support
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
        (((toEnd R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (↥b.support ⊕ ι → R) :
                Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
              (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Module.End R (↥b.support ⊕ ι → R))
            (e i) :
          Module.End R (↥b.support ⊕ ι → R)) :
      R)
    (0 : R)

Tactic:
simpa using Matrix.isNilpotent_trace_of_isNilpotent (isNilpotent_e i)

Premises used: RootPairing.GeckConstruction.isNilpotent_e, Matrix.isNilpotent_trace_of_isNilpotent
-- 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 ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
i : ↥b.support
⊢ Eq.{u_2 + 1} (α := R)
    ((trace R (↥b.support ⊕ ι → R) : (a : (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) → R)
        (((toEnd R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (↥b.support ⊕ ι → R) :
                Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
              (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Module.End R (↥b.support ⊕ ι → R))
            (f i) :
          Module.End R (↥b.support ⊕ ι → R)) :
      R)
    (0 : R)

Tactic:
simpa using Matrix.isNilpotent_trace_of_isNilpotent (isNilpotent_f i)

Premises used: RootPairing.GeckConstruction.isNilpotent_f, Matrix.isNilpotent_trace_of_isNilpotent
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
χ : ↥H → K
hχ : χ ≠ 0
hχ' : Ne (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
this :
  ∀ {w : ↥b.support ⊕ ι → K} (hw₀ : w ≠ 0)
    (hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w),
    ∃ (i : ι) (t : K), t • w = v b i
⊢ ∃ (w : ↥U), Membership.mem (γ := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) w ∧ w ≠ 0

Tactic:
simpa only [ne_eq, LieSubmodule.eq_bot_iff, not_forall, exists_prop] using hχ'

Premises used: exists_prop, ne_eq, Classical.not_forall, LieSubmodule.eq_bot_iff