awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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) ⋯
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ range e₀ ∪ range f₀))
have simp : Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
  (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ (range e₀ ∪ range f₀)))
Tactic: simp only [union_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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) ⋯
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ (range e₀ ∪ range f₀)))
have refine : LE.le (α := LieSubalgebra K ↥(lieAlgebra b))
  (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ (range e₀ ∪ range f₀)))
  (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
Tactic: refine le_antisymm (LieSubalgebra.lieSpan_mono <| by simp) ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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) ⋯
⊢ LE.le (α := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ (range e₀ ∪ range f₀)))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
have rw : range h₀ ∪ (range e₀ ∪ range f₀) ⊆
  (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
Tactic: rw [LieSubalgebra.lieSpan_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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) ⋯
⊢ range h₀ ∪ (range e₀ ∪ range f₀) ⊆
    (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
have refine : range h₀ ⊆ (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
Tactic: refine union_subset ?_ LieSubalgebra.subset_lieSpan
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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⁆
have a : (↑(h₀ i) : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) = (↑⁅e₀ i, f₀ i⁆ : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
Tactic: ext1
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (hypothesis)
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 ∈ (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
have hef : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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⁆
⊢ h₀ i ∈ (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
have rw : ⁅e₀ i, f₀ i⁆ ∈ (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
Tactic: rw [hef]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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, f₀ i⁆ ∈ (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
have hx : Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
  (e₀ i)
Tactic: apply LieSubalgebra.lie_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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)
⊢ ⁅e₀ i, f₀ i⁆ ∈ (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
have hy : Membership.mem (γ := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
  (f₀ i)
Tactic: apply LieSubalgebra.lie_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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 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) ⋯
have 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) sorry)
Tactic: apply LinearIndependent.of_comp (lieAlgebra b).subtype
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
hkj : k ≠ j
hk' :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M))
have inl : ∀ (hm : 0 < P.pairingIn ℤ j k),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M))
Tactic: rcases lt_or_ge 0 (P.pairingIn ℤ j k) with hm | hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
hkj : k ≠ j
hk' :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
inl :
  ∀ (hm : 0 < P.pairingIn ℤ j k),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M))
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M))
have inr : ∀ (hm : P.pairingIn ℤ j k ≤ 0),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M))
Tactic: rcases lt_or_ge 0 (P.pairingIn ℤ j k) with hm | hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
hkj : k ≠ j
hk' :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
hm : 0 < P.pairingIn ℤ j k
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M))
have inl : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
  (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) k : M))
Tactic: rw [← neg_mem_range_root_iff, neg_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
i j k : ι
hij : i ≠ j
hi : i ∈ b.support
hj : j ∈ b.support
hk :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
      ((P.root : (a : ι) → M) j : M))
hkj : k ≠ j
hk' :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
hm : P.pairingIn ℤ j k ≤ 0
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M))
have inr : ∀ (l : ι)
  (hl :
    (P.root : (a : ι) → M) l =
      HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) i : M))
        ((P.root : (a : ι) → M) j : M)),
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) j : M))
Tactic: obtain ⟨l, hl⟩ := hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
P : RootPairing ι R M N
inst_7 : Finite ι
inst_8 : P.IsCrystallographic
b : P.Base
j k : ι
hj : j ∈ b.support
hkj : k ≠ j
hm : P.pairingIn ℤ j k ≤ 0
l : ι
hij : l ≠ j
hi : l ∈ b.support
hk' :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) l : M))
hl :
  (P.root : (a : ι) → M) l =
    HSub.hSub (β := M) (HAdd.hAdd («α» := M) (β := M) ((P.root : (a : ι) → M) k : M) ((P.root : (a : ι) → M) l : M))
      ((P.root : (a : ι) → M) j : M)
⊢ False
have hl₁ : k = j
Tactic: rw [add_comm, add_sub_assoc, left_eq_add, sub_eq_zero, P.root.injective.eq_iff] at hl
Cleared hypotheses: hl