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.IsCrystallographic
b : P.Base
i : ↥b.support
refine_2 :
  ∀ (x : ↥H),
    ∃ (k : ℕ),
      Eq (α := ↥b.support ⊕ ι → K)
        ((HSub.hSub (α := Module.End K (↥b.support ⊕ ι → K))
                  (((toEnd K (↥H) (↥b.support ⊕ ι → K) : ↥H →ₗ⁅K⁆ Module.End K (↥b.support ⊕ ι → K)) :
                        (a : ↥H) → Module.End K (↥b.support ⊕ ι → K))
                      x :
                    Module.End K (↥b.support ⊕ ι → K))
                  (HSMul.hSMul (α := K) (β := Module.End K (↥b.support ⊕ ι → K)) (0 x) 1) ^
                k :
              (a : ↥b.support ⊕ ι → K) → ↥b.support ⊕ ι → K)
            (u i) :
          ↥b.support ⊕ ι → K)
        (0 : ↥b.support ⊕ ι → K)
⊢ u i ∈
    (↑((↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K)) :
          Submodule K (↥b.support ⊕ ι → K)) :
      Set (↥b.support ⊕ ι → K))

Tactic:
simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule, mem_genWeightSpace]

Premises used: LieSubmodule.mem_toSubmodule, LieModule.mem_genWeightSpace, SetLike.mem_coe
-- 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
i : ↥b.support
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K
property :
  Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b) x
hx :
  Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H
    (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)
      x property)
j : ↥b.support ⊕ ι
⊢ Eq.{u_2 + 1} (α := K)
    ((HPow.hPow (β := ℕ)
            (HSub.hSub (α := Module.End K (↥b.support ⊕ ι → K))
              (((toEnd K (↥H) (↥b.support ⊕ ι → K) : ↥H →ₗ⁅K⁆ Module.End K (↥b.support ⊕ ι → K)) :
                    (a : ↥H) → Module.End K (↥b.support ⊕ ι → K))
                  (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
                    Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
                    (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
                      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
                        (lieAlgebra b) x)
                      x property)
                    hx) :
                Module.End K (↥b.support ⊕ ι → K))
              (HSMul.hSMul (α := K) (β := Module.End K (↥b.support ⊕ ι → K))
                (0
                  (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
                    Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
                    (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
                      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
                        (lieAlgebra b) x)
                      x property)
                    hx))
                1))
            1 :
          (a : ↥b.support ⊕ ι → K) → ↥b.support ⊕ ι → K)
        (u i) j :
      K)
    (0 j : K)

Tactic:
simpa using apply_sum_inl_eq_zero_of_mem_span_h i j hx

Premises used: RootPairing.GeckConstruction.apply_sum_inl_eq_zero_of_mem_span_h
-- 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
i : ↥b.support
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K
property :
  Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b) x
hx :
  Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H
    (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)
      x property)
⊢ ∃ (k : ℕ),
    Eq (α := ↥b.support ⊕ ι → K)
      ((HSub.hSub (α := Module.End K (↥b.support ⊕ ι → K))
                (((toEnd K (↥H) (↥b.support ⊕ ι → K) : ↥H →ₗ⁅K⁆ Module.End K (↥b.support ⊕ ι → K)) :
                      (a : ↥H) → Module.End K (↥b.support ⊕ ι → K))
                    (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
                      Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
                      (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
                        Membership.mem (γ :=
                          LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
                          x)
                        x property)
                      hx) :
                  Module.End K (↥b.support ⊕ ι → K))
                (HSMul.hSMul (α := K) (β := Module.End K (↥b.support ⊕ ι → K))
                  (0
                    (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
                      Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) H x)
                      (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
                        Membership.mem (γ :=
                          LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
                          x)
                        x property)
                      hx))
                  1) ^
              k :
            (a : ↥b.support ⊕ ι → K) → ↥b.support ⊕ ι → K)
          (u i) :
        ↥b.support ⊕ ι → K)
      (0 : ↥b.support ⊕ ι → K)

Tactic:
exact ⟨1, funext fun j ↦ by simpa using apply_sum_inl_eq_zero_of_mem_span_h i 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 ι
⊢ LieModule.IsIrreducible K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)

Tactic:
LieModule.IsIrreducible.mk fun U hU ↦ ?_

Premises used: LieModule.IsIrreducible.mk
-- 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 ι
refine : ∀ (U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)) (hU : U ≠ ⊥), U = ⊤
⊢ LieModule.IsIrreducible K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)

