-- 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
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)
⊢ 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 hx₁ : Membership.mem (α := M) (γ := Submodule S M) (span S (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
  ((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)
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))