perf(Abelian.InjectiveResolution): refactor CochainComplex.mkAux (#…

…11349)

Similar to the changes for `ChainComplex.mkAux` we remove the ad-hoc `MkStruct` and replace with it `ShortComplex`.

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -988,37 +988,15 @@ end OfHom
 
 section Mk
 
--- porting note (#10927): removed @[nolint has_nonempty_instance]
-/-- Auxiliary structure for setting up the recursion in `mk`.
-This is purely an implementation detail: for some reason just using the dependent 6-tuple directly
-results in `mkAux` taking much longer (well over the `-T100000` limit) to elaborate.
--/
-structure MkStruct where
-  (X₀ X₁ X₂ : V)
-  d₀ : X₀ ⟶ X₁
-  d₁ : X₁ ⟶ X₂
-  s : d₀ ≫ d₁ = 0
-#align cochain_complex.mk_struct CochainComplex.MkStruct
-
 variable {V}
 
-/-- Flatten to a tuple. -/
-def MkStruct.flat (t : MkStruct V) :
-    Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0 :=
-  ⟨t.X₀, t.X₁, t.X₂, t.d₀, t.d₁, t.s⟩
-#align cochain_complex.mk_struct.flat CochainComplex.MkStruct.flat
-
 variable (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : d₀ ≫ d₁ = 0)
-  (succ :
-    ∀ t : Σ' (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂), d₀ ≫ d₁ = 0,
-      Σ' (X₃ : V) (d₂ : t.2.2.1 ⟶ X₃), t.2.2.2.2.1 ≫ d₂ = 0)
+  (succ : ∀ (S : ShortComplex V), Σ' (X₄ : V) (d₂ : S.X₃ ⟶ X₄), S.g ≫ d₂ = 0)
 
 /-- Auxiliary definition for `mk`. -/
-def mkAux : ℕ → MkStruct V
-  | 0 => ⟨X₀, X₁, X₂, d₀, d₁, s⟩
-  | n + 1 =>
-    let p := mkAux n
-    ⟨p.X₁, p.X₂, (succ p.flat).1, p.d₁, (succ p.flat).2.1, (succ p.flat).2.2⟩
+def mkAux : ℕ → ShortComplex V
+  | 0 => ShortComplex.mk _ _ s
+  | n + 1 => ShortComplex.mk _ _ (succ (mkAux n)).2.2
 #align cochain_complex.mk_aux CochainComplex.mkAux
 
 /-- An inductive constructor for `ℕ`-indexed cochain complexes.
@@ -1030,8 +1008,8 @@ and returns the next object, its differential, and the fact it composes appropri
 See also `mk'`, which only sees the previous differential in the inductive step.
 -/
 def mk : CochainComplex V ℕ :=
-  of (fun n => (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₀) (fun n => (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).d₀)
-    fun n => (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).s
+  of (fun n => (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₁) (fun n => (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).f)
+    fun n => (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).zero
 #align cochain_complex.mk CochainComplex.mk
 
 @[simp]
@@ -1072,13 +1050,13 @@ then a function which takes a differential,
 and returns the next object, its differential, and the fact it composes appropriately to zero.
 -/
 def mk' (X₀ X₁ : V) (d : X₀ ⟶ X₁)
-    (succ' : ∀ t : ΣX₀ X₁ : V, X₀ ⟶ X₁, Σ' (X₂ : V) (d : t.2.1 ⟶ X₂), t.2.2 ≫ d = 0) :
+    -- (succ' : ∀  : ΣX₀ X₁ : V, X₀ ⟶ X₁, Σ' (X₂ : V) (d : t.2.1 ⟶ X₂), t.2.2 ≫ d = 0) :
+    (succ' : ∀ {X₀ X₁ : V} (f : X₀ ⟶ X₁), Σ' (X₂ : V) (d : X₁ ⟶ X₂), f ≫ d = 0) :
     CochainComplex V ℕ :=
-  mk X₀ X₁ (succ' ⟨X₀, X₁, d⟩).1 d (succ' ⟨X₀, X₁, d⟩).2.1 (succ' ⟨X₀, X₁, d⟩).2.2 fun t =>
-    succ' ⟨t.2.1, t.2.2.1, t.2.2.2.2.1⟩
+  mk _ _ _ _ _ (succ' d).2.2 (fun S => succ' S.g)
 #align cochain_complex.mk' CochainComplex.mk'
 
-variable (succ' : ∀ t : ΣX₀ X₁ : V, X₀ ⟶ X₁, Σ' (X₂ : V) (d : t.2.1 ⟶ X₂), t.2.2 ≫ d = 0)
+variable (succ' : ∀ {X₀ X₁ : V} (f : X₀ ⟶ X₁), Σ' (X₂ : V) (d : X₁ ⟶ X₂), f ≫ d = 0)
 
 @[simp]
 theorem mk'_X_0 : (mk' X₀ X₁ d₀ succ').X 0 = X₀ :=

Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean

@@ -28,7 +28,6 @@ When the underlying category is abelian:
   is injective, we can apply `Injective.d` repeatedly to obtain an injective resolution of `X`.
 -/
 
-
 noncomputable section
 
 open CategoryTheory Category Limits
@@ -313,24 +312,26 @@ variable [Abelian C] [EnoughInjectives C] (Z : C)
 /-- Auxiliary definition for `InjectiveResolution.of`. -/
 def ofCocomplex : CochainComplex C ℕ :=
   CochainComplex.mk' (Injective.under Z) (Injective.syzygies (Injective.ι Z))
-    (Injective.d (Injective.ι Z)) fun ⟨_, _, f⟩ =>
-    ⟨Injective.syzygies f, Injective.d f, by simp⟩
+    (Injective.d (Injective.ι Z)) fun f => ⟨_, Injective.d f, by simp⟩
 set_option linter.uppercaseLean3 false in
 #align category_theory.InjectiveResolution.of_cocomplex CategoryTheory.InjectiveResolution.ofCocomplex
 
 lemma ofCocomplex_d_0_1 :
     (ofCocomplex Z).d 0 1 = d (Injective.ι Z) := by
   simp [ofCocomplex]
 
+--Adaptation note: nightly-2024-03-11. This takes takes forever now
 lemma ofCocomplex_exactAt_succ (n : ℕ) :
     (ofCocomplex Z).ExactAt (n + 1) := by
   rw [HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 1 + 1) (by simp) (by simp)]
-  cases n
-  all_goals
-    dsimp [ofCocomplex, HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor',
-      CochainComplex.mk', CochainComplex.mk]
-    simp only [CochainComplex.of_d]
-    apply exact_f_d
+  dsimp [ofCocomplex, CochainComplex.mk', CochainComplex.mk, HomologicalComplex.sc',
+      HomologicalComplex.shortComplexFunctor']
+  simp only [CochainComplex.of_d]
+  match n with
+  | 0 => apply exact_f_d ((CochainComplex.mkAux _ _ _
+      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ 0).f)
+  | n+1 => apply exact_f_d ((CochainComplex.mkAux _ _ _
+      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ (n+1)).f)
 
 instance (n : ℕ) : Injective ((ofCocomplex Z).X n) := by
   obtain (_ | _ | _ | n) := n <;> apply Injective.injective_under