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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
rw :
  ∃ (v : ↥b.support → K),
    v ≠ 0 ∧
      Eq (α := ↥b.support → K)
        ((RingHom.mapMatrix (Int.castRingHom K) :
              (a : Matrix ↥b.support ↥b.support ℤ) → Matrix (↥b.support) (↥b.support) K)
            (4 - b.cartanMatrix) *ᵥ
          v)
        0
⊢ Eq.{u_2 + 1} (α := K)
    (det.{u_2, u_1} (n := ↥b.support)
      ((RingHom.mapMatrix (Int.castRingHom K) :
          (a : Matrix ↥b.support ↥b.support ℤ) → Matrix (↥b.support) (↥b.support) K)
        (4 - b.cartanMatrix)))
    0

Tactic:
rw [← exists_mulVec_eq_zero_iff]

Premises used: Matrix.exists_mulVec_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
this : (b.cartanMatrix.map abs).map Int.cast *ᵥ c = 0
⊢ Eq (α := ↥b.support → K)
    ((RingHom.mapMatrix (Int.castRingHom K) : (a : Matrix ↥b.support ↥b.support ℤ) → Matrix (↥b.support) (↥b.support) K)
        (4 - b.cartanMatrix) *ᵥ
      c)
    0

Tactic:
simpa using 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
suffices : (b.cartanMatrix.map abs).map Int.cast *ᵥ c = 0
⊢ ∃ (v : ↥b.support → K),
    v ≠ 0 ∧
      Eq (α := ↥b.support → K)
        ((RingHom.mapMatrix (Int.castRingHom K) :
              (a : Matrix ↥b.support ↥b.support ℤ) → Matrix (↥b.support) (↥b.support) K)
            (4 - b.cartanMatrix) *ᵥ
          v)
        0

Tactic:
suffices (b.cartanMatrix.map abs).map (↑) *ᵥ c = 0 from ⟨c, hCM, by simpa using 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
h : ∀ (j : ↥b.support), ((b.cartanMatrix.map abs).map Int.cast *ᵥ c) j = 0 j
⊢ (b.cartanMatrix.map abs).map Int.cast *ᵥ c = 0

Tactic:
ext 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.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
this : Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
⊢ ((b.cartanMatrix.map abs).map Int.cast *ᵥ c) j = 0 j

Tactic:
simpa [mulVec_eq_sum, -Base.cartanMatrix_map_abs]

Premises used: RootPairing.Base.cartanMatrix_map_abs, Matrix.mulVec_eq_sum
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
h : Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
⊢ ((b.cartanMatrix.map abs).map Int.cast *ᵥ c) j = 0 j

Tactic:
suffices ∑ k, c k * |b.cartanMatrix j k| = 0 by
    simpa [mulVec_eq_sum, -Base.cartanMatrix_map_abs]
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
h : ∀ (contra : ¬Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0), False
⊢ Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0

Tactic:
by_contra contra
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
⊢ ⁅e j, x⁆ ∈ U

Tactic:
have : ⁅e j, x⁆ ∈ U := U.lie_mem (x := ⟨e j, e_mem_lieAlgebra j⟩) hx
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
this : ⁅e j, x⁆ ∈ U
⊢ ∀ (k : ↥b.support), ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b (↑j : ι)

Tactic:
have aux (k : b.support) : ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b j := e_lie_u j k
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
this : ⁅e j, x⁆ ∈ U
aux : ∀ (k : ↥b.support), ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b (↑j : ι)
⊢ v b (↑j : ι) ∈ (↑U : Submodule K (↥b.support ⊕ ι → K))

Tactic:
simp_rw [← hc, lie_sum, lie_smul, aux, smul_comm (M := K), ← smul_assoc, ← Finset.sum_smul,
      zsmul_eq_mul, mul_comm, ← LieSubmodule.mem_toSubmodule, U.smul_mem_iff contra] at this

Premises used: Finset.sum_smul, zsmul_eq_mul, lie_sum, smul_assoc, LieSubmodule.mem_toSubmodule, lie_smul, LieSubmodule.toSubmodule, Submodule.smul_mem_iff, mul_comm, SMulCommClass.smul_comm
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
aux : ∀ (k : ↥b.support), ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b (↑j : ι)
this : v b (↑j : ι) ∈ (↑U : Submodule K (↥b.support ⊕ ι → K))
⊢ v b (↑j : ι) ∈ U

Tactic:
assumption
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
⊢ v b (↑j : ι) ∈ U

