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 ι
x_1 x_2 : ↥(cartanSubalgebra' b)
x : 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)) (lieAlgebra b) x
hx' :
  Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
    (Subtype.mk (p := fun (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)
        x)
      x hx)
y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hy : Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) y
hy' :
  Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
    (Subtype.mk (p := fun (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)
        x)
      y hy)
x' : ↥(cartanSubalgebra b) :=
  Subtype.mk (p := fun (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))
      (cartanSubalgebra b) x)
    x hx'
y' : ↥(cartanSubalgebra b) :=
  Subtype.mk (p := fun (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))
      (cartanSubalgebra b) x)
    y hy'
suffices : ⁅x', y'⁆ = 0
⊢ ⁅Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
        Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b) x)
        (Subtype.mk (p := fun (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) x)
          x hx)
        hx',
      Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
        Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b) x)
        (Subtype.mk (p := fun (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) x)
          y hy)
        hy'⁆ =
    0

Tactic:
suffices ⁅x', y'⁆ = 0 by simpa [x', y', Subtype.ext_iff] using this
-- 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_1 x_2 : ↥(cartanSubalgebra' b)
x : 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)) (lieAlgebra b) x
hx' :
  Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
    (Subtype.mk (p := fun (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)
        x)
      x hx)
y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hy : Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) y
hy' :
  Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
    (Subtype.mk (p := fun (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)
        x)
      y hy)
x' : ↥(cartanSubalgebra b) :=
  Subtype.mk (p := fun (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))
      (cartanSubalgebra b) x)
    x hx'
y' : ↥(cartanSubalgebra b) :=
  Subtype.mk (p := fun (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))
      (cartanSubalgebra b) x)
    y hy'
⊢ ⁅x', y'⁆ = 0

Tactic:
simp [trivial_lie_zero]

