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 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k : ↥b.support
l : ι
⊢ (ω b * e i) (Sum.inl k) (Sum.inr l) = (f i * ω b) (Sum.inl k) (Sum.inr l)
have a : HAdd.hAdd (α := R)
    (∑ x : ↥b.support,
      if x = i ∧ l = -(↑i : ι) then
        HMul.hMul (α := R)
          (Matrix.fromBlocks (m := ι) (o := ι) 1 0 0
            ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦ if i = -j then 1 else 0) (Sum.inl k)
            (Sum.inl x))
          1
      else 0)
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
        0 k x *
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
            1
      else 0) =
  ∑ x : ↥b.support,
      HMul.hMul (α := R)
        (Matrix.fromBlocks (m := ι) (o := ι) 0
          ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R) fun (i' : ↥b.support) (j : ι) ↦
            if i' = i ∧ j = (↑i : ι) then 1 else 0)
          ((Matrix.of : (a : ι → ↥b.support → R) → Matrix ι (↥b.support) R) fun (i' : ι) (j : ↥b.support) ↦
            if i' = -(↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
          ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i' j : ι) ↦
            if
                (P.root : (a : ι) → M) i' =
                  HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) (↑i : ι) : M) then
              HAdd.hAdd (α := R)
                (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j) : R) 1
            else 0)
          (Sum.inl k) (Sum.inl x))
        (0 x l) +
    if Membership.mem (γ := Finset ι) Finset.univ (-l) then
      HMul.hMul (α := R) (if k = i ∧ -l = (↑i : ι) then 1 else 0) 1
    else 0
Tactic: simp only [ω, e, f, mul_ite, mul_zero, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply,
      Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Finset.sum_ite_eq']
-- 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 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
k l : ι
⊢ (ω b * e i) (Sum.inr k) (Sum.inr l) = (f i * ω b) (Sum.inr k) (Sum.inr l)
have a : HAdd.hAdd (α := R)
    (∑ x : ↥b.support,
      HMul.hMul (α := R) (0 k x)
        (Matrix.fromBlocks (l := ↥b.support) (o := ι) 0
          ((Matrix.of : (a : ↥b.support → ι → R) → Matrix (↥b.support) ι R) fun (i' : ↥b.support) (j : ι) ↦
            if i' = i ∧ j = -(↑i : ι) then 1 else 0)
          ((Matrix.of : (a : ι → ↥b.support → R) → Matrix ι (↥b.support) R) fun (i' : ι) (j : ↥b.support) ↦
            if i' = (↑i : ι) then (↑|b.cartanMatrix i j| : R) else 0)
          ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i' j : ι) ↦
            if
                (P.root : (a : ι) → M) i' =
                  HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) j : M) then
              HAdd.hAdd (α := R)
                (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) j) : R) 1
            else 0)
          (Sum.inl x) (Sum.inr l)))
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
        (if -k = x then 1 else 0) *
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
            1
      else HMul.hMul (α := R) (if -k = x then 1 else 0) 0) =
  HAdd.hAdd (α := R)
    (∑ x : ↥b.support,
      HMul.hMul (α := R) (if -k = (↑i : ι) then (↑|b.cartanMatrix i x| : R) else 0)
        (Matrix.fromBlocks (l := ↥b.support) (o := ι) 1 0 0
          ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦ if i = -j then 1 else 0) (Sum.inl x)
          (Sum.inr l)))
    (∑ x : ι,
      if x = -l then
        (if
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M) then
            HAdd.hAdd (α := R)
              (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R) 1
          else 0) *
          1
      else
        (if
              (P.root : (a : ι) → M) k =
                HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) x : M) ((P.root : (a : ι) → M) (↑i : ι) : M) then
            HAdd.hAdd (α := R)
              (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R) 1
          else 0) *
          0)
