-- 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
x_1 x_2 : ↥(span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
x : M
hx : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
y : M
hy : Membership.mem (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) y
⊢ Membership.mem (α := R) (γ := Submodule S R) (LinearMap.range (Algebra.linearMap S R))
    ((((B.form : (a : M) → M →ₗ[R] R)
              ((Submodule.subtype (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :
                  (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → 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)
                  x hx)) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((Submodule.subtype (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) :
              (a : ↥(span S (range (⇑P.root : (a : ι) → M)))) → 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) y
              hy) :
          M) :
      R)
have hB : ∀ (x : M),
  Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x →
    ∀ (y : M),
      Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) y →
        Membership.mem (α := R) (γ := Submodule S R) (LinearMap.range (Algebra.linearMap S R))
          ((((LinearMap.restrictScalarsₗ S R M R S ∘ₗ
                        (↑S :
                            {S_1 : Type u_2} →
                              {M : Type u_4} →
                                {M₂ : Type (max u_2 u_4)} →
                                  [inst : Semiring S] →
                                    [inst_12 : Semiring S_1] →
                                      [inst_13 : AddCommMonoid M] →
                                        [inst_14 : AddCommMonoid M₂] →
                                          [inst_15 : Module S M] →
                                            [inst_16 : Module S M₂] →
                                              [inst_17 : Module S_1 M] →
                                                [inst_18 : Module S_1 M₂] →
                                                  [LinearMap.CompatibleSMul M M₂ S S_1] →
                                                    (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                          B.form :
                      (a : M) → M →ₗ[S] R)
                    x :
                  M →ₗ[S] R) :
                (a : M) → R)
              y :
            R)
Tactic: apply LinearMap.BilinMap.apply_apply_mem_of_mem_span
      (s := range P.root) (t := range P.root)
      (B := (LinearMap.restrictScalarsₗ S R _ _ _).comp (B.form.restrictScalars S))