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
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)
hU : U ≠ ⊥
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
⊢ ¬U' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
have contrapose : ∀ (hU : U' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0), U = ⊥
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
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' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
have rwa : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ (↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K))
Tactic: rwa [← coe_genWeightSpace_zero_eq_span_range_u]
-- 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
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' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ U = ⊥
have hU₁ : (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)
Tactic: replace hU : U ≤ span K (range (u (b := b))) := by rwa [← coe_genWeightSpace_zero_eq_span_range_u]
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
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)
⊢ U = ⊥
have refine : ∀ (x : ↥b.support ⊕ ι → K) (hx : x ∈ U), x = 0
Tactic: refine (LieSubmodule.eq_bot_iff _).mpr fun x hx ↦ ?_
-- 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
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
⊢ x = 0
have obtain : ∀ (c : ↥b.support → K) (hc : ∑ i : ↥b.support, c i • u i = x), x = 0
Tactic: obtain ⟨c, hc⟩ : ∃ c : b.support → K, ∑ i, c i • u i = x :=
    (mem_span_range_iff_exists_fun K).mp <| hU hx
-- 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
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
⊢ x = 0
have suffices : c = 0
Tactic: suffices c = 0 by simp [this, ← hc]
-- 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
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
⊢ c = 0
have hCM : (4 - b.cartanMatrix).det ≠ 0
Tactic: have hCM : (4 - b.cartanMatrix).det ≠ 0 := Fact.out
-- 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
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 : (4 - b.cartanMatrix).det ≠ 0
⊢ c = 0
have contrapose! : ∀ (hCM : c ≠ 0), (4 - b.cartanMatrix).det = 0
Tactic: contrapose! hCM
Cleared hypotheses: hCM
-- 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
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
⊢ (4 - b.cartanMatrix).det = 0
have suffices : 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: suffices ((Int.castRingHom K).mapMatrix (4 - b.cartanMatrix)).det = 0 by
    simpa only [← RingHom.map_det, eq_intCast, Int.cast_eq_zero] using 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
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
⊢ 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
have 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
Tactic: rw [← exists_mulVec_eq_zero_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
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
⊢ ∃ (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
have suffices : (b.cartanMatrix.map abs).map Int.cast *ᵥ c = 0
Tactic: suffices (b.cartanMatrix.map abs).map (↑) *ᵥ c = 0 from ⟨c, hCM, by simpa using 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
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
⊢ (b.cartanMatrix.map abs).map Int.cast *ᵥ c = 0
have h : ∀ (j : ↥b.support), ((b.cartanMatrix.map abs).map Int.cast *ᵥ c) j = 0 j
Tactic: ext 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
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
⊢ ((b.cartanMatrix.map abs).map Int.cast *ᵥ c) j = 0 j
have h : Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
Tactic: suffices ∑ k, c k * |b.cartanMatrix j k| = 0 by
    simpa [mulVec_eq_sum, -Base.cartanMatrix_map_abs]
-- 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
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
⊢ Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0
have h : ∀ (contra : ¬Eq.{u_2 + 1} (α := K) (∑ k : ↥b.support, c k * (↑|b.cartanMatrix j k| : K)) 0), False
Tactic: by_contra contra
-- 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
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
have this : ⁅e j, x⁆ ∈ U
Tactic: have : ⁅e j, x⁆ ∈ U := U.lie_mem (x := ⟨e j, e_mem_lieAlgebra j⟩) hx
-- 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
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
⊢ v b (↑j : ι) ∈ U
have aux : ∀ (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
-- 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
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
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple (hypothesis)
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : CharZero K
inst_2 : DecidableEq ι
inst_3 : Fintype ι
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsRootSystem
inst_9 : P.IsCrystallographic
b : P.Base
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
⊢ False
have key : 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
-- 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
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
⊢ False
have this : 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)
-- 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
inst_10 : Fact ((4 - b.cartanMatrix).det ≠ 0)
inst_11 : P.IsReduced
inst_12 : P.IsIrreducible
inst_13 : IsAlgClosed K
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)
have inl : IsEmpty ι → LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)
Tactic: cases isEmpty_or_nonempty ι
-- 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
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)
⊢ LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)
have inr : Nonempty ι → LieAlgebra.HasTrivialRadical K ↥(lieAlgebra b)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Hom (goal)
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
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
inst_5 : AddCommGroup M₁
inst_6 : Module R M₁
inst_7 : AddCommGroup N₁
inst_8 : Module R N₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
inst_11 : AddCommGroup N₂
inst_12 : Module R N₂
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
g : P₁.Hom P₂
f : P.Hom P₁
⊢ (g.weightMap ∘ₗ f.weightMap).dualMap ∘ₗ (↑P₂.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) =
    (↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ f.coweightMap ∘ₗ g.coweightMap
have h : ∀ (φ : N₂) (x : M),
  Eq.{u_2 + 1} (α := R)
    (((((g.weightMap ∘ₗ f.weightMap).dualMap ∘ₗ (↑P₂.flip.toPerfPair : N₂ →ₗ[R] Module.Dual R M₂) :
                (a : N₂) → Module.Dual R M)
              φ :
            Module.Dual R M) :
          (a : M) → R)
        x :
      R)
    (((((↑P.flip.toPerfPair : N →ₗ[R] Module.Dual R M) ∘ₗ f.coweightMap ∘ₗ g.coweightMap : (a : N₂) → Module.Dual R M)
              φ :
            Module.Dual R M) :
          (a : M) → R)
        x :
      R)
Tactic: ext φ x