-- Mathlib/CategoryTheory/Shift/Quotient.lean
@[simp]
lemma iso_hom_app (a : A) (X : C) :
    (iso F r hF a).hom.app ((functor r).obj X) =
      (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫
      (F.commShiftIso a).hom.app X

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ (natTransLift r
          (((functor r).associator (shiftFunctor (Quotient r) a) (lift r F hF)).symm ≪≫
              isoWhiskerRight ((functor r).commShiftIso a).symm (lift r F hF) ≪≫
                (shiftFunctor C a).associator (functor r) (lift r F hF) ≪≫
                  isoWhiskerLeft (shiftFunctor C a) (lift.isLift r F hF) ≪≫
                    F.commShiftIso a ≪≫
                      isoWhiskerRight (lift.isLift r F hF).symm (shiftFunctor D a) ≪≫
                        (functor r).associator (lift r F hF) (shiftFunctor D a)).hom).app
      ((functor r).obj X) =
    (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X

Tactic:
rw [natTransLift_app]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ (((functor r).associator (shiftFunctor (Quotient r) a) (lift r F hF)).symm ≪≫
            isoWhiskerRight ((functor r).commShiftIso a).symm (lift r F hF) ≪≫
              (shiftFunctor C a).associator (functor r) (lift r F hF) ≪≫
                isoWhiskerLeft (shiftFunctor C a) (lift.isLift r F hF) ≪≫
                  F.commShiftIso a ≪≫
                    isoWhiskerRight (lift.isLift r F hF).symm (shiftFunctor D a) ≪≫
                      (functor r).associator (lift r F hF) (shiftFunctor D a)).hom.app
      X =
    (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ (iso F r hF a).hom.app ((functor r).obj X) =
    (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X

Tactic:
dsimp only [iso, natIsoLift]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ (natTransLift r
          (((functor r).associator (shiftFunctor (Quotient r) a) (lift r F hF)).symm ≪≫
              isoWhiskerRight ((functor r).commShiftIso a).symm (lift r F hF) ≪≫
                (shiftFunctor C a).associator (functor r) (lift r F hF) ≪≫
                  isoWhiskerLeft (shiftFunctor C a) (lift.isLift r F hF) ≪≫
                    F.commShiftIso a ≪≫
                      isoWhiskerRight (lift.isLift r F hF).symm (shiftFunctor D a) ≪≫
                        (functor r).associator (lift r F hF) (shiftFunctor D a)).hom).app
      ((functor r).obj X) =
    (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ 𝟙 ((lift r F hF).obj ((shiftFunctor (Quotient r) a).obj ((functor r).obj X))) ≫
      (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫
        𝟙 ((lift r F hF).obj ((functor r).obj ((shiftFunctor C a).obj X))) ≫
          𝟙 (F.obj ((shiftFunctor C a).obj X)) ≫
            (F.commShiftIso a).hom.app X ≫
              (shiftFunctor D a).map (𝟙 (F.obj X)) ≫
                𝟙 ((shiftFunctor D a).obj ((lift r F hF).obj ((functor r).obj X))) =
    (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X

Tactic:
erw [comp_id, id_comp, id_comp, id_comp, Functor.map_id, comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ (((functor r).associator (shiftFunctor (Quotient r) a) (lift r F hF)).symm ≪≫
            isoWhiskerRight ((functor r).commShiftIso a).symm (lift r F hF) ≪≫
              (shiftFunctor C a).associator (functor r) (lift r F hF) ≪≫
                isoWhiskerLeft (shiftFunctor C a) (lift.isLift r F hF) ≪≫
                  F.commShiftIso a ≪≫
                    isoWhiskerRight (lift.isLift r F hF).symm (shiftFunctor D a) ≪≫
                      (functor r).associator (lift r F hF) (shiftFunctor D a)).hom.app
      X =
    (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X

Tactic:
dsimp

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ 𝟙 ((lift r F hF).obj ((shiftFunctor (Quotient r) a).obj ((functor r).obj X))) ≫
      (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫
        𝟙 ((lift r F hF).obj ((functor r).obj ((shiftFunctor C a).obj X))) ≫
          𝟙 (F.obj ((shiftFunctor C a).obj X)) ≫
            (F.commShiftIso a).hom.app X ≫
              (shiftFunctor D a).map (𝟙 (F.obj X)) ≫
                𝟙 ((shiftFunctor D a).obj ((lift r F hF).obj ((functor r).obj X))) =
    (lift r F hF).map (((functor r).commShiftIso a).inv.app X) ≫ (F.commShiftIso a).hom.app X