awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
⊢ P.pairing ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairing i j
have rw : (P.root' ((P.reflectionPerm i : (a : ι) → ι) i) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
Tactic: rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw : (P.root' ((P.reflectionPerm i : (a : ι) → ι) i) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
⊢ P.pairing ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairing i j
have rw₁ : (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι)) :
        N →ₗ[R] R) :
      (a : N) → R)
    ((P.coroot : (a : ι) → N) j : N) =
  -P.pairing i j
Tactic: rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw : (P.root' ((P.reflectionPerm i : (a : ι) → ι) i) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₁ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι)) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
⊢ P.pairing ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairing i j
have rw₂ : (((P.toLinearMap : (a : M) → N →ₗ[R] R)
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
            (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
              ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
                  ((P.coroot : (a : ι) → N) i : N) :
                R)
              ((P.root : (a : ι) → M) i : M))) :
        N →ₗ[R] R) :
      (a : N) → R)
    ((P.coroot : (a : ι) → N) j : N) =
  -P.pairing i j
Tactic: rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw : (P.root' ((P.reflectionPerm i : (a : ι) → ι) i) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₁ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι)) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₂ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
                ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
                    ((P.coroot : (a : ι) → N) i : N) :
                  R)
                ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
⊢ P.pairing ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairing i j
have rw₃ : (((P.toLinearMap : (a : M) → N →ₗ[R] R)
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
            (HSMul.hSMul (β := M) (P.pairing i i) ((P.root : (a : ι) → M) i : M))) :
        N →ₗ[R] R) :
      (a : N) → R)
    ((P.coroot : (a : ι) → N) j : N) =
  -P.pairing i j
Tactic: rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw : (P.root' ((P.reflectionPerm i : (a : ι) → ι) i) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₁ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι)) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₂ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
                ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
                    ((P.coroot : (a : ι) → N) i : N) :
                  R)
                ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₃ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul (β := M) (P.pairing i i) ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
⊢ P.pairing ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairing i j
have rw₄ : (((P.toLinearMap : (a : M) → N →ₗ[R] R)
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
            (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))) :
        N →ₗ[R] R) :
      (a : N) → R)
    ((P.coroot : (a : ι) → N) j : N) =
  -P.pairing i j
Tactic: rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw : (P.root' ((P.reflectionPerm i : (a : ι) → ι) i) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₁ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι)) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₂ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
                ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
                    ((P.coroot : (a : ι) → N) i : N) :
                  R)
                ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₃ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul (β := M) (P.pairing i i) ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₄ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
⊢ P.pairing ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairing i j
have rw₅ : (((P.toLinearMap : (a : M) → N →ₗ[R] R)
          (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
            (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) i : M))) :
        N →ₗ[R] R) :
      (a : N) → R)
    ((P.coroot : (a : ι) → N) j : N) =
  -P.pairing i j
Tactic: rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw : (P.root' ((P.reflectionPerm i : (a : ι) → ι) i) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₁ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι)) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₂ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
                ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
                    ((P.coroot : (a : ι) → N) i : N) :
                  R)
                ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₃ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul (β := M) (P.pairing i i) ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₄ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₅ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
