diff --git a/Mathlib.lean b/Mathlib.lean
index 29fab9214c3cc1..4b153c50fa43c0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6923,6 +6923,9 @@ public import Mathlib.RingTheory.Kaehler.Basic
 public import Mathlib.RingTheory.Kaehler.JacobiZariski
 public import Mathlib.RingTheory.Kaehler.Polynomial
 public import Mathlib.RingTheory.Kaehler.TensorProduct
+public import Mathlib.RingTheory.KoszulComplex.Cocomplex
+public import Mathlib.RingTheory.KoszulComplex.Complex
+public import Mathlib.RingTheory.KoszulComplex.Homotopy
 public import Mathlib.RingTheory.KrullDimension.Basic
 public import Mathlib.RingTheory.KrullDimension.Field
 public import Mathlib.RingTheory.KrullDimension.LocalRing
diff --git a/Mathlib/Algebra/Homology/HomologicalComplex.lean b/Mathlib/Algebra/Homology/HomologicalComplex.lean
index 50646b814429df..e716fa54812349 100644
--- a/Mathlib/Algebra/Homology/HomologicalComplex.lean
+++ b/Mathlib/Algebra/Homology/HomologicalComplex.lean
@@ -636,19 +636,15 @@ section Of
 
 variable {V} {α : Type*} [AddRightCancelSemigroup α] [One α] [DecidableEq α]
 
-/-- Auxiliary definition for differentials for `ChainComplex.of`. -/
-def of.d (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (i : α) (j : α) : X i ⟶ X j :=
-  if h : i = j + 1 then eqToHom (by rw [h]) ≫ d j else 0
-
 /-- Construct an `α`-indexed chain complex from a dependently-typed differential.
 -/
-abbrev of (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) ≫ d n = 0) :
+@[implicit_reducible]
+def of (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) ≫ d n = 0) :
     ChainComplex V α :=
   { X := X
-    d := of.d X d
-    shape := fun i j w => by simp [of.d, (Ne.symm w)]
+    d i j := if h : i = j + 1 then eqToHom (by rw [h]) ≫ d j else 0
+    shape := fun i j w => by simp [(Ne.symm w)]
     d_comp_d' := fun i j k hij hjk => by
-      dsimp [of.d] at hij hjk ⊢
       subst hij hjk
       simp only [eqToHom_refl, id_comp, dite_eq_ite, ite_true, sq] }
 
@@ -657,13 +653,16 @@ variable (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) 
 theorem of_X : (of X d sq).X = X :=
   rfl
 
+theorem of_d (j : α) : (of X d sq).d (j + 1) j = d j := by
+  simp [of]
+
 @[simp]
-theorem of_d (j : α) : of.d X d (j + 1) j = d j := by
-  dsimp [of.d]
-  rw [ite_eq_left rfl, Category.id_comp]
+theorem of_d' (j i : α) (h : i = j + 1 := by omega) : (of X d sq).d i j =
+    eqToHom (by rw [h, of_X]) ≫ d j := by
+  simp [of, h]
 
-theorem of_d_ne {i j : α} (h : i ≠ j + 1) : of.d X d i j = 0 := by
-  simp [of.d, dite_eq_right h]
+theorem of_d_ne {i j : α} (h : i ≠ j + 1) : (of X d sq).d i j = 0 := by
+  simp [of, dite_eq_right h]
 
 end Of
 
@@ -747,7 +746,8 @@ lemma mkAux_eq_shortComplex_mk_d_comp_d (n : ℕ) :
     mkAux X₀ X₁ X₂ d₀ d₁ s succ n =
       ShortComplex.mk _ _ ((mk X₀ X₁ X₂ d₀ d₁ s succ).d_comp_d (n + 2) (n + 1) n) := by
   rw [show n + 2 = n + 1 + 1 from rfl]
-  simp [mk, mkAux]
+  simp only [mk, mkAux, of_d]
+  rfl
 
 /-- The isomorphism from `(mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3)` that is given by
 the inductive construction. -/
@@ -769,7 +769,7 @@ lemma mk_d (n : ℕ) :
   set_option backward.isDefEq.respectTransparency false in
     rw [eqToHom_refl, comp_id] at eq
   refine Eq.trans ?_ eq
-  dsimp only [mk, of, of.d]
+  dsimp only [mk, of]
   rw [dite_eq_left (by rfl), eqToHom_refl, id_comp]
   rfl
 
@@ -807,7 +807,7 @@ def mk'XIso (n : ℕ) :
     (mk' X₀ X₁ d₀ succ').X (n + 2) ≅ (succ' ((mk' X₀ X₁ d₀ succ').d (n + 1) n)).1 := by
   obtain _ | n := n
   · apply eqToIso
-    dsimp [mk', mk, of, mkAux, of.d]
+    dsimp [mk', mk, of, mkAux]
     rw [id_comp]
   · exact mkXIso _ _ _ _ _ (succ' d₀).2.2 (fun S => succ' S.f) n
 
diff --git a/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean b/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
index 57359217877e99..6ddcf95be7d52a 100644
--- a/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
+++ b/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
@@ -273,7 +273,8 @@ def inclusionOfMooreComplexMap (X : SimplicialObject A) :
   rw [Fin.sum_univ_succ, Fintype.sum_eq_zero]
   swap
   · intro j
-    rw [NormalizedMooreComplex.objX_add_one, comp_zsmul,
+    simp_rw [NormalizedMooreComplex.objX_add_one]
+    rw [comp_zsmul,
       ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ _ (Finset.mem_univ j)),
       Category.assoc, kernelSubobject_arrow_comp, comp_zero, smul_zero]
   -- finally, we study the remaining term which is induced by X.δ 0
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean b/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
index 135fc034add4ed..81fa54808a7119 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
@@ -69,27 +69,24 @@ def PInftyToNormalizedMooreComplex (X : SimplicialObject A) : K[X] ⟶ N[X] :=
   ChainComplex.ofHom
     (fun n => factorThru _ _ (factors_normalizedMooreComplex_PInfty n)) fun n => by
     rw [← cancel_mono (NormalizedMooreComplex.objX X n).arrow, assoc, assoc, factorThru_arrow,
-      ← inclusionOfMooreComplexMap_f, NormalizedMooreComplex.obj_d, ChainComplex.of_d,
-      ← normalizedMooreComplex_objD, ← (inclusionOfMooreComplexMap X).comm (n + 1) n,
+      ← inclusionOfMooreComplexMap_f, NormalizedMooreComplex.obj_d',
+      ChainComplex.of_d, ← normalizedMooreComplex_objD,
+      ← (inclusionOfMooreComplexMap X).comm (n + 1) n,
       inclusionOfMooreComplexMap_f, factorThru_arrow_assoc, alternatingFaceMapComplex_obj_d,
       ← alternatingFaceMapComplex_obj_d]
     exact PInfty.comm (n + 1) n
 
 set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 theorem PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap (X : SimplicialObject A) :
     PInftyToNormalizedMooreComplex X ≫ inclusionOfMooreComplexMap X = PInfty := by cat_disch
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 @[reassoc (attr := simp)]
 theorem PInftyToNormalizedMooreComplex_naturality {X Y : SimplicialObject A} (f : X ⟶ Y) :
     AlternatingFaceMapComplex.map f ≫ PInftyToNormalizedMooreComplex Y =
       PInftyToNormalizedMooreComplex X ≫ NormalizedMooreComplex.map f := by
   cat_disch
 
-set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 theorem PInfty_comp_PInftyToNormalizedMooreComplex (X : SimplicialObject A) :
     PInfty ≫ PInftyToNormalizedMooreComplex X = PInftyToNormalizedMooreComplex X := by cat_disch
diff --git a/Mathlib/AlgebraicTopology/MooreComplex.lean b/Mathlib/AlgebraicTopology/MooreComplex.lean
index a277f19c694d80..58af172b3e2b5d 100644
--- a/Mathlib/AlgebraicTopology/MooreComplex.lean
+++ b/Mathlib/AlgebraicTopology/MooreComplex.lean
@@ -63,6 +63,7 @@ variable (X : SimplicialObject C)
 
 /-- The normalized Moore complex in degree `n`, as a subobject of `X n`.
 -/
+@[implicit_reducible]
 def objX : ∀ n : ℕ, Subobject (X.obj (op ⦋n⦌))
   | 0 => ⊤
   | n + 1 => Finset.univ.inf fun k : Fin (n + 1) => kernelSubobject (X.δ k.succ)
@@ -114,12 +115,16 @@ theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
 
 /-- The normalized Moore complex functor, on objects.
 -/
-@[simps!]
+@[implicit_reducible, simps!]
 def obj (X : SimplicialObject C) : ChainComplex C ℕ :=
   ChainComplex.of (fun n => (objX X n : C))
     (-- the coercion here picks a representative of the subobject
       objD X) (d_squared X)
 
+lemma obj_d' (X : SimplicialObject C) (i j : ℕ) :
+    (obj X).d i j =
+      (ChainComplex.of (fun n ↦ underlying.obj (objX X n)) (objD X) (d_squared X)).d i j  := rfl
+
 variable {X} {Y : SimplicialObject C} (f : X ⟶ Y)
 
 set_option backward.isDefEq.respectTransparency.types false in
@@ -137,7 +142,7 @@ def map (f : X ⟶ Y) : obj X ⟶ obj Y :=
           ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i (by simp)),
           Category.assoc]
         rw [← SimplicialObject.δ_def, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]))
