awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l m : ι
hm :
  (P.root : (a : ι) → M) m = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) l : M)
hk : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (aux : ∀ (k : ↥b.support), u k ∈ U), v b k ∈ U
hl : l ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
⊢ v b m ∈ U
have h₂ : ∀
  (hm :
    (P.root : (a : ι) → M) m =
      HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) k : M))
  (hk : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (aux : ∀ (k : ↥b.support), u k ∈ U), v b k ∈ U)
  (hl : l ∈ b.support) {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (aux : ∀ (k : ↥b.support), u k ∈ U),
  v b m ∈ U
Tactic: rw [add_comm] at hm
Cleared hypotheses: hm, hk, hl, U, aux
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l m : ι
hm :
  (P.root : (a : ι) → M) m = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) k : M)
hk : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (aux : ∀ (k : ↥b.support), u k ∈ U), v b k ∈ U
hl : l ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
e' : ↥(lieAlgebra b) :=
  Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
    Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b) x)
    (e (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) l hl)) ⋯
⊢ v b m ∈ U
have this : ⁅e', v b k⁆ =
  HAdd.hAdd (α := K) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := K) (M := M) (N := N) (P := P) l k) : K) 1 • v b m
Tactic: have : ⁅e', v b k⁆ = (P.chainBotCoeff l k + 1 : K) • v b m := e_lie_v_ne hm
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l m : ι
hm :
  (P.root : (a : ι) → M) m = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) k : M)
hk : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (aux : ∀ (k : ↥b.support), u k ∈ U), v b k ∈ U
hl : l ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
e' : ↥(lieAlgebra b) :=
  Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
    Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b) x)
    (e (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) l hl)) ⋯
this :
  ⁅e', v b k⁆ =
    HAdd.hAdd (α := K) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := K) (M := M) (N := N) (P := P) l k) : K) 1 • v b m
⊢ HAdd.hAdd (α := K) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := K) (M := M) (N := N) (P := P) l k) : K) 1 • v b m ∈ U
have rw : ⁅e', v b k⁆ ∈ U
Tactic: rw [← this]
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l m : ι
hm :
  (P.root : (a : ι) → M) m = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) k : M)
hk : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (aux : ∀ (k : ↥b.support), u k ∈ U), v b k ∈ U
hl : l ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
e' : ↥(lieAlgebra b) :=
  Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
    Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b) x)
    (e (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) l hl)) ⋯
this :
  ⁅e', v b k⁆ =
    HAdd.hAdd (α := K) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := K) (M := M) (N := N) (P := P) l k) : K) 1 • v b m
⊢ v b m ∈ U
have this₁ : HAdd.hAdd (α := K) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := K) (M := M) (N := N) (P := P) l k) : K) 1 • v b m ∈ U
Tactic: replace this : (P.chainBotCoeff l k + 1 : K) • v b m ∈ U := by
      rw [← this]
      exact U.lie_mem (hk aux)
Cleared hypotheses: this
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l m : ι
hm :
  (P.root : (a : ι) → M) m = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) l : M) ((P.root : (a : ι) → M) k : M)
hk : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (aux : ∀ (k : ↥b.support), u k ∈ U), v b k ∈ U
hl : l ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
e' : ↥(lieAlgebra b) :=
  Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
    Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b) x)
    (e (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) l hl)) ⋯
this :
  HAdd.hAdd (α := K) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := K) (M := M) (N := N) (P := P) l k) : K) 1 • v b m ∈ U
⊢ HAdd.hAdd (α := K) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := K) (M := M) (N := N) (P := P) l k) : K) 1 ≠ 0
have norm_cast : ¬False
Tactic: norm_cast
-- 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.IsCrystallographic
b : P.Base
⊢ Eq (α := Submodule K (↥b.support ⊕ ι → K))
    ((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) : Submodule K (↥b.support ⊕ ι → K))
    (span K (range u) : Submodule K (↥b.support ⊕ ι → K))
have refine_1 : ∀ (w : ↥b.support ⊕ ι → K)
  (hw :
    Membership.mem (γ := Submodule K (↥b.support ⊕ ι → K))
      ((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) : Submodule K (↥b.support ⊕ ι → K))
      w)
  (i : ι), w (Sum.inr i) = 0
