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.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
l : ↥b.support
hl : χ (h' l) ≠ 0
hw₀ : ∀ (i : ι), w (Sum.inr i) = 0
this : ∀ (i : ↥b.support), w (Sum.inl i) = 0
h : ∀ (k : ↥b.support), w (Sum.inl k) = 0 (Sum.inl k)
⊢ w = 0
have h₁ : ∀ (k : ι), w (Sum.inr k) = 0 (Sum.inr k)
Tactic: ext (k | k)
-- 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
χ : ↥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
l : ↥b.support
hl : χ (h' l) ≠ 0
hw₀ : ∀ (i : ι), w (Sum.inr i) = 0
⊢ w = 0
have suffices : ∀ (i : ↥b.support), w (Sum.inl i) = 0
Tactic: suffices ∀ i : b.support, w (Sum.inl i) = 0 by ext (k | k) <;> simp [hw₀, 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.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
l : ↥b.support
hl : χ (h' l) ≠ 0
hw₀ : ∀ (i : ι), w (Sum.inr i) = 0
i : ↥b.support
⊢ w (Sum.inl i) = 0
have hw₁ : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpaceOf (↥b.support ⊕ ι → K) (χ (h' l)) (h' l))
  w
Tactic: replace hw := genWeightSpace_le_genWeightSpaceOf (b.support ⊕ ι → K) (h' l) χ hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
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
hw₀ : ∀ (i : ι), w (Sum.inr i) = 0
i : ↥b.support
hw :
  Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K))
    (genWeightSpaceOf (↥b.support ⊕ ι → K) (χ (h' l)) (h' l)) w
⊢ w (Sum.inl i) = 0
have hw₁ : ∃ (k : ℕ),
  diagonal
        (((Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑l : ι)) : K)) -
            HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ (h' l)) 1) ^
          k) *ᵥ
      w =
    0
Tactic: rw [aux (Sum.elim 0 (P.pairingIn ℤ · l)) (h' l) (h_eq_diagonal l)] at 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.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
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
hw₀ : ∀ (i : ι), w (Sum.inr i) = 0
i : ↥b.support
hw :
  ∃ (k : ℕ),
    diagonal
          (((Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑l : ι)) : K)) -
              HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ (h' l)) 1) ^
            k) *ᵥ
        w =
      0
⊢ w (Sum.inl i) = 0
have obtain : ∀ (k : ℕ)
  (hk :
    diagonal
          (((Sum.elim 0 fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑l : ι)) : K)) -
              HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ (h' l)) 1) ^
            k) *ᵥ
        w =
      0),
  w (Sum.inl i) = 0
Tactic: obtain ⟨k, hk⟩ := 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.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
⊢ ∃ (i : ι) (t : K), t • w = v b i
have obtain : ∀ (i : ι) (hi : w (Sum.inr i) ≠ 0), ∃ (i : ι) (t : K), t • w = v b i
Tactic: obtain ⟨i, hi⟩ : ∃ i, w (Sum.inr i) ≠ 0 := by
    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]
    contrapose! hw₀
    suffices ∀ i : b.support, w (Sum.inl i) = 0 by ext (k | k) <;> simp [hw₀, this]
    intro i
    replace hw := genWeightSpace_le_genWeightSpaceOf (b.support ⊕ ι → K) (h' l) χ hw
    rw [aux (Sum.elim 0 (P.pairingIn ℤ · l)) (h' l) (h_eq_diagonal l)] at hw
    obtain ⟨k, hk⟩ := hw
    simpa [mulVec_eq_sum, diagonal_apply, hl] using congr_fun hk (Sum.inl i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥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
i : ι
hi : w (Sum.inr i) ≠ 0
⊢ ∃ (i : ι) (t : K), t • w = v b i
have refine : (w (Sum.inr i))⁻¹ • w = v b i
Tactic: refine ⟨i, (w (Sum.inr i))⁻¹, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥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
i : ι
hi : w (Sum.inr i) ≠ 0
this :
  ∃ (d : ι → K),
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
          (cartanSubalgebra b) (diagonal (Sum.elim 0 d))
⊢ (w (Sum.inr i))⁻¹ • w = v b i
have obtain : ∀ (d : ι → K) (hd₀ : ∀ (i : ι), d i ≠ 0) (hd₁ : Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d))
  (hd₂ :
    Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
      (cartanSubalgebra b) (diagonal (Sum.elim 0 d))),
  (w (Sum.inr i))⁻¹ • w = v b i
Tactic: obtain ⟨d, hd₀, hd₁, hd₂⟩ := this
Cleared hypotheses: 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.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
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
hd₂ :
  Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
    (cartanSubalgebra b) (diagonal (Sum.elim 0 d))
x : ↥H :=
  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)
      (diagonal (Sum.elim 0 d)) ⋯)
    hd₂
⊢ (w (Sum.inr i))⁻¹ • w = v b i
have hw₁ : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x) w
Tactic: replace hw := genWeightSpace_le_genWeightSpaceOf (b.support ⊕ ι → K) x χ hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
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
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
hd₂ :
  Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
    (cartanSubalgebra b) (diagonal (Sum.elim 0 d))
x : ↥H :=
  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)
      (diagonal (Sum.elim 0 d)) ⋯)
    hd₂
