awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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 i) ⋯
refine : range h₀ ⊆ (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
⊢ range h₀ ∪ (range e₀ ∪ range f₀) ⊆
    (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))

Tactic:
refine union_subset ?_ LieSubalgebra.subset_lieSpan

Premises used: LieSubalgebra.subset_lieSpan, Set.union_subset
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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 i) ⋯
i : ↥b.support
a :
  (↑(h₀ i) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = (↑⁅e₀ i, f₀ i⁆ : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
⊢ h₀ i = ⁅e₀ i, f₀ i⁆

Tactic:
ext1
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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 i) ⋯
i : ↥b.support
⊢ (↑(h₀ i) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = (↑⁅e₀ i, f₀ i⁆ : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)

Tactic:
simp [h₀, e₀, f₀, (isSl2Triple i).lie_e_f]

Premises used: RootPairing.GeckConstruction.isSl2Triple, IsSl2Triple.lie_e_f
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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 i) ⋯
i : ↥b.support
⊢ h₀ i = ⁅e₀ i, f₀ i⁆

Tactic:
have hef : h₀ i = ⁅e₀ i, f₀ i⁆ := by ext1; simp [h₀, e₀, f₀, (isSl2Triple i).lie_e_f]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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 i) ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
rw : ⁅e₀ i, f₀ i⁆ ∈ (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
⊢ h₀ i ∈ (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))

Tactic:
rw [hef]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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 i) ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
hx :
  Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) (e₀ i)
hy :
  Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) (f₀ i)
⊢ ⁅e₀ i, f₀ i⁆ ∈ (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))

Tactic:
apply LieSubalgebra.lie_mem

Premises used: LieSubalgebra.lie_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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 i) ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ e₀ i ∈ range e₀ ∪ range f₀

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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 i) ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) (e₀ i)

Tactic:
exact LieSubalgebra.subset_lieSpan <| by simp

Premises used: LieSubalgebra.subset_lieSpan
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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 i) ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ f₀ i ∈ range e₀ ∪ range f₀

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    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 i) ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) (f₀ i)

Tactic:
exact LieSubalgebra.subset_lieSpan <| by simp

Premises used: LieSubalgebra.subset_lieSpan
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
apply :
  LinearIndependent (ι := ↥b.support) K (M := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
    (Function.comp (β := ↥(LieSubalgebra.toSubmodule (lieAlgebra b)))
      (⇑(Submodule.subtype (LieSubalgebra.toSubmodule (lieAlgebra b))) :
        (a : ↥(lieAlgebra b).toSubmodule) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
      fun (i : ↥b.support) ↦
      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)
        (h i) ⋯)
⊢ LinearIndependent K (M := ↥(lieAlgebra b)) fun (i : ↥b.support) ↦
    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)
      (h i) ⋯

Tactic:
apply LinearIndependent.of_comp (lieAlgebra b).subtype

Premises used: RootPairing.GeckConstruction.lieAlgebra, LinearIndependent.of_comp, Submodule.subtype, LieSubalgebra.toSubmodule
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
⊢ LinearIndependent (ι := ↥b.support) K (M := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
    (Function.comp (β := ↥(LieSubalgebra.toSubmodule (lieAlgebra b)))
      (⇑(Submodule.subtype (LieSubalgebra.toSubmodule (lieAlgebra b))) :
        (a : ↥(lieAlgebra b).toSubmodule) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
      fun (i : ↥b.support) ↦
      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)
        (h i) ⋯)

Tactic:
linearIndependent_h b

Premises used: Matrix.fromBlocks, RootPairing.GeckConstruction.h, RootPairing.GeckConstruction.linearIndependent_h
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
⊢ LinearIndependent (ι := ↥b.support) K (M := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
    (Function.comp (β := ↥(LieSubalgebra.toSubmodule (lieAlgebra b)))
      (⇑(Submodule.subtype (LieSubalgebra.toSubmodule (lieAlgebra b))) :
        (a : ↥(lieAlgebra b).toSubmodule) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
      fun (i : ↥b.support) ↦
      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)
        (h i) ⋯)

Tactic:
exact linearIndependent_h b

Premises used: RootPairing.GeckConstruction.linearIndependent_h
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
i : ↥b.support
t : IsSl2Triple (h i) (e i) (f i) := ⋯
⊢ Ne (α := ↥(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)
      (h i) ⋯)
    0

Tactic:
simp [Subtype.ext_iff, t.h_ne_zero]

Premises used: Subtype.ext_iff, IsSl2Triple.h_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
i : ↥b.support
t : IsSl2Triple (h i) (e i) (f i) := ⋯
⊢ Eq (α := ↥(lieAlgebra b))
    (Bracket.bracket (L := ↥(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)
        (e i) ⋯)
      (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 i) ⋯))
    (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)
      (h i) ⋯)

Tactic:
simp [Subtype.ext_iff, t.lie_e_f]

Premises used: Subtype.ext_iff, IsSl2Triple.lie_e_f
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
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.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
i : ↥b.support
t : IsSl2Triple (h i) (e i) (f i) := ⋯
⊢ Bracket.bracket (L := ↥(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)
        (h i) ⋯)
      (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)
        (e i) ⋯) =
    HSMul.hSMul (α := ℕ) (β := ↥(lieAlgebra b)) 2
      (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)
        (e i) ⋯)

Tactic:
simp [Subtype.ext_iff, t.lie_h_e_nsmul]

Premises used: Subtype.ext_iff, IsSl2Triple.lie_h_e_nsmul