awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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'
⊢ ⁅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
have suffices : ⁅x', y'⁆ = 0
Tactic: suffices ⁅x', y'⁆ = 0 by simpa [x', y', Subtype.ext_iff] using this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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)
have 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))
        φ)
    ⊤
Tactic: refine ⟨fun ⟨⟨x, hx'⟩, hx⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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 ι
⊢ LE.le (α := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (cartanSubalgebra b)
    (lieAlgebra b)
have 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))
Tactic: rw [cartanSubalgebra, lieAlgebra, ← LieSubalgebra.toSubmodule_le_toSubmodule, Submodule.span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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
⊢ ⁅e i, u j⁆ = |b.cartanMatrix i j| • v b (↑i : ι)
have h : ∀ (k : ↥b.support), ⁅e i, u j⁆ (Sum.inl k) = (|b.cartanMatrix i j| • v b (↑i : ι)) (Sum.inl k)
Tactic: ext (k | k)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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)
⊢ ⁅e i, u j⁆ = |b.cartanMatrix i j| • v b (↑i : ι)
have h₁ : ∀ (k : ι), ⁅e i, u j⁆ (Sum.inr k) = (|b.cartanMatrix i j| • v b (↑i : ι)) (Sum.inr k)
Tactic: ext (k | k)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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
⊢ ⁅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
have 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)
Tactic: ext (l | l)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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)
⊢ ⁅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
have 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)
Tactic: ext (l | l)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (hypothesis)
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
⊢ ⁅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)
have h₁ : i ≠ -(↑k : ι)
Tactic: replace h : i ≠ -k := by rintro rfl; exact P.ne_zero j <| by simpa using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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
⊢ ⁅f i, v b (↑i : ι)⁆ = u i
have h : ∀ (j : ↥b.support), ⁅f i, v b (↑i : ι)⁆ (Sum.inl j) = u i (Sum.inl j)
Tactic: ext (j | j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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)
⊢ ⁅f i, v b (↑i : ι)⁆ = u i
have h₁ : ∀ (j : ι), ⁅f i, v b (↑i : ι)⁆ (Sum.inr j) = u i (Sum.inr j)
Tactic: ext (j | j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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)
⊢ ⁅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
have 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)
Tactic: ext (l | l)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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)
⊢ ⁅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
have 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)
Tactic: ext (l | l)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (hypothesis)
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
⊢ ⁅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)
have h₁ : i ≠ (↑k : ι)
Tactic: replace h : i ≠ k := by rintro rfl; exact P.ne_zero j <| by simpa using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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⁆
have simp : ω b * (x * y - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
Tactic: simp only [Ring.lie_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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 - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
have nth_rw : ω b * (x * 1 * y - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
Tactic: nth_rw 1 [← mul_one x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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 * 1 * y - y * x) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
have nth_rw : ω b * (x * 1 * y - y * (1 * x)) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
Tactic: nth_rw 2 [← one_mul x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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 * 1 * y - y * (1 * x)) * ω b = ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
have simp : ω b * (x * (ω b * ω b) * y - y * (ω b * ω b * x)) * ω b =
  ω b * x * ω b * (ω b * y * ω b) - ω b * y * ω b * (ω b * x * ω b)
Tactic: simp only [← ω_mul_ω (b := b)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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
⊢ (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
have simp : x * ω b * ω b = x
Tactic: simp only [← mul_assoc, ω_mul_ω, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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
⊢ 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)
have 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)
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
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
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)
⊢ 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)
have 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)
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
Cleared hypotheses: u, hu