Premises used: trivial_lie_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 ι
⊢ LieModule.IsTriangularizable R (↥(cartanSubalgebra' b)) (↥b.support ⊕ ι → R)

Tactic:
⟨fun ⟨⟨x, hx'⟩, hx⟩ ↦ ?_⟩

Premises used: LieModule.IsTriangularizable.mk, iSup, Membership.mem, Subtype, Module.End.maxGenEigenspace, _private.0.RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'.match_1, LieModule.toEnd, RootPairing.GeckConstruction.cartanSubalgebra', Top.top, Eq, DFunLike.coe
-- 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 ι
refine :
  ∀ (x : ↥(cartanSubalgebra' b)) (x : 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)) (lieAlgebra b)
        x)
    (hx :
      Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
        (Subtype.mk (p := fun (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) x)
          x hx')),
    Eq (α := Submodule R (↥b.support ⊕ ι → R))
      (⨆ (φ : R),
        Module.End.maxGenEigenspace (M := ↥b.support ⊕ ι → R)
          (((LieModule.toEnd R (↥(cartanSubalgebra' b)) (↥b.support ⊕ ι → R) :
                ↥(cartanSubalgebra' b) →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
              (a : ↥(cartanSubalgebra' b)) → Module.End R (↥b.support ⊕ ι → R))
            (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
              Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b) x)
              (Subtype.mk (p := fun (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) x)
                x hx')
              hx))
          φ)
      ⊤
⊢ LieModule.IsTriangularizable R (↥(cartanSubalgebra' b)) (↥b.support ⊕ ι → R)

Tactic:
refine ⟨fun ⟨⟨x, hx'⟩, hx⟩ ↦ ?_⟩
-- 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_1 : ↥(cartanSubalgebra' b)
x : 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)) (lieAlgebra b) x
hx :
  Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
    (Subtype.mk (p := fun (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)
        x)
      x hx')
⊢ Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) x

Tactic:
simpa using hx
-- 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 : ↥(cartanSubalgebra' b)
d : ↥b.support ⊕ ι → R
hx' :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    (Matrix.diagonal d)
hx :
  Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
    (Subtype.mk (p := fun (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)
        x)
      (Matrix.diagonal d) hx')
⊢ Eq (α := Submodule R (↥b.support ⊕ ι → R))
    (⨆ (φ : R),
      Module.End.maxGenEigenspace (M := ↥b.support ⊕ ι → R)
        (((LieModule.toEnd R (↥(cartanSubalgebra' b)) (↥b.support ⊕ ι → R) :
              ↥(cartanSubalgebra' b) →ₗ⁅R⁆ Module.End R (↥b.support ⊕ ι → R)) :
            (a : ↥(cartanSubalgebra' b)) → Module.End R (↥b.support ⊕ ι → R))
          (Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
            Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b) x)
            (Subtype.mk (p := fun (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) x)
              (Matrix.diagonal d) hx')
            hx))
        φ)
    ⊤

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 ι
rw :
  range h ⊆
    (↑(LieSubalgebra.toSubmodule
            (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
              (range h ∪ range e ∪ range f)) :
          Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
⊢ LE.le (α := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (cartanSubalgebra b)
    (lieAlgebra b)

Tactic:
rw [cartanSubalgebra, lieAlgebra, ← LieSubalgebra.toSubmodule_le_toSubmodule, Submodule.span_le]

Premises used: LieSubalgebra.toSubmodule_le_toSubmodule, RootPairing.GeckConstruction.lieAlgebra, RootPairing.GeckConstruction.cartanSubalgebra, Submodule.span_le
-- 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 : ↥b.support
⊢ h i ∈
    (↑(LieSubalgebra.toSubmodule
            (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
              (range h ∪ range e ∪ range f)) :
          Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))

Tactic:
LieSubalgebra.subset_lieSpan <| Or.inl <| Or.inl <| mem_range_self i

Premises used: Set.mem_range_self, Set.Mem, LieSubalgebra.subset_lieSpan, Or.inl
-- 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 : ↥b.support
⊢ h i ∈
    (↑(LieSubalgebra.toSubmodule
            (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
              (range h ∪ range e ∪ range f)) :
          Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))

Tactic:
exact LieSubalgebra.subset_lieSpan <| Or.inl <| Or.inl <| mem_range_self i

Premises used: Set.mem_range_self, LieSubalgebra.subset_lieSpan, Or.inl
-- 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 : ↥b.support
h : ∀ (k : ↥b.support), ⁅e i, u j⁆ (Sum.inl k) = (|b.cartanMatrix i j| • v b (↑i : ι)) (Sum.inl k)
h₁ : ∀ (k : ι), ⁅e i, u j⁆ (Sum.inr k) = (|b.cartanMatrix i j| • v b (↑i : ι)) (Sum.inr k)
⊢ ⁅e i, u j⁆ = |b.cartanMatrix i j| • v b (↑i : ι)

Tactic:
ext (k | k)
-- 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
⊢ ⁅e i, u j⁆ (Sum.inl k) = (|b.cartanMatrix i j| • v b (↑i : ι)) (Sum.inl k)

Tactic:
simp [e, Pi.single_apply]

Premises used: Pi.single_apply, RootPairing.GeckConstruction.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 ι
i j : ↥b.support
k : ι
⊢ ⁅e i, u j⁆ (Sum.inr k) = (|b.cartanMatrix i j| • v b (↑i : ι)) (Sum.inr k)

Tactic:
simp [e, Pi.single_apply]

Premises used: Pi.single_apply, RootPairing.GeckConstruction.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 ι
i j : ι
k : ↥b.support
h :
  (P.root : (a : ι) → M) j =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑k : ι) : M) ((P.root : (a : ι) → M) i : M)
this : InvolutiveNeg ι := P.indexNeg
h₁ :
  ∀ (l : ↥b.support),
    ⁅e k, v b i⁆ (Sum.inl l) =
      (HAdd.hAdd (α := R) (↑(chainBotCoeff.{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)
h₂ :
  ∀ (l : ι),
    ⁅e k, v b i⁆ (Sum.inr l) =
      (HAdd.hAdd (α := R) (↑(chainBotCoeff.{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)
⊢ ⁅e k, v b i⁆ =
    HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑k : ι) i) : R) 1 •
      v b j

Tactic:
ext (l | l)
-- 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 : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
l : ↥b.support
h :
  (P.root : (a : ι) → M) j =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑k : ι) : M) ((P.root : (a : ι) → M) (-(↑k : ι)) : M)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M)

Tactic:
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 ι
j : ι
k : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
l : ↥b.support
h :
  (P.root : (a : ι) → M) j =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑k : ι) : 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) j =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑k : ι) : M) ((P.root : (a : ι) → M) i : M)
this : InvolutiveNeg ι := P.indexNeg
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 : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
l : ↥b.support
h : i ≠ -(↑k : ι)
⊢ ⁅e k, v b i⁆ (Sum.inl l) =
    (HAdd.hAdd (α := R) (↑(chainBotCoeff.{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 [e, h, -indexNeg_neg]

Premises used: RootPairing.indexNeg_neg, RootPairing.GeckConstruction.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 ι
i j : ι
k : ↥b.support
h :
  (P.root : (a : ι) → M) j =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑k : ι) : M) ((P.root : (a : ι) → M) i : M)
this : InvolutiveNeg ι := P.indexNeg
l : ι
⊢ ⁅e k, v b i⁆ (Sum.inr l) =
    (HAdd.hAdd (α := R) (↑(chainBotCoeff.{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 [e, ← h, Pi.single_apply]

Premises used: Pi.single_apply, RootPairing.GeckConstruction.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 ι
i : ↥b.support
h : ∀ (j : ↥b.support), ⁅f i, v b (↑i : ι)⁆ (Sum.inl j) = u i (Sum.inl j)
h₁ : ∀ (j : ι), ⁅f i, v b (↑i : ι)⁆ (Sum.inr j) = u i (Sum.inr j)
⊢ ⁅f i, v b (↑i : ι)⁆ = u i

Tactic:
ext (j | j)
-- 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 : ↥b.support
⊢ ⁅f i, v b (↑i : ι)⁆ (Sum.inl j) = u i (Sum.inl j)

Tactic:
simp [f, 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 ι
i : ↥b.support
j : ι
⊢ ⁅f i, v b (↑i : ι)⁆ (Sum.inr j) = u i (Sum.inr j)

Tactic:
simp [f, P.ne_zero j]

Premises used: RootPairing.GeckConstruction.f, 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)
h₁ :
  ∀ (l : ↥b.support),
    ⁅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)
h₂ :
  ∀ (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)
⊢ ⁅f k, v b i⁆ =
    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

Tactic:
ext (l | l)
-- 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)
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (0 : M)

Tactic:
simpa using h