awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
k l : ι
⊢ ⁅h j, e i⁆ (Sum.inr k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inr l)
have a : HSub.hSub (α := R)
    (∑ x : ι,
      if
          (P.root : (a : ι) → M) x =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
        Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) 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 : ι,
      if
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
            1 *
          Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) x l
      else 0) =
  if
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
    HMul.hMul (α := R) (↑(b.cartanMatrix i j) : R)
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
      (↑(b.cartanMatrix i j) : R)
  else 0
Tactic: simp only [h, e, indexNeg_neg, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply,
      Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁, Matrix.zero_apply, Matrix.fromBlocks_apply₁₂,
      Matrix.of_apply, mul_ite, mul_one, mul_zero, ite_self, Finset.sum_const_zero,
      Matrix.fromBlocks_apply₂₂, zero_add, ite_mul, zero_mul, Matrix.smul_apply, smul_ite, smul_add,
      zsmul_eq_mul, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
k l : ι
⊢ HSub.hSub (α := R)
      (∑ x : ι,
        if
            (P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
          Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) 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 : ι,
        if
            (P.root : (a : ι) → M) k =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
              1 *
            Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) x l
        else 0) =
    if
        (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
      HMul.hMul (α := R) (↑(b.cartanMatrix i j) : R)
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
        (↑(b.cartanMatrix i j) : R)
    else 0
have a : ∑ x ∈ {k, l},
    ((if
          (P.root : (a : ι) → M) x =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
        Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) 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) -
      if
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
            1 *
          Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) x l
      else 0) =
  if
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
    HMul.hMul (α := R) (↑(b.cartanMatrix i j) : R)
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
      (↑(b.cartanMatrix i j) : R)
  else 0
Tactic: rw [← Finset.sum_sub_distrib, ← Finset.sum_subset (Finset.subset_univ {k, l}) (by aesop)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
k l : ι
⊢ ∑ x ∈ {k, l},
      ((if
            (P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
          Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) 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) -
        if
            (P.root : (a : ι) → M) k =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
              1 *
            Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) x l
        else 0) =
    if
        (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
      HMul.hMul (α := R) (↑(b.cartanMatrix i j) : R)
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
        (↑(b.cartanMatrix i j) : R)
    else 0
have a : ∑ x ∈ {k, k},
    ((if
          (P.root : (a : ι) → M) x =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M) then
        Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) k x *
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R)
            1
      else 0) -
      if
          (P.root : (a : ι) → M) k =
            HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
            1 *
          Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) x k
      else 0) =
  if
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) k : M) then
    HMul.hMul (α := R) (↑(b.cartanMatrix i j) : R)
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) k) : R) +
      (↑(b.cartanMatrix i j) : R)
  else 0