Tactic:
have key : v b j ∈ U := by
    have : ⁅e j, x⁆ ∈ U := U.lie_mem (x := ⟨e j, e_mem_lieAlgebra j⟩) hx
    have aux (k : b.support) : ⁅e j, u k⁆ = |b.cartanMatrix j k| • v b j := e_lie_u j k
    simp_rw [← hc, lie_sum, lie_smul, aux, smul_comm (M := K), ← smul_assoc, ← Finset.sum_smul,
      zsmul_eq_mul, mul_comm, ← LieSubmodule.mem_toSubmodule, U.smul_mem_iff contra] at this
    assumption
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
key hj : v b (↑j : ι) ∈ U
⊢ False

Tactic:
simpa [v] using apply_inr_eq_zero_of_mem_span_range_u b j (hU hj)

Premises used: RootPairing.GeckConstruction.v, Subtype.val, RootPairing.GeckConstruction.apply_inr_eq_zero_of_mem_span_range_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.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
key : v b (↑j : ι) ∈ U
⊢ v b (↑j : ι) ∉ U

Tactic:
have : v b j ∉ U := fun hj ↦ by simpa [v] using apply_inr_eq_zero_of_mem_span_range_u b j (hU 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.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : Nonempty ι
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
hU : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
x : ↥b.support ⊕ ι → K
hx : x ∈ U
c : ↥b.support → K
hc : ∑ i : ↥b.support, c i • u i = x
hCM : c ≠ 0
j : ↥b.support
contra : ¬Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
key : v b (↑j : ι) ∈ U
this : v b (↑j : ι) ∉ U
⊢ False

Tactic:
contradiction
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : IsAlgClosed K
inl : IsEmpty ι → LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)
inr : Nonempty ι → LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : IsAlgClosed K
h : IsEmpty ι
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)

Tactic:
infer_instance
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : IsAlgClosed K
h : Nonempty ι
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)

Tactic:
LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful K _ _ trace_toEnd_eq_zero

Premises used: RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : IsAlgClosed K
h : Nonempty ι
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)

Tactic:
exact LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful K _ _ trace_toEnd_eq_zero

Premises used: RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
x : N₂
f : P.Hom Q
⊢ Eq (α := Module.Dual R M)
    ((f.weightMap.dualMap : (a : Module.Dual R M₂) → Module.Dual R M)
        ((Q.flip.toPerfPair : (a : N₂) → Module.Dual R M₂) x) :
      Module.Dual R M)
    ((P.flip.toPerfPair : (a : N) → Module.Dual R M) ((f.coweightMap : (a : N₂) → N) x) : Module.Dual R M)

Tactic:
Eq.mp (propext LinearMap.ext_iff) f.weight_coweight_transpose x

Premises used: RootPairing.Hom.weight_coweight_transpose, Eq.mp, LinearMap.ext_iff, propext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
i : ι
f : P.Hom Q
⊢ Eq.{u_6 + 1} (α := M₂) ((f.weightMap : (a : M) → M₂) ((P.root : (a : ι) → M) i : M) : M₂)
    ((Q.root : (a : ι₂) → M₂) ((f.indexEquiv : (a : ι) → ι₂) i : ι₂) : M₂)

Tactic:
Eq.mp (propext funext_iff) f.root_weightMap i

Premises used: RootPairing.Hom.root_weightMap, funext_iff, Eq.mp, propext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : AddCommGroup N₂
inst_8 : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
i : ι₂
f : P.Hom Q
⊢ Eq.{u_4 + 1} (α := N) ((f.coweightMap : (a : N₂) → N) ((Q.coroot : (a : ι₂) → N₂) i : N₂) : N)
    ((P.coroot : (a : ι) → N) ((f.indexEquiv.symm : (a : ι₂) → ι) i : ι) : N)

Tactic:
Eq.mp (propext funext_iff) f.coroot_coweightMap i

Premises used: funext_iff, Eq.mp, RootPairing.Hom.coroot_coweightMap, propext
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ LinearMap.dualMap LinearMap.id ∘ₗ (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ LinearMap.id

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ Eq (α := ι → M) (comp (β := M) (⇑LinearMap.id : (a : M) → M) (⇑P.root : (a : ι) → M))
    (comp (β := ι) (⇑P.root : (a : ι) → M) (⇑(Equiv.refl ι) : (a : ι) → ι))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Hom
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
⊢ Eq (α := ι → N) (comp (β := N) (⇑LinearMap.id : (a : N) → N) (⇑P.coroot : (a : ι) → N))
    (comp (β := ι) (⇑P.coroot : (a : ι) → N) (⇑(Equiv.refl ι).symm : (a : ι) → ι))

Tactic:
simp