-    fun n => by cases n <;> dsimp [objD, objX, ChainComplex.of.d] <;> cat_disch
+    fun n => by cases n <;> dsimp [objD, objX] <;> cat_disch
 
 end NormalizedMooreComplex
 
@@ -164,6 +169,6 @@ set_option backward.defeqAttrib.useBackward true in
 -- Not `@[simp]` as `simp` can prove this.
 theorem normalizedMooreComplex_objD (X : SimplicialObject C) (n : ℕ) :
     ((normalizedMooreComplex C).obj X).d (n + 1) n = NormalizedMooreComplex.objD X n := by
-  simp [-objD, -obj_X]
+  simp [normalizedMooreComplex, obj]
 
 end AlgebraicTopology
diff --git a/Mathlib/CategoryTheory/Linear/Basic.lean b/Mathlib/CategoryTheory/Linear/Basic.lean
index 6c51e2c5320a45..756ffa82b8047d 100644
--- a/Mathlib/CategoryTheory/Linear/Basic.lean
+++ b/Mathlib/CategoryTheory/Linear/Basic.lean
@@ -120,7 +120,7 @@ instance fullSubcategory (Z : ObjectProperty C) : Linear.{w, v} R Z.FullSubcateg
 variable (R)
 
 /-- Composition by a fixed left argument as an `R`-linear map. -/
-@[simps]
+@[implicit_reducible, simps]
 def leftComp {X Y : C} (Z : C) (f : X ⟶ Y) : (Y ⟶ Z) →ₗ[R] X ⟶ Z where
   toFun g := f ≫ g
   map_add' := by simp
diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean
index 866833debeef4e..7a3934840f57c3 100644
--- a/Mathlib/Data/Fin/Tuple/Basic.lean
+++ b/Mathlib/Data/Fin/Tuple/Basic.lean
@@ -1100,6 +1100,9 @@ theorem removeNth_removeNth_eq_swap {α : Sort*} (m : Fin (n + 2) → α)
     i.removeNth (j.removeNth m) = (i.predAbove j).removeNth ((j.succAbove i).removeNth m) :=
   heq_iff_eq.mp (removeNth_removeNth_heq_swap m i j)
 
+theorem removeNth_comp {M N : Type*} (f : M → N) (i : ℕ) (v : Fin (i + 1) → M) (x : Fin (i + 1)) :
+    x.removeNth (f ∘ v) = f ∘ x.removeNth v := rfl
+
 end InsertNth
 
 section Find