Tactic:
refine LieModule.IsIrreducible.mk fun U hU ↦ ?_

Premises used: LieModule.IsIrreducible.mk
-- 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)
hU : U ≠ ⊥
this : ∃ (i : ι), v b i ∈ U
obtain : ∀ (i : ι) (hi : v b i ∈ U), U = ⊤
⊢ U = ⊤

Tactic:
obtain ⟨i, hi⟩ := 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)
hU : U ≠ ⊥
i : ι
hi : v b i ∈ U
⊢ U = ⊤

Tactic:
instIsIrreducible_aux₂ hi

Premises used: _private.0.RootPairing.GeckConstruction.instIsIrreducible_aux₂
-- 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)
hU : U ≠ ⊥
i : ι
hi : v b i ∈ U
⊢ U = ⊤

Tactic:
exact instIsIrreducible_aux₂ hi

Premises used: _private.0.RootPairing.GeckConstruction.instIsIrreducible_aux₂
-- 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)
hU : U ≠ ⊥
suffices : ∃ (i : ι), v b i ∈ U
⊢ U = ⊤

Tactic:
suffices ∃ i, v b i ∈ U by obtain ⟨i, hi⟩ := this; exact instIsIrreducible_aux₂ 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.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 := ⋯ }
apply : ¬U' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ ∃ (i : ι), v b i ∈ U

Tactic:
apply instIsIrreducible_aux₁ U'

Premises used: _private.0.RootPairing.GeckConstruction.instIsIrreducible_aux₁
-- 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)
hU : U ≠ ⊥
U' : LieSubmodule K (↥H) (↥b.support ⊕ ι → K) :=
  { toSubmodule := (↑U : Submodule K (↥b.support ⊕ ι → K)), lie_mem := ⋯ }
contrapose : ∀ (hU : U' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0), U = ⊥
⊢ ¬U' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0

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
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
rwa rwa₁ rwa₂ rwa₃ :
  (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤
    (↑(genWeightSpace (↥b.support ⊕ ι → K) 0) : Submodule K (↥b.support ⊕ ι → K))
⊢ (↑U : Submodule K (↥b.support ⊕ ι → K)) ≤ span K (range u)

Tactic:
rwa [← coe_genWeightSpace_zero_eq_span_range_u]

Premises used: RootPairing.GeckConstruction.coe_genWeightSpace_zero_eq_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' ≤ genWeightSpace (↥b.support ⊕ ι → K) 0
⊢ (↑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]
-- 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)
⊢ U = ⊥

Tactic:
(LieSubmodule.eq_bot_iff _).mpr fun x hx ↦ ?_

Premises used: Iff.mpr, LieSubmodule.eq_bot_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)
refine : ∀ (x : ↥b.support ⊕ ι → K) (hx : x ∈ U), x = 0
⊢ U = ⊥

Tactic:
refine (LieSubmodule.eq_bot_iff _).mpr fun x hx ↦ ?_

Premises used: Iff.mpr, LieSubmodule.eq_bot_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), ∑ i : ↥b.support, c i • u i = x

Tactic:
(mem_span_range_iff_exists_fun K).mp <| hU hx

Premises used: Submodule.mem_span_range_iff_exists_fun, Iff.mp
-- 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
obtain : ∀ (c : ↥b.support → K) (hc : ∑ i : ↥b.support, c i • u i = x), x = 0
⊢ 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

Premises used: Submodule.mem_span_range_iff_exists_fun, Iff.mp
-- 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
this : c = 0
⊢ x = 0

Tactic:
simp [this, ← hc]
-- 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
suffices : c = 0
⊢ x = 0

Tactic:
suffices c = 0 by simp [this, ← hc]
-- 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
⊢ (4 - b.cartanMatrix).det ≠ 0

Tactic:
have hCM : (4 - b.cartanMatrix).det ≠ 0 := Fact.out
-- 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 : (4 - b.cartanMatrix).det ≠ 0
contrapose! : ∀ (hCM : c ≠ 0), (4 - b.cartanMatrix).det = 0
⊢ c = 0

Tactic:
contrapose! hCM
-- 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 :
  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
⊢ (4 - b.cartanMatrix).det = 0

Tactic:
simpa only [← RingHom.map_det, eq_intCast, Int.cast_eq_zero] using this

Premises used: eq_intCast, RingHom.map_det, Int.cast_eq_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
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 :
  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
⊢ (4 - b.cartanMatrix).det = 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