-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
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 ⋯
⊢ 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)))
have 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 sorry))) :
        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 sorry),
  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)))
Tactic: rw [this, LinearMap.rTensor_comp] at h
Cleared hypotheses: h, x_1, hx, this