chore(CategoryTheory/HomologicalComplex): make ChainComplex.of and CochainComplex.of implicit reducible

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -636,34 +636,30 @@ 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, simps X]
+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] }
 
 variable (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) ≫ d n = 0)
 
-theorem of_X : (of X d sq).X = X :=
-  rfl
-
 @[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 : α) : dsimp% (of X d sq).d (j + 1) j = d j := by
+  simp [of]
+
+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 +743,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 +766,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 +804,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
 
@@ -896,36 +893,32 @@ section Of
 
 variable {V} {α : Type*} [AddRightCancelSemigroup α] [One α] [DecidableEq α]
 
-/-- Auxiliary definition for differentials for `CochainComplex.of`. -/
-def of.d (X : α → V) (d : ∀ n, X n ⟶ X (n + 1)) (i : α) (j : α) : X i ⟶ X j :=
-  if h : i + 1 = j then d _ ≫ eqToHom (by rw [h]) else 0
-
 /-- Construct an `α`-indexed cochain complex from a dependently-typed differential.
 -/
-abbrev of (X : α → V) (d : ∀ n, X n ⟶ X (n + 1)) (sq : ∀ n, d n ≫ d (n + 1) = 0) :
+@[implicit_reducible, simps X]
+def of (X : α → V) (d : ∀ n, X n ⟶ X (n + 1)) (sq : ∀ n, d n ≫ d (n + 1) = 0) :
     CochainComplex V α :=
   { X := X
-    d := of.d X d
+    d i j := if h : i + 1 = j then d _ ≫ eqToHom (by rw [h]) else 0
     shape := fun i j w => dite_eq_right (c := i + 1 = j) w
     d_comp_d' := fun i j k => by
-      dsimp [of.d]
       split_ifs with h h' h'
       · subst h h'
         simp [sq]
       all_goals simp }
 
 variable (X : α → V) (d : ∀ n, X n ⟶ X (n + 1)) (sq : ∀ n, d n ≫ d (n + 1) = 0)
 
-theorem of_X : (of X d sq).X = X :=
-  rfl
-
 @[simp]
-theorem of_d (j : α) : of.d X d j (j + 1) = d j := by
-  dsimp [of.d]
-  rw [ite_eq_left rfl, Category.comp_id]
+theorem of_d (j : α) : dsimp% (of X d sq).d j (j + 1) = d j := by
+  simp [of]
+
+theorem of_d' (i j : α) (h : i = j + 1 := by omega) : (of X d sq).d j i =
+    d j ≫ eqToHom (by rw [h, of_X]) := by
+  simp [of, h]
 
-theorem of_d_ne {i j : α} (h : i + 1 ≠ j) : of.d X d i j = 0 := by
-  simp [of.d, dite_eq_right h]
+theorem of_d_ne {i j : α} (h : i + 1 ≠ j) : (of X d sq).d i j = 0 := by
+  simp [of, dite_eq_right h]
 
 end Of
 

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

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

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

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

Mathlib/RepresentationTheory/Homological/ContCohomology/Basic.lean

@@ -122,7 +122,8 @@ lemma homogeneousCochains.d_eq (X : TopRep k G) (i : ℕ) :
 
 lemma homogeneousCochains.d_apply (X : TopRep k G) (i : ℕ)
     (σ : (homogeneousCochains X).X i) :
