-- Module: Mathlib.RingTheory.Finiteness.Descent
Goal:
R : Type u_1
inst : CommRing R
T : Type u_3
inst_1 : CommRing T
inst_2 : Algebra R T
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : FaithfullyFlat R T
inst_6 : Module.Finite T (T ⊗[R] M)
obtain :
  ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤),
    Module.Finite R M
obtain₁ :
  ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤)
    (k : (i : Fin n) → ℕ) (t : (i : Fin n) → Fin (k i) → T) (m : (i : Fin n) → Fin (k i) → M)
    (h : ∀ (i : Fin n), s i = ∑ j : Fin (k i), t i j ⊗ₜ[R] m i j), Module.Finite R M
obtain₂ :
  ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤)
    (k : (i : Fin n) → ℕ) (t : (i : Fin n) → Fin (k i) → T) (m : (i : Fin n) → Fin (k i) → M)
    (h : ∀ (i : Fin n), s i = ∑ j : Fin (k i), t i j ⊗ₜ[R] m i j), Module.Finite R M
obtain₃ :
  ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤)
    (k : (i : Fin n) → ℕ) (t : (i : Fin n) → Fin (k i) → T) (m : (i : Fin n) → Fin (k i) → M)
    (h : ∀ (i : Fin n), s i = ∑ j : Fin (k i), t i j ⊗ₜ[R] m i j),
    let f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
      (Basis.constr (Pi.basisFun R ((i : Fin n) × Fin (k i))) R :
          (a : (i : Fin n) × Fin (k i) → M) → ((i : Fin n) × Fin (k i) → R) →ₗ[R] M)
        fun (x : (i : Fin n) × Fin (k i)) ↦
        match (motive := (i : Fin n) × Fin (k i) → M) x with
        | ⟨i, j⟩ => m i j;
    Function.Surjective.{u_1 + 1, u_4 + 1} (α := (i : Fin n) × Fin (k i) → R) (β := M)
      (⇑f₀ : (a : (i : Fin n) × Fin (k i) → R) → M)
obtain₄ :
  ∀ (n : ℕ) (s : Fin n → T ⊗[R] M) (hs : Eq (α := Submodule T (T ⊗[R] M)) (Submodule.span T (Set.range s)) ⊤)
    (k : (i : Fin n) → ℕ) (t : (i : Fin n) → Fin (k i) → T) (m : (i : Fin n) → Fin (k i) → M)
    (h : ∀ (i : Fin n), s i = ∑ j : Fin (k i), t i j ⊗ₜ[R] m i j),
    let f₀ : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M :=
      (Basis.constr (Pi.basisFun R ((i : Fin n) × Fin (k i))) R :
          (a : (i : Fin n) × Fin (k i) → M) → ((i : Fin n) × Fin (k i) → R) →ₗ[R] M)
        fun (x : (i : Fin n) × Fin (k i)) ↦
        match (motive := (i : Fin n) × Fin (k i) → M) x with
        | ⟨i, j⟩ => m i j;
    ∀
      (this :
        Function.Surjective (α := T ⊗[R] ((i : Fin n) × Fin (k i) → R)) (β := T ⊗[R] M)
          (⇑(((AlgebraTensorModule.lTensor T T :
                      (((i : Fin n) × Fin (k i) → R) →ₗ[R] M) →ₗ[R]
                        T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
                    (a : ((i : Fin n) × Fin (k i) → R) →ₗ[R] M) → T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M)
                  f₀ :
                T ⊗[R] ((i : Fin n) × Fin (k i) → R) →ₗ[T] T ⊗[R] M) :
            (a : T ⊗[R] ((i : Fin n) × Fin (k i) → R)) → T ⊗[R] M)),
      Function.Surjective.{u_1 + 1, u_4 + 1} (α := (i : Fin n) × Fin (k i) → R) (β := M)
        (⇑f₀ : (a : (i : Fin n) × Fin (k i) → R) → M)
⊢ Module.Finite R M

Tactic:
classical
  obtain ⟨n, s, hs⟩ := Module.Finite.exists_fin (R := T) (M := T ⊗[R] M)
  choose k t m h using fun i : Fin n ↦ TensorProduct.exists_sum_tmul_eq (s i)
  let f₀ : ((Σ i, Fin (k i)) → R) →ₗ[R] M := (Pi.basisFun R _).constr R fun ⟨i, j⟩ ↦ m i j
  apply of_surjective f₀
  have : Function.Surjective (AlgebraTensorModule.lTensor T T f₀) := by
    rw [← LinearMap.range_eq_top, eq_top_iff, ← hs, Submodule.span_le, Set.range_subset_iff]
    intro i
    use ∑ (j : Fin (k i)), t i j ⊗ₜ Pi.basisFun R _ ⟨i, j⟩
    simp [f₀, -Pi.basisFun_equivFun, -Pi.basisFun_apply, h i]
  rwa [← Module.FaithfullyFlat.lTensor_surjective_iff_surjective _ T]

Premises used: Module.FaithfullyFlat.lTensor_surjective_iff_surjective, Module.Finite.exists_fin