Tactic: rcases eq_or_ne k l with rfl | hkl
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
k l : ι
hkl : k ≠ l
⊢ ∑ x ∈ {k, l},
      ((if
            (P.root : (a : ι) → M) x =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
          Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) 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) -
        if
            (P.root : (a : ι) → M) k =
              HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) x : M) then
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) x) : R)
              1 *
            Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑j : ι)) : R)) x l
        else 0) =
    if
        (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
      HMul.hMul (α := R) (↑(b.cartanMatrix i j) : R)
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
        (↑(b.cartanMatrix i j) : R)
    else 0
have a : (if
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
    (↑(P.pairingIn ℤ k (↑j : ι)) : R) *
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
          1 -
      HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) 1 *
        (↑(P.pairingIn ℤ l (↑j : ι)) : R)
  else 0) =
  if
      (P.root : (a : ι) → M) k =
        HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
    HMul.hMul (α := R) (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
      (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
  else 0
Tactic: simp only [Matrix.diagonal_apply, ite_mul, zero_mul, mul_ite, mul_zero, Finset.sum_sub_distrib,
      Finset.mem_singleton, Finset.sum_singleton, Finset.sum_insert, hkl, not_false_eq_true,
      reduceIte, right_eq_add, ite_self, add_zero, zero_add, ite_sub_ite, sub_self,
      Base.cartanMatrix, Base.cartanMatrixIn_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
k l : ι
hkl : k ≠ l
⊢ (if
        (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
      (↑(P.pairingIn ℤ k (↑j : ι)) : R) *
          HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
            1 -
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
            1 *
          (↑(P.pairingIn ℤ l (↑j : ι)) : R)
    else 0) =
    if
        (P.root : (a : ι) → M) k =
          HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M) then
      HMul.hMul (α := R) (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
          (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
        (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
    else 0
have a : ∀
  (hkil :
    (P.root : (a : ι) → M) k =
      HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M)),
  (↑(P.pairingIn ℤ k (↑j : ι)) : R) *
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
          1 -
      HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) 1 *
        (↑(P.pairingIn ℤ l (↑j : ι)) : R) =
    HMul.hMul (α := R) (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
      (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
Tactic: refine ite_congr rfl (fun hkil ↦ ?_) (fun _ ↦ rfl)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
k l : ι
hkl : k ≠ l
hkil :
  (P.root : (a : ι) → M) k =
    HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) (↑i : ι) : M) ((P.root : (a : ι) → M) l : M)
⊢ (↑(P.pairingIn ℤ k (↑j : ι)) : R) *
        HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R)
          1 -
      HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) 1 *
        (↑(P.pairingIn ℤ l (↑j : ι)) : R) =
    HMul.hMul (α := R) (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
        (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
      (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
have a : HAdd.hAdd (α := R) (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R) (↑(P.pairingIn ℤ l (↑j : ι)) : R) *
      HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) 1 -
    HAdd.hAdd (α := R) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) 1 *
      (↑(P.pairingIn ℤ l (↑j : ι)) : R) =
  HMul.hMul (α := R) (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) (↑i : ι) l) : R) +
    (↑(P.pairingIn ℤ (↑i : ι) (↑j : ι)) : R)
Tactic: simp only [pairingIn_eq_add_of_root_eq_add hkil, Int.cast_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
⊢ ⁅h j, e i⁆ = b.cartanMatrix i j • e i
have a : ∀ (k l : ↥b.support), ⁅h j, e i⁆ (Sum.inl k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inl l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [h, e]
  · simp only [h, e, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
      Matrix.fromBlocks_apply₁₂, Matrix.zero_apply, zero_mul, add_zero, Finset.sum_const_zero]
    rw [Finset.sum_eq_ite l (by aesop)]
    aesop
  · simp only [h, e]
    aesop
  · simp only [h, e, indexNeg_neg, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply,
      Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁, Matrix.zero_apply, Matrix.fromBlocks_apply₁₂,
      Matrix.of_apply, mul_ite, mul_one, mul_zero, ite_self, Finset.sum_const_zero,
      Matrix.fromBlocks_apply₂₂, zero_add, ite_mul, zero_mul, Matrix.smul_apply, smul_ite, smul_add,
      zsmul_eq_mul, smul_zero]
    rw [← Finset.sum_sub_distrib, ← Finset.sum_subset (Finset.subset_univ {k, l}) (by aesop)]
    rcases eq_or_ne k l with rfl | hkl; · simp [P.ne_zero i]
    simp only [Matrix.diagonal_apply, ite_mul, zero_mul, mul_ite, mul_zero, Finset.sum_sub_distrib,
      Finset.mem_singleton, Finset.sum_singleton, Finset.sum_insert, hkl, not_false_eq_true,
      reduceIte, right_eq_add, ite_self, add_zero, zero_add, ite_sub_ite, sub_self,
      Base.cartanMatrix, Base.cartanMatrixIn_def]
    refine ite_congr rfl (fun hkil ↦ ?_) (fun _ ↦ rfl)
    simp only [pairingIn_eq_add_of_root_eq_add hkil, Int.cast_add]
    ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
a : ∀ (k l : ↥b.support), ⁅h j, e i⁆ (Sum.inl k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inl l)
⊢ ⁅h j, e i⁆ = b.cartanMatrix i j • e i
have a₁ : ∀ (k : ↥b.support) (l : ι), ⁅h j, e i⁆ (Sum.inl k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inr l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [h, e]
  · simp only [h, e, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
      Matrix.fromBlocks_apply₁₂, Matrix.zero_apply, zero_mul, add_zero, Finset.sum_const_zero]
    rw [Finset.sum_eq_ite l (by aesop)]
    aesop
  · simp only [h, e]
    aesop
  · simp only [h, e, indexNeg_neg, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply,
      Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁, Matrix.zero_apply, Matrix.fromBlocks_apply₁₂,
      Matrix.of_apply, mul_ite, mul_one, mul_zero, ite_self, Finset.sum_const_zero,
      Matrix.fromBlocks_apply₂₂, zero_add, ite_mul, zero_mul, Matrix.smul_apply, smul_ite, smul_add,
      zsmul_eq_mul, smul_zero]
    rw [← Finset.sum_sub_distrib, ← Finset.sum_subset (Finset.subset_univ {k, l}) (by aesop)]
    rcases eq_or_ne k l with rfl | hkl; · simp [P.ne_zero i]
    simp only [Matrix.diagonal_apply, ite_mul, zero_mul, mul_ite, mul_zero, Finset.sum_sub_distrib,
      Finset.mem_singleton, Finset.sum_singleton, Finset.sum_insert, hkl, not_false_eq_true,
      reduceIte, right_eq_add, ite_self, add_zero, zero_add, ite_sub_ite, sub_self,
      Base.cartanMatrix, Base.cartanMatrixIn_def]
    refine ite_congr rfl (fun hkil ↦ ?_) (fun _ ↦ rfl)
    simp only [pairingIn_eq_add_of_root_eq_add hkil, Int.cast_add]
    ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
a : ∀ (k l : ↥b.support), ⁅h j, e i⁆ (Sum.inl k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), ⁅h j, e i⁆ (Sum.inl k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inr l)
⊢ ⁅h j, e i⁆ = b.cartanMatrix i j • e i
have a₂ : ∀ (k : ι) (l : ↥b.support), ⁅h j, e i⁆ (Sum.inr k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inl l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [h, e]
  · simp only [h, e, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
      Matrix.fromBlocks_apply₁₂, Matrix.zero_apply, zero_mul, add_zero, Finset.sum_const_zero]
    rw [Finset.sum_eq_ite l (by aesop)]
    aesop
  · simp only [h, e]
    aesop
  · simp only [h, e, indexNeg_neg, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply,
      Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁, Matrix.zero_apply, Matrix.fromBlocks_apply₁₂,
      Matrix.of_apply, mul_ite, mul_one, mul_zero, ite_self, Finset.sum_const_zero,
      Matrix.fromBlocks_apply₂₂, zero_add, ite_mul, zero_mul, Matrix.smul_apply, smul_ite, smul_add,
      zsmul_eq_mul, smul_zero]
    rw [← Finset.sum_sub_distrib, ← Finset.sum_subset (Finset.subset_univ {k, l}) (by aesop)]
    rcases eq_or_ne k l with rfl | hkl; · simp [P.ne_zero i]
    simp only [Matrix.diagonal_apply, ite_mul, zero_mul, mul_ite, mul_zero, Finset.sum_sub_distrib,
      Finset.mem_singleton, Finset.sum_singleton, Finset.sum_insert, hkl, not_false_eq_true,
      reduceIte, right_eq_add, ite_self, add_zero, zero_add, ite_sub_ite, sub_self,
      Base.cartanMatrix, Base.cartanMatrixIn_def]
    refine ite_congr rfl (fun hkil ↦ ?_) (fun _ ↦ rfl)
    simp only [pairingIn_eq_add_of_root_eq_add hkil, Int.cast_add]
    ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
a : ∀ (k l : ↥b.support), ⁅h j, e i⁆ (Sum.inl k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), ⁅h j, e i⁆ (Sum.inl k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), ⁅h j, e i⁆ (Sum.inr k) (Sum.inl l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inl l)
⊢ ⁅h j, e i⁆ = b.cartanMatrix i j • e i
have a₃ : ∀ (k l : ι), ⁅h j, e i⁆ (Sum.inr k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inr l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [h, e]
  · simp only [h, e, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply, Fintype.sum_sum_type,
      Matrix.fromBlocks_apply₁₂, Matrix.zero_apply, zero_mul, add_zero, Finset.sum_const_zero]
    rw [Finset.sum_eq_ite l (by aesop)]
    aesop
  · simp only [h, e]
    aesop
  · simp only [h, e, indexNeg_neg, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply,
      Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁, Matrix.zero_apply, Matrix.fromBlocks_apply₁₂,
      Matrix.of_apply, mul_ite, mul_one, mul_zero, ite_self, Finset.sum_const_zero,
      Matrix.fromBlocks_apply₂₂, zero_add, ite_mul, zero_mul, Matrix.smul_apply, smul_ite, smul_add,
      zsmul_eq_mul, smul_zero]
    rw [← Finset.sum_sub_distrib, ← Finset.sum_subset (Finset.subset_univ {k, l}) (by aesop)]
    rcases eq_or_ne k l with rfl | hkl; · simp [P.ne_zero i]
    simp only [Matrix.diagonal_apply, ite_mul, zero_mul, mul_ite, mul_zero, Finset.sum_sub_distrib,
      Finset.mem_singleton, Finset.sum_singleton, Finset.sum_insert, hkl, not_false_eq_true,
      reduceIte, right_eq_add, ite_self, add_zero, zero_add, ite_sub_ite, sub_self,
      Base.cartanMatrix, Base.cartanMatrixIn_def]
    refine ite_congr rfl (fun hkil ↦ ?_) (fun _ ↦ rfl)
    simp only [pairingIn_eq_add_of_root_eq_add hkil, Int.cast_add]
    ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
this : ω b * ⁅h j, f i⁆ = ω b * -b.cartanMatrix i j • f i
⊢ ⁅h j, f i⁆ = -b.cartanMatrix i j • f i
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) ↦ ω b * x) (ω b * ⁅h j, f i⁆))
  ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (ω b * -b.cartanMatrix i j • f i))
Tactic: replace this := congr_arg (ω b * ·) this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : IsDomain R
inst_3 : CharZero R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
b : P.Base
inst_9 : Fintype ι
i j : ↥b.support
⊢ ⁅h j, f i⁆ = -b.cartanMatrix i j • f i
have suffices : ω b * ⁅h j, f i⁆ = ω b * -b.cartanMatrix i j • f i
Tactic: suffices ω b * ⁅h j, f i⁆ = ω b * (-b.cartanMatrix i j • f i) by
    replace this := congr_arg (ω b * ·) this
    simpa [← mul_assoc, ω_mul_ω] using this