-    ((homogeneousCochains X).d i (i + 1)).hom σ = (d X (i + 1)).hom σ := by
+    (((homogeneousCochains X).d i (i + 1)).hom σ : X.resolution'.X (i + 1)) =
+      (d X (i + 1)).hom σ.1 := by
   rw [homogeneousCochains.d_eq]
   dsimp [ContIntertwiningMap.mapInvariants_apply]
 

Mathlib/RepresentationTheory/Homological/ContCohomology/Functoriality.lean

@@ -99,7 +99,7 @@ lemma resolutionMap_comp_d (φ : H →ₜ* G) (f : res φ X ⟶ Y) (i : ℕ) :
 /-- The cochain map `homogeneousCochains X ⟶ homogeneousCochains Y` induced by a continuous
 group homomorphism `φ : H →ₜ* G` and a morphism of topological `H`-representations
 `f : res φ X ⟶ Y`, sending an invariant function `σ : C(G, C(G, ⋯))` to `f ∘ σ ∘ φ`. -/
-@[simps! -isSimp f f_hom]
+@[implicit_reducible, simps! -isSimp f f_hom]
 def cochainsMap (φ : H →ₜ* G) (f : res φ X ⟶ Y) :
     homogeneousCochains X ⟶ homogeneousCochains Y where
   f i := invariantsResMap φ (resolutionMap φ f (i + 1))
@@ -121,8 +121,9 @@ lemma cochainsMap_id (X : TopRep k G) :
 lemma cochainsMap_comp (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : res φ X ⟶ Y) (g : res ψ Y ⟶ Z) :
     cochainsMap (φ.comp ψ) (X := X) ((resFunctor (ψ : K →* H)).map f ≫ g) =
       cochainsMap φ f ≫ cochainsMap ψ g := by
-  ext i v x
-  exact congr($(resolutionMap_comp φ ψ f g (i + 1)).hom v.1 x)
+  ext i x
+  simp only [CochainComplex.of_X, cochainsMap, resolutionMap_comp φ ψ f g (i + 1)]
+  rfl
 
 /-- The map `Zⁿ(G, X) ⟶ Zⁿ(H, Y)` on cocycles induced by a continuous group homomorphism
 `φ : H →ₜ* G` and a morphism of topological `H`-representations `f : res φ X ⟶ Y`. -/

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
 
@@ -140,7 +145,7 @@ theorem inhomogeneousCochains.d_def (n : ℕ) :
 set_option backward.defeqAttrib.useBackward true in
 theorem inhomogeneousCochains.d_comp_d :
     d A n ≫ d A (n + 1) = 0 := by
-  simpa [CochainComplex.of.d] using (inhomogeneousCochains A).d_comp_d n (n + 1) (n + 2)
+  simpa [CochainComplex.of_d'] using (inhomogeneousCochains A).d_comp_d n (n + 1) (n + 2)
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Given a `k`-linear `G`-representation `A`, the complex of inhomogeneous cochains is isomorphic

Mathlib/RepresentationTheory/Homological/GroupCohomology/Functoriality.lean

@@ -57,7 +57,7 @@ noncomputable def cochainsMap :
   comm' i j (hij : _ = _) := by
     subst hij
     ext
-    simpa [inhomogeneousCochains.d_hom_apply, Fin.comp_contractNth, CochainComplex.of.d]
+    simpa [inhomogeneousCochains.d_hom_apply, Fin.comp_contractNth, CochainComplex.of_d]
       using! (hom_comm_apply φ _ _).symm
 
 @[simp]

Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean

@@ -114,7 +114,7 @@ Stated for readability of `δ_apply`. -/
 noncomputable abbrev cocyclesMkOfCompEqD {i j : ℕ} {y : (Fin i → G) → X.X₂}
     {x : (Fin j → G) → X.X₁} (hx : X.f.hom ∘ x = (inhomogeneousCochains X.X₂).d i j y) :
     cocycles X.X₁ j :=
-  cocyclesMk x <| by simpa [CochainComplex.of.d] using!
+  cocyclesMk x <| by simpa [CochainComplex.of_d] using!
     ((map_cochainsFunctor_shortExact hX).d_eq_zero_of_f_eq_d_apply i j y x
       (by simpa using! hx) (j + 1))
 
@@ -127,7 +127,7 @@ theorem δ_apply {i j : ℕ} (hij : i + 1 = j)
     -- Let `x` be an `i + 1`-cochain for `X₁` such that `f ∘ x = d(y)`
     (x : (Fin j → G) → X.X₁) (hx : X.f.hom ∘ x = (inhomogeneousCochains X.X₂).d i j y) :
     -- Then `x` is an `i + 1`-cocycle and `δ z = x` in `Hⁱ⁺¹(X₁)`.
-    δ hX i j hij (π X.X₃ i <| cocyclesMk z (by subst hij; simpa [CochainComplex.of.d] using! hz)) =
+    δ hX i j hij (π X.X₃ i <| cocyclesMk z (by subst hij; simpa [CochainComplex.of_d] using! hz)) =
       π X.X₁ j (cocyclesMkOfCompEqD hX hx) := by
   exact (map_cochainsFunctor_shortExact hX).δ_apply i j hij z hz y hy x
     (by simpa using! hx) (j + 1) (by simp)

Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean

@@ -158,18 +158,11 @@ where the vertical arrows are `cochainsIso₀` and `cochainsIso₁` respectively
 theorem comp_d₀₁_eq :
     (cochainsIso₀ A).hom ≫ d₀₁ A =
       (inhomogeneousCochains A).d 0 1 ≫ (cochainsIso₁ A).hom := by
-  ext x a y
-  simp only [cochainsIso₀, LinearEquiv.toModuleIso_hom, ModuleCat.hom_comp,
-    ConcreteCategory.hom_ofHom, LinearMap.coe_comp, LinearEquiv.coe_coe,
-    LinearEquiv.funUnique_apply, LinearMap.coe_single, Function.comp_apply, Function.eval,
-    d₀₁_hom_apply, zero_add, ↓reduceDIte, Nat.reduceAdd, eqToHom_refl, Category.comp_id,
-    cochainsIso₁, Iso.symm_hom, LinearEquiv.toModuleIso_inv, LinearEquiv.funCongrLeft_symm,
-    LinearEquiv.funCongrLeft_apply, Equiv.funUnique_symm_apply, LinearMap.funLeft_apply,
-    inhomogeneousCochains.d_hom_apply, Fin.isValue, uniqueElim_const, Finset.univ_unique,
-    Fin.default_eq_zero, Fin.val_eq_zero, pow_one, neg_smul, one_smul, Finset.sum_neg_distrib,
-    Finset.sum_singleton, ← sub_eq_add_neg, CochainComplex.of.d]
-  rw [← Subsingleton.elim (α := Fin 0 → G) default (fun i ↦ y), Subsingleton.elim
-    (Fin.contractNth 0 _) default, Pi.default_def]
+  ext x a
+  simp [cochainsIso₀, LinearEquiv.toModuleIso_hom, d₀₁_hom_apply, eqToHom_refl,
+    cochainsIso₁, LinearEquiv.toModuleIso_inv, LinearEquiv.funCongrLeft_symm,
+    LinearEquiv.funCongrLeft_apply, inhomogeneousCochains.d_hom_apply,
+    ← sub_eq_add_neg, CochainComplex.of_d', ← Subsingleton.elim (α := Fin 0 → G) default]
 
 -- @[reassoc (attr := simp), elementwise (attr := simp)]
 @[reassoc, elementwise]
@@ -1014,8 +1007,9 @@ group homs `G → A`. -/
 def H1IsoOfIsTrivial :
     H1 A ≅ ↧(Additive G →+ A) :=
   (HomologicalComplex.isoHomologyπ _ 0 1 (CochainComplex.prev_nat_succ 0) <| by
-    ext; simp [inhomogeneousCochains.d, Unique.eq_default (α := Fin 0 → G),
-      CochainComplex.of.d, isTrivial_apply]).symm ≪≫
+    ext
+    simp [-CochainComplex.of_d, inhomogeneousCochains.d, Unique.eq_default (α := Fin 0 → G),
+      CochainComplex.of_d', isTrivial_apply, (Pi.zero_apply)]).symm ≪≫
   isoCocycles₁ A ≪≫ cocycles₁IsoOfIsTrivial A
 
 set_option backward.isDefEq.respectTransparency false in

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. -/