Lean4
/-- Shifting by `i` and shifting by `j` forms an equivalence when `i + j = 0`. -/
@[simps]
def shiftEquiv' (i j : A) (h : i + j = 0) : C ≌ C
where
functor := shiftFunctor C i
inverse := shiftFunctor C j
unitIso := (shiftFunctorCompIsoId C i j h).symm
counitIso := shiftFunctorCompIsoId C j i (by rw [← add_left_inj j, add_assoc, h, zero_add, add_zero])
functor_unitIso_comp
X :=
by
convert
(equivOfTensorIsoUnit (shiftMonoidalFunctor C A) ⟨i⟩ ⟨j⟩ (Discrete.eqToIso h)
(Discrete.eqToIso (by dsimp; rw [← add_left_inj j, add_assoc, h, zero_add, add_zero]))
(Subsingleton.elim _ _)).functor_unitIso_comp
X
all_goals
ext X
dsimp [shiftFunctorCompIsoId, unitOfTensorIsoUnit, shiftFunctorAdd']
simp only [Category.assoc, eqToHom_map]
rfl
