-- Module: Mathlib.RingTheory.LinearDisjoint
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
inst_3 : Algebra.IsIntegral.{u, v} R ↥A
H : ∀ A' ≤ A, ∀ [Module.Finite.{u, v} R ↥A'], A'.LinearDisjoint B
x y :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hxy :
  Eq (α := S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        x :
      S)
    ((Submodule.mulMap ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A)
            ((toSubmodule : (a : Subalgebra R S) → Submodule R S) B) :
          (a :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)) →
            S)
        y :
      S)
M' : Submodule R S
hM : M' ≤ (toSubmodule : (a : Subalgebra R S) → Submodule R S) A
hf : Module.Finite.{u, v} R ↥M'
h :
  {x, y} ⊆
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hM))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
s : Finset S
hs : Submodule.span R (↑s : Set S) = M'
hs' : (↑s : Set S) ⊆ (↑A : Set S)
A' : Subalgebra R S := Algebra.adjoin R (↑s : Set S)
hf' : Module.Finite.{u, v} R ↥A'
hA :
  LE.le (α := Submodule R S) ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A' : Submodule R S)
    ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)
x_1 :
  ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
    ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)
hx :
  Membership.mem (γ :=
    Set
      (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
        ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)))
    {x, y} x_1
this : Submodule.inclusion hM = Submodule.inclusion hA ∘ₗ Submodule.inclusion ⋯
rw :
  ∀
    (h :
      {x, y} ⊆
        (↑(LinearMap.range (M := ↥M' ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
              (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
                  (Submodule.inclusion hA) ∘ₗ
                LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
                  (Submodule.inclusion ⋯))) :
          Set
            (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B))))
    (x_2 :
      ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
        ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
    (hx :
      Membership.mem (γ :=
        Set
          (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S)))
        {x, y} x_2)
    (this : Submodule.inclusion hM = Submodule.inclusion hA ∘ₗ Submodule.inclusion ⋯),
    x_2 ∈
      (↑(LinearMap.range
            (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
              (Submodule.inclusion hA))) :
        Set
          (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))
⊢ x_1 ∈
    (↑(LinearMap.range
          (LinearMap.rTensor (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B : Submodule R S))
            (Submodule.inclusion hA))) :
      Set
        (↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) ⊗[R]
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) B)))

Tactic:
rw [this, LinearMap.rTensor_comp] at h

Premises used: LinearMap.rTensor_comp