awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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
S : Type u_5
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : Module S M
inst_9 : IsScalarTower S R M
inst_10 : Module S N
inst_11 : IsScalarTower S R N
inst_12 : P.IsValuedIn S
inst_13 : Fintype ι
i : ι
c : S
hc :
  ∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i) =
    HMul.hMul (α := S)
      ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
              LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
            (a : ↥(P.rootSpan S)) → S)
          (P.rootSpanMem S i) :
        S)
      c
h :
  HSMul.hSMul (β := N) c
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
          (HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) :
        N) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
h₁ :
  HSMul.hSMul (β := N) c
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
          (HAdd.hAdd (α := ↥(P.rootSpan S)) (P.rootSpanMem S i) (P.rootSpanMem S i)) :
        N) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
h₂ :
  HSMul.hSMul (β := N) c
      ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
          (HAdd.hAdd (α := ↥(P.rootSpan S)) (P.rootSpanMem S i) (P.rootSpanMem S i)) :
        N) =
    c •
      HAdd.hAdd (α := N) (β := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
        ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
h₃ h₄ :
  c •
      HAdd.hAdd (α := N) (β := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
        ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N) =
    c •
      HAdd.hAdd (α := N) (β := N) ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
        ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)
⊢ (P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N)
      (c • HSMul.hSMul (α := ℕ) (β := ↥(P.rootSpan S)) 2 (P.rootSpanMem S i)) =
    c • HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn S : (a : ↥(P.rootSpan S)) → N) (P.rootSpanMem S i) : N)

Tactic:
rw [map_smul, two_smul, two_smul, map_add]

Premises used: two_smul, map_add, map_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i : ι
rw :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
              LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
            (a : ↥(P.rootSpan R)) → R)
          (P.rootSpanMem R i) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
rw₁ :
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.PolarizationIn R : (a : ↥(P.rootSpan R)) → N) (P.rootSpanMem R i) : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
rw₂ rw₃ :
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) (↑(P.rootSpanMem R i) : M) : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
⊢ HSMul.hSMul (α := R) (β := N)
      ((algebraMap R R : (a : R) → R)
          ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                  LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
                (a : ↥(P.rootSpan R)) → R)
              (P.rootSpanMem R i) :
            R) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)

Tactic:
rw [Algebra.algebraMap_self_apply, P.rootFormIn_self_smul_coroot R i, PolarizationIn_eq]

Premises used: Algebra.algebraMap_self_apply, RootPairing.PolarizationIn_eq, RootPairing.rootFormIn_self_smul_coroot
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i : ι
⊢ HSMul.hSMul (α := R) (β := N)
      ((algebraMap R R : (a : R) → R)
          ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                  LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
                (a : ↥(P.rootSpan R)) → R)
              (P.rootSpanMem R i) :
            R) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)

Tactic:
have : (algebraMap R R) ((P.RootFormIn R) (P.rootSpanMem R i) (P.rootSpanMem R i)) • P.coroot i =
      2 • P.Polarization (P.root i) := by
    rw [Algebra.algebraMap_self_apply, P.rootFormIn_self_smul_coroot R i, PolarizationIn_eq]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i : ι
this :
  HSMul.hSMul (α := R) (β := N)
      ((algebraMap R R : (a : R) → R)
          ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                  LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
                (a : ↥(P.rootSpan R)) → R)
              (P.rootSpanMem R i) :
            R) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)
rw :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := R) (β := N)
      ((algebraMap R R : (a : R) → R)
          ((((P.RootFormIn R : (a : ↥(P.rootSpan R)) → ↥(P.rootSpan R) →ₗ[R] R) (P.rootSpanMem R i) :
                  LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥(P.rootSpan R)) R) :
                (a : ↥(P.rootSpan R)) → R)
              (P.rootSpanMem R i) :
            R) :
        R)
      ((P.coroot : (a : ι) → N) i : N)
rw₁ rw₂ :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑(P.rootSpanMem R i) : M) : M →ₗ[R] R) : (a : M) → R)
          (↑(P.rootSpanMem R i) : M) :
        R)
      ((P.coroot : (a : ι) → N) i : N)
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := N)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R)
      ((P.coroot : (a : ι) → N) i : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)

Tactic:
rw [← this, algebraMap_rootFormIn]

