perf (Homology.ProjectiveResolution): remove MkStruct, re-jigger pr…

…oof, and suppress compilation (#9555)

Currently `CategoryTheory.Abelian.ProjectiveResolution` requires more than double the next largest file in terms of CPU instructions. This reduces the load by replacing ad-hoc `MkStruct` with `ShortComplex` and pushing around the existing proof. Follow-up clean-up should be done.

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin, Scott Morrison
 import Mathlib.Algebra.Homology.ComplexShape
 import Mathlib.CategoryTheory.Subobject.Limits
 import Mathlib.CategoryTheory.GradedObject
+import Mathlib.Algebra.Homology.ShortComplex.Basic
 
 #align_import algebra.homology.homological_complex from "leanprover-community/mathlib"@"88bca0ce5d22ebfd9e73e682e51d60ea13b48347"
 
@@ -732,37 +733,16 @@ end OfHom
 
 section Mk
 
--- porting note: 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 `mk_aux` 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 chain_complex.mk_struct ChainComplex.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 chain_complex.mk_struct.flat ChainComplex.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₂ : X₃ ⟶ t.2.2.1), d₂ ≫ t.2.2.2.2.1 = 0)
+  (succ : ∀ (S : ShortComplex V), Σ' (X₃ : V) (d₂ : X₃ ⟶ S.X₁), d₂ ≫ S.f = 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 chain_complex.mk_aux ChainComplex.mkAux
 
 /-- An inductive constructor for `ℕ`-indexed chain complexes.
@@ -774,8 +754,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 : ChainComplex 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).g)
+    fun n => (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).zero
 #align chain_complex.mk ChainComplex.mk
 
 @[simp]
@@ -816,13 +796,12 @@ 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 : X₂ ⟶ t.2.1), d ≫ t.2.2 = 0) :
+    (succ' : ∀ {X₀ X₁ : V} (f : X₁ ⟶ X₀), Σ' (X₂ : V) (d : X₂ ⟶ X₁), d ≫ f = 0) :
     ChainComplex 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.f)
 #align chain_complex.mk' ChainComplex.mk'
 
-variable (succ' : ∀ t : ΣX₀ X₁ : V, X₁ ⟶ X₀, Σ' (X₂ : V) (d : X₂ ⟶ t.2.1), d ≫ t.2.2 = 0)
+variable (succ' : ∀ {X₀ X₁ : V} (f : X₁ ⟶ X₀), Σ' (X₂ : V) (d : X₂ ⟶ X₁), d ≫ f = 0)
 
 @[simp]
 theorem mk'_X_0 : (mk' X₀ X₁ d₀ succ').X 0 = X₀ :=

Mathlib/CategoryTheory/Abelian/ProjectiveResolution.lean

@@ -5,6 +5,7 @@ Authors: Markus Himmel, Scott Morrison, Jakob von Raumer, Joël Riou
 -/
 import Mathlib.CategoryTheory.Preadditive.ProjectiveResolution
 import Mathlib.Algebra.Homology.HomotopyCategory
+import Mathlib.Tactic.SuppressCompilation
 
 /-!
 # Abelian categories with enough projectives have projective resolutions
@@ -26,6 +27,7 @@ When the underlying category is abelian:
   is projective, we can apply `Projective.d` repeatedly to obtain a projective resolution of `X`.
 -/
 
+suppress_compilation
 
 noncomputable section
 
@@ -296,8 +298,7 @@ variable (Z : C)
 /-- Auxiliary definition for `ProjectiveResolution.of`. -/
 def ofComplex : ChainComplex C ℕ :=
   ChainComplex.mk' (Projective.over Z) (Projective.syzygies (Projective.π Z))
-    (Projective.d (Projective.π Z)) fun ⟨_, _, f⟩ =>
-    ⟨Projective.syzygies f, Projective.d f, by simp⟩
+    (Projective.d (Projective.π Z)) (fun f => ⟨_, Projective.d f, by simp⟩)
 #align category_theory.ProjectiveResolution.of_complex CategoryTheory.ProjectiveResolution.ofComplex
 
 lemma ofComplex_d_1_0 :
@@ -307,12 +308,17 @@ lemma ofComplex_d_1_0 :
 lemma ofComplex_exactAt_succ (n : ℕ) :
     (ofComplex Z).ExactAt (n + 1) := by
   rw [HomologicalComplex.exactAt_iff' _ (n + 1 + 1) (n + 1) n (by simp) (by simp)]
-  cases n
-  all_goals
-    dsimp [ofComplex, HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor',
-      ChainComplex.mk, ChainComplex.mk']
-    simp
-    apply exact_d_f
+  dsimp [ofComplex, HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor',
+      ChainComplex.mk', ChainComplex.mk]
+  simp only [ChainComplex.of_d]
+  -- TODO: this should just be apply exact_d_f so something is missing
+  match n with
+  | 0 =>
+    apply exact_d_f ((ChainComplex.mkAux _ _ _ (d (Projective.π Z)) (d (d (Projective.π Z))) _ _
+      0).g)
+  | n+1 =>
+    apply exact_d_f ((ChainComplex.mkAux _ _ _ (d (Projective.π Z)) (d (d (Projective.π Z))) _ _
+      (n+1)).g)
 
 instance (n : ℕ) : Projective ((ofComplex Z).X n) := by
   obtain (_ | _ | _ | n) := n <;> apply Projective.projective_over