Tactic: refine le_antisymm (fun w hw ↦ Pi.mem_span_range_single_inl_iff.mpr fun 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.IsCrystallographic
b : P.Base
refine_1 :
  ∀ (w : ↥b.support ⊕ ι → K)
    (hw :
      Membership.mem (γ := Submodule K (↥b.support ⊕ ι → K))
        ((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) :
          Submodule K (↥b.support ⊕ ι → K))
        w)
    (i : ι), w (Sum.inr i) = 0
⊢ Eq (α := Submodule K (↥b.support ⊕ ι → K))
    ((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) : Submodule K (↥b.support ⊕ ι → K))
    (span K (range u) : Submodule K (↥b.support ⊕ ι → K))
have refine_2 : LE.le (α := Submodule K (↥b.support ⊕ ι → K)) (span K (range u) : Submodule K (↥b.support ⊕ ι → K))
  ((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) : Submodule K (↥b.support ⊕ ι → K))
Tactic: refine le_antisymm (fun w hw ↦ Pi.mem_span_range_single_inl_iff.mpr fun i ↦ ?_) ?_
-- 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.IsCrystallographic
b : P.Base
w : ↥b.support ⊕ ι → K
hw :
  Membership.mem (γ := Submodule K (↥b.support ⊕ ι → K))
    ((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) : Submodule K (↥b.support ⊕ ι → K)) w
i : ι
⊢ w (Sum.inr i) = 0
have hw₁ : ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
  (hx :
    Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
      x),
  Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H
      (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
        Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
          (lieAlgebra b) x)
        x hx) →
    ∃ (k : ℕ),
      Eq (α := ↥b.support ⊕ ι → K)
        ((HPow.hPow (α := (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                ((toLin' :
                      (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) → (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                    x :
                  (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                k :
              (a : ↥b.support ⊕ ι → K) → ↥b.support ⊕ ι → K)
            w :
          ↥b.support ⊕ ι → K)
        (0 : ↥b.support ⊕ ι → K)
Tactic: replace hw : ∀ (x) (hx : x ∈ lieAlgebra b), ⟨x, hx⟩ ∈ H →
        ∃ k, (x.toLin' ^ k) w = 0 := by simpa [mem_genWeightSpace] using hw
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.IsCrystallographic
b : P.Base
w : ↥b.support ⊕ ι → K
i : ι
hw :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
    (hx :
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x),
    Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H
        (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
          Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
            (lieAlgebra b) x)
          x hx) →
      ∃ (k : ℕ),
        Eq (α := ↥b.support ⊕ ι → K)
          ((HPow.hPow (α := (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                  ((toLin' :
                        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) →
                          (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                      x :
                    (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                  k :
                (a : ↥b.support ⊕ ι → K) → ↥b.support ⊕ ι → K)
              w :
            ↥b.support ⊕ ι → K)
          (0 : ↥b.support ⊕ ι → K)
⊢ ∃ (j : ↥b.support), P.pairingIn ℤ i (↑j : ι) ≠ 0
have obtain : ∀ (j : ι) (hj : j ∈ b.support) (hj₀ : P.pairingIn ℤ j i ≠ 0), ∃ (j : ↥b.support), P.pairingIn ℤ i (↑j : ι) ≠ 0
Tactic: obtain ⟨j, hj, hj₀⟩ := b.exists_mem_support_pos_pairingIn_ne_zero i
-- 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.IsCrystallographic
b : P.Base
w : ↥b.support ⊕ ι → K
i : ι
hw :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
    (hx :
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x),
    Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H
        (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
          Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
            (lieAlgebra b) x)
          x hx) →
      ∃ (k : ℕ),
        Eq (α := ↥b.support ⊕ ι → K)
          ((HPow.hPow (α := (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                  ((toLin' :
                        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) →
                          (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                      x :
                    (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                  k :
                (a : ↥b.support ⊕ ι → K) → ↥b.support ⊕ ι → K)
              w :
            ↥b.support ⊕ ι → K)
          (0 : ↥b.support ⊕ ι → K)
j : ι
hj : j ∈ b.support
hj₀ : P.pairingIn ℤ j i ≠ 0
⊢ ∃ (j : ↥b.support), P.pairingIn ℤ i (↑j : ι) ≠ 0
have hj₁ : ¬P.pairingIn ℤ i j = 0
Tactic: rw [ne_eq, P.pairingIn_eq_zero_iff] at hj₀
Cleared hypotheses: hj₀
-- 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.IsCrystallographic
b : P.Base
w : ↥b.support ⊕ ι → K
i : ι
hw :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
    (hx :
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x),
    Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H
        (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
          Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
            (lieAlgebra b) x)
          x hx) →
      ∃ (k : ℕ),
        Eq (α := ↥b.support ⊕ ι → K)
          ((HPow.hPow (α := (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                  ((toLin' :
                        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) →
                          (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                      x :
                    (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                  k :
                (a : ↥b.support ⊕ ι → K) → ↥b.support ⊕ ι → K)
              w :
            ↥b.support ⊕ ι → K)
          (0 : ↥b.support ⊕ ι → K)
⊢ w (Sum.inr i) = 0
have refine_1 : ∀ (j : ↥b.support) (hj : P.pairingIn ℤ i (↑j : ι) ≠ 0), w (Sum.inr i) = 0
Tactic: obtain ⟨j, hj⟩ : ∃ j : b.support, P.pairingIn ℤ i j ≠ 0 := by
      obtain ⟨j, hj, hj₀⟩ := b.exists_mem_support_pos_pairingIn_ne_zero i
      rw [ne_eq, P.pairingIn_eq_zero_iff] at hj₀
      exact ⟨⟨j, hj⟩, hj₀⟩
-- 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.IsCrystallographic
b : P.Base
w : ↥b.support ⊕ ι → K
i : ι
hw :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
    (hx :
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x),
    Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H
        (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
          Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
            (lieAlgebra b) x)
          x hx) →
      ∃ (k : ℕ),
        Eq (α := ↥b.support ⊕ ι → K)
          ((HPow.hPow (α := (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                  ((toLin' :
                        (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) →
                          (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                      x :
                    (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                  k :
                (a : ↥b.support ⊕ ι → K) → ↥b.support ⊕ ι → K)
              w :
            ↥b.support ⊕ ι → K)
          (0 : ↥b.support ⊕ ι → K)
j : ↥b.support
hj : P.pairingIn ℤ i (↑j : ι) ≠ 0
⊢ w (Sum.inr i) = 0
have refine_1 : ∀ (k : ℕ)
  (hk :
    Eq (α := ↥b.support ⊕ ι → K)
      ((HPow.hPow (α := (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
              ((toLin' :
                    (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) → (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
                  (h j) :
                (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
              k :
            (a : ↥b.support ⊕ ι → K) → ↥b.support ⊕ ι → K)
          w :
        ↥b.support ⊕ ι → K)
      (0 : ↥b.support ⊕ ι → K)),
  w (Sum.inr i) = 0
Tactic: obtain ⟨k, hk⟩ := hw (h j) (h_mem_lieAlgebra j) (h_mem_cartanSubalgebra' j _)
-- 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.IsCrystallographic
b : P.Base
⊢ LE.le (α := Submodule K (↥b.support ⊕ ι → K)) (span K (range u) : Submodule K (↥b.support ⊕ ι → K))
    ((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) : Submodule K (↥b.support ⊕ ι → K))
have refine_2 : range u ⊆
  (↑((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) : Submodule K (↥b.support ⊕ ι → K)) :
    Set (↥b.support ⊕ ι → K))
Tactic: rw [span_le]
-- 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.IsCrystallographic
b : P.Base
i : ↥b.support
⊢ u i ∈
    (↑((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) :
          Submodule K (↥b.support ⊕ ι → K)) :
      Set (↥b.support ⊕ ι → K))
have refine_2 : ∀ (x : ↥H),
  ∃ (k : ℕ),
    Eq (α := ↥b.support ⊕ ι → K)
      ((HSub.hSub (α := Module.End K (↥b.support ⊕ ι → K))
                (((toEnd K (↥H) (↥b.support ⊕ ι → K) : ↥H →ₗ⁅K⁆ Module.End K (↥b.support ⊕ ι → K)) :
                      (a : ↥H) → Module.End K (↥b.support ⊕ ι → K))
                    x :
                  Module.End K (↥b.support ⊕ ι → K))
                (HSMul.hSMul (α := K) (β := Module.End K (↥b.support ⊕ ι → K)) (0 x) 1) ^
              k :
            (a : ↥b.support ⊕ ι → K) → ↥b.support ⊕ ι → K)
          (u i) :
        ↥b.support ⊕ ι → K)
      (0 : ↥b.support ⊕ ι → K)
Tactic: simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule, mem_genWeightSpace]
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
⊢ LieModule.IsIrreducible K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
have refine : ∀ (U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)) (hU : U ≠ ⊥), U = ⊤
Tactic: refine LieModule.IsIrreducible.mk fun U hU ↦ ?_
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hU : U ≠ ⊥
this : ∃ (i : ι), v b i ∈ U
⊢ U = ⊤
have obtain : ∀ (i : ι) (hi : v b i ∈ U), U = ⊤
Tactic: obtain ⟨i, hi⟩ := this
Cleared hypotheses: this
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hU : U ≠ ⊥
⊢ U = ⊤
have suffices : ∃ (i : ι), v b i ∈ U
Tactic: suffices ∃ i, v b i ∈ U by obtain ⟨i, hi⟩ := this; exact instIsIrreducible_aux₂ hi
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hU : U ≠ ⊥
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
⊢ ∃ (i : ι), v b i ∈ U
have apply : ¬U' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
Tactic: apply instIsIrreducible_aux₁ U'