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
n : ℕ
ih : ω b * f i ^ n = e i ^ n * ω b
⊢ ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b
have succ : ω b * (f i ^ n * f i) = e i ^ (n + 1) * ω b
Tactic: rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]
-- 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 : ℕ
ih : ω b * f i ^ n = e i ^ n * ω b
succ : ω b * (f i ^ n * f i) = e i ^ (n + 1) * ω b
⊢ ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b
have succ₁ : ω b * (f i ^ n * f i) = e i ^ n * e i * ω b
Tactic: rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]
-- 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 : ℕ
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
⊢ ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b
have succ₂ : ω b * f i ^ n * f i = e i ^ n * e i * ω b
Tactic: rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]
-- 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 : ℕ
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
⊢ ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b
have succ₃ : e i ^ n * ω b * f i = e i ^ n * e i * ω b
Tactic: rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]
-- 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 : ℕ
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
⊢ ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b
have succ₄ : e i ^ n * (ω b * f i) = e i ^ n * e i * ω b
Tactic: rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]
-- 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 : ℕ
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
⊢ ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b
have succ₅ : e i ^ n * (e i * ω b) = e i ^ n * e i * ω b
Tactic: rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]
-- 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 : ℕ
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
⊢ ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b
have succ₆ : e i ^ n * e i * ω b = e i ^ n * e i * ω b
Tactic: rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]
-- 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 : ℕ
⊢ ω b * f i ^ n = e i ^ n * ω b
have zero : ω b * HPow.hPow (β := ℕ) (f i) 0 = HPow.hPow (β := ℕ) (e i) 0 * ω b
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]
Cleared hypotheses: n
-- 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 : ℕ
zero : ω b * HPow.hPow (β := ℕ) (f i) 0 = HPow.hPow (β := ℕ) (e i) 0 * ω b
⊢ ω b * f i ^ n = e i ^ n * ω b
have succ : ∀ (n : ℕ) (ih : ω b * f i ^ n = e i ^ n * ω b), ω b * f i ^ (n + 1) = e i ^ (n + 1) * ω b
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, pow_succ, ← mul_assoc, ih, mul_assoc, ω_mul_f, ← mul_assoc]
Cleared hypotheses: n
-- 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 : 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
⊢ (h i).trace = 0
have simp : Eq.{u_2 + 1} (α := R) (∑ x : ι, (↑(P.pairingIn ℤ x (↑i : ι)) : R)) 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]
-- 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 : 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
⊢ (h i).trace = 0
have suffices : Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ j (↑i : ι)) 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
-- 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 : 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
⊢ Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ j (↑i : ι)) 0
have suffices : Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ (-j) (↑i : ι)) (∑ j : ι, P.pairingIn ℤ j (↑i : ι))
Tactic: suffices ∑ j, P.pairingIn ℤ (-j) i = ∑ j, P.pairingIn ℤ j i from
    eq_zero_of_neg_eq <| by simpa using 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 : 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
⊢ (h i).trace = 0
have letI₃ : Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ j (↑i : ι)) 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)
-- 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 : 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
⊢ (h i).trace = 0
have letI₄ : let _i := P.indexNeg;
Eq (α := ℤ) (∑ j : ι, P.pairingIn ℤ (-j) (↑i : ι)) (∑ j : ι, P.pairingIn ℤ j (↑i : ι))
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)
-- 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 ι
x : ↥(lieAlgebra b)
⊢ 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)
have 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)
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- 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 ι
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)
have 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)
Tactic: suffices trace R _ x.toLin' = 0 by simpa
-- 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 ι
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)
have 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)
Tactic: refine LieAlgebra.trace_toEnd_eq_zero ?_ hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
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
⊢ ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
have obtain : ∀ (w : ↥U) (hw : Membership.mem (γ := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) w) (hw₀ : w ≠ 0),
  ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
Tactic: obtain ⟨w, hw, hw₀⟩ : ∃ w ∈ genWeightSpace U χ, w ≠ 0 := by
      simpa only [ne_eq, LieSubmodule.eq_bot_iff, not_forall, exists_prop] using hχ'
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
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
hw : Membership.mem (γ := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) w
hw₀ : w ≠ 0
⊢ ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
have hw₁ : Membership.mem (α := ↥b.support ⊕ ι → K) (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K))
  (genWeightSpace (↥b.support ⊕ ι → K) χ) ((U.incl : (a : ↥U) → ↥b.support ⊕ ι → K) w : ↥b.support ⊕ ι → K)
Tactic: replace hw : U.incl w ∈ genWeightSpace (b.support ⊕ ι → K) χ :=
      map_genWeightSpace_le (f := U.incl) <| by simpa
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
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
hw₀ : w ≠ 0
hw :
  Membership.mem (α := ↥b.support ⊕ ι → K) (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K))
    (genWeightSpace (↥b.support ⊕ ι → K) χ) ((U.incl : (a : ↥U) → ↥b.support ⊕ ι → K) w : ↥b.support ⊕ ι → K)
⊢ ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
have obtain : ∀ (i : ι) (t : K) (hi : t • (↑w : ↥b.support ⊕ ι → K) = v b i),
  ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
Tactic: obtain ⟨i, t, hi : t • w = v b i⟩ := this (by simpa) hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
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
hw₀ : w ≠ 0
hw :
  Membership.mem (α := ↥b.support ⊕ ι → K) (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K))
    (genWeightSpace (↥b.support ⊕ ι → K) χ) ((U.incl : (a : ↥U) → ↥b.support ⊕ ι → K) w : ↥b.support ⊕ ι → K)
i : ι
t : K
hi : t • (↑w : ↥b.support ⊕ ι → K) = v b i
⊢ ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
have h : v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
Tactic: use i
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
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
hw₀ : w ≠ 0
hw :
  Membership.mem (α := ↥b.support ⊕ ι → K) (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K))
    (genWeightSpace (↥b.support ⊕ ι → K) χ) ((U.incl : (a : ↥U) → ↥b.support ⊕ ι → K) w : ↥b.support ⊕ ι → K)
i : ι
t : K
hi : t • (↑w : ↥b.support ⊕ ι → K) = v b i
⊢ v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
have h : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ)
    (t • (↑w : ↥b.support ⊕ ι → K)) ∧
  t • (↑w : ↥b.support ⊕ ι → K) ∈ U
Tactic: rw [map_genWeightSpace_eq_of_injective U.injective_incl, LieSubmodule.range_incl, ← hi,
      LieSubmodule.mem_inf]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
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) χ) ⊥
⊢ ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
have suffices : ∀ {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
Tactic: suffices ∀ {w : b.support ⊕ ι → K} (hw₀ : w ≠ 0) (hw : w ∈ genWeightSpace (b.support ⊕ ι → K) χ),
      ∃ (i : ι) (t : K), t • w = v b i by
    obtain ⟨w, hw, hw₀⟩ : ∃ w ∈ genWeightSpace U χ, w ≠ 0 := by
      simpa only [ne_eq, LieSubmodule.eq_bot_iff, not_forall, exists_prop] using hχ'
    replace hw : U.incl w ∈ genWeightSpace (b.support ⊕ ι → K) χ :=
      map_genWeightSpace_le (f := U.incl) <| by simpa
    obtain ⟨i, t, hi : t • w = v b i⟩ := this (by simpa) hw
    use i
    rw [map_genWeightSpace_eq_of_injective U.injective_incl, LieSubmodule.range_incl, ← hi,
      LieSubmodule.mem_inf]
    exact ⟨SMulMemClass.smul_mem _ hw, SMulMemClass.smul_mem _ w.property⟩