⊢ P.pairing ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairing i j
have rw₆ : (((P.toLinearMap : (a : M) → N →ₗ[R] R) (-(P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
    ((P.coroot : (a : ι) → N) j : N) =
  -P.pairing i j
Tactic: rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw : (P.root' ((P.reflectionPerm i : (a : ι) → ι) i) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₁ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι)) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₂ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
                ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
                    ((P.coroot : (a : ι) → N) i : N) :
                  R)
                ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₃ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul (β := M) (P.pairing i i) ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₄ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₅ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₆ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) (-(P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
⊢ P.pairing ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairing i j
have rw₇ : -(((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
  -P.pairing i j
Tactic: rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw : (P.root' ((P.reflectionPerm i : (a : ι) → ι) i) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = -P.pairing i j
rw₁ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) i : ι)) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₂ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
                ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
                    ((P.coroot : (a : ι) → N) i : N) :
                  R)
                ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₃ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul (β := M) (P.pairing i i) ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₄ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₅ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R)
            (HSub.hSub (α := M) ((P.root : (a : ι) → M) i : M)
              (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) i : M))) :
          N →ₗ[R] R) :
        (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₆ :
  (((P.toLinearMap : (a : M) → N →ₗ[R] R) (-(P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
rw₇ :
  -(((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
        ((P.coroot : (a : ι) → N) j : N) =
    -P.pairing i j
⊢ P.pairing ((P.reflectionPerm i : (a : ι) → ι) i) j = -P.pairing i j
have rw₈ : -P.pairing i j = -P.pairing i j
Tactic: rw [pairing, root', ← reflectionPerm_root, root'_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, LinearMap.map_neg₂, root'_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
⊢ P.pairing i ((P.reflectionPerm j : (a : ι) → ι) j) = -P.pairing i j
have rw : (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : N) = -P.pairing i j
Tactic: rw [pairing, ← reflectionPerm_coroot, root_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, map_neg, root_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw :
  (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : N) = -P.pairing i j
⊢ P.pairing i ((P.reflectionPerm j : (a : ι) → ι) j) = -P.pairing i j
have rw₁ : (P.root' i : (a : N) → R)
    (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
            ((P.coroot : (a : ι) → N) j : N) :
          R)
        ((P.coroot : (a : ι) → N) j : N))) =
  -P.pairing i j
Tactic: rw [pairing, ← reflectionPerm_coroot, root_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, map_neg, root_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw :
  (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : N) = -P.pairing i j
rw₁ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
              ((P.coroot : (a : ι) → N) j : N) :
            R)
          ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
⊢ P.pairing i ((P.reflectionPerm j : (a : ι) → ι) j) = -P.pairing i j
have rw₂ : (P.root' i : (a : N) → R)
    (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
      (HSMul.hSMul (β := N) (P.pairing j j) ((P.coroot : (a : ι) → N) j : N))) =
  -P.pairing i j
Tactic: rw [pairing, ← reflectionPerm_coroot, root_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, map_neg, root_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw :
  (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : N) = -P.pairing i j
rw₁ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
              ((P.coroot : (a : ι) → N) j : N) :
            R)
          ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₂ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul (β := N) (P.pairing j j) ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
⊢ P.pairing i ((P.reflectionPerm j : (a : ι) → ι) j) = -P.pairing i j
have rw₃ : (P.root' i : (a : N) → R)
    (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N))) =
  -P.pairing i j
Tactic: rw [pairing, ← reflectionPerm_coroot, root_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, map_neg, root_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw :
  (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : N) = -P.pairing i j
rw₁ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
              ((P.coroot : (a : ι) → N) j : N) :
            R)
          ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₂ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul (β := N) (P.pairing j j) ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₃ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
⊢ P.pairing i ((P.reflectionPerm j : (a : ι) → ι) j) = -P.pairing i j
have rw₄ : (P.root' i : (a : N) → R)
    (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
      (HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) j : N))) =
  -P.pairing i j
Tactic: rw [pairing, ← reflectionPerm_coroot, root_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, map_neg, root_coroot_eq_pairing]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Defs (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
i j : ι
rw :
  (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : N) = -P.pairing i j
rw₁ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
          ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
              ((P.coroot : (a : ι) → N) j : N) :
            R)
          ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₂ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul (β := N) (P.pairing j j) ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₃ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
rw₄ :
  (P.root' i : (a : N) → R)
      (HSub.hSub (α := N) ((P.coroot : (a : ι) → N) j : N)
        (HAdd.hAdd (α := N) (β := N) ((P.coroot : (a : ι) → N) j : N) ((P.coroot : (a : ι) → N) j : N))) =
    -P.pairing i j
⊢ P.pairing i ((P.reflectionPerm j : (a : ι) → ι) j) = -P.pairing i j
have rw₅ : (P.root' i : (a : N) → R) (-(P.coroot : (a : ι) → N) j : N) = -P.pairing i j
Tactic: rw [pairing, ← reflectionPerm_coroot, root_coroot_eq_pairing, pairing_same, two_smul,
    sub_add_cancel_left, map_neg, root_coroot_eq_pairing]