Tactic: simp only [ω, e, f, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Matrix.of_apply, mul_ite, ← neg_eq_iff_eq_neg (a := 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 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
⊢ ω b * e i = f i * ω b
have a : ∀ (k l : ↥b.support), (ω b * e i) (Sum.inl k) (Sum.inl l) = (f i * ω b) (Sum.inl k) (Sum.inl l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [ω, e, f]
  · simp only [ω, e, f, mul_ite, mul_zero, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply,
      Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Finset.sum_ite_eq']
    rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by simp_all)]
    simp [← ite_and, and_comm, -indexNeg_neg, neg_eq_iff_eq_neg]
  · simp [ω, e, f]
  · simp only [ω, e, f, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Matrix.of_apply, mul_ite, ← neg_eq_iff_eq_neg (a := k)]
    rw [Finset.sum_eq_single_of_mem (-k) (Finset.mem_univ _) (by aesop)]
    simp [neg_eq_iff_eq_neg, sub_eq_add_neg]
-- 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 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
a : ∀ (k l : ↥b.support), (ω b * e i) (Sum.inl k) (Sum.inl l) = (f i * ω b) (Sum.inl k) (Sum.inl l)
⊢ ω b * e i = f i * ω b
have a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * e i) (Sum.inl k) (Sum.inr l) = (f i * ω b) (Sum.inl k) (Sum.inr l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [ω, e, f]
  · simp only [ω, e, f, mul_ite, mul_zero, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply,
      Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Finset.sum_ite_eq']
    rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by simp_all)]
    simp [← ite_and, and_comm, -indexNeg_neg, neg_eq_iff_eq_neg]
  · simp [ω, e, f]
  · simp only [ω, e, f, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Matrix.of_apply, mul_ite, ← neg_eq_iff_eq_neg (a := k)]
    rw [Finset.sum_eq_single_of_mem (-k) (Finset.mem_univ _) (by aesop)]
    simp [neg_eq_iff_eq_neg, sub_eq_add_neg]
-- 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 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
a : ∀ (k l : ↥b.support), (ω b * e i) (Sum.inl k) (Sum.inl l) = (f i * ω b) (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * e i) (Sum.inl k) (Sum.inr l) = (f i * ω b) (Sum.inl k) (Sum.inr l)
⊢ ω b * e i = f i * ω b
have a₂ : ∀ (k : ι) (l : ↥b.support), (ω b * e i) (Sum.inr k) (Sum.inl l) = (f i * ω b) (Sum.inr k) (Sum.inl l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [ω, e, f]
  · simp only [ω, e, f, mul_ite, mul_zero, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply,
      Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Finset.sum_ite_eq']
    rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by simp_all)]
    simp [← ite_and, and_comm, -indexNeg_neg, neg_eq_iff_eq_neg]
  · simp [ω, e, f]
  · simp only [ω, e, f, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Matrix.of_apply, mul_ite, ← neg_eq_iff_eq_neg (a := k)]
    rw [Finset.sum_eq_single_of_mem (-k) (Finset.mem_univ _) (by aesop)]
    simp [neg_eq_iff_eq_neg, sub_eq_add_neg]
-- 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 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
a : ∀ (k l : ↥b.support), (ω b * e i) (Sum.inl k) (Sum.inl l) = (f i * ω b) (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * e i) (Sum.inl k) (Sum.inr l) = (f i * ω b) (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), (ω b * e i) (Sum.inr k) (Sum.inl l) = (f i * ω b) (Sum.inr k) (Sum.inl l)
⊢ ω b * e i = f i * ω b
have a₃ : ∀ (k l : ι), (ω b * e i) (Sum.inr k) (Sum.inr l) = (f i * ω b) (Sum.inr k) (Sum.inr l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [ω, e, f]
  · simp only [ω, e, f, mul_ite, mul_zero, Fintype.sum_sum_type, Matrix.mul_apply, Matrix.of_apply,
      Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Finset.sum_ite_eq']
    rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _) (by simp_all)]
    simp [← ite_and, and_comm, -indexNeg_neg, neg_eq_iff_eq_neg]
  · simp [ω, e, f]
  · simp only [ω, e, f, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁,
      Matrix.fromBlocks_apply₂₂, Matrix.of_apply, mul_ite, ← neg_eq_iff_eq_neg (a := k)]
    rw [Finset.sum_eq_single_of_mem (-k) (Finset.mem_univ _) (by aesop)]
    simp [neg_eq_iff_eq_neg, sub_eq_add_neg]
-- 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 : Fintype ι
i : ↥b.support
⊢ ω b * f i = e i * ω b
have this : Eq (α := 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) ↦ x * ω b)
    ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (ω b * e i)))
  ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ x * ω b)
    ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (f i * ω b)))
Tactic: have := congr_arg (· * ω b) (congr_arg (ω b * ·) (ω_mul_e i))
-- 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 : Fintype ι
i : ↥b.support
this :
  Eq (α := 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) ↦ x * ω b)
      ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (ω b * e i)))
    ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ x * ω b)
      ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (f i * ω b)))
⊢ ω b * f i = e i * ω b
have this₁ : 1 * e i * ω b = ω b * f i * ω b * ω b
Tactic: simp only [← mul_assoc, ω_mul_ω] at this
Cleared hypotheses: 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 : Fintype ι
i : ↥b.support
⊢ ω b * f i = e i * ω b
have have : ∀
  (this :
    Eq (α := 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) ↦ x * ω b)
        ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (ω b * e i)))
      ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ x * ω b)
        ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (f i * ω b)))),
  ω b * f i = e i * ω b
Tactic: classical
  have := congr_arg (· * ω b) (congr_arg (ω b * ·) (ω_mul_e i))
  simp only [← mul_assoc, ω_mul_ω] at this
  simpa [mul_assoc, ω_mul_ω] using this.symm