hw : Membership.mem (γ := LieSubmodule K (↥H) (↥b.support ⊕ ι → K)) (genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x) w
⊢ (w (Sum.inr i))⁻¹ • w = v b i
have hw₁ : ∃ (k : ℕ), diagonal ((Sum.elim 0 d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ x) 1) ^ k) *ᵥ w = 0
Tactic: rw [aux (Sum.elim 0 d) x rfl] at 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.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
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
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
hd₂ :
  Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
    (cartanSubalgebra b) (diagonal (Sum.elim 0 d))
x : ↥H :=
  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)
      (diagonal (Sum.elim 0 d)) ⋯)
    hd₂
hw : ∃ (k : ℕ), diagonal ((Sum.elim 0 d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ x) 1) ^ k) *ᵥ w = 0
⊢ (w (Sum.inr i))⁻¹ • w = v b i
have obtain : ∀ (k : ℕ) (hk : diagonal ((Sum.elim 0 d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ x) 1) ^ k) *ᵥ w = 0),
  (w (Sum.inr i))⁻¹ • w = v b i
Tactic: obtain ⟨k, hk⟩ := hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
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
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
hd₂ :
  Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
    (cartanSubalgebra b) (diagonal (Sum.elim 0 d))
x : ↥H :=
  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)
      (diagonal (Sum.elim 0 d)) ⋯)
    hd₂
k : ℕ
hk : diagonal ((Sum.elim 0 d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ x) 1) ^ k) *ᵥ w = 0
⊢ (w (Sum.inr i))⁻¹ • w = v b i
have hχx : d i = χ x
Tactic: obtain ⟨hχx, hk₀⟩ : d i = χ x ∧ k ≠ 0 := by
      simpa [hi, mulVec_eq_sum, diagonal_apply, sub_eq_zero] using congr_fun hk (Sum.inr 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.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
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
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
hd₂ :
  Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
    (cartanSubalgebra b) (diagonal (Sum.elim 0 d))
x : ↥H :=
  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)
      (diagonal (Sum.elim 0 d)) ⋯)
    hd₂
k : ℕ
hk : diagonal ((Sum.elim 0 d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ x) 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
⊢ (w (Sum.inr i))⁻¹ • w = v b i
have hk₀ : k ≠ 0
Tactic: obtain ⟨hχx, hk₀⟩ : d i = χ x ∧ k ≠ 0 := by
      simpa [hi, mulVec_eq_sum, diagonal_apply, sub_eq_zero] using congr_fun hk (Sum.inr i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
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
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
hd₂ :
  Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
    (cartanSubalgebra b) (diagonal (Sum.elim 0 d))
x : ↥H :=
  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)
      (diagonal (Sum.elim 0 d)) ⋯)
    hd₂
k : ℕ
hk : diagonal ((Sum.elim 0 d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ x) 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
⊢ (w (Sum.inr i))⁻¹ • w = v b i
have h : ∀ (j : ↥b.support), ((w (Sum.inr i))⁻¹ • w) (Sum.inl j) = v b i (Sum.inl j)
Tactic: ext (j | 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.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
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
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
hd₂ :
  Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
    (cartanSubalgebra b) (diagonal (Sum.elim 0 d))
x : ↥H :=
  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)
      (diagonal (Sum.elim 0 d)) ⋯)
    hd₂
k : ℕ
hk : diagonal ((Sum.elim 0 d - HSMul.hSMul (β := ↥b.support ⊕ ι → K) (χ x) 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
h : ∀ (j : ↥b.support), ((w (Sum.inr i))⁻¹ • w) (Sum.inl j) = v b i (Sum.inl j)
⊢ (w (Sum.inr i))⁻¹ • w = v b i
have h₁ : ∀ (j : ι), ((w (Sum.inr i))⁻¹ • w) (Sum.inr j) = v b i (Sum.inr j)
Tactic: ext (j | j)