diff --git a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean
index ecf58e38be6e60..a0ee385ddd0bd1 100644
--- a/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean
+++ b/Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean
@@ -105,8 +105,13 @@ theorem d_eq :
       (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv ≫
         ((barComplex k G).linearYonedaObj k A).d n (n + 1) ≫
           (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.hom := by
-  ext
-  simp [d_hom_apply, map_add, barComplex.d_single (k := k), homEquiv]
+  ext x y
+  -- try to remove `ChainComplex.of_X`, if removing it need erw `barComplex.d_single`
+  -- which needs `(barComplex k G) n = free k G (Fin n → G)`
+  -- the equality works with `with_implicit rfl`, but not `with_reducible_and_instances rfl`
+  -- attempts: setting `ChainComplex.of` instance reducible won't work,
+  -- only setting reducible would help
+  simp [d_hom_apply, homEquiv, Linear.leftComp, ChainComplex.of_X, barComplex.d_single (k := k) n y]
 
 end inhomogeneousCochains
 
diff --git a/Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean b/Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean
index 7f5a69a1b47c91..219573a27d7c7c 100644
--- a/Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean
+++ b/Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean
@@ -145,8 +145,14 @@ theorem d_eq [DecidableEq G] :
       ((barComplex k G).coinvariantsTensorObj A).d (n + 1) n ≫
       (coinvariantsTensorFreeLEquiv A (Fin n → G)).toModuleIso.hom := by
   ext : 3
-  simp [d_single (k := k), TensorProduct.tmul_add, TensorProduct.tmul_sum,
-    barComplex.d_single (k := k)]
+  -- try remove `ChainComplex.of_X`, if removing it needs erw `Coinvariants.map_mk`
+  -- which needs `Representation.free k G (Fin (n + 1) → G) =`
+  -- `ρ (HomologicalComplex.X (barComplex k G) (n + 1))`
+  -- the equality works with `with_implicit rfl`, but not `with_reducible_and_instances rfl`
+  -- attempts: setting `ChainComplex.of` instance reducible won't work,
+  -- only setting reducible would help
+  simp [d_single (k := k), ChainComplex.of_X, barComplex.d_single (k := k), TensorProduct.tmul_add,
+    TensorProduct.tmul_sum]
 
 end inhomogeneousChains
 
@@ -175,10 +181,9 @@ theorem inhomogeneousChains.d_def (n : ℕ) :
     (inhomogeneousChains A).d (n + 1) n = d A n := by
   simp [inhomogeneousChains]
 
-set_option backward.defeqAttrib.useBackward true in
 theorem inhomogeneousChains.d_comp_d :
     d A (n + 1) ≫ d A n = 0 := by
-  simpa [ChainComplex.of.d] using ((inhomogeneousChains A).d_comp_d (n + 2) (n + 1) n)
+  simp [← (inhomogeneousChains A).d_comp_d (n + 1 + 1) (n + 1) n]
 
 /-- Given a `k`-linear `G`-representation `A`, the complex of inhomogeneous chains is isomorphic
 to `(A ⊗[k] P)_G`, where `P` is the bar resolution of `k` as a trivial `G`-representation. -/
diff --git a/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean b/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean
index dbec9594e66168..f41c2bd94e5592 100644
--- a/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean
+++ b/Mathlib/RepresentationTheory/Homological/GroupHomology/Functoriality.lean
@@ -60,9 +60,16 @@ noncomputable def chainsMap :
   f i := ModuleCat.ofHom <| mapRange.linearMap φ.hom.toLinearMap ∘ₗ lmapDomain A k (f ∘ ·)
   comm' i j (hij : _ = _) := by
     subst hij
-    ext
-    simp [Fin.comp_contractNth, map_add, inhomogeneousChains.d, Rep.hom_comm_apply φ]
-    rfl
+    ext g
+    simp only [res_obj_ρ, ModuleCat.ofHom_comp, ChainComplex.of_d',
+      inhomogeneousChains.d, eqToHom_refl, Category.id_comp, Category.assoc, ModuleCat.hom_comp,
+      ConcreteCategory.hom_ofHom, LinearMap.coe_comp, Function.comp_apply, lsingle_apply,
+      lmapDomain_apply, mapDomain_single, coe_lsum, LinearMap.coe_add, LinearMap.coe_sum,
+      LinearMap.coe_smul, Pi.add_apply, map_zero, Finset.sum_apply, Pi.smul_apply,
+      smul_zero, Finset.sum_const_zero, add_zero, sum_single_index, smul_single, map_add, map_sum]
+    simp [mapRange.linearMap_apply _, lmapDomain_apply _, IntertwiningMap.coe_toLinearMap,
+      lsum_apply _, Rep.hom_comm_apply φ, res_obj_ρ, Fin.comp_contractNth,
+      Function.comp_def f (fun i : Fin _ ↦ g i.succ)]
 
 lemma chainsMap_congr {f g : G →* H} {φ : A ⟶ res f B} {ψ : A ⟶ res g B} (hfg : f = g)
     (hφψ : φ.hom.toLinearMap = ψ.hom.toLinearMap) :
@@ -74,11 +81,15 @@ lemma lsingle_comp_chainsMap_f (n : ℕ) (x : Fin n → G) :
     ModuleCat.ofHom (lsingle x) ≫ (chainsMap f φ).f n =
       ModuleCat.ofHom (lsingle (f ∘ x) ∘ₗ φ.hom.toLinearMap) := by
   ext
-  simp [chainsMap_f]
+  simp [chainsMap_f, lmapDomain_apply, res_obj_ρ,
+    IntertwiningMap.coe_toLinearMap, (mapRange.linearMap_apply), (lsingle_apply)]
 
 lemma chainsMap_f_single (n : ℕ) (x : Fin n → G) (a : A) :
     (chainsMap f φ).f n (single x a) = single (f ∘ x) (φ.hom a) := by
-  simp [chainsMap_f]
+  simp only [chainsMap_f, ModuleCat.hom_comp, ConcreteCategory.hom_ofHom, LinearMap.coe_comp,
+    Function.comp_apply, res_obj_ρ]
+  rw [mapRange.linearMap_apply, lmapDomain_apply]
+  simp
 
 @[simp]
 lemma chainsMap_id :
@@ -97,7 +108,9 @@ lemma chainsMap_comp {G H K : Type u} [Group G] [Group H] [Group K]
     (f : G →* H) (g : H →* K) (φ : A ⟶ res f B) (ψ : B ⟶ res g C) :
     chainsMap (g.comp f) (φ ≫ (resFunctor f).map ψ) = chainsMap f φ ≫ chainsMap g ψ := by
   ext
-  simp [chainsMap_f, Function.comp_assoc]
+  simp [chainsMap_f, MonoidHom.coe_comp, Function.comp_assoc, Rep.hom_comp, res_obj_ρ,
+    IntertwiningMap.comp_toLinearMap, resMap_hom_toLinearMap,
+    Category.assoc, (mapRange.linearMap_apply), (lmapDomain_apply)]
 
 lemma chainsMap_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
     chainsMap (MonoidHom.id G) (φ ≫ ψ) =
@@ -106,7 +119,8 @@ lemma chainsMap_id_comp {A B C : Rep k G} (φ : A ⟶ B) (ψ : B ⟶ C) :
 
 @[simp]
 lemma chainsMap_zero : chainsMap f (0 : A ⟶ res f B) = 0 := by
-  ext; simp [chainsMap_f, LinearMap.zero_apply (M₂ := B)]
+  ext
+  simp [chainsMap_f, IntertwiningMap.zero_toLinearMap, lmapDomain_apply, (mapRange.linearMap_apply)]
 
 lemma chainsMap_f_map_mono (hf : Function.Injective f) [Mono φ] (i : ℕ) :
     Mono ((chainsMap f φ).f i) := by
@@ -227,26 +241,31 @@ noncomputable abbrev chainsMap₃ :
 lemma chainsMap_f_0_comp_chainsIso₀ :
     (chainsMap f φ).f 0 ≫ (chainsIso₀ B).hom = (chainsIso₀ A).hom ≫ φ.toModuleCatHom := by
   ext
-  simp [chainsMap_f, Unique.eq_default (α := Fin 0 → G), Unique.eq_default (α := Fin 0 → H),
-    chainsIso₀]
+  simp [Unique.eq_default (α := Fin 0 → G), chainsMap_f, Unique.eq_default (α := Fin 0 → H),
+    chainsIso₀, Category.assoc, lmapDomain_apply, (mapRange.linearMap_apply),
+    IntertwiningMap.coe_toLinearMap, res_obj_ρ, (uniqueLinearEquiv_apply _)]
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma chainsMap_f_1_comp_chainsIso₁ :
     (chainsMap f φ).f 1 ≫ (chainsIso₁ B).hom = (chainsIso₁ A).hom ≫ chainsMap₁ f φ := by
   ext x
-  simp [chainsMap_f, chainsIso₁]
+  simp [chainsMap_f, chainsIso₁, (domLCongr_apply), (mapRange.linearMap_apply), Category.assoc,
+    lmapDomain_apply, mapDomain_single, res_obj_ρ, domCongr_apply, equivMapDomain_single,
+    IntertwiningMap.coe_toLinearMap, mapRange_single]
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma chainsMap_f_2_comp_chainsIso₂ :
     (chainsMap f φ).f 2 ≫ (chainsIso₂ B).hom = (chainsIso₂ A).hom ≫ chainsMap₂ f φ := by
   ext
-  simp [chainsMap_f, chainsIso₂]
+  simp [chainsMap_f, (domLCongr_apply), (mapRange.linearMap_apply), chainsIso₂,
+    lmapDomain_apply, mapDomain_single, res_obj_ρ, domCongr_apply, IntertwiningMap.coe_toLinearMap]
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma chainsMap_f_3_comp_chainsIso₃ :
     (chainsMap f φ).f 3 ≫ (chainsIso₃ B).hom = (chainsIso₃ A).hom ≫ chainsMap₃ f φ := by
   ext
-  simp [chainsMap_f, chainsIso₃, ← Fin.comp_tail]
+  simp [chainsMap_f, chainsIso₃, (domLCongr_apply), (mapRange.linearMap_apply), ← Fin.comp_tail,
+    Category.assoc, lmapDomain_apply, IntertwiningMap.coe_toLinearMap, mapRange_single]
 
 open ShortComplex
 
diff --git a/Mathlib/RepresentationTheory/Homological/GroupHomology/LongExactSequence.lean b/Mathlib/RepresentationTheory/Homological/GroupHomology/LongExactSequence.lean
index d10cf6d45bdfa1..53398209f789df 100644
--- a/Mathlib/RepresentationTheory/Homological/GroupHomology/LongExactSequence.lean
+++ b/Mathlib/RepresentationTheory/Homological/GroupHomology/LongExactSequence.lean
@@ -48,9 +48,11 @@ lemma map_chainsFunctor_shortExact :
     exact := by
       have : LinearMap.range X.f.hom.toLinearMap = LinearMap.ker X.g.hom.toLinearMap :=
         (hX.exact.map (forget₂ (Rep k G) (ModuleCat k))).moduleCat_range_eq_ker
-      simp [moduleCat_exact_iff_range_eq_ker, ker_mapRange,
-        range_mapRange_linearMap X.f.hom.toLinearMap (LinearMap.ker_eq_bot.2 <|
-        (Rep.mono_iff_injective X.f).1 hX.mono_f), this]
+      simp [moduleCat_exact_iff_range_eq_ker, map_X₂, chainsFunctor_obj,
+        chainsMap_id_f_hom_eq_mapRange,
+        range_mapRange_linearMap X.f.hom.toLinearMap
+            (LinearMap.ker_eq_bot.2 <| (Rep.mono_iff_injective X.f).1 hX.mono_f),
+        this, (ker_mapRange)]
     mono_f := chainsMap_id_f_map_mono X.f i
     epi_g := letI := hX.epi_g; chainsMap_id_f_map_epi X.g i }
 
@@ -144,7 +146,10 @@ theorem δ₀_apply
     ← cyclesMk₀_eq X.X₁, ← cyclesMk₁_eq X.X₃]
   using! δ_apply hX (i := 1) (j := 0) rfl ((chainsIso₁ X.X₃).inv z.1) (by
     rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]; simp)
-    ((chainsIso₁ X.X₂).inv y) (Finsupp.ext fun _ => by simp [chainsIso₁, ← hy])
+    ((chainsIso₁ X.X₂).inv y) (Finsupp.ext fun _ => by
+      simp [chainsMap_id_f_hom_eq_mapRange, chainsIso₁, domLCongr_symm, domLCongr_apply, ← hy,
+        Representation.IntertwiningMap.coe_toLinearMap, equivMapDomain_apply,
+        Equiv.funUnique_apply, (mapRange.linearMap_apply)])
     ((chainsIso₀ X.X₁).inv x) (Finsupp.ext fun _ => by
       conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₁₀_comp_inv]
       simp [chainsIso₀, ← hx])
@@ -171,7 +176,10 @@ theorem δ₁_apply
     ← cyclesMk₂_eq X.X₃, ← cyclesMk₁_eq X.X₁]
   using! δ_apply hX (i := 2) (j := 1) rfl ((chainsIso₂ X.X₃).inv z.1) (by
     rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]; simp)
-    ((chainsIso₂ X.X₂).inv y) (Finsupp.ext fun _ => by simp [chainsIso₂, ← hy])
+    ((chainsIso₂ X.X₂).inv y) (Finsupp.ext fun _ => by
+      simp [chainsMap_id_f_hom_eq_mapRange, chainsIso₂, domLCongr_symm, domLCongr_apply, ← hy,
+        Representation.IntertwiningMap.coe_toLinearMap, equivMapDomain_apply,
+        mapRange_apply, (mapRange.linearMap_apply)])
     ((chainsIso₁ X.X₁).inv x) (Finsupp.ext fun _ => by
     conv_rhs => rw [← LinearMap.comp_apply, ← ModuleCat.hom_comp, eq_d₂₁_comp_inv]
     simp [← hx, chainsIso₁])
diff --git a/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean b/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean
index 6c7ff337eb8bd6..2aca806fd81412 100644
--- a/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean
+++ b/Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean
@@ -231,8 +231,9 @@ where the vertical arrows are `chainsIso₁` and `chainsIso₀` respectively.
 theorem comp_d₁₀_eq :
     (chainsIso₁ A).hom ≫ d₁₀ A = (inhomogeneousChains A).d 1 0 ≫ (chainsIso₀ A).hom :=
   ModuleCat.hom_ext <| lhom_ext fun _ _ => by
