chore(Algebra/Homology/HomologicalComplex): backport fixes from nightly-testing (leanprover-community#38458)

Author: jcommelin

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -631,18 +631,17 @@ def of (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) ≫
 variable (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) ≫ d n = 0)
 
 @[simp]
-theorem of_x (n : α) : (of X d sq).X n = X n :=
+theorem of_X : (of X d sq).X = X :=
   rfl
 
 @[simp]
 theorem of_d (j : α) : (of X d sq).d (j + 1) j = d j := by
   dsimp [of]
   rw [if_pos rfl, Category.id_comp]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem of_d_ne {i j : α} (h : i ≠ j + 1) : (of X d sq).d i j = 0 := by
-  dsimp [of]
-  rw [dif_neg h]
+  rw [of]
+  simp [dif_neg h]
 
 end Of
 
@@ -652,7 +651,6 @@ variable {V} {α : Type*} [AddRightCancelSemigroup α] [One α] [DecidableEq α]
 variable (X : α → V) (d_X : ∀ n, X (n + 1) ⟶ X n) (sq_X : ∀ n, d_X (n + 1) ≫ d_X n = 0) (Y : α → V)
   (d_Y : ∀ n, Y (n + 1) ⟶ Y n) (sq_Y : ∀ n, d_Y (n + 1) ≫ d_Y n = 0)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- A constructor for chain maps between `α`-indexed chain complexes built using `ChainComplex.of`,
 from a dependently typed collection of morphisms.
 -/
@@ -661,11 +659,9 @@ def ofHom (f : ∀ i : α, X i ⟶ Y i) (comm : ∀ i : α, f (i + 1) ≫ d_Y i
     of X d_X sq_X ⟶ of Y d_Y sq_Y :=
   { f
     comm' := fun n m => by
-      by_cases h : n = m + 1
-      · subst h
-        simpa using comm m
-      · rw [of_d_ne X _ _ h, of_d_ne Y _ _ h]
-        simp }
+      simp only [ComplexShape.down_Rel]
+      rintro rfl
+      simpa using comm m }
 
 end OfHom
 
@@ -727,9 +723,8 @@ lemma mk_congr_succ_d₂ {S S' : ShortComplex V} (h : S = S') :
 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
-  change ShortComplex.mk _ _ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n).zero = _
-  dsimp [mk, of, mkAux]
-  simp
+  rw [show n + 2 = n + 1 + 1 from rfl]
+  simp only [mk, of_X, of_d, mkAux]
 
 /-- The isomorphism from `(mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3)` that is given by
 the inductive construction. -/
@@ -741,14 +736,14 @@ def mkXIso (n : ℕ) :
       (mkAux_eq_shortComplex_mk_d_comp_d X₀ X₁ X₂ d₀ d₁ s succ n)]
     rfl)
 
-set_option backward.isDefEq.respectTransparency false in
 lemma mk_d (n : ℕ) :
     (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 3) (n + 2) =
       (mkXIso X₀ X₁ X₂ d₀ d₁ s succ n).hom ≫ (succ
         (ShortComplex.mk _ _ ((mk X₀ X₁ X₂ d₀ d₁ s succ).d_comp_d (n + 2) (n + 1) n))).2.1 := by
   have eq := mk_congr_succ_d₂ succ
     (mkAux_eq_shortComplex_mk_d_comp_d X₀ X₁ X₂ d₀ d₁ s succ n)
-  rw [eqToHom_refl, comp_id] at eq
+  set_option backward.isDefEq.respectTransparency false in
+    rw [eqToHom_refl, comp_id] at eq
   refine Eq.trans ?_ eq
   dsimp only [mk, of]
   rw [dif_pos (by rfl), eqToHom_refl, id_comp]
@@ -895,18 +890,17 @@ def of (X : α → V) (d : ∀ n, X n ⟶ X (n + 1)) (sq : ∀ n, d n ≫ d (n +
 variable (X : α → V) (d : ∀ n, X n ⟶ X (n + 1)) (sq : ∀ n, d n ≫ d (n + 1) = 0)
 
 @[simp]
-theorem of_x (n : α) : (of X d sq).X n = X n :=
+theorem of_X : (of X d sq).X = X :=
   rfl
 
 @[simp]
 theorem of_d (j : α) : (of X d sq).d j (j + 1) = d j := by
   dsimp [of]
   rw [if_pos rfl, Category.comp_id]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem of_d_ne {i j : α} (h : i + 1 ≠ j) : (of X d sq).d i j = 0 := by
-  dsimp [of]
-  rw [dif_neg h]
+  rw [of]
+  simp [dif_neg h]
 
 end Of
 
@@ -916,7 +910,6 @@ variable {V} {α : Type*} [AddRightCancelSemigroup α] [One α] [DecidableEq α]
 variable (X : α → V) (d_X : ∀ n, X n ⟶ X (n + 1)) (sq_X : ∀ n, d_X n ≫ d_X (n + 1) = 0) (Y : α → V)
   (d_Y : ∀ n, Y n ⟶ Y (n + 1)) (sq_Y : ∀ n, d_Y n ≫ d_Y (n + 1) = 0)
 
-set_option backward.isDefEq.respectTransparency false in
 /--
 A constructor for chain maps between `α`-indexed cochain complexes built using `CochainComplex.of`,
 from a dependently typed collection of morphisms.
@@ -926,11 +919,9 @@ def ofHom (f : ∀ i : α, X i ⟶ Y i) (comm : ∀ i : α, f i ≫ d_Y i = d_X
     of X d_X sq_X ⟶ of Y d_Y sq_Y :=
   { f
     comm' := fun n m => by
-      by_cases h : n + 1 = m
-      · subst h
-        simpa using comm n
-      · rw [of_d_ne X _ _ h, of_d_ne Y _ _ h]
-        simp }
+      simp only [ComplexShape.up_Rel]
+      rintro rfl
+      simpa using comm n }
 
 end OfHom
 

Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

@@ -776,7 +776,7 @@ lemma cyclesMk₁_eq (x : cycles₁ A) :
     cyclesMk 1 0 (by simp) ((chainsIso₁ A).inv x) (by simp +instances) = (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 [ChainComplex.of_X, isoCycles₁_inv_comp_iCycles_apply]
     rfl
 
 end isoCycles₁
@@ -822,7 +822,7 @@ lemma cyclesMk₂_eq (x : cycles₂ A) :
     cyclesMk 2 1 (by simp) ((chainsIso₂ A).inv x) (by simp +instances) = (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 [ChainComplex.of_X, isoCycles₂_inv_comp_iCycles_apply]
     rfl
 
 end isoCycles₂

Mathlib/RepresentationTheory/Homological/Resolution.lean

@@ -416,7 +416,7 @@ set_option backward.isDefEq.respectTransparency false in
 def isoStandardComplex : barComplex k G ≅ standardComplex k G :=
   HomologicalComplex.Hom.isoOfComponents (fun i => (diagonalSuccIsoFree k G i).symm) fun i j => by
     rintro (rfl : j + 1 = i)
-    simp only [ChainComplex.of_x, Iso.symm_hom, d_def, d_comp_diagonalSuccIsoFree_inv_eq]
+    simp only [ChainComplex.of_X, Iso.symm_hom, d_def, d_comp_diagonalSuccIsoFree_inv_eq]
 
 end barComplex