awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
j : ι
k l : ↥b.support
h :
  (P.root : (a : ι) → M) (↑k : ι) =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (↑k : ι) : M)
⊢ False

Tactic:
exact P.ne_zero j <| by simpa using h

Premises used: RootPairing.ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
i j : ι
k : ↥b.support
h :
  (P.root : (a : ι) → M) i =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (↑k : ι) : M)
l : ↥b.support
⊢ i ≠ (↑k : ι)

Tactic:
replace h : i ≠ k := by rintro rfl; exact P.ne_zero j <| by simpa using h
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
i j : ι
k l : ↥b.support
h : i ≠ (↑k : ι)
⊢ ⁅f k, v b i⁆ (Sum.inl l) =
    (HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑k : ι) i) : R) 1 •
        v b j)
      (Sum.inl l)

Tactic:
simp [f, h]

Premises used: RootPairing.GeckConstruction.f
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
i j : ι
k : ↥b.support
h :
  (P.root : (a : ι) → M) i =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (↑k : ι) : M)
l : ι
⊢ ⁅f k, v b i⁆ (Sum.inr l) =
    (HAdd.hAdd (α := R) (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑k : ι) i) : R) 1 •
        v b j)
      (Sum.inr l)

Tactic:
simp [f, h, Pi.single_apply]

Premises used: RootPairing.GeckConstruction.f, Pi.single_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ ω b * (x + y) * ω b = ω b * x * ω b + ω b * y * ω b

Tactic:
noncomm_ring
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
t : R
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ ω b * t • x * ω b = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) t : R) (ω b * x * ω b)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
simp : ω b * (x * y - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
⊢ ω b * ⁅x, y⁆ * ω b = ⁅ω b * x * ω b, ω b * y * ω b⁆

Tactic:
simp only [Ring.lie_def]

Premises used: Ring.lie_def
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
nth_rw : ω b * (x * 1 * y - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
⊢ ω b * (x * y - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)

Tactic:
nth_rw 1 [← mul_one x]

Premises used: mul_one
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
nth_rw : ω b * (x * 1 * y - y * (1 * x)) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
⊢ ω b * (x * 1 * y - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)

Tactic:
nth_rw 2 [← one_mul x]

Premises used: one_mul
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
simp :
  ω b * (x * (ω b * ω b) * y - y * (ω b * ω b * x)) * ω b =
    ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
⊢ ω b * (x * 1 * y - y * (1 * x)) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)

Tactic:
simp only [← ω_mul_ω (b := b)]

Premises used: RootPairing.GeckConstruction.ω_mul_ω
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ ω b * (x * (ω b * ω b) * y - y * (ω b * ω b * x)) * ω b =
    ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)

Tactic:
noncomm_ring
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
simp : x * ω b * ω b = x
⊢ (fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x * ω b)
      ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x * ω b) x) =
    x

Tactic:
simp only [← mul_assoc, ω_mul_ω, one_mul]

Premises used: mul_assoc, RootPairing.GeckConstruction.ω_mul_ω, one_mul
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ x * ω b * ω b = x

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x u : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f) u
⊢ (∃ (j : ↥b.support), h j = u) ∨ (∃ (j : ↥b.support), e j = u) ∨ ∃ (j : ↥b.support), f j = u

Tactic:
simpa only [mem_union, mem_range, or_assoc] using hu

Premises used: Set.mem_union, Set.mem_range, or_assoc
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x u : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f) u
mem :
  ∀ (i : ↥b.support)
    (hu :
      Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
        (range h ∪ range e ∪ range f) (h i)),
    Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
      LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
      ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (h i) :
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
mem₁ :
  ∀ (i : ↥b.support)
    (hu :
      Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
        (range h ∪ range e ∪ range f) (e i)),
    Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
      LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
      ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (e i) :
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
mem₂ :
  ∀ (i : ↥b.support)
    (hu :
      Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
        (range h ∪ range e ∪ range f) (f i)),
    Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
      LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
      ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (f i) :
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) u :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Tactic:
obtain (⟨i, rfl⟩ | ⟨i, rfl⟩ | ⟨i, rfl⟩) : (∃ j, h j = u) ∨ (∃ j, e j = u) ∨ (∃ j, f j = u) := by
      simpa only [mem_union, mem_range, or_assoc] using hu

Premises used: RootPairing.GeckConstruction.f, RootPairing.GeckConstruction.h, Exists, Eq, RootPairing.GeckConstruction.e, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (h i)
mem :
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    (-(ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (h i) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (h i) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Tactic:
rw [← neg_mem_iff]

Premises used: neg_mem_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (h i)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (-(ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (h i) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Tactic:
simp [ω_mul_h, mul_assoc]

Premises used: mul_assoc, RootPairing.GeckConstruction.ω_mul_h
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (h i)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    (-(ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (h i) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Tactic:
exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_h, mul_assoc]

Premises used: LieSubalgebra.subset_lieSpan
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (e i)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (e i) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Tactic:
simp [ω_mul_e, mul_assoc]

Premises used: mul_assoc, RootPairing.GeckConstruction.ω_mul_e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (e i)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (e i) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Tactic:
exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_e, mul_assoc]

Premises used: LieSubalgebra.subset_lieSpan
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (f i)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (f i) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Tactic:
simp [ω_mul_f, mul_assoc]

Premises used: mul_assoc, RootPairing.GeckConstruction.ω_mul_f
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (f i)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (f i) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Tactic:
exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_f, mul_assoc]

Premises used: LieSubalgebra.subset_lieSpan
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
⊢ Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) 0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
x u v : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f))
    u
hy :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f))
    v
hu :
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) u :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
hv :
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) v :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (u + v) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Tactic:
simpa [mul_add, add_mul] using add_mem hu hv

Premises used: add_mul, AddMemClass.add_mem, mul_add