awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.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

Tactic:
replace this : (P.chainBotCoeff l k + 1 : K) • v b m ∈ U := by
      rw [← this]
      exact U.lie_mem (hk aux)
-- 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.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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬False
⊢ 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

Tactic:
norm_cast
-- 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.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
⊢ v b m ∈ U

Tactic:
exact (U.smul_mem_iff (by norm_cast)).mp this

Premises used: LieSubmodule.toSubmodule, Submodule.smul_mem_iff, Iff.mp
-- 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.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))

Tactic:
le_antisymm (fun w hw ↦ Pi.mem_span_range_single_inl_iff.mpr fun i ↦ ?_) ?_

Premises used: Iff.mpr, le_antisymm, Pi.mem_span_range_single_inl_iff
-- 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.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
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))
⊢ 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))

Tactic:
refine le_antisymm (fun w hw ↦ Pi.mem_span_range_single_inl_iff.mpr fun i ↦ ?_) ?_

Premises used: le_antisymm
-- 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.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 : ι
⊢ ∀ (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:
simpa [mem_genWeightSpace] using hw

Premises used: LieModule.mem_genWeightSpace
-- 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.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 : ι
⊢ ∀ (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
-- 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.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)
obtain : ∀ (j : ι) (hj : j ∈ b.support) (hj₀ : P.pairingIn ℤ j i ≠ 0), ∃ (j : ↥b.support), P.pairingIn ℤ i (↑j : ι) ≠ 0
⊢ ∃ (j : ↥b.support), P.pairingIn ℤ i (↑j : ι) ≠ 0

Tactic:
obtain ⟨j, hj, hj₀⟩ := b.exists_mem_support_pos_pairingIn_ne_zero i

Premises used: RootPairing.Base.exists_mem_support_pos_pairingIn_ne_zero
-- 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.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
⊢ ¬P.pairingIn ℤ i j = 0

Tactic:
rw [ne_eq, P.pairingIn_eq_zero_iff] at hj₀

Premises used: ne_eq, RootPairing.pairingIn_eq_zero_iff
-- 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.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 ℤ i j = 0
⊢ ∃ (j : ↥b.support), P.pairingIn ℤ i (↑j : ι) ≠ 0

Tactic:
⟨⟨j, hj⟩, hj₀⟩

Premises used: Subtype.mk, Exists.intro
-- 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.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 ℤ i j = 0
⊢ ∃ (j : ↥b.support), P.pairingIn ℤ i (↑j : ι) ≠ 0

Tactic:
exact ⟨⟨j, hj⟩, hj₀⟩
-- 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.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)
refine_1 : ∀ (j : ↥b.support) (hj : P.pairingIn ℤ i (↑j : ι) ≠ 0), w (Sum.inr i) = 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₀⟩

Premises used: RootPairing.Base.support
-- 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.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
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
⊢ w (Sum.inr i) = 0

Tactic:
obtain ⟨k, hk⟩ := hw (h j) (h_mem_lieAlgebra j) (h_mem_cartanSubalgebra' j _)

Premises used: RootPairing.GeckConstruction.h, RootPairing.GeckConstruction.h_mem_cartanSubalgebra', RootPairing.GeckConstruction.h_mem_lieAlgebra
-- 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.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
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:
simpa [h_eq_diagonal, ← toLin'_pow, fromBlocks_diagonal_pow, diagonal_pow,
      mulVec_eq_sum, diagonal_apply, hj] using congr_fun hk (Sum.inr i)

Premises used: Matrix.diagonal_pow, Matrix.toLin'_pow, Matrix.mulVec_eq_sum, Sum.inr, Matrix.diagonal_apply, congr_fun, RootPairing.GeckConstruction.h_eq_diagonal, Matrix.fromBlocks_diagonal_pow
-- 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.IsCrystallographic
b : P.Base
refine_2 :
  range u ⊆
    (↑((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) :
          Submodule K (↥b.support ⊕ ι → K)) :
      Set (↥b.support ⊕ ι → K))
⊢ 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:
rw [span_le]

Premises used: Submodule.span_le