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
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K) (_ : χ ≠ 0), Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
⊢ U ≤ LieSubmodule.map U.incl (genWeightSpace (↥U) 0)
have suffices : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) ⊤
Tactic: suffices genWeightSpace U (0 : H → K) = ⊤ by simp [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
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K) (_ : χ ≠ 0), Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
⊢ Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) ⊤
have this : Eq (α := LieSubmodule K ↥H ↥U) (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ 0), ⊥) ⊥
Tactic: have : ⨆ (χ : H → K), ⨆ (_ : χ ≠ 0), (⊥ : LieSubmodule K H U) = ⊥ := biSup_const ⟨1, one_ne_zero⟩
-- 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) χ) ⊥
this : Eq (α := LieSubmodule K ↥H ↥U) (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ 0), ⊥) ⊥
⊢ Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) ⊤
have rw : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (⨆ (χ : ↥H → K), genWeightSpace (↥U) χ)
Tactic: rw [← iSup_genWeightSpace_eq_top K H U, iSup_split_single _ 0, biSup_congr hU, this, sup_bot_eq]
-- 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) χ) ⊥
this : Eq (α := LieSubmodule K ↥H ↥U) (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ 0), ⊥) ⊥
rw : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (⨆ (χ : ↥H → K), genWeightSpace (↥U) χ)
⊢ Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) ⊤
have rw₁ : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0)
  (genWeightSpace (↥U) 0 ⊔ ⨆ (i : ↥H → K), ⨆ (_ : i ≠ 0), genWeightSpace (↥U) i)
Tactic: rw [← iSup_genWeightSpace_eq_top K H U, iSup_split_single _ 0, biSup_congr hU, this, sup_bot_eq]
-- 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) χ) ⊥
this : Eq (α := LieSubmodule K ↥H ↥U) (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ 0), ⊥) ⊥
rw : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (⨆ (χ : ↥H → K), genWeightSpace (↥U) χ)
rw₁ :
  Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0)
    (genWeightSpace (↥U) 0 ⊔ ⨆ (i : ↥H → K), ⨆ (_ : i ≠ 0), genWeightSpace (↥U) i)
⊢ Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) ⊤
have rw₂ : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (genWeightSpace (↥U) 0 ⊔ ⨆ (i : ↥H → K), ⨆ (_ : i ≠ 0), ⊥)
Tactic: rw [← iSup_genWeightSpace_eq_top K H U, iSup_split_single _ 0, biSup_congr hU, this, sup_bot_eq]
-- 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) χ) ⊥
this : Eq (α := LieSubmodule K ↥H ↥U) (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ 0), ⊥) ⊥
rw : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (⨆ (χ : ↥H → K), genWeightSpace (↥U) χ)
rw₁ :
  Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0)
    (genWeightSpace (↥U) 0 ⊔ ⨆ (i : ↥H → K), ⨆ (_ : i ≠ 0), genWeightSpace (↥U) i)
rw₂ : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (genWeightSpace (↥U) 0 ⊔ ⨆ (i : ↥H → K), ⨆ (_ : i ≠ 0), ⊥)
⊢ Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) ⊤
have rw₃ : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (genWeightSpace (↥U) 0 ⊔ ⊥)
Tactic: rw [← iSup_genWeightSpace_eq_top K H U, iSup_split_single _ 0, biSup_congr hU, this, sup_bot_eq]
-- 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) χ) ⊥
this : Eq (α := LieSubmodule K ↥H ↥U) (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ 0), ⊥) ⊥
rw : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (⨆ (χ : ↥H → K), genWeightSpace (↥U) χ)
rw₁ :
  Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0)
    (genWeightSpace (↥U) 0 ⊔ ⨆ (i : ↥H → K), ⨆ (_ : i ≠ 0), genWeightSpace (↥U) i)
rw₂ : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (genWeightSpace (↥U) 0 ⊔ ⨆ (i : ↥H → K), ⨆ (_ : i ≠ 0), ⊥)
rw₃ : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (genWeightSpace (↥U) 0 ⊔ ⊥)
⊢ Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) ⊤
have rw₄ : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (genWeightSpace (↥U) 0)
Tactic: rw [← iSup_genWeightSpace_eq_top K H U, iSup_split_single _ 0, biSup_congr hU, this, sup_bot_eq]
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i_1 : ι
hi : v b i_1 ∈ U
_i : InvolutiveNeg ι := P.indexNeg
i : ↥b.support
⊢ ω b *ᵥ u i = u i
have h : ∀ (j : ↥b.support), (ω b *ᵥ u i) (Sum.inl j) = u 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i_1 : ι
hi : v b i_1 ∈ U
_i : InvolutiveNeg ι := P.indexNeg
i : ↥b.support
h : ∀ (j : ↥b.support), (ω b *ᵥ u i) (Sum.inl j) = u i (Sum.inl j)
⊢ ω b *ᵥ u i = u i
have h₁ : ∀ (j : ι), (ω b *ᵥ u i) (Sum.inr j) = u i (Sum.inr j)
Tactic: ext (j | j)
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i : ι
hi : v b i ∈ U
_i : InvolutiveNeg ι := P.indexNeg
⊢ U = ⊤
have hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
Tactic: have hωu (i : b.support) : ω b *ᵥ (u i) = u i := by
    ext (j | j) <;> simp [ω, u, Pi.single_apply, one_apply]
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i_1 : ι
hi : v b i_1 ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
i : ι
⊢ ω b *ᵥ v b i = v b (-i)
have h : ∀ (j : ↥b.support), (ω b *ᵥ v b i) (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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i_1 : ι
hi : v b i_1 ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
i : ι
h : ∀ (j : ↥b.support), (ω b *ᵥ v b i) (Sum.inl j) = v b (-i) (Sum.inl j)
⊢ ω b *ᵥ v b i = v b (-i)
have h₁ : ∀ (j : ι), (ω b *ᵥ v b i) (Sum.inr j) = v b (-i) (Sum.inr j)
Tactic: ext (j | j)
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i : ι
hi : v b i ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
⊢ U = ⊤
have hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
Tactic: have hωv (i : ι) : ω b *ᵥ (v b i) = v b (-i) := by ext (j | j) <;> simp [ω, v, Pi.single_apply]
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
i : ι
hi : v b i ∈ U
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∃ (j : ↥b.support), u j ∈ U
have revert : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U
Tactic: revert U
Cleared hypotheses: U, 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
⊢ ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U
have h₀ : ∀ (i : ι),
  (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U) →
    ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b ((P.reflectionPerm i : (a : ι) → ι) i) ∈ U),
      ∃ (j : ↥b.support), u j ∈ U
