feat(RingTheory): homotopy of Koszul complex and cocomplex

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

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
 

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

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
 

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

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
 

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₁])