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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
        ((P.root : (a : ι) → M) j : M))
have h₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M))
Tactic: calc 2 • P.toLinearMap x (P.coroot i) • P.root i
      = P.toLinearMap x (P.coroot i) • ((2 : R) • P.root i) := ?_
    _ = P.toLinearMap x (P.coroot i) • (P.pairing i j • P.root j) := ?_
    _ = P.toLinearMap x (P.pairing i j • P.coroot i) • (P.root j) := ?_
    _ = P.toLinearMap x ((2 : R) • P.coroot j) • (P.root j) := ?_
    _ = 2 • P.toLinearMap x (P.coroot j) • P.root j := ?_
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
h₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M))
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
        ((P.root : (a : ι) → M) j : M))
have h₂ : HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
      R)
    ((P.root : (a : ι) → M) j : M)
Tactic: calc 2 • P.toLinearMap x (P.coroot i) • P.root i
      = P.toLinearMap x (P.coroot i) • ((2 : R) • P.root i) := ?_
    _ = P.toLinearMap x (P.coroot i) • (P.pairing i j • P.root j) := ?_
    _ = P.toLinearMap x (P.pairing i j • P.coroot i) • (P.root j) := ?_
    _ = P.toLinearMap x ((2 : R) • P.coroot j) • (P.root j) := ?_
    _ = 2 • P.toLinearMap x (P.coroot j) • P.root j := ?_
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
h₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M))
h₂ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) : R)
        ((P.root : (a : ι) → M) j : M))
have h₃ : HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
      R)
    ((P.root : (a : ι) → M) j : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
      R)
    ((P.root : (a : ι) → M) j : M)
Tactic: calc 2 • P.toLinearMap x (P.coroot i) • P.root i
      = P.toLinearMap x (P.coroot i) • ((2 : R) • P.root i) := ?_
    _ = P.toLinearMap x (P.coroot i) • (P.pairing i j • P.root j) := ?_
    _ = P.toLinearMap x (P.pairing i j • P.coroot i) • (P.root j) := ?_
    _ = P.toLinearMap x ((2 : R) • P.coroot j) • (P.root j) := ?_
    _ = 2 • P.toLinearMap x (P.coroot j) • P.root j := ?_
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
have h : HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
Tactic: rw [smul_comm, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
have h₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (↑2 : R) ((P.root : (a : ι) → M) i : M)) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
Tactic: rw [smul_comm, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
h₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) (↑2 : R) ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
⊢ HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
have h₂ : HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
Tactic: rw [smul_comm, ← Nat.cast_smul_eq_nsmul R, Nat.cast_ofNat]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M))
have h : HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul (β := M) (P.pairing i i) ((P.root : (a : ι) → M) i : M))
Tactic: rw [P.pairing_smul_root_eq j i i hij.symm, pairing_same]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i i) ((P.root : (a : ι) → M) i : M))
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M))
have h₁ : HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
    (HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M))
Tactic: rw [P.pairing_smul_root_eq j i i hij.symm, pairing_same]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)
have h : P.pairing i j •
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      ((P.root : (a : ι) → M) j : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
      R)
    ((P.root : (a : ι) → M) j : M)
Tactic: rw [← smul_comm, ← smul_assoc, map_smul]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  P.pairing i j •
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)
have h₁ : HSMul.hSMul (β := M)
    (HSMul.hSMul (β := R) (P.pairing i j)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R))
    ((P.root : (a : ι) → M) j : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
      R)
    ((P.root : (a : ι) → M) j : M)
Tactic: rw [← smul_comm, ← smul_assoc, map_smul]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
h :
  P.pairing i j •
      HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
        ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)
h₁ :
  HSMul.hSMul (β := M)
      (HSMul.hSMul (β := R) (P.pairing i j)
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R))
      ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R)
      (HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M)) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)
have h₂ : HSMul.hSMul (β := M)
    (HSMul.hSMul (β := R) (P.pairing i j)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R))
    ((P.root : (a : ι) → M) j : M) =
  HSMul.hSMul (β := M)
    (HSMul.hSMul (β := R) (P.pairing i j)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R) ((P.coroot : (a : ι) → N) i : N) : R))
    ((P.root : (a : ι) → M) j : M)
Tactic: rw [← smul_comm, ← smul_assoc, map_smul]
-- 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 : ι
hij : P.reflectionPerm i = P.reflectionPerm j
x : M
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N)) :
        R)
      ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
        R)
      ((P.root : (a : ι) → M) j : M)
have h : HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul (β := N) (P.pairing j j) ((P.coroot : (a : ι) → N) j : N)) :
      R)
    ((P.root : (a : ι) → M) j : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
    ((((P.toLinearMap : (a : M) → N →ₗ[R] R) x : N →ₗ[R] R) : (a : N) → R)
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N) 2 ((P.coroot : (a : ι) → N) j : N)) :
      R)
    ((P.root : (a : ι) → M) j : M)
Tactic: rw [← P.pairing_smul_coroot_eq j i j hij.symm, pairing_same]