-    simp [chainsIso₀, chainsIso₁, d₁₀_single (G := G), ChainComplex.of.d,
-      Unique.eq_default (α := Fin 0 → G), sub_eq_add_neg, inhomogeneousChains.d_single (G := G)]
+    simp [chainsIso₁, domLCongr_apply, domCongr_apply, d₁₀_single (G := G), sub_eq_add_neg,
+      chainsIso₀, inhomogeneousChains.d_single (G := G), Unique.eq_default (α := Fin 0 → G),
+      uniqueLinearEquiv_apply _, single_eq_same]
 
 -- @[reassoc (attr := simp), elementwise (attr := simp)]
 @[reassoc, elementwise]
@@ -256,9 +257,9 @@ where the vertical arrows are `chainsIso₂` and `chainsIso₁` respectively.
 theorem comp_d₂₁_eq :
     (chainsIso₂ A).hom ≫ d₂₁ A = (inhomogeneousChains A).d 2 1 ≫ (chainsIso₁ A).hom :=
   ModuleCat.hom_ext <| lhom_ext fun _ _ => by
-    simp [chainsIso₁, add_assoc, chainsIso₂, d₂₁_single (G := G),
-      -Finsupp.domLCongr_apply, domLCongr_single, sub_eq_add_neg, ChainComplex.of.d,
-      Fin.contractNth, inhomogeneousChains.d_single (G := G)]
+    simp [chainsIso₂, (domLCongr_single), d₂₁_single (G := G), sub_eq_add_neg,
+      add_assoc, chainsIso₁, inhomogeneousChains.d_single (G := G),
+      Fin.contractNth_apply_of_lt, Fin.contractNth_apply_of_eq]
 
 @[reassoc, elementwise]
 theorem eq_d₂₁_comp_inv :
@@ -281,11 +282,12 @@ where the vertical arrows are `chainsIso₃` and `chainsIso₂` respectively.
 theorem comp_d₃₂_eq :
     (chainsIso₃ A).hom ≫ d₃₂ A = (inhomogeneousChains A).d 3 2 ≫ (chainsIso₂ A).hom :=
   ModuleCat.hom_ext <| lhom_ext fun _ _ => by
-    simp [chainsIso₂, ChainComplex.of.d, pow_succ, chainsIso₃,
-      -domLCongr_apply, domLCongr_single, d₃₂, Fin.sum_univ_three,
-      Fin.contractNth, Fin.tail_def, sub_eq_add_neg, add_assoc,
+    simp [chainsIso₂, (domLCongr_single), pow_succ, chainsIso₃,
+      -domLCongr_apply, d₃₂, Fin.sum_univ_three,
+      Fin.tail_def, sub_eq_add_neg, add_assoc,
       inhomogeneousChains.d_single (G := G), add_rotate' (-(single (_ * _, _) _)),
-      add_left_comm (single (_, _ * _) _)]
+      add_left_comm (single (_, _ * _) _),
+      Fin.contractNth_apply_of_lt, Fin.contractNth_apply_of_eq, Fin.contractNth_apply_of_gt]
 
 @[reassoc, elementwise]
 theorem eq_d₃₂_comp_inv :
@@ -300,7 +302,7 @@ theorem d₂₁_comp_d₁₀ : d₂₁ A ≫ d₁₀ A = 0 := by
 @[reassoc (attr := simp), elementwise (attr := simp)]
 theorem d₃₂_comp_d₂₁ : d₃₂ A ≫ d₂₁ A = 0 := by
   simp [← cancel_mono (chainsIso₁ A).inv, ← eq_d₂₁_comp_inv, ← eq_d₃₂_comp_inv_assoc,
-    ChainComplex.of.d, inhomogeneousChains.d_comp_d]
+    ChainComplex.of_d', inhomogeneousChains.d_comp_d]
 
 open ShortComplex
 
@@ -695,7 +697,7 @@ lemma shortComplexH0_exact : (shortComplexH0 A).Exact := by
 
 /-- The 0-cycles of the complex of inhomogeneous chains of `A` are isomorphic to `A`. -/
 def cyclesIso₀ : cycles A 0 ≅ ↧A.V :=
-  (inhomogeneousChains A).iCyclesIso _ 0 (by simp) (by simp [ChainComplex.of.d]) ≪≫ chainsIso₀ A
+  (inhomogeneousChains A).iCyclesIso _ 0 (by simp) (by simp) ≪≫ chainsIso₀ A
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 lemma cyclesIso₀_inv_comp_iCycles :
@@ -729,7 +731,7 @@ lemma coinvariantsMk_comp_opcyclesIso₀_inv :
   (CommSq.vert_inv ⟨pOpcycles_comp_opcyclesIso_hom A⟩).w
 
 lemma cyclesMk₀_eq (x : A) :
-    cyclesMk 0 0 (by simp) ((chainsIso₀ A).inv x) (by simp [ChainComplex.of.d]) =
+    cyclesMk 0 0 (by simp) ((chainsIso₀ A).inv x) (by simp) =
     (cyclesIso₀ A).inv x :=
   (ModuleCat.mono_iff_injective <| iCycles A 0).1 inferInstance <| by rw [iCycles_mk]; simp
 
@@ -782,7 +784,7 @@ lemma cyclesMk₁_eq (x : cycles₁ A) :
       (isoCycles₁ A).inv x :=
   (ModuleCat.mono_iff_injective <| iCycles A 1).1 inferInstance <| by
     rw [iCycles_mk]
-    simp only [ChainComplex.of_X, isoCycles₁_inv_comp_iCycles_apply]
+    simp only [isoCycles₁_inv_comp_iCycles_apply]
     rfl
 
 end isoCycles₁
@@ -834,7 +836,7 @@ lemma cyclesMk₂_eq (x : cycles₂ A) :
       simp) = (isoCycles₂ A).inv x :=
   (ModuleCat.mono_iff_injective <| iCycles A 2).1 inferInstance <| by
     rw [iCycles_mk]
-    simp only [ChainComplex.of_X, isoCycles₂_inv_comp_iCycles_apply]
+    simp only [isoCycles₂_inv_comp_iCycles_apply]
     rfl
 
 end isoCycles₂
