awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ¬U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
contrapose! :
  ∀ (hU : ∀ (χ : ↥H → K) (_ : χ ≠ 0), Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥),
    U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ ∃ (χ : ↥H → K), χ ≠ 0 ∧ Ne (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥

Tactic:
contrapose! hU
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K) (_ : χ ≠ 0), Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
⊢ U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0

Tactic:
le_trans ?_ (map_genWeightSpace_le (f := U.incl))

Premises used: LieModule.map_genWeightSpace_le, LieSubmodule.incl, le_trans
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K) (_ : χ ≠ 0), Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
refine : U ≤ LieSubmodule.map U.incl (genWeightSpace (↥U) 0)
⊢ U ≤ genWeightSpace (↥b.support ⊕ ι → K) 0

Tactic:
refine le_trans ?_ (map_genWeightSpace_le (f := U.incl))

Premises used: LieModule.map_genWeightSpace_le, LieSubmodule.incl, le_trans
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K) (_ : χ ≠ 0), Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
this : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) ⊤
⊢ U ≤ LieSubmodule.map U.incl (genWeightSpace (↥U) 0)

Tactic:
simp [this]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K) (_ : χ ≠ 0), Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
suffices : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) ⊤
⊢ U ≤ LieSubmodule.map U.incl (genWeightSpace (↥U) 0)

Tactic:
suffices genWeightSpace U (0 : H → K) = ⊤ by simp [this]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
hU : ∀ (χ : ↥H → K) (_ : χ ≠ 0), Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) χ) ⊥
⊢ Eq (α := LieSubmodule K ↥H ↥U) (⨆ (χ : ↥H → K), ⨆ (_ : χ ≠ 0), ⊥) ⊥

Tactic:
have : ⨆ (χ : H → K), ⨆ (_ : χ ≠ 0), (⊥ : LieSubmodule K H U) = ⊥ := biSup_const ⟨1, one_ne_zero⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
U : LieSubmodule K (↥H) (↥b.support ⊕ ι → K)
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 ⊔ ⊥)
rw₄ rw₅ : Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) (genWeightSpace (↥U) 0)
⊢ Eq (α := LieSubmodule K ↥H ↥U) (genWeightSpace (↥U) 0) ⊤

Tactic:
rw [← iSup_genWeightSpace_eq_top K H U, iSup_split_single _ 0, biSup_congr hU, this, sup_bot_eq]

Premises used: iSup_split_single, sup_bot_eq, OfNat.ofNat, biSup_congr
-- 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.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)
h₁ : ∀ (j : ι), (ω b *ᵥ u i) (Sum.inr j) = u i (Sum.inr j)
⊢ ω b *ᵥ u i = u i

Tactic:
ext (j | j)
-- 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.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 j : ↥b.support
⊢ (ω b *ᵥ u i) (Sum.inl j) = u i (Sum.inl j)

Tactic:
simp [ω, u, Pi.single_apply, one_apply]

Premises used: Matrix.one_apply, RootPairing.GeckConstruction.ω, Pi.single_apply, RootPairing.GeckConstruction.u
-- 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.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
j : ι
⊢ (ω b *ᵥ u i) (Sum.inr j) = u i (Sum.inr j)

Tactic:
simp [ω, u, Pi.single_apply, one_apply]

Premises used: Matrix.one_apply, RootPairing.GeckConstruction.ω, Pi.single_apply, RootPairing.GeckConstruction.u
-- 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.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
⊢ ∀ (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]
-- 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.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)
h₁ : ∀ (j : ι), (ω b *ᵥ v b i) (Sum.inr j) = v b (-i) (Sum.inr j)
⊢ ω b *ᵥ v b i = v b (-i)

Tactic:
ext (j | j)
-- 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.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 : ι
j : ↥b.support
⊢ (ω b *ᵥ v b i) (Sum.inl j) = v b (-i) (Sum.inl j)

Tactic:
simp [ω, v, Pi.single_apply]

Premises used: RootPairing.GeckConstruction.ω, Pi.single_apply, RootPairing.GeckConstruction.v
-- 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.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 j : ι
⊢ (ω b *ᵥ v b i) (Sum.inr j) = v b (-i) (Sum.inr j)

Tactic:
simp [ω, v, Pi.single_apply]

Premises used: RootPairing.GeckConstruction.ω, Pi.single_apply, RootPairing.GeckConstruction.v
-- 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.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
⊢ ∀ (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]
-- 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.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)
revert : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)} (hi : v b i ∈ U), ∃ (j : ↥b.support), u j ∈ U
⊢ ∃ (j : ↥b.support), u j ∈ U

Tactic:
revert U
-- 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.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
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
⊢ ∀ {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

Premises used: RootPairing.Base.induction_add
-- 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.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
⊢ v b i ∈ ωConjLieSubmodule U

Tactic:
simpa [hωv]
-- 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.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
⊢ v b i ∈ ωConjLieSubmodule U

Tactic:
replace hi : v b i ∈ ωConjLieSubmodule U := by simpa [hωv]
-- 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.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
h₀ : ∀ (j : ↥b.support) (hj : u j ∈ ωConjLieSubmodule U), ∃ (j : ↥b.support), u j ∈ U
⊢ ∃ (j : ↥b.support), u j ∈ U

Tactic:
obtain ⟨j, hj⟩ := h hi
-- 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.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
hj : u j ∈ ωConjLieSubmodule U
⊢ u j ∈ U

Tactic:
simpa [hωu] using hj
-- 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.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
hj : u j ∈ ωConjLieSubmodule U
⊢ ∃ (j : ↥b.support), u j ∈ U

Tactic:
exact ⟨j, by simpa [hωu] using hj⟩
-- 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.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)) ⋯
⊢ ⁅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⟩
-- 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.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)
rw : ⁅f', v b j⁆ ∈ U
⊢ u (Subtype.mk (p := fun (x : ι) ↦ x ∈ b.support) j hj) ∈ U

Tactic:
rw [← this]
-- 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.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)
⊢ ⁅f', v b j⁆ ∈ U

Tactic:
U.lie_mem (x := f') hj'

Premises used: Set.Mem, LieSubmodule.lie_mem
-- 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.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)
⊢ ⁅f', v b j⁆ ∈ U

Tactic:
exact U.lie_mem (x := f') hj'

Premises used: LieSubmodule.lie_mem
-- 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.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

Tactic:
replace this : u ⟨j, hj⟩ ∈ U := by
        rw [← this]
        exact U.lie_mem (x := f') hj'