Premises used: RootPairing.algebraMap_rootFormIn
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i : ι
⊢ HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.CorootForm : (a : N) → N →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : N →ₗ[R] R) : (a : N) → R)
          ((P.coroot : (a : ι) → N) i : N) :
        R)
      ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (α := ℕ) (β := M) 2 ((P.CoPolarization : (a : N) → M) ((P.coroot : (a : ι) → N) i : N) : M)

Tactic:
rootForm_self_smul_coroot (P.flip) i

Premises used: RootPairing.rootForm_self_smul_coroot, RootPairing.flip
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i j : ι
rw :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
rw₁ :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R) =
    HSMul.hSMul (α := ℕ) 2
      (HSMul.hSMul (α := ℕ) (β := R) 2
        ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
            ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
          R))
rw₂ :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R) =
    HSMul.hSMul (β := R) (HSMul.hSMul (α := ℕ) (β := ℕ) 2 2)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R)
rw₃ rw₄ :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R) =
    HSMul.hSMul (β := R) (HMul.hMul (α := ℕ) 2 2)
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N) :
        R)
⊢ HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)

Tactic:
rw [← toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower, ← smul_assoc,
      Nat.nsmul_eq_mul]

Premises used: smul_assoc, RootPairing.toLinearMap_apply_apply_Polarization, Nat.nsmul_eq_mul, LinearMap.map_smul_of_tower
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i j : ι
⊢ HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)

Tactic:
have hij : 4 • (P.RootForm (P.root i)) (P.root j) =
      2 • P.toLinearMap (P.root j) (2 • P.Polarization (P.root i)) := by
    rw [← toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower, ← smul_assoc,
      Nat.nsmul_eq_mul]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i j : ι
hij :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)

Tactic:
apply (rootForm_symmetric P).eq

Premises used: LinearMap.IsSymm.eq, RootPairing.rootForm_symmetric
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i j : ι
hij :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
rw :
  HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
rw₁ :
  HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
rw₂ rw₃ :
  HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
          ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N) :
        R)
⊢ HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))

Tactic:
rw [show (P.RootForm (P.root i)) (P.root j) = (P.RootForm (P.root j)) (P.root i) by
      apply (rootForm_symmetric P).eq, ← toLinearMap_apply_apply_Polarization,
      LinearMap.map_smul_of_tower]

Premises used: RootPairing.toLinearMap_apply_apply_Polarization, LinearMap.map_smul_of_tower
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i j : ι
hij :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
⊢ HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))

Tactic:
have hji : 2 • (P.RootForm (P.root i)) (P.root j) =
      P.toLinearMap (P.root i) (2 • P.Polarization (P.root j)) := by
    rw [show (P.RootForm (P.root i)) (P.root j) = (P.RootForm (P.root j)) (P.root i) by
      apply (rootForm_symmetric P).eq, ← toLinearMap_apply_apply_Polarization,
      LinearMap.map_smul_of_tower]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i j : ι
hij :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
hji :
  HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
rw :
  HMul.hMul (α := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        (P.pairing j i) *
      HMul.hMul (α := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
        (P.pairing i j) =
    P.pairing i j * P.pairing j i *
      HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
⊢ HSMul.hSMul (α := ℕ) 4
      (HPow.hPow (α := R) (β := ℕ)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
        2) =
    P.coxeterWeight i j •
      HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)

Tactic:
rw [sq, nsmul_eq_mul, ← mul_assoc, ← nsmul_eq_mul, hij, ← rootForm_self_smul_coroot,
    smul_mul_assoc 2, ← mul_smul_comm, hji, ← rootForm_self_smul_coroot, map_smul, ← pairing,
    map_smul, ← pairing, smul_eq_mul, smul_eq_mul, smul_eq_mul, coxeterWeight]

Premises used: RootPairing.rootForm_self_smul_coroot, RootPairing.coxeterWeight, RootPairing.pairing, mul_assoc, smul_mul_assoc, sq, nsmul_eq_mul, mul_smul_comm, smul_eq_mul, OfNat.ofNat, map_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
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 : Fintype ι
i j : ι
hij :
  HSMul.hSMul (α := ℕ) (β := R) 4
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) j) : N →ₗ[R] R) : (a : N) → R)
          (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) :
        R)
hji :
  HSMul.hSMul (α := ℕ) (β := R) 2
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      (HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
⊢ HMul.hMul (α := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        (P.pairing j i) *
      HMul.hMul (α := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)
        (P.pairing i j) =
    P.pairing i j * P.pairing j i *
      HMul.hMul (α := R) (β := R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) j : M) :
          R)

Tactic:
ring