diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
index 15f5e057ea6a85..ef03db1257a724 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
@@ -803,6 +803,20 @@ instance isIso_ι_initial [HasInitial J] (F : J ⥤ C) [∀ (i j : J) (f : i ⟶
   isIso_ι_of_isInitial initialIsInitial F
 #align category_theory.limits.is_iso_ι_initial CategoryTheory.Limits.isIso_ι_initial
 
+/-- Any morphism between terminal objects is an isomorphism. -/
+lemma isIso_of_isTerminal {X Y : C} (hX : IsTerminal X) (hY : IsTerminal Y) (f : X ⟶ Y) :
+    IsIso f := by
+  refine ⟨⟨IsTerminal.from hX Y, ?_⟩⟩
+  simp only [IsTerminal.comp_from, IsTerminal.from_self, true_and]
+  apply IsTerminal.hom_ext hY
+
+/-- Any morphism between initial objects is an isomorphism. -/
+lemma isIso_of_isInitial {X Y : C} (hX : IsInitial X) (hY : IsInitial Y) (f : X ⟶ Y) :
+    IsIso f := by
+  refine ⟨⟨IsInitial.to hY X, ?_⟩⟩
+  simp only [IsInitial.to_comp, IsInitial.to_self, and_true]
+  apply IsInitial.hom_ext hX
+
 end
 
 end CategoryTheory.Limits
diff --git a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
index 13182a9c7c3b83..fac622842d38e2 100644
--- a/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
+++ b/Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
@@ -3,9 +3,12 @@ Copyright (c) 2024 Judith Ludwig, Christian Merten. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Judith Ludwig, Christian Merten
 -/
+import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
+import Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
 import Mathlib.LinearAlgebra.TensorProduct.Pi
+import Mathlib.LinearAlgebra.TensorProduct.RightExactness
 import Mathlib.RingTheory.AdicCompletion.Exactness
-import Mathlib.RingTheory.TensorProduct.Basic
+import Mathlib.RingTheory.Flat.Algebra
 
 /-!
 
@@ -13,12 +16,18 @@ import Mathlib.RingTheory.TensorProduct.Basic
 
 In this file we examine properties of the natural map
 
-`(AdicCompletion I R) ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M`.
+`AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M`.
 
-We show
+We show (in the `AdicCompletion` namespace):
 
-- it is an isomorphism if `M = R^n`.
-- it is surjective, if `M` is a finite `R`-module.
+- `ofTensorProduct_bijective_of_pi_of_fintype`: it is an isomorphism if `M = R^n`.
+- `ofTensorProduct_surjective_of_finite`: it is surjective, if `M` is a finite `R`-module.
+- `ofTensorProduct_bijective_of_finite_of_isNoetherian`: it is an isomorphism if `R` is Noetherian
+  and `M` is a finite `R`-module.
+
+As a corollary we obtain
+
+- `flat_of_isNoetherian`: the adic completion of a Noetherian ring `R` is `R`-flat.
 
 ## TODO
 
@@ -27,6 +36,10 @@ We show
 
 -/
 
+suppress_compilation
+
+universe u v
+
 variable {R : Type*} [CommRing R] (I : Ideal R)
 variable (M : Type*) [AddCommGroup M] [Module R M]
 variable {N : Type*} [AddCommGroup N] [Module R N]
@@ -35,7 +48,7 @@ open TensorProduct
 
 namespace AdicCompletion
 
-private noncomputable
+private
 def ofTensorProductBil : AdicCompletion I R →ₗ[AdicCompletion I R] M →ₗ[R] AdicCompletion I M where
   toFun r := LinearMap.lsmul (AdicCompletion I R) (AdicCompletion I M) r ∘ₗ of I M
   map_add' x y := by
@@ -54,7 +67,6 @@ private lemma ofTensorProductBil_apply_apply (r : AdicCompletion I R) (x : M) :
 
 /-- The natural `AdicCompletion I R`-linear map from `AdicCompletion I R ⊗[R] M` to
 the adic completion of `M`. -/
-noncomputable
 def ofTensorProduct : AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M :=
   TensorProduct.AlgebraTensorModule.lift (ofTensorProductBil I M)
 
@@ -94,7 +106,7 @@ private lemma ofTensorProduct_eq :
   simp
 
 /- If `M = R^ι` and `ι` is finite, we may construct an inverse to `ofTensorProduct I (ι → R)`. -/
-private noncomputable def ofTensorProductInvOfPiFintype :
+private def ofTensorProductInvOfPiFintype :
     AdicCompletion I (ι → R) ≃ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] (ι → R) :=
   letI f := piEquivOfFintype I (fun _ : ι ↦ R)
   letI g := (TensorProduct.piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm
@@ -114,7 +126,7 @@ private lemma ofTensorProduct_comp_ofTensorProductInvOfPiFintype :
   simp
 
 /-- `ofTensorProduct` as an equiv in the case of `M = R^ι` where `ι` is finite. -/
-noncomputable def ofTensorProductEquivOfPiFintype :
+def ofTensorProductEquivOfPiFintype :
     AdicCompletion I R ⊗[R] (ι → R) ≃ₗ[AdicCompletion I R] AdicCompletion I (ι → R) :=
   LinearEquiv.ofLinear
     (ofTensorProduct I (ι → R))
@@ -131,7 +143,7 @@ end PiFintype
 
 /-- If `M` is a finite `R`-module, then the canonical map
 `AdicCompletion I R ⊗[R] M →ₗ AdicCompletion I M` is surjective. -/
-lemma ofTensorProduct_surjective_of_fg [Module.Finite R M] :
+lemma ofTensorProduct_surjective_of_finite [Module.Finite R M] :
     Function.Surjective (ofTensorProduct I M) := by
   obtain ⟨n, p, hp⟩ := Module.Finite.exists_fin' R M
   let f := ofTensorProduct I M ∘ₗ p.baseChange (AdicCompletion I R)
@@ -146,4 +158,205 @@ lemma ofTensorProduct_surjective_of_fg [Module.Finite R M] :
     · exact (ofTensorProduct_bijective_of_pi_of_fintype I (Fin n)).surjective
   exact Function.Surjective.of_comp hf
 
+section Noetherian
+
+variable {R : Type u} [CommRing R] (I : Ideal R)
+variable (M : Type u) [AddCommGroup M] [Module R M]
+variable [IsNoetherianRing R]
+
+/-!
+
+### Noetherian case
+
+Suppose `R` is Noetherian. Then we show that the canonical map
+`AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I M` is an isomorphism for every
+finite `R`-module `M`.
+
+The strategy is the following: Choose a surjection `f : (ι → R) →ₗ[R] M` and consider the following
+commutative diagram:
+
+ AdicCompletion I R ⊗[R] ker f -→ AdicCompletion I R ⊗[R] (ι → R) -→ AdicCompletion I R ⊗[R] M -→ 0
+               |                             |                                 |                  |
+               ↓                             ↓                                 ↓                  ↓
+    AdicCompletion I (ker f) ------→ AdicCompletion I (ι → R) -------→ AdicCompletion I M ------→ 0
+
+The vertical maps are given by `ofTensorProduct`. By the previous section we know that the second
+vertical map is an isomorphism. Since `R` is Noetherian, `ker f` is finitely-generated, so again
+by the previous section the first vertical map is surjective.
+
+Moreover, both rows are exact by right-exactness of the tensor product and exactness of adic
+completions over Noetherian rings. Hence we conclude by the 5-lemma.
+
+-/
+
+open CategoryTheory
+
+section
+
+variable {ι : Type} [Fintype ι] [DecidableEq ι] (f : (ι → R) →ₗ[R] M) (hf : Function.Surjective f)
+
+/- The first horizontal arrow in the top row. -/
+private
+def lTensorKerIncl : AdicCompletion I R ⊗[R] LinearMap.ker f →ₗ[AdicCompletion I R]
+    AdicCompletion I R ⊗[R] (ι → R) :=
+  AlgebraTensorModule.map LinearMap.id (LinearMap.ker f).subtype
+
+/- The second horizontal arrow in the top row. -/
+private def lTensorf :
+    AdicCompletion I R ⊗[R] (ι → R) →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] M :=
+  AlgebraTensorModule.map LinearMap.id f
+
+private lemma if_exact : Function.Exact (LinearMap.ker f).subtype f := fun x ↦
+  ⟨fun hx ↦ ⟨⟨x, hx⟩, rfl⟩, by rintro ⟨x, rfl⟩; exact x.property⟩
+
+private lemma tens_exact : Function.Exact (lTensorKerIncl I M f) (lTensorf I M f) :=
+  lTensor_exact (AdicCompletion I R) (if_exact M f) hf
+
+private lemma tens_surj : Function.Surjective (lTensorf I M f) :=
+  LinearMap.lTensor_surjective (AdicCompletion I R) hf
+
+private lemma adic_exact : Function.Exact (map I (LinearMap.ker f).subtype) (map I f) :=
+  map_exact (Submodule.injective_subtype _) (if_exact M f) hf
+
+private lemma adic_surj : Function.Surjective (map I f) :=
+  map_surjective I hf
+
+/- Instance to speed up instance inference. -/
+private instance : AddCommGroup (AdicCompletion I R ⊗[R] (LinearMap.ker f)) :=
+  inferInstance
+
+private def firstRow : ComposableArrows (ModuleCat (AdicCompletion I R)) 4 :=
+  ComposableArrows.mk₄
+    (ModuleCat.ofHom <| lTensorKerIncl I M f)
+    (ModuleCat.ofHom <| lTensorf I M f)
+    (ModuleCat.ofHom (0 : AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] PUnit))
+    (ModuleCat.ofHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
+
+private def secondRow : ComposableArrows (ModuleCat (AdicCompletion I R)) 4 :=
+  ComposableArrows.mk₄
+    (ModuleCat.ofHom (map I <| (LinearMap.ker f).subtype))
+    (ModuleCat.ofHom (map I f))
+    (ModuleCat.ofHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
+    (ModuleCat.ofHom (0 : _ →ₗ[AdicCompletion I R] PUnit))
+
+private lemma firstRow_exact : (firstRow I M f).Exact where
+  zero k _ := match k with
+    | 0 => (tens_exact I M f hf).linearMap_comp_eq_zero
+    | 1 => LinearMap.zero_comp _
+    | 2 => LinearMap.zero_comp 0
+  exact k _ := by
+    rw [ShortComplex.moduleCat_exact_iff]
+    match k with
+    | 0 => intro x hx; exact (tens_exact I M f hf x).mp hx
+    | 1 => intro x _; exact (tens_surj I M f hf) x
+    | 2 => intro _ _; exact ⟨0, rfl⟩
+
+private lemma secondRow_exact : (secondRow I M f).Exact where
+  zero k _ := match k with
+    | 0 => (adic_exact I M f hf).linearMap_comp_eq_zero
+    | 1 => LinearMap.zero_comp (map I f)
+    | 2 => LinearMap.zero_comp 0
+  exact k _ := by
+    rw [ShortComplex.moduleCat_exact_iff]
+    match k with
+    | 0 => intro x hx; exact (adic_exact I M f hf x).mp hx
+    | 1 => intro x _; exact (adic_surj I M f hf) x
+    | 2 => intro _ _; exact ⟨0, rfl⟩
+
+/- The compatible vertical maps between the first and the second row. -/
+private def firstRowToSecondRow : firstRow I M f ⟶ secondRow I M f :=
+  ComposableArrows.homMk₄
+    (ModuleCat.ofHom (ofTensorProduct I (LinearMap.ker f)))
+    (ModuleCat.ofHom (ofTensorProduct I (ι → R)))
+    (ModuleCat.ofHom (ofTensorProduct I M))
+    (ModuleCat.ofHom 0)
+    (ModuleCat.ofHom 0)
+    (ofTensorProduct_naturality I <| (LinearMap.ker f).subtype).symm
+    (ofTensorProduct_naturality I f).symm
+    rfl
+    rfl
+
+private lemma ofTensorProduct_iso : IsIso (ModuleCat.ofHom (ofTensorProduct I M)) := by
+  refine Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
+    (firstRow_exact I M f hf) (secondRow_exact I M f hf) (firstRowToSecondRow I M f) ?_ ?_ ?_ ?_
+  · apply ConcreteCategory.epi_of_surjective
+    exact ofTensorProduct_surjective_of_finite I (LinearMap.ker f)
+  · apply (ConcreteCategory.isIso_iff_bijective _).mpr
+    exact ofTensorProduct_bijective_of_pi_of_fintype I ι
+  · show IsIso (ModuleCat.ofHom 0)
+    apply Limits.isIso_of_isTerminal
+      <;> exact Limits.IsZero.isTerminal (ModuleCat.isZero_of_subsingleton _)
+  · apply ConcreteCategory.mono_of_injective
+    intro x y _
+    rfl
+
+private
+lemma ofTensorProduct_bijective_of_map_from_fin : Function.Bijective (ofTensorProduct I M) := by
+  have : IsIso (ModuleCat.ofHom (ofTensorProduct I M)) :=
+    ofTensorProduct_iso I M f hf
+  exact ConcreteCategory.bijective_of_isIso (ModuleCat.ofHom (ofTensorProduct I M))
+
+end
+
+/-- If `R` is a Noetherian ring and `M` is a finite `R`-module, then the natural map
+given by `AdicCompletion.ofTensorProduct` is an isomorphism. -/
+theorem ofTensorProduct_bijective_of_finite_of_isNoetherian [Module.Finite R M] :
+    Function.Bijective (ofTensorProduct I M) := by
+  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
+  exact ofTensorProduct_bijective_of_map_from_fin I M f hf
+
+/-- `ofTensorProduct` packaged as linear equiv if `M` is a finite `R`-module and `R` is
+Noetherian. -/
+def ofTensorProductEquivOfFiniteNoetherian [Module.Finite R M] :
+    AdicCompletion I R ⊗[R] M ≃ₗ[AdicCompletion I R] AdicCompletion I M :=
+  LinearEquiv.ofBijective (ofTensorProduct I M)
+    (ofTensorProduct_bijective_of_finite_of_isNoetherian I M)
+
+@[simp]
+lemma ofTensorProductEquivOfFiniteNoetherian_apply [Module.Finite R M]
+    (x : AdicCompletion I R ⊗[R] M) :
+    ofTensorProductEquivOfFiniteNoetherian I M x = ofTensorProduct I M x :=
+  rfl
+
+@[simp]
+lemma ofTensorProductEquivOfFiniteNoetherian_symm_of [Module.Finite R M] (x : M) :
+    (ofTensorProductEquivOfFiniteNoetherian I M).symm ((of I M) x) = 1 ⊗ₜ x := by
+  have h : (of I M) x = ofTensorProductEquivOfFiniteNoetherian I M (1 ⊗ₜ x) := by
+    simp
+  rw [h, LinearEquiv.symm_apply_apply]
+
+section
+
+variable {M : Type u} [AddCommGroup M] [Module R M]
+variable {N : Type u} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N)
+variable [Module.Finite R M] [Module.Finite R N]
+
+lemma tensor_map_id_left_eq_map :
+    (AlgebraTensorModule.map LinearMap.id f) =
+      (ofTensorProductEquivOfFiniteNoetherian I N).symm.toLinearMap ∘ₗ
+      map I f ∘ₗ
+      (ofTensorProductEquivOfFiniteNoetherian I M).toLinearMap := by
+  erw [ofTensorProduct_naturality I f]
+  ext x
+  simp
+
+variable {f}
+
+lemma tensor_map_id_left_injective_of_injective (hf : Function.Injective f) :
+    Function.Injective (AlgebraTensorModule.map LinearMap.id f :
+        AdicCompletion I R ⊗[R] M →ₗ[AdicCompletion I R] AdicCompletion I R ⊗[R] N) := by
+  rw [tensor_map_id_left_eq_map I f]
+  simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, EmbeddingLike.comp_injective,
+    EquivLike.injective_comp]
+  exact map_injective I hf
+
+end
+
+/-- Adic completion of a Noetherian ring `R` is flat over `R`. -/
+instance flat_of_isNoetherian [IsNoetherianRing R] : Algebra.Flat R (AdicCompletion I R) where
+  out := (Module.Flat.iff_lTensor_injective' R (AdicCompletion I R)).mpr <| fun J ↦
+    tensor_map_id_left_injective_of_injective I (Submodule.injective_subtype J)
+
+end Noetherian
+
 end AdicCompletion