Tactic: apply b.induction_add 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
h₀ :
  ∀ (i : ι),
    (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U) →
      ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}
        (hi : v b ((P.reflectionPerm i : (a : ι) → ι) i) ∈ U), ∃ (j : ↥b.support), u j ∈ U
⊢ ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U
have h₁ : ∀ i ∈ b.support,
  ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U
Tactic: apply b.induction_add 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
h₀ :
  ∀ (i : ι),
    (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U) →
      ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}
        (hi : v b ((P.reflectionPerm i : (a : ι) → ι) i) ∈ U), ∃ (j : ↥b.support), u j ∈ U
h₁ :
  ∀ i ∈ b.support,
    ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U
⊢ ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U
have h₂ : ∀ (i j k : ι),
  (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M) →
    (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U) →
      j ∈ b.support →
        ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b k ∈ U), ∃ (j : ↥b.support), u j ∈ U
Tactic: apply b.induction_add 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
i_1 : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
i : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hi : v b ((P.reflectionPerm i : (a : ι) → ι) i) ∈ U
⊢ ∃ (j : ↥b.support), u j ∈ U
have hi₁ : v b i ∈ ωConjLieSubmodule U
Tactic: replace hi : v b i ∈ ωConjLieSubmodule U := by simpa [hωv]
Cleared hypotheses: 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
i_1 : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
i : ι
h : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hi : v b i ∈ ωConjLieSubmodule U
⊢ ∃ (j : ↥b.support), u j ∈ U
have h₀ : ∀ (j : ↥b.support) (hj : u j ∈ ωConjLieSubmodule U), ∃ (j : ↥b.support), u j ∈ U
Tactic: obtain ⟨j, hj⟩ := h hi
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j : ι
hj : j ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hj' : v b j ∈ U
f' : ↥(lieAlgebra b) :=
  Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
    Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b) x)
    (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) j hj)) ⋯
⊢ ∃ (j : ↥b.support), u j ∈ U
have this : ⁅f', v b j⁆ = u (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) j hj)
Tactic: have : ⁅f', v b j⁆ = u ⟨j, hj⟩ := f_lie_v_same ⟨j, hj⟩
-- 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j : ι
hj : j ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hj' : v b j ∈ U
f' : ↥(lieAlgebra b) :=
  Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
    Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b) x)
    (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) j hj)) ⋯
this : ⁅f', v b j⁆ = u (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) j hj)
⊢ u (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) j hj) ∈ U
have rw : ⁅f', v b j⁆ ∈ U
Tactic: rw [← 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j : ι
hj : j ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hj' : v b j ∈ U
f' : ↥(lieAlgebra b) :=
  Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
    Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b) x)
    (f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) j hj)) ⋯
this : ⁅f', v b j⁆ = u (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) j hj)
⊢ ∃ (j : ↥b.support), u j ∈ U
have this₁ : u (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) j hj) ∈ U
Tactic: replace this : u ⟨j, hj⟩ ∈ U := by
        rw [← this]
        exact U.lie_mem (x := f') hj'
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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
h₂ : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b j ∈ U), ∃ (j : ↥b.support), u j ∈ U
hk : k ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hl : v b l ∈ U
⊢ ∃ (j : ↥b.support), u j ∈ U
have this : ⁅f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) k hk), v b l⁆ =
  HAdd.hAdd (α := K) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := K) (M := M) (N := N) (P := P) k l) : K) 1 • v b j
Tactic: have : ⁅f ⟨k, hk⟩, v b l⁆ = (P.chainTopCoeff k l + 1 : K) • v b j := f_lie_v_ne 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.IsCrystallographic
b : P.Base
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
i : ι
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l : ι
h₁ :
  (P.root : (a : ι) → M) l = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M)
h₂ : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b j ∈ U), ∃ (j : ↥b.support), u j ∈ U
hk : k ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
hl : v b l ∈ U
this :
  ⁅f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) k hk), v b l⁆ =
    HAdd.hAdd (α := K) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := K) (M := M) (N := N) (P := P) k l) : K) 1 • v b j
⊢ HAdd.hAdd (α := K) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := K) (M := M) (N := N) (P := P) k l) : K) 1 • v b j ∈ U
have rw : ⁅f (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) k hk), v b l⁆ ∈ U
Tactic: rw [← this]