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
χ : ↥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)
μ : 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
⊢ ∀ (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:
have this (d : b.support ⊕ ι → K) (μ : K) :
        (diagonal d).toLin' - μ • 1 = (diagonal (d - μ • 1)).toLin' := by
      aesop (add simp Pi.single_apply)
-- 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)
μ : 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
this :
  ∀ (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))
⊢ 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

Tactic:
simp [mem_genWeightSpaceOf, hdx, this, ← toLin'_pow, diagonal_pow]

Premises used: Matrix.diagonal_pow, Matrix.toLin'_pow, LieModule.mem_genWeightSpaceOf
-- 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),
    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:
have aux (d : b.support ⊕ ι → K) (x : H) (hdx : x = diagonal d) :
      w ∈ genWeightSpaceOf (b.support ⊕ ι → K) (χ x) x ↔
        ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0 := by
    set μ := χ x
    obtain ⟨⟨x, hx⟩, hx'⟩ := x
    replace hdx : x = diagonal d := by simpa using hdx
    have this (d : b.support ⊕ ι → K) (μ : K) :
        (diagonal d).toLin' - μ • 1 = (diagonal (d - μ • 1)).toLin' := by
      aesop (add simp Pi.single_apply)
    simp [mem_genWeightSpaceOf, hdx, this, ← toLin'_pow, 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.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
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
contrapose :
  ∀ (hw₀ : Eq (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥), w = 0
⊢ Ne (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥

Tactic:
contrapose 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
hw₀ : Eq (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥
⊢ ∀ (m : ↥b.support ⊕ ι → K),
    Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) m → m = 0

Tactic:
rw [LieSubmodule.eq_bot_iff] at hw₀

Premises used: LieSubmodule.eq_bot_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.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
hw₀ :
  ∀ (m : ↥b.support ⊕ ι → K),
    Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) m → m = 0
⊢ w = 0

Tactic:
hw₀ _ 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
hw₀ :
  ∀ (m : ↥b.support ⊕ ι → K),
    Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) m → m = 0
⊢ w = 0

Tactic:
exact hw₀ _ 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
χ : ↥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
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
⊢ Ne (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥

Tactic:
replace hw₀ : genWeightSpace (b.support ⊕ ι → K) χ ≠ ⊥ := by
        contrapose hw₀; rw [LieSubmodule.eq_bot_iff] at hw₀; exact hw₀ _ 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
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
hw₀ : Ne (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥
χ' : ↥H →ₗ[K] K :=
  Weight.toLinear K (↥H) (↥b.support ⊕ ι → K)
    { toFun := χ, genWeightSpace_ne_bot' := hw₀ : Weight K (↥H) (↥b.support ⊕ ι → K) }
contrapose : ∀ (hχ : χ' = 0), χ = 0
⊢ χ' ≠ 0

Tactic:
contrapose hχ
-- 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
w : ↥b.support ⊕ ι → K
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
hw₀ : Ne (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥
χ' : ↥H →ₗ[K] K :=
  Weight.toLinear K (↥H) (↥b.support ⊕ ι → K)
    { toFun := χ, genWeightSpace_ne_bot' := hw₀ : Weight K (↥H) (↥b.support ⊕ ι → K) }
hχ : χ' = 0
h : ∀ (x : ↥H), χ x = 0 x
⊢ χ = 0

Tactic:
ext 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
w : ↥b.support ⊕ ι → K
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
hw₀ : Ne (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥
χ' : ↥H →ₗ[K] K :=
  Weight.toLinear K (↥H) (↥b.support ⊕ ι → K)
    { toFun := χ, genWeightSpace_ne_bot' := hw₀ : Weight K (↥H) (↥b.support ⊕ ι → K) }
hχ : χ' = 0
x : ↥H
⊢ χ x = 0 x

Tactic:
simpa using LinearMap.congr_fun hχ x

Premises used: LinearMap.congr_fun
-- 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 : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
hw₀ : Ne (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥
χ' : ↥H →ₗ[K] K :=
  Weight.toLinear K (↥H) (↥b.support ⊕ ι → K)
    { toFun := χ, genWeightSpace_ne_bot' := hw₀ : Weight K (↥H) (↥b.support ⊕ ι → K) }
⊢ χ' ≠ 0

Tactic:
replace hχ : χ' ≠ 0 := by contrapose hχ; ext x; simpa using LinearMap.congr_fun hχ 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
w : ↥b.support ⊕ ι → K
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
hw₀ : Ne (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥
χ' : ↥H →ₗ[K] K :=
  Weight.toLinear K (↥H) (↥b.support ⊕ ι → K)
    { toFun := χ, genWeightSpace_ne_bot' := hw₀ : Weight K (↥H) (↥b.support ⊕ ι → K) }
hχ : χ' ≠ 0
contrapose! : ∀ (hχ : ∀ (l : ↥b.support), χ (h' l) = 0), χ' = 0
⊢ ∃ (l : ↥b.support), χ (h' l) ≠ 0

Tactic:
contrapose! hχ
-- 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
w : ↥b.support ⊕ ι → K
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
hw₀ : Ne (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥
χ' : ↥H →ₗ[K] K :=
  Weight.toLinear K (↥H) (↥b.support ⊕ ι → K)
    { toFun := χ, genWeightSpace_ne_bot' := hw₀ : Weight K (↥H) (↥b.support ⊕ ι → K) }
hχ : ∀ (l : ↥b.support), χ (h' l) = 0
apply : EqOn (α := ↥H) (β := K) (⇑χ' : (a : ↥H) → K) (⇑0 : (a : ↥H) → K) (range h')
⊢ χ' = 0

Tactic:
apply LinearMap.ext_on (span_range_h'_eq_top b)

Premises used: LinearMap.ext_on, RootPairing.GeckConstruction.span_range_h'_eq_top
-- 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
w : ↥b.support ⊕ ι → K
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) w
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
hw₀ : Ne (α := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpace (↥b.support ⊕ ι → K) χ) ⊥
χ' : ↥H →ₗ[K] K :=
  Weight.toLinear K (↥H) (↥b.support ⊕ ι → K)
    { toFun := χ, genWeightSpace_ne_bot' := hw₀ : Weight K (↥H) (↥b.support ⊕ ι → K) }
hχ : ∀ (l : ↥b.support), χ (h' l) = 0
l : ↥b.support
⊢ Eq.{u_2 + 1} (α := K) ((χ' : (a : ↥H) → K) (h' l) : K) ((0 : (a : ↥H) → K) (h' l) : K)

Tactic:
simp [χ', hχ l]
-- 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
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
obtain : ∀ (l : ↥b.support) (hl : χ (h' l) ≠ 0), ∃ (i : ι), w (Sum.inr i) ≠ 0
⊢ ∃ (i : ι), w (Sum.inr i) ≠ 0

Tactic:
obtain ⟨l, hl⟩ : ∃ l, χ (h' l) ≠ 0 := by
      replace hw₀ : genWeightSpace (b.support ⊕ ι → K) χ ≠ ⊥ := by
        contrapose hw₀; rw [LieSubmodule.eq_bot_iff] at hw₀; exact hw₀ _ hw
      let χ' : H →ₗ[K] K := (Weight.mk χ hw₀).toLinear
      replace hχ : χ' ≠ 0 := by contrapose hχ; ext x; simpa using LinearMap.congr_fun hχ x
      contrapose! hχ
      apply LinearMap.ext_on (span_range_h'_eq_top b)
      rintro - ⟨l, rfl⟩
      simp [χ', hχ l]
-- 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
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H)
    (hdx : (↑(↑x : ↥(lieAlgebra b)) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = diagonal d),
    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
l : ↥b.support
hl : χ (h' l) ≠ 0
contrapose! : ∀ (hw₀ : ∀ (i : ι), w (Sum.inr i) = 0), w = 0
⊢ ∃ (i : ι), w (Sum.inr i) ≠ 0

Tactic:
contrapose! hw₀