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.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
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) χ)
⊢ ∃ (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χ'

Premises used: Membership.mem, Subtype, LieModule.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.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
⊢ Membership.mem (α := ↥b.support ⊕ ι → K) (LieSubmodule.map U.incl (genWeightSpace (↥U) χ))
    ((U.incl : (a : ↥U) → ↥b.support ⊕ ι → K) w : ↥b.support ⊕ ι → K)

Tactic:
simpa
-- 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
hw : Membership.mem (γ := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) w
hw₀ : w ≠ 0
⊢ 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
-- 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
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)
⊢ Ne (α := ↥b.support ⊕ ι → K) ((U.incl : (a : ↥U) → ↥b.support ⊕ ι → K) w : ↥b.support ⊕ ι → K)
    (0 : ↥b.support ⊕ ι → K)

Tactic:
simpa
-- 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
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)
obtain :
  ∀ (i : ι) (t : K) (hi : t • (↑w : ↥b.support ⊕ ι → K) = v b i),
    ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
⊢ ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)

Tactic:
obtain ⟨i, t, hi : t • w = v b i⟩ := this (by simpa) 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.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
h : v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)
⊢ ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)

Tactic:
use i
-- 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
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
h :
  Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ)
      (t • (↑w : ↥b.support ⊕ ι → K)) ∧
    t • (↑w : ↥b.support ⊕ ι → K) ∈ U
⊢ v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)

Tactic:
rw [map_genWeightSpace_eq_of_injective U.injective_incl, LieSubmodule.range_incl, ← hi,
      LieSubmodule.mem_inf]

Premises used: LieSubmodule.mem_inf, LieSubmodule.range_incl, LieModule.map_genWeightSpace_eq_of_injective, LieSubmodule.injective_incl
-- 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
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
⊢ Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ)
      (t • (↑w : ↥b.support ⊕ ι → K)) ∧
    t • (↑w : ↥b.support ⊕ ι → K) ∈ U

Tactic:
⟨SMulMemClass.smul_mem _ hw, SMulMemClass.smul_mem _ w.property⟩

Premises used: SMulMemClass.smul_mem, And.intro, Subtype.property
-- 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
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
⊢ Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ)
      (t • (↑w : ↥b.support ⊕ ι → K)) ∧
    t • (↑w : ↥b.support ⊕ ι → K) ∈ U

Tactic:
exact ⟨SMulMemClass.smul_mem _ hw, SMulMemClass.smul_mem _ w.property⟩
-- 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) χ) ⊥
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
⊢ ∃ (i : ι), v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)

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⟩
-- 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
d : ↥b.support ⊕ ι → K
x : ↥H
hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d
set :
  let μ := χ x;
  Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpaceOf (↥b.support ⊕ ι → K) μ x) w ↔
    ∃ (k : ℕ), diagonal ((d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) μ 1) ^ k) *ᵥ w = 0
⊢ Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x) w ↔
    ∃ (k : ℕ), diagonal ((d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ x) 1) ^ k) *ᵥ w = 0

Tactic:
set μ := χ x
-- 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
d : ↥b.support ⊕ ι → K
x : ↥H
hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d
μ : K := χ x
obtain :
  ∀ (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)
    (hx' :
      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))
    (hdx :
      (↑(↑(Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦ Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
                  (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)
                  hx') :
              ↥(lieAlgebra b)) :
          Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) =
        diagonal d),
    let μ :=
      χ
        (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦ Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
          (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)
          hx');
    Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K))
        (genWeightSpaceOf (↥b.support ⊕ ι → K) μ
          (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦ Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
            (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)
            hx'))
        w ↔
      ∃ (k : ℕ), diagonal ((d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) μ 1) ^ k) *ᵥ w = 0
⊢ Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpaceOf (↥b.support ⊕ ι → K) μ x) w ↔
    ∃ (k : ℕ), diagonal ((d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) μ 1) ^ k) *ᵥ w = 0

Tactic:
obtain ⟨⟨x, hx⟩, hx'⟩ := x
-- 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
d : ↥b.support ⊕ ι → K
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
hx' :
  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)
hdx :
  (↑(↑(Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦ Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
              (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)
              hx') :
          ↥(lieAlgebra b)) :
      Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) =
    diagonal d
μ : K :=
  χ
    (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦ Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
      (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)
      hx')
⊢ x = diagonal d

Tactic:
simpa using hdx
-- 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
d : ↥b.support ⊕ ι → K
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
hx' :
  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)
hdx :
  (↑(↑(Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦ Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
              (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)
              hx') :
          ↥(lieAlgebra b)) :
      Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) =
    diagonal d
μ : K :=
  χ
    (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦ Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
      (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)
      hx')
⊢ x = diagonal d

Tactic:
replace hdx : x = diagonal d := by simpa using hdx
-- 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
d_1 : ↥b.support ⊕ ι → K
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
hx' :
  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)
μ_1 : K :=
  χ
    (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦ Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
      (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)
      hx')
hdx : x = diagonal d_1
d : ↥b.support ⊕ ι → K
μ : K
⊢ HSub.hSub (α := (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
      ((toLin' : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) → (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
          (diagonal d) :
        (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
      (HSMul.hSMul (β := (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K) μ 1) =
    (toLin' : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) → (↥b.support ⊕ ι → K) →ₗ[K] ↥b.support ⊕ ι → K)
      (diagonal (d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) μ 1))

Tactic:
aesop (add simp Pi.single_apply)

Premises used: Pi.single_apply