awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hk₀ : k ≠ 0
j : ↥b.support
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inl j) = v b i (Sum.inl j)
have this : χ x ≠ 0
Tactic: have : χ x ≠ 0 := hχx ▸ hd₀ 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
j : ι
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inr j) = v b i (Sum.inr j)
have h : ((w (Sum.inr i))⁻¹ • w) (Sum.inr i) = v b i (Sum.inr i)
Tactic: rcases eq_or_ne i j with rfl | hij
Cleared hypotheses: 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
j : ι
h : ((w (Sum.inr i))⁻¹ • w) (Sum.inr i) = v b i (Sum.inr i)
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inr j) = v b i (Sum.inr j)
have h₁ : ∀ (hij : i ≠ j), ((w (Sum.inr i))⁻¹ • w) (Sum.inr j) = v b i (Sum.inr j)
Tactic: rcases eq_or_ne i j with rfl | hij
-- 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
j : ι
hij : i ≠ j
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inr j) = v b i (Sum.inr j)
have h : d j ≠ χ x
Tactic: suffices d j ≠ χ x by
          simpa [mulVec_eq_sum, diagonal_apply, sub_eq_zero, this, hij, hi] using
            congr_fun hk (Sum.inr 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
j : ι
hij : i ≠ j
⊢ d j ≠ χ x
have h : d j ≠ d i
Tactic: rw [← hχx]
-- 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
⊢ ∃ (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))
have simp_rw : ∃ (d : ι → K),
  (∀ (i : ι), d i ≠ 0) ∧
    Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
      Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
Tactic: simp_rw [cartanSubalgebra, LieSubalgebra.mem_mk_iff', diagonal_elim_mem_span_h_iff]
-- 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
d : ι → K
⊢ Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ↔
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
have mp : Membership.mem (γ := Submodule K ((j : ι) → K))
      (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
    (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) →
  (∀ (i : ι), d i ≠ 0) ∧
    Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
      Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
Tactic: tauto
-- 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
d : ι → K
mp :
  Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) →
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
⊢ Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ↔
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
have mpr : (∀ (i : ι), d i ≠ 0) ∧
    Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
      Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
  Membership.mem (γ := Submodule K ((j : ι) → K))
      (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
    (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
Tactic: tauto
-- 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
d : ι → K
mp :
  Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) →
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
mpr :
  (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
    Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
⊢ Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ↔
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
have mp₁ : Membership.mem (γ := Submodule K ((j : ι) → K))
    (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
  (∀ (i : ι), d i ≠ 0) →
    Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) →
      (∀ (i : ι), d i ≠ 0) ∧
        Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
          Membership.mem (γ := Submodule K ((j : ι) → K))
            (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
Tactic: tauto
-- 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
d : ι → K
mp :
  Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) →
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
mpr :
  (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
    Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d)
mp₁ mp₂ :
  Membership.mem (γ := Submodule K ((j : ι) → K))
      (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
    (∀ (i : ι), d i ≠ 0) →
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) →
        (∀ (i : ι), d i ≠ 0) ∧
          Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
            Membership.mem (γ := Submodule K ((j : ι) → K))
              (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
⊢ Membership.mem (γ := Submodule K ((j : ι) → K))
        (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d ∧
      (∀ (i : ι), d i ≠ 0) ∧ Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ↔
    (∀ (i : ι), d i ≠ 0) ∧
      Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) ∧
        Membership.mem (γ := Submodule K ((j : ι) → K))
          (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d
have mp₃ : Membership.mem (γ := Submodule K ((j : ι) → K))
    (span K (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : K))) d →
  (∀ (i : ι), d i ≠ 0) → Pairwise ((fun (x1 x2 : K) ↦ x1 ≠ x2) on d) → ∀ (i : ι), d i ≠ 0
Tactic: tauto
-- 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
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ¬U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
this : ∃ (χ : ↥H → K), χ ≠ 0 ∧ Ne (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
⊢ ∃ (i : ι), v b i ∈ U
have obtain : ∀ (χ : ↥H → K) (hχ₀ : χ ≠ 0) (hχ : Ne (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥), ∃ (i : ι), v b i ∈ U
Tactic: obtain ⟨χ, hχ₀, hχ⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ¬U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
χ : ↥H → K
hχ₀ : χ ≠ 0
hχ : Ne (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
⊢ ∃ (i : ι), v b i ∈ U
have obtain : ∀ (i : ι) (hi : v b i ∈ LieSubmodule.map U.incl (genWeightSpace (↥U) χ)), ∃ (i : ι), v b i ∈ U
Tactic: obtain ⟨i, hi⟩ := instIsIrreducible_aux₀ χ hχ₀ hχ
-- 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
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ¬U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ ∃ (i : ι), v b i ∈ U
have suffices : ∃ (χ : ↥H → K), χ ≠ 0 ∧ Ne (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
Tactic: suffices ∃ χ : H → K, χ ≠ 0 ∧ genWeightSpace U χ ≠ ⊥ by
    obtain ⟨χ, hχ₀, hχ⟩ := this
    obtain ⟨i, hi⟩ := instIsIrreducible_aux₀ χ hχ₀ hχ
    exact ⟨i, LieSubmodule.map_incl_le hi⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ¬U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ ∃ (χ : ↥H → K), χ ≠ 0 ∧ Ne (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
have contrapose! : ∀ (hU : ∀ (χ : ↥H → K) (_ : χ ≠ 0), Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥),
  U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
Tactic: contrapose! hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (goal)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K) (_ : χ ≠ 0), Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
⊢ U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
have refine : U ≤ LieSubmodule.map U.incl (genWeightSpace (↥U) 0)
Tactic: refine le_trans ?_ (map_genWeightSpace_le (f := U.incl))