-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.RootPositive (goal)
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
rw :
  LT.lt.{u_3} (α := S) (0 : S)
      ((((B.posForm :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                (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) ⋯) :
              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)
          (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) ⋯ :
            ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) :
        S) ↔
    0 < P.pairingIn S j i
rw₁ :
  LT.lt (α := S) (0 : S)
      ((RingHom.id S : (a : S) → S)
          ((((B.posForm :
                      (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) →
                        ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
                    (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) ⋯) :
                  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)
              (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) ⋯ :
                ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) :
            S) :
        S) ↔
    0 < P.pairingIn S j i
⊢ 0 < P.pairingIn S i j ↔ 0 < P.pairingIn S j i
have rw₂ : LT.lt.{u_3} (α := S) (0 : S)
    ((((B.posForm : (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → ↥(span S (range (⇑P.root : (a : ι) → M))) →ₗ[S] S)
              (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) sorry) :
            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)
        (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) sorry :
          ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) :
      S) ↔
  0 < P.pairingIn S j i
Tactic: rw [← B.zero_lt_apply_root_root_iff, ← B.isSymm_posForm.eq, RingHom.id_apply,
    B.zero_lt_apply_root_root_iff]