@@ -892,7 +894,7 @@ variable [A.IsTrivial]
 def H0IsoOfIsTrivial :
     H0 A ≅ ↧A.V :=
   ((inhomogeneousChains A).isoHomologyπ 1 0 (by simp) <| by
-    ext; simp [inhomogeneousChains.d_single (G := G), ChainComplex.of.d,
+    ext; simp [inhomogeneousChains.d_single (G := G),
        Unique.eq_default (α := Fin 0 → G), isTrivial_apply]).symm ≪≫ cyclesIso₀ A
 
 @[simp]
diff --git a/Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean b/Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean
index 6682ccaeddc090..76ffbeb21a33f4 100644
--- a/Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean
+++ b/Mathlib/RepresentationTheory/Homological/TateCohomology/Basic.lean
@@ -83,7 +83,8 @@ lemma Rep.comp_eq_zero : d₁₀ M ≫ M.norm.toModuleCatHom = 0 := by
 
 lemma Rep.d_comp_tateNorm : (inhomogeneousChains M).d 1 0 ≫ M.tateNorm = 0 := by
   simp only [tateNorm, ← Category.assoc, Preadditive.IsIso.comp_right_eq_zero]
-  simp [← comp_d₁₀_eq _]
+  rw [← comp_d₁₀_eq _]
+  simp
 
 /-- The Tate norm connecting complexes of inhomogeneous chains and cochains. -/
 @[simps]
@@ -110,7 +111,10 @@ lemma tateComplex_d_neg (n : ℕ) :
 def tateComplex.map (φ : X ⟶ Y) : tateComplex X ⟶ tateComplex Y := by
   refine CochainComplex.ConnectData.map _ _ (chainsMap (.id G) φ) (cochainsMap (.id G) φ) ?_
   ext
-  simp [Rep.tateNorm_eq, Representation.norm, Rep.hom_comm_apply]
+  simp [tateComplexConnectData_d₀, Rep.tateNorm_eq, Representation.norm,
+    lsingle_comp_chainsMap_f_assoc, MonoidHom.coe_id, CompTriple.comp_eq, Category.assoc,
+    Representation.IntertwiningMap.coe_toLinearMap,  cochainsMap_id_f_hom_eq_compLeft,
+    Rep.hom_comm_apply, (Finsupp.lsum_apply), (Finsupp.lsingle_apply)]
 
 @[simp]
 lemma tateComplex.map_zero : tateComplex.map (0 : X ⟶ Y) = 0 := by cat_disch
diff --git a/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean
new file mode 100644
index 00000000000000..ce7b79f7fe1201
--- /dev/null
+++ b/Mathlib/RingTheory/KoszulComplex/Cocomplex.lean
@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2026 Nailin Guan, Jingting Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nailin Guan, Jingting Wang
+-/
+module
+
+public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower
+public import Mathlib.Algebra.Homology.HomologicalComplex
+public import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
+public import Mathlib.LinearAlgebra.ExteriorPower.Basis
+
+/-!
+
+# Definition of Koszul cocomplex
+
+Given a commutative ring `R`, an `R`-module `M` and an element `x : M`, the
+*Koszul cocomplex* `K(x)` is the cochain complex of `R`-modules whose `n`-th term is the exterior
+power `⋀[R]^n M` and whose differential `⋀[R]^n M → ⋀[R]^(n + 1) M` is `y ↦ y ∧ x`.
+
+The Koszul complex of a sequence `f₁, …, fᵣ` of elements of `R` is the special case
+`M = Rʳ`, `x = (f₁, …, fᵣ)`.
+
+## Main definitions
+
+* `koszulCocomplex.d x n`: the induced linear map `⋀[R]^n M →ₗ[R] ⋀[R]^(n + 1) M`, the Koszul
+  differential.
+* `koszulCocomplex φ`: the Koszul complex of `φ`, as a `ChainComplex (ModuleCat R) ℕ`.
+* `koszulCocomplex.ofList l`: the Koszul complex of a list `l` of elements of `R`.
+* `koszulCocomplex.map`: the chain map `koszulCocomplex φ ⟶ koszulCocomplex φ'` induced by a
+  linear map `f : M →ₗ[R] N` with `φ' ∘ₗ f = φ`, and `koszulCocomplex.isoOfEquiv`, the
+  isomorphism induced by a linear equivalence.
+
+## Main results
+
+* `koszulCocomplex.map_comp`: `koszulCocomplex.map` is compatible with composition.
+* `koszulCocomplex.isZero_X_of_card_generators_le`: if `M` is generated by `k` elements then
+  `koszulCocomplex φ` vanishes in degrees `> k`; in particular
+  (`koszulCocomplex.isZero_X_ofList_of_length_le`) the Koszul complex of a list of length `r`
+  vanishes in degrees `> r`.
+
+-/
+
+@[expose] public section
+
+universe u v w w'
+
+open CategoryTheory Category MonoidalCategory Limits Module ModuleCat
+
+section GradedAlgebra
+
+variable {ι R A : Type*} [DecidableEq ι] [AddMonoid ι]
+    [CommSemiring R] [Semiring A] [Algebra R A] (𝒜 : ι → Submodule R A) [GradedAlgebra 𝒜]
+    {i j k : ι}
+
+/-- The linear graded multiplication for general index. -/
+def GradedAlgebra.linearGMul (h : k = i + j) : 𝒜 i →ₗ[R] (𝒜 j →ₗ[R] 𝒜 k) :=
+  h ▸ DirectSum.gMulLHom (R := R) (A := fun n ↦ 𝒜 n)
+
+@[simp]
+lemma GradedAlgebra.linearGMul_eq_mul (h : k = i + j) (x : 𝒜 i) (y : 𝒜 j) :
+    (GradedAlgebra.linearGMul 𝒜 h) x y = x.1 * y.1 := by
+  subst h
+  rfl
+
+end GradedAlgebra
+
+section
+
+variable (R : Type u) [CommRing R] (M : Type v) [AddCommGroup M] [Module R M]
+
+/-- The differential of Koszul cocoplex defined as wedging with `x` on the right. -/
+noncomputable abbrev koszulCocomplex.d (x : M) (n : ℕ) :
+    ⋀[R]^n M →ₗ[R] ⋀[R]^(n + 1) M :=
+  GradedAlgebra.linearGMul (fun i : ℕ ↦ ⋀[R]^i M) (add_comm n 1)
+    ((exteriorPower.oneEquiv R M).symm x)
+
+lemma koszulCocomplex.d_apply_ιMulti (x : M) (i : ℕ) (m : Fin i → M) :
+    koszulCocomplex.d R M x i (exteriorPower.ιMulti R i m) =
+      exteriorPower.ιMulti R (i + 1) (Matrix.vecCons x m) := by
+  apply Subtype.ext
+  simp [koszulCocomplex.d, exteriorPower.oneEquiv_symm_apply,
+    GradedAlgebra.linearGMul_eq_mul, exteriorPower.ιMulti_apply_coe,
+    ExteriorAlgebra.ιMulti_succ_apply]
+
+variable {M} in
+/-- The Koszul cocomplex with objects exterior powers and differential `koszulCocomplex.d`. -/
+noncomputable abbrev koszulCocomplex (x : M) : CochainComplex (ModuleCat.{max u v} R) ℕ :=
+  CochainComplex.of (fun n ↦ of R (⋀[R]^n M))
+    (fun n ↦ ofHom (koszulCocomplex.d R M x n))
+    (fun n ↦ by
+      simp only [← ofHom_comp]
+      congr
+      refine LinearMap.ext fun x ↦ Subtype.ext ?_
+      simp [exteriorPower.oneEquiv_symm_apply, LinearMap.coe_comp, Function.comp_apply,
+        GradedAlgebra.linearGMul_eq_mul, exteriorPower.ιMulti_apply_coe,
+        ExteriorAlgebra.ιMulti_succ_apply, ExteriorAlgebra.ιMulti_zero_apply, mul_one, ← mul_assoc,
+        CliffordAlgebra.ι_sq_scalar, zero_apply, map_zero, zero_mul])
+
+namespace koszulCocomplex
+
+theorem d_def (x : M) (i : ℕ) :
+    (koszulCocomplex R x).d i (i + 1) = ofHom (koszulCocomplex.d R M x i) := by
+  simp [koszulCocomplex]
+
+variable {R} in
+/-- The abbreviation for the Koszul cocomplex generated by a list of elements in the ring. -/
+noncomputable abbrev ofList (l : List R) :=
+  koszulCocomplex R l.get
+
+instance free [Module.Free R M] (x : M) (i : ℕ) : Module.Free R ((koszulCocomplex R x).X i) :=
+  inferInstanceAs <| Module.Free R (⋀[R]^i M)
+
+variable {M} {N : Type v} [AddCommGroup N] [Module R N]
+
+section functoriality
+
+/-- The map between two Koszul complex when give a linear map between module that maps
+the two defining elements. -/
+noncomputable def map (f : M →ₗ[R] N) {x : M} {y : N} (h : f x = y) :
+    koszulCocomplex R x ⟶ koszulCocomplex R y :=
+  CochainComplex.ofHom (fun i ↦ ofHom (exteriorPower.map i f))
+    (fun i ↦ hom_ext <| LinearMap.ext fun z ↦ Subtype.ext
+      (by simp [koszulCocomplex.d, exteriorPower.oneEquiv_symm_apply, h]))
+
+lemma map_f (f : M →ₗ[R] N) (x : M) (y : N) (h : f x = y) (i : ℕ) :
+    (map R f h).f i = ofHom (exteriorPower.map i f) := rfl
+
+@[reassoc]
+lemma map_id_refl (x : M) : koszulCocomplex.map R (M := M) .id (Eq.refl x) = 𝟙 _ := by
+  ext i x
+  simp [map_f]
+
+@[reassoc]
+lemma map_id (x y : M) (h : x = y) : koszulCocomplex.map R (M := M) .id h =
+  eqToHom (congrArg _ h) := by
+  subst h
+  exact map_id_refl R x
+
+@[reassoc]
+lemma map_comp {P : Type v} [AddCommGroup P] [Module R P]
+    (f : M →ₗ[R] N) (g : N →ₗ[R] P) {x : M} {y : N} {z : P} (hxy : f x = y) (hyz : g y = z) :
+    koszulCocomplex.map R f hxy ≫ koszulCocomplex.map R g hyz =
+    koszulCocomplex.map R (g ∘ₗ f) (hxy ▸ hyz : g (f x) = z) := by
+  refine HomologicalComplex.hom_ext _ _ fun i ↦ ?_
+  simp only [HomologicalComplex.comp_f, map_f, exteriorPower.map_comp, ofHom_comp]
+
+/-- The map between two Koszul complex when give an linear equiv between module that maps
+the two defining elements. -/
+noncomputable def isoOfEquiv (f : M ≃ₗ[R] N) {x : M} {y : N} (h : f x = y) :
+    koszulCocomplex R x ≅ koszulCocomplex R y where
+  hom := koszulCocomplex.map R f h
+  inv := koszulCocomplex.map R f.symm (f.injective (by simpa using h.symm))
+  hom_inv_id := by simp [map_comp, map_id_refl]
+  inv_hom_id := by simp [map_comp, map_id_refl]
+
+end functoriality
+
+lemma isZero_X_of_span_eq_top (x : M) {ι : Type*} [Finite ι] (g : ι → M)
+    (hg : Submodule.span R (Set.range g) = ⊤) (i : ℕ) (hi : Nat.card ι < i) :
+    IsZero ((koszulCocomplex R x).X i) :=
+  isZero_of_iff_subsingleton.mpr (exteriorPower.subsingleton_of_span_eq_top_of_card_lt g hg i hi)
+
+lemma isZero_X_ofList_of_length_le (l : List R) (i : ℕ) (hi : l.length < i) :
+    IsZero ((ofList l).X i) :=
+  isZero_X_of_span_eq_top R l.get
+  (Pi.basisFun R (Fin l.length)) (Pi.basisFun R (Fin l.length)).span_eq i
+  (by grind [Nat.card_eq_fintype_card, Fintype.card_fin])
+
+end koszulCocomplex
diff --git a/Mathlib/RingTheory/KoszulComplex/Complex.lean b/Mathlib/RingTheory/KoszulComplex/Complex.lean
new file mode 100644
index 00000000000000..76b49d232a8b22
--- /dev/null
+++ b/Mathlib/RingTheory/KoszulComplex/Complex.lean
@@ -0,0 +1,184 @@
+/-
+Copyright (c) 2026 Nailin Guan, Jingting Wang, Yi Yuan, Yongle Hu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nailin Guan, Jingting Wang, Yi Yuan, Yongle Hu
+-/
+module
+
+public import Mathlib.Algebra.Category.ModuleCat.ExteriorPower
+public import Mathlib.Algebra.Homology.HomologicalComplex
+public import Mathlib.LinearAlgebra.ExteriorPower.Basis
+public import Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
+
+/-!
+# The Koszul complex
+
+Given a commutative ring `R`, an `R`-module `M` and a linear map `φ : M →ₗ[R] R`, the
+*Koszul complex* `K(φ)` is the chain complex of `R`-modules whose `n`-th term is the exterior
+power `⋀[R]^n M` and whose differential `⋀[R]^(n + 1) M → ⋀[R]^n M` is
+
+`x₀ ∧ ⋯ ∧ xₙ ↦ ∑ i, (-1) ^ i • φ (xᵢ) • x₀ ∧ ⋯ ∧ x̂ᵢ ∧ ⋯ ∧ xₙ`.
+
+The Koszul complex of a sequence `f₁, …, fᵣ` of elements of `R` is the special case
+`M = Rʳ`, `φ = (a₁, …, aᵣ) ↦ ∑ aᵢ fᵢ`.
+
+## Main definitions
+
+* `koszulComplex.dAlternating φ n`: the alternating map `M [⋀^Fin (n + 1)]→ₗ[R] ⋀[R]^n M`
+  displayed above, defined as the alternatisation of `x ↦ φ x • ιMulti`.
+* `koszulComplex.d φ n`: the induced linear map `⋀[R]^(n + 1) M →ₗ[R] ⋀[R]^n M`, the Koszul
+  differential.
+* `koszulComplex φ`: the Koszul complex of `φ`, as a `ChainComplex (ModuleCat R) ℕ`.
+* `koszulComplex.ofList l`: the Koszul complex of a list `l` of elements of `R`.
+* `koszulComplex.map`: the chain map `koszulComplex φ ⟶ koszulComplex φ'` induced by a
+  linear map `f : M →ₗ[R] N` with `φ' ∘ₗ f = φ`, and `koszulComplex.isoOfEquiv`, the
+  isomorphism induced by a linear equivalence.
+
+## Main results
+
+* `koszulComplex.d_comp_d`: the Koszul differential squares to zero.
+* `koszulComplex.map_comp`: `koszulComplex.map` is compatible with composition.
+* `koszulComplex.isZero_X_of_card_generators_lt`: if `M` is generated by `k` elements then
+  `koszulComplex φ` vanishes in degrees `> k`; in particular
+  (`koszulComplex.isZero_X_ofList_of_length_lt`) the Koszul complex of a list of length `r`
+  vanishes in degrees `> r`.
+
+## Implementation notes
+
+* The Stacks project defines the Koszul complex as a commutative differential graded algebra,
+  the exterior algebra `⋀ M` with `d` the unique derivation extending `φ`; here we only record
+  the underlying chain complex.
+
+## References
+
+* [The Stacks project, Section 15.29 *The Koszul complex*](https://stacks.math.columbia.edu/tag/0621)
+-/
+
+@[expose] public section
+
+universe u v
+
+open CategoryTheory Category Limits Module ExteriorAlgebra ModuleCat
+
+variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M] (φ : M →ₗ[R] R)
+
+/-- The alternating map for the Koszul differential. -/
+noncomputable def koszulComplex.dAlternating (n : ℕ) :
+    M [⋀^Fin (n + 1)]→ₗ[R] ⋀[R]^n M :=
+  AlternatingMap.alternatizeUncurryFin (φ.smulRight (exteriorPower.ιMulti R n))
+
+lemma koszulComplex.dAlternating_apply (n : ℕ) (x : Fin (n + 1) → M) :
+    koszulComplex.dAlternating φ n x =
+      ∑ i : Fin (n + 1),
+        ((-1 : R) ^ (i : ℕ) * φ (x i)) • exteriorPower.ιMulti R n (i.removeNth x) := by
+  rw [koszulComplex.dAlternating, AlternatingMap.alternatizeUncurryFin_apply]
+  refine Finset.sum_congr rfl ?_
+  intro i _
+  simp [← Int.cast_smul_eq_zsmul R, smul_smul]
+
+/-- The differential for the Koszul complex. -/
+noncomputable def koszulComplex.d (n : ℕ) : ⋀[R]^(n + 1) M →ₗ[R] ⋀[R]^n M :=
+  exteriorPower.alternatingMapLinearEquiv (koszulComplex.dAlternating φ n)
+
+lemma koszulComplex.d_comp_d (n : ℕ) :
+    koszulComplex.d φ n ∘ₗ koszulComplex.d φ (n + 1) = 0 := by
+  let β : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] ⋀[R]^n M :=
+    φ.smulRight (φ.smulRight (exteriorPower.ιMulti R n))
+  have hβ (x y : M) : β x y = β y x := by
+    ext v
+    simp [β, smul_smul, mul_comm]
+  have : (koszulComplex.d φ n).compAlternatingMap (koszulComplex.dAlternating φ (n + 1)) = 0 := by
+    rw [← AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric hβ]
+    ext v
+    simp [koszulComplex.d, koszulComplex.dAlternating, β,
+      AlternatingMap.alternatizeUncurryFin_apply, Finset.smul_sum]
+  simpa [koszulComplex.d, ← exteriorPower.alternatingMapLinearEquiv_comp]
+
+/-- The Koszul complex, with objects exterior powers and differential `koszulComplex.d`. -/
+@[stacks 0622 "only recording chain complex"]
+noncomputable abbrev koszulComplex : ChainComplex (ModuleCat R) ℕ :=
+  ChainComplex.of (fun n ↦ of R (⋀[R]^n M))
+    (fun n ↦ ofHom (koszulComplex.d φ n))
+    (fun n ↦ by rw [← ofHom_comp, koszulComplex.d_comp_d, ofHom_zero])
+
+lemma koszulComplex.d_def (i : ℕ) :
+    (koszulComplex φ).d (i + 1) i = ofHom (koszulComplex.d φ i) := by
+  simp [koszulComplex]
+
+namespace koszulComplex
+
+variable {N : Type v} [AddCommGroup N] [Module R N]
+
+/-- The Koszul complex generated by a list of elements in the ring. -/
+@[stacks 0623]
+noncomputable def ofList (l : List R) : ChainComplex (ModuleCat R) ℕ :=
+    koszulComplex (Fintype.linearCombination R l.get)
+
+section functoriality
+
+lemma map_dAlternating_apply (f : M →ₗ[R] N) (φ' : N →ₗ[R] R) (h : φ' ∘ₗ f = φ)
+    (i : ℕ) (v : Fin (i + 1) → M) :
+    ((koszulComplex.dAlternating φ' i) (f ∘ v) : ⋀[R]^i N) =
+      exteriorPower.map i f ((koszulComplex.dAlternating φ i) v) := by
+  subst h
+  simp [dAlternating_apply, exteriorPower.map_apply_ιMulti, Fin.removeNth_comp]
+
+lemma map_d_comm (f : M →ₗ[R] N) (φ' : N →ₗ[R] R) (h : φ' ∘ₗ f = φ) (i : ℕ) :
+    ofHom (exteriorPower.map (i + 1) f) ≫ ofHom (koszulComplex.d φ' i) =
+      ofHom (koszulComplex.d φ i) ≫ ofHom (exteriorPower.map i f) := by
+  ext v
+  simp [koszulComplex.d, map_dAlternating_apply (φ := φ) (f := f) (φ' := φ') h]
+
+/-- The chain map `koszulComplex φ ⟶ koszulComplex φ'` induced by a linear map `f : M →ₗ[R] N`
+with `φ' ∘ₗ f = φ`. -/
+@[stacks 0624 "only recording chain complex map"]
+noncomputable def map (f : M →ₗ[R] N) (φ' : N →ₗ[R] R) (h : φ' ∘ₗ f = φ) :
+    koszulComplex φ ⟶ koszulComplex φ' :=
+  ChainComplex.ofHom (fun i ↦ ofHom (exteriorPower.map i f))
+    (fun i ↦ by simpa [d_def] using map_d_comm φ f φ' h i)
+
+lemma map_f (f : M →ₗ[R] N) (φ' : N →ₗ[R] R) (h : φ' ∘ₗ f = φ) (i : ℕ) :
+    (map φ f φ' h).f i = ofHom (exteriorPower.map i f) := rfl
+
+variable {L : Type v} [AddCommGroup L] [Module R L]
+
+@[reassoc]
+lemma map_id : map φ LinearMap.id φ (LinearMap.comp_id φ) = 𝟙 _ := by
+  ext i x
+  simp [map_f, exteriorPower.map_id, ChainComplex.of_X]
+
+@[reassoc]
+lemma map_comp (f : M →ₗ[R] N) (φ' : N →ₗ[R] R) (g : N →ₗ[R] L) (φ'' : L →ₗ[R] R)
+    (h : φ' ∘ₗ f = φ) (h' : φ'' ∘ₗ g = φ') (h'' : φ'' ∘ₗ g ∘ₗ f = φ) :
+    koszulComplex.map φ f φ' h ≫ koszulComplex.map φ' g φ'' h' =
+      koszulComplex.map φ (g ∘ₗ f) φ'' h'' := by
+  ext i x
+  simp [map_f, exteriorPower.map_comp]
+
+/-- The isomorphism between two Koszul complexes induced by an isomorphism between modules which
+commutes with the two defining linear maps. -/
+@[stacks 0625 "general version for linear equivalences"]
+noncomputable def isoOfEquiv (f : M ≃ₗ[R] N) (φ' : N →ₗ[R] R) (h : φ' ∘ₗ f = φ) :
+    koszulComplex φ ≅ koszulComplex φ' where
+  hom := koszulComplex.map φ f φ' h
+  inv := koszulComplex.map φ' f.symm φ ((f.comp_toLinearMap_symm_eq φ' φ).mpr h.symm)
+  hom_inv_id := by
+    ext i x
+    simp [-LinearMap.coe_comp, map_f, ← exteriorPower.map_comp _]
+  inv_hom_id := by
+    ext i x
+    simp [-LinearMap.coe_comp, map_f, ← exteriorPower.map_comp _]
+
+end functoriality
+
+lemma isZero_X_of_span_eq_top {ι : Type*} [Finite ι] (g : ι → M)
+    (hg : Submodule.span R (Set.range g) = ⊤) (i : ℕ) (hi : Nat.card ι < i) :
+    IsZero ((koszulComplex φ).X i) :=
+  isZero_of_iff_subsingleton.mpr (exteriorPower.subsingleton_of_span_eq_top_of_card_lt g hg i hi)
+
+lemma isZero_X_ofList_of_length_lt (l : List R) (i : ℕ) (hi : l.length < i) :
+    IsZero ((ofList l).X i) := isZero_X_of_span_eq_top _
+  (Pi.basisFun R (Fin l.length)) (Pi.basisFun R (Fin l.length)).span_eq i
+  (by grind [Nat.card_eq_fintype_card, Fintype.card_fin])
+
+end koszulComplex
diff --git a/Mathlib/RingTheory/KoszulComplex/Homotopy.lean b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean
new file mode 100644
index 00000000000000..75750afcfd26c3
--- /dev/null
+++ b/Mathlib/RingTheory/KoszulComplex/Homotopy.lean
@@ -0,0 +1,209 @@
+/-
+Copyright (c) 2026 Nailin Guan, Jingting Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nailin Guan, Jingting Wang
+-/
+module
+
+public import Mathlib.Algebra.Category.ModuleCat.Abelian
+public import Mathlib.Algebra.Homology.Homotopy
+public import Mathlib.Algebra.Homology.ShortComplex.Linear
+public import Mathlib.RingTheory.KoszulComplex.Cocomplex
+public import Mathlib.RingTheory.KoszulComplex.Complex
+public import Mathlib.RingTheory.Regular.RegularSequence
+
+/-!
+# Homotopy on Koszul complex
+-/
+
+@[expose] public section
+
+universe u v
+
+open ExteriorAlgebra CategoryTheory
+
+variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
+  (φ : M →ₗ[R] R) (x : M)
+
+section homotopy
+
+lemma contraction_wedge_zero_degree
+    (x : M) (φ : M →ₗ[R] R) :
+    (koszulComplex.d φ 0).comp (koszulCocomplex.d R M x 0) = (φ x) • LinearMap.id := by
+  -- Degree `0` has only the empty wedge generator, so the scalar term is the whole answer.
+  apply exteriorPower.linearMap_ext
+  ext v
+  have hwedge : koszulCocomplex.d R M x 0 ((exteriorPower.ιMulti R 0) v) =
+      exteriorPower.ιMulti R 1 (Matrix.vecCons x v) := by
+    apply Subtype.ext
+    simp [koszulCocomplex.d, exteriorPower.oneEquiv_symm_apply, GradedAlgebra.linearGMul_eq_mul,
+      exteriorPower.ιMulti_apply_coe, ExteriorAlgebra.ιMulti_succ_apply]
+  simp only [LinearMap.smul_compAlternatingMap, AlternatingMap.smul_apply,
+    LinearMap.compAlternatingMap_apply, LinearMap.id_apply, LinearMap.comp_apply, koszulComplex.d]
+  rw  [hwedge, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti]
+  simp [koszulComplex.dAlternating, AlternatingMap.alternatizeUncurryFin_apply]
+
+@[stacks 0626]
+lemma contraction_wedge_cartan_formula (x : M) (φ : M →ₗ[R] R) (n : ℕ) :
+    (koszulCocomplex.d R M x n).comp (koszulComplex.d φ n) +
+      (koszulComplex.d φ (n + 1)).comp (koszulCocomplex.d R M x (n + 1)) =
+        (φ x) • LinearMap.id := by
+  -- Compare the two operators on the standard exterior-power generators `ιMulti`.
+  apply exteriorPower.linearMap_ext
+  ext v
+  -- After expanding contraction on `x ∧ v`, the terms cancel pairwise except for `φ x`.
+  simp only [LinearMap.add_compAlternatingMap, LinearMap.smul_compAlternatingMap,
+    AlternatingMap.add_apply, AlternatingMap.smul_apply, LinearMap.compAlternatingMap_apply,
+    LinearMap.id_apply, koszulComplex.d]
+  have hwedge : koszulCocomplex.d R M x (n + 1) ((exteriorPower.ιMulti R (n + 1)) v) =
+      exteriorPower.ιMulti R (n + 2) (Matrix.vecCons x v) := by
+    apply Subtype.ext
+    simp [koszulCocomplex.d, exteriorPower.oneEquiv_symm_apply, GradedAlgebra.linearGMul_eq_mul,
+      exteriorPower.ιMulti_apply_coe, ExteriorAlgebra.ιMulti_succ_apply]
+  rw [LinearMap.comp_apply, LinearMap.comp_apply,
+    exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, hwedge,
+    exteriorPower.alternatingMapLinearEquiv_apply_ιMulti]
+  rw [koszulComplex.dAlternating, AlternatingMap.alternatizeUncurryFin_apply,
+      koszulComplex.dAlternating, AlternatingMap.alternatizeUncurryFin_apply, Fin.sum_univ_succ,
+      Fin.sum_univ_succ]
+  -- Rewrite the removed tuples so both Leibniz expansions are indexed the same way.
+  have hremove (i : Fin (n + 1)) :
+      i.succ.removeNth (Matrix.vecCons x v) = Matrix.vecCons x (i.removeNth v) := by
+    ext j
+    exact Fin.cases (by simp [Fin.removeNth]) (fun j ↦ (by simp [Fin.removeNth])) j
+  simp only [koszulCocomplex.d, exteriorPower.oneEquiv_symm_apply, Int.reduceNeg,
+    Fin.coe_ofNat_eq_mod, Nat.zero_mod, pow_zero, LinearMap.coe_smulRight, Fin.removeNth_zero,
+    AlternatingMap.smul_apply, one_smul, Fin.val_succ, pow_succ, mul_comm, neg_mul, one_mul,
+    neg_smul, Finset.sum_neg_distrib, map_add, map_smul, map_neg, map_sum,
+    LinearMap.map_smul_of_tower, Matrix.cons_val_zero, Fin.tail_vecCons, Matrix.cons_val_succ,
+    hremove, Submodule.coe_add, SetLike.val_smul, GradedAlgebra.linearGMul_eq_mul,
+    exteriorPower.ιMulti_apply_coe, ιMulti_succ_apply, ιMulti_zero_apply, mul_one,
+    NegMemClass.coe_neg, AddSubmonoidClass.coe_finsetSum, SetLike.val_smul_of_tower, zsmul_eq_mul,
+    Int.cast_pow, Int.cast_neg, Int.cast_one, Algebra.mul_smul_comm, Matrix.tail_cons,
+    Fin.sum_univ_succ, neg_add_rev, neg_neg]
+  abel
+
+lemma koszulCocomplex.scalar_homotopy_comm_zero (x : M) (φ : M →ₗ[R] R) :
+    (((φ x) • (𝟙 (koszulCocomplex R x))).f 0) =
+      dNext 0 (fun i j =>
+        if h : j + 1 = i then h ▸ ModuleCat.ofHom (koszulComplex.d φ j) else 0) +
+          prevD 0 (fun i j =>
+            if h : j + 1 = i then h ▸ ModuleCat.ofHom (koszulComplex.d φ j) else 0) := by
+  -- In degree `0`, only the `δ_φ d_x` term survives.
+  rw [Homotopy.dNext_cochainComplex, Homotopy.prevD_zero_cochainComplex]
+  simp only [↓reduceDIte, HomologicalComplex.smul_f_apply, HomologicalComplex.id_f, Nat.reduceAdd,
+    zero_add, add_zero]
+  exact congrArg ModuleCat.ofHom (contraction_wedge_zero_degree x φ).symm
+
+lemma koszulComplex.scalar_homotopy_comm_zero (x : M) (φ : M →ₗ[R] R) :
+    (((φ x) • 𝟙 (koszulComplex φ)).f 0) =
+      dNext 0 (fun i j =>
+        if h : i + 1 = j then h ▸ ModuleCat.ofHom (koszulCocomplex.d R M x i) else 0) +
+          prevD 0 (fun i j =>
+            if h : i + 1 = j then h ▸ ModuleCat.ofHom (koszulCocomplex.d R M x i) else 0) := by
+  -- In degree `0`, only the `d_x δ_φ` term survives.
+  rw [Homotopy.dNext_zero_chainComplex, Homotopy.prevD_chainComplex]
+  simp only [↓reduceDIte, zero_add, HomologicalComplex.smul_f_apply,
+    HomologicalComplex.id_f, Nat.reduceAdd]
+  exact congrArg ModuleCat.ofHom (contraction_wedge_zero_degree x φ).symm
+
+lemma koszulCocomplex.scalar_homotopy_comm (x : M) (φ : M →ₗ[R] R) (i : ℕ) :
+    (((φ x) • 𝟙 (koszulCocomplex R x)).f (i + 1)) =
+      dNext (i + 1) (fun i j =>
+        if h : j + 1 = i then h ▸ ModuleCat.ofHom (koszulComplex.d φ j) else 0) +
+          prevD (i + 1) (fun i j =>
+            if h : j + 1 = i then h ▸ ModuleCat.ofHom (koszulComplex.d φ j) else 0) := by
+  -- In positive degrees, the homotopy relation is exactly the Cartan formula.
+  rw [Homotopy.dNext_cochainComplex, Homotopy.prevD_succ_cochainComplex]
+  simp only [HomologicalComplex.smul_f_apply, HomologicalComplex.id_f, CochainComplex.of_d,
+    ↓reduceDIte]
+  let A := (koszulCocomplex.d R M x i).comp (koszulComplex.d φ i)
+  let B := (koszulComplex.d φ (i + 1)).comp (koszulCocomplex.d R M x (i + 1))
+  have hcartan : (φ x) • LinearMap.id = B + A := by
+    simpa [A, B, ← add_comm A B] using (contraction_wedge_cartan_formula x φ i).symm
+  exact congrArg ModuleCat.ofHom hcartan
+
+
+lemma koszulComplex.scalar_homotopy_comm (x : M) (φ : M →ₗ[R] R) (i : ℕ) :
+    (((φ x) • 𝟙 (koszulComplex φ)).f (i + 1)) =
+      dNext (i + 1) (fun i j =>
+        if h : i + 1 = j then h ▸ ModuleCat.ofHom (koszulCocomplex.d R M x i) else 0) +
+          prevD (i + 1) (fun i j =>
+            if h : i + 1 = j then h ▸ ModuleCat.ofHom (koszulCocomplex.d R M x i) else 0) := by
+  -- In positive degrees, the homotopy relation is exactly the Cartan formula.
+  rw [Homotopy.dNext_succ_chainComplex, Homotopy.prevD_chainComplex]
+  simp only [HomologicalComplex.smul_f_apply, HomologicalComplex.id_f, ChainComplex.of_d,
+    ↓reduceDIte]
+  exact congrArg ModuleCat.ofHom (contraction_wedge_cartan_formula x φ i).symm
+
+/-- Given `φ : M →ₗ[R] R`, `φ x` times identity is homotopic to zero for Koszul cocomplex
+defined by `x`. -/
+noncomputable def koszulCocomplex.homotopySMulIdZero (x : M) (φ : M →ₗ[R] R) :
+    Homotopy ((φ x) • 𝟙 (koszulCocomplex R x))
+      (0 : koszulCocomplex R x ⟶ koszulCocomplex R x) where
+  hom i j := if h : j + 1 = i then h ▸ ModuleCat.ofHom (koszulComplex.d φ j) else 0
+  zero i j hij := by
+    simp only [ComplexShape.up_Rel] at hij
+    simp [hij]
+  comm i := by
+    cases i with
+    | zero => simpa using! scalar_homotopy_comm_zero x φ
+    | succ i => simpa using! scalar_homotopy_comm x φ i
+
+/-- Given `x : M`, `φ x` times identity is homotopic to zero for Koszul complex defined by `φ`. -/
+noncomputable def koszulComplex.homotopySMulIdZero (x : M) (φ : M →ₗ[R] R) :
+    Homotopy ((φ x) • 𝟙 (koszulComplex φ)) (0 : koszulComplex φ ⟶ koszulComplex φ) where
+  hom := fun i j =>
+    if h : i + 1 = j then h ▸ ModuleCat.ofHom (koszulCocomplex.d R M x i) else 0
+  zero i j hij := by
+    simp only [ComplexShape.down_Rel] at hij
+    simp [hij]
+  comm i := by
+    cases i with
+    | zero => simpa using! scalar_homotopy_comm_zero x φ
+    | succ i => simpa using! scalar_homotopy_comm x φ i
+
+end homotopy
+
+section homology_annihilator
+
+set_option backward.isDefEq.respectTransparency false in
+lemma koszulComplex.mem_annihilator_homology (i : ℕ) :
+    φ x ∈ Module.annihilator R ((koszulComplex φ).homology i) := by
+  rw [Module.mem_annihilator]
+  intro z
+  have ofht : (HomologicalComplex.homologyMap (φ x • 𝟙 (koszulComplex φ)) i).hom z = 0 := by
+    simp [(homotopySMulIdZero x φ).homologyMap_eq i]
+  have : (ShortComplex.homologyMap (φ x • ((HomologicalComplex.shortComplexFunctor _ _ i).map
+    (𝟙 (koszulComplex φ))))).hom z = φ x • z := by simp
+  exact this.symm.trans ofht
+
+lemma koszulComplex.range_le_annihilator_homology (i : ℕ) :
+    φ.range ≤ Module.annihilator R ((koszulComplex φ).homology i) := by
+  rintro _ ⟨x, rfl⟩
+  exact mem_annihilator_homology φ x i
+
+lemma koszulComplex.ofList_ideal_annihilator_homology (l : List R) (i : ℕ) :
+    Ideal.ofList l ≤ Module.annihilator R ((ofList l).homology i) :=
+  le_of_eq_of_le (by simp) (range_le_annihilator_homology (Fintype.linearCombination R l.get) i)
+
+set_option backward.isDefEq.respectTransparency false in
+lemma koszulCocomplex.mem_annihilator_homology (i : ℕ) :
+    φ x ∈ Module.annihilator R ((koszulCocomplex R x).homology i) := by
+  rw [Module.mem_annihilator]
+  intro z
+  have ofht : (HomologicalComplex.homologyMap (φ x • 𝟙 (koszulCocomplex R x)) i).hom z = 0 := by
+    simp [(homotopySMulIdZero x φ).homologyMap_eq i]
+  have : (ShortComplex.homologyMap (φ x • ((HomologicalComplex.shortComplexFunctor _ _ i).map
+    (𝟙 (koszulCocomplex R x))))).hom z = φ x • z := by simp
+  exact this.symm.trans ofht
+
+lemma koszulCocomplex.ofList_ideal_le_mem_annihilator_homology (l : List R) (i : ℕ) :
+    Ideal.ofList l ≤ Module.annihilator R ((koszulCocomplex.ofList l).homology i) := by
+  intro r hr
+  have hr' : r ∈ Ideal.span (Set.range l.get) := by simpa only [Set.range_list_get l]
+  rcases Ideal.mem_span_range_iff_exists_fun.mp hr' with ⟨c, hc⟩
+  convert mem_annihilator_homology (Fintype.linearCombination R c) l.get i
+  simp [← hc, Fintype.linearCombination_apply, mul_comm (c _)]
+
+end homology_annihilator