-- 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 : Fintype ι
i : ↥b.support
have have₁ have₂ :
  ∀
    (this :
      Eq (α := 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) ↦ x * ω b)
          ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (ω b * e i)))
        ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ x * ω b)
          ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (f i * ω b)))),
    ω b * f i = e i * ω b
⊢ ω b * f i = e i * ω b
have have₃ : ∀ (this : 1 * e i * ω b = ω b * f i * ω b * ω b), ω b * f i = e i * ω b
Tactic: classical
  have := congr_arg (· * ω b) (congr_arg (ω b * ·) (ω_mul_e i))
  simp only [← mul_assoc, ω_mul_ω] at this
  simpa [mul_assoc, ω_mul_ω] using this.symm
-- 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 : Fintype ι
i j : ↥b.support
⊢ ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b
have rw : (e i * f j - f j * e i) * ω b = e i * f j * ω b - f j * e i * ω b
Tactic: rw [Ring.lie_def, sub_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 : Fintype ι
i j : ↥b.support
rw : (e i * f j - f j * e i) * ω b = e i * f j * ω b - f j * e i * ω b
⊢ ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b
have rw₁ : e i * f j * ω b - f j * e i * ω b = e i * f j * ω b - f j * e i * ω b
Tactic: rw [Ring.lie_def, sub_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 : Fintype ι
i j : ↥b.support
⊢ e i * f j * ω b - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
have rw : e i * (f j * ω b) - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
Tactic: rw [mul_assoc, mul_assoc]
-- 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 : Fintype ι
i j : ↥b.support
rw : e i * (f j * ω b) - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
⊢ e i * f j * ω b - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
have rw₁ : e i * (f j * ω b) - f j * (e i * ω b) = e i * (f j * ω b) - f j * (e i * ω b)
Tactic: rw [mul_assoc, mul_assoc]
-- 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 : Fintype ι
i j : ↥b.support
⊢ e i * (f j * ω b) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
have rw : e i * (ω b * e j) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
Tactic: rw [← ω_mul_e, ← ω_mul_f]
-- 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 : Fintype ι
i j : ↥b.support
rw : e i * (ω b * e j) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
⊢ e i * (f j * ω b) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
have rw₁ : e i * (ω b * e j) - f j * (ω b * f i) = e i * (ω b * e j) - f j * (ω b * f i)
Tactic: rw [← ω_mul_e, ← ω_mul_f]
-- 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 : Fintype ι
i j : ↥b.support
⊢ e i * (ω b * e j) - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i
have rw : e i * ω b * e j - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i
Tactic: rw [← mul_assoc, ← mul_assoc]
-- 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 : Fintype ι
i j : ↥b.support
rw : e i * ω b * e j - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i
⊢ e i * (ω b * e j) - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i
have rw₁ : e i * ω b * e j - f j * ω b * f i = e i * ω b * e j - f j * ω b * f i
Tactic: rw [← mul_assoc, ← mul_assoc]
-- 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 : Fintype ι
i j : ↥b.support
⊢ e i * ω b * e j - f j * ω b * f i = ω b * f i * e j - ω b * e j * f i
have rw : e i * ω b * e j - ω b * e j * f i = ω b * f i * e j - ω b * e j * f i
Tactic: rw [← ω_mul_e, ← ω_mul_f]
-- 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 : Fintype ι
i j : ↥b.support
rw : e i * ω b * e j - ω b * e j * f i = ω b * f i * e j - ω b * e j * f i
⊢ e i * ω b * e j - f j * ω b * f i = ω b * f i * e j - ω b * e j * f i
have rw₁ : ω b * f i * e j - ω b * e j * f i = ω b * f i * e j - ω b * e j * f i
Tactic: rw [← ω_mul_e, ← ω_mul_f]
-- 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 : Fintype ι
i j : ↥b.support
⊢ ω b * f i * e j - ω b * e j * f i = ω b * (f i * e j) - ω b * (e j * f i)
have rw : ω b * (f i * e j) - ω b * e j * f i = ω b * (f i * e j) - ω b * (e j * f i)
Tactic: rw [mul_assoc, mul_assoc]
-- 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 : Fintype ι
i j : ↥b.support
rw : ω b * (f i * e j) - ω b * e j * f i = ω b * (f i * e j) - ω b * (e j * f i)
⊢ ω b * f i * e j - ω b * e j * f i = ω b * (f i * e j) - ω b * (e j * f i)
have rw₁ : ω b * (f i * e j) - ω b * (e j * f i) = ω b * (f i * e j) - ω b * (e j * f i)
Tactic: rw [mul_assoc, mul_assoc]
-- 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 : Fintype ι
i j : ↥b.support
⊢ ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆
have calc : ω b * (f i * e j) - ω b * (e j * f i) = -ω b * ⁅e j, f i⁆
Tactic: calc ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_