-- Module: Mathlib.LinearAlgebra.RootSystem.RootPositive
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : CommRing R
inst_3 : Algebra S 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.IsValuedIn S
B : RootPositiveForm S P
i j : ι
inst_9 : FaithfulSMul S R
inst_10 : Module S M
inst_11 : IsScalarTower S R M
inst_12 : IsStrictOrderedRing S
hi :
  Membership.mem.{u_4, u_4} (α := M) (γ := Submodule S M)
    (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ((P.root : (a : ι) → M) i : M)
hj :
  Membership.mem.{u_4, u_4} (α := M) (γ := Submodule S M)
    (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) ((P.root : (a : ι) → M) j : M)
ri : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) i) hi
rj : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :=
  Subtype.mk (p := fun (x : M) ↦
    Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
    ((P.root : (a : ι) → M) j) hj
a :
  Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        (HMul.hMul (α := S) (β := S) (2 : S)
          ((((B.posForm :
                      (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) →
                        ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                    ri :
                  LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                    (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
              rj :
            S)) :
      R)
    ((algebraMap S R : (a : S) → R)
        (HMul.hMul (β := S) (P.pairingIn S i j)
          ((((B.posForm :
                      (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) →
                        ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                    rj :
                  LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                    (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
                (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
              rj :
            S)) :
      R)
⊢ HMul.hMul (α := S) (β := S) (2 : S)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                ri :
              LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
          rj :
        S) =
    HMul.hMul (β := S) (P.pairingIn S i j)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                rj :
              LinearMap.{u_3, u_3, u_4, u_3} (RingHom.id S)
                (↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) S) :
            (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → S)
          rj :
        S)

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Premises used: FaithfulSMul.algebraMap_injective