-- Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid N
inst_6 : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : Eq (α := S ⊗[R] N) ((LinearMap.baseChange S f : (a : S ⊗[R] M) → S ⊗[R] N) t : S ⊗[R] N) (0 : S ⊗[R] N)
obtain :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t),
    ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
        (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
obtain₁ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M)
    (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t),
    ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
        (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
obtain₂ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M) (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t)
    (this :
      ∀
        (h :
          Eq (α := S ⊗[R] N)
            ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              S ⊗[R] N)
            ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N) 0 : S ⊗[R] N)),
        ∃ (B : Subalgebra R S) (hAB : A ≤ B),
          B.FG ∧
            Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
              ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                  ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
                TensorProduct.{u_1, u_2, u_4} R (↥B) N)
              ((rTensor N (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N) 0 :
                TensorProduct.{u_1, u_2, u_4} R (↥B) N)),
    ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
        (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
obtain₃ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M) (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t)
    (this :
      ∀
        (h :
          Eq (α := S ⊗[R] N)
            ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              S ⊗[R] N)
            (0 : S ⊗[R] N)),
        ∃ (B : Subalgebra R S),
          B.FG ∧
            ∃ (x : A ≤ B),
              Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                    ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
                  TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)),
    ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
        (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
obtain₄ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M) (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t)
    (this :
      ∀
        (h :
          Eq (α := S ⊗[R] N)
            ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              S ⊗[R] N)
            (0 : S ⊗[R] N)),
        ∃ (B : Subalgebra R S),
          B.FG ∧
            ∃ (x : A ≤ B),
              Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                    ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
                  TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N))
    (hu' :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N)),
    ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
        (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
obtain₅ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M) (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t)
    (this :
      ∀
        (h :
          Eq (α := S ⊗[R] N)
            ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              S ⊗[R] N)
            (0 : S ⊗[R] N)),
        ∃ (B : Subalgebra R S),
          B.FG ∧
            ∃ (x : A ≤ B),
              Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                    ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
                  TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N))
    (hu' :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N))
    (B : Subalgebra R S) (hB : B.FG) (hAB : A ≤ B)
    (hu' :
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)),
    ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
          (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
        (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t
h :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M) (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t)
    (this :
      ∀
        (h :
          Eq (α := S ⊗[R] N)
            ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              S ⊗[R] N)
            (0 : S ⊗[R] N)),
        ∃ (B : Subalgebra R S),
          B.FG ∧
            ∃ (x : A ≤ B),
              Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                    ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
                  TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N))
    (hu' :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N))
    (B : Subalgebra R S) (hB : B.FG) (hAB : A ≤ B)
    (hu' :
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)),
    Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((LinearMap.baseChange (↥B) f : (a : ↥B ⊗[R] M) → ↥B ⊗[R] N)
            ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N) ∧
      (rTensor M B.val.toLinearMap : (a : ↥B ⊗[R] M) → S ⊗[R] M)
          ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) =
        t
h₁ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M) (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t)
    (this :
      ∀
        (h :
          Eq (α := S ⊗[R] N)
            ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              S ⊗[R] N)
            (0 : S ⊗[R] N)),
        ∃ (B : Subalgebra R S),
          B.FG ∧
            ∃ (x : A ≤ B),
              Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                    ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
                  TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N))
    (hu' :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N))
    (B : Subalgebra R S) (hB : B.FG) (hAB : A ≤ B)
    (hu' :
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)),
    Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
      ((LinearMap.baseChange (↥B) f : (a : ↥B ⊗[R] M) → ↥B ⊗[R] N)
          ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) :
        TensorProduct.{u_1, u_2, u_4} R (↥B) N)
      (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)
h₂ h₃ :
  ∀ (A : Subalgebra R S) (hA : A.FG)
    (ht_memA : Membership.mem (γ := Submodule R (S ⊗[R] M)) (range (rTensor M A.val.toLinearMap)) t)
    (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M) (hu : (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t)
    (this :
      ∀
        (h :
          Eq (α := S ⊗[R] N)
            ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
                ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
              S ⊗[R] N)
            (0 : S ⊗[R] N)),
        ∃ (B : Subalgebra R S),
          B.FG ∧
            ∃ (x : A ≤ B),
              Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
                    ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
                  TensorProduct.{u_1, u_2, u_4} R (↥B) N)
                (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N))
    (hu' :
      Eq (α := S ⊗[R] N)
        ((rTensor N A.val.toLinearMap : (a : ↥A ⊗[R] N) → S ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          S ⊗[R] N)
        (0 : S ⊗[R] N))
    (B : Subalgebra R S) (hB : B.FG) (hAB : A ≤ B)
    (hu' :
      Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        ((rTensor N (Subalgebra.inclusion ⋯).toLinearMap : (a : ↥A ⊗[R] N) → ↥B ⊗[R] N)
            ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u) :
          TensorProduct.{u_1, u_2, u_4} R (↥B) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥B) N)),
    (rTensor M B.val.toLinearMap : (a : ↥B ⊗[R] M) → S ⊗[R] M)
        ((rTensor M (Subalgebra.inclusion hAB).toLinearMap : (a : ↥A ⊗[R] M) → ↥B ⊗[R] M) u) =
      t
⊢ ∃ (A : Subalgebra R S) (_ : A.FG) (u : TensorProduct.{u_1, u_2, u_3} R (↥A) M),
    Eq (α := TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        ((LinearMap.baseChange (↥A) f : (a : ↥A ⊗[R] M) → ↥A ⊗[R] N) u : TensorProduct.{u_1, u_2, u_4} R (↥A) N)
        (0 : TensorProduct.{u_1, u_2, u_4} R (↥A) N) ∧
      (rTensor M A.val.toLinearMap : (a : ↥A ⊗[R] M) → S ⊗[R] M) u = t

Tactic:
classical
  obtain ⟨A, hA, ht_memA⟩ := TensorProduct.Algebra.exists_of_fg t
  obtain ⟨u, hu⟩ := _root_.id ht_memA
  have := TensorProduct.Algebra.eq_of_fg_of_subtype_eq hA (t := f.baseChange _ u) (t' := 0)
  simp only [map_zero, exists_and_left] at this
  have hu' : (A.val.toLinearMap.rTensor N) (f.baseChange (↥A) u) = 0 := by
    rw [← ht, ← hu, rTensor_baseChange]
  obtain ⟨B, hB, hAB, hu'⟩ := this hu'
  use B, hB, rTensor M (Subalgebra.inclusion hAB).toLinearMap u
  constructor
  · rw [← rTensor_baseChange, hu']
  · rw [← comp_apply, ← rTensor_comp, ← hu]
    congr

Premises used: TensorProduct.Algebra.exists_of_fg, LinearMap.comp_apply, map_zero, exists_and_left, LinearMap.rTensor_baseChange, LinearMap.rTensor_comp