-- 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
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)
rw :
  ¬LE.le.{u_3} (α := 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) hi) :
                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) hj :
              ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) :
          S)
        (0 : S) ↔
    ¬P.pairingIn S i j ≤ 0
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) hi) :
              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) hj :
            ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) :
        S) ↔
    ¬P.pairingIn S i j ≤ 0
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) hi) :
              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) hj :
            ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) :
        S) ↔
    0 < P.pairingIn S i j
⊢ LE.le.{u_3} (α := 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) hi) :
              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) hj :
            ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) :
        S)
      (0 : S) ↔
    P.pairingIn S i j ≤ 0
have rw₃ : 0 < P.pairingIn S i j ↔ 0 < P.pairingIn S i j
Tactic: rw [← not_iff_not, not_le, not_le, zero_lt_apply_root_root_iff]