awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Pullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : HasShift.{v_1, u_1, u_3} C B
φ : A →+ B
X : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = (φ : (a : A) → B) a₁
h₂ : b₂ = (φ : (a : A) → B) a₂
h₃ : b₃ = (φ : (a : A) → B) a₃
D : Type u_4
inst_4 : Category.{v_2, u_4} D
inst_5 : HasShift.{v_2, u_4, u_3} D B
F : Functor.{v_1, v_2, u_1, u_4} C D
inst_6 : F.CommShift B
G : Functor.{v_1, v_2, u_1, u_4} C D
inst_7 : G.CommShift B
x : A
x_1 : PullbackShift.{v_1, u_1, u_2, u_3} C φ
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x ⋙ 𝟭 (PullbackShift.{v_1, u_1, u_2, u_3} C φ)) x_1 ⟶
      Functor.obj (PullbackShift.functor φ (𝟭 C) ⋙ shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_1)
    (app
      (Iso.hom (Functor.commShiftIso (𝟭 (PullbackShift.{v_1, u_1, u_2, u_3} C φ)) x) ≫
        Functor.whiskerRight (Iso.hom (PullbackShift.natIsoId C φ))
          (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x))
      x_1)
    (app
      (Functor.whiskerLeft (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x)
          (Iso.hom (PullbackShift.natIsoId C φ)) ≫
        Iso.hom (Functor.commShiftIso (PullbackShift.functor φ (𝟭 C)) x))
      x_1)

Tactic:
simp [PullbackShift.natIsoId, Functor.commShiftPullback_iso_eq]

Premises used: CategoryTheory.Functor.commShiftPullback_iso_eq, CategoryTheory.NatTrans.PullbackShift.natIsoId
-- Module: Mathlib.CategoryTheory.Shift.Pullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : HasShift.{v_1, u_1, u_3} C B
φ : A →+ B
X : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = (φ : (a : A) → B) a₁
h₂ : b₂ = (φ : (a : A) → B) a₂
h₃ : b₃ = (φ : (a : A) → B) a₃
D : Type u_4
inst_4 : Category.{v_2, u_4} D
inst_5 : HasShift.{v_2, u_4, u_3} D B
F : Functor.{v_1, v_2, u_1, u_4} C D
inst_6 : F.CommShift B
G_1 : Functor.{v_1, v_2, u_1, u_4} C D
inst_7 : G_1.CommShift B
E : Type u_5
inst_8 : Category.{v_3, u_5} E
inst_9 : HasShift.{v_3, u_5, u_3} E B
G : Functor.{v_2, v_3, u_4, u_5} D E
inst_10 : G.CommShift B
x : A
w :
  ∀ (x_1 : PullbackShift.{v_1, u_1, u_2, u_3} C φ),
    Eq (α :=
      Quiver.Hom (V := PullbackShift.{v_3, u_5, u_2, u_3} E φ)
        (obj (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x ⋙ PullbackShift.functor φ (F ⋙ G)) x_1)
        (obj
          (comp (D := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ F) (PullbackShift.functor φ G) ⋙
            shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x)
          x_1))
      (app
        (Iso.hom (commShiftIso (PullbackShift.functor φ (F ⋙ G)) x) ≫
          whiskerRight (Iso.hom (PullbackShift.natIsoComp φ F G))
            (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x))
        x_1)
      (app
        (whiskerLeft (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x)
            (Iso.hom (PullbackShift.natIsoComp φ F G)) ≫
          Iso.hom
            (commShiftIso
              (comp (D := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ F)
                (PullbackShift.functor φ G))
              x))
        x_1)
⊢ Eq (α :=
    Quiver.Hom (V :=
      Functor.{v_1, v_3, u_1, u_5} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (PullbackShift.{v_3, u_5, u_2, u_3} E φ))
      (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x ⋙ PullbackShift.functor φ (F ⋙ G))
      (comp (D := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ F) (PullbackShift.functor φ G) ⋙
        shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x))
    (Iso.hom (commShiftIso (PullbackShift.functor φ (F ⋙ G)) x) ≫
      whiskerRight (Iso.hom (PullbackShift.natIsoComp φ F G)) (shiftFunctor (PullbackShift.{v_3, u_5, u_2, u_3} E φ) x))
    (whiskerLeft (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) (Iso.hom (PullbackShift.natIsoComp φ F G)) ≫
      Iso.hom
        (commShiftIso
          (comp (D := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ F) (PullbackShift.functor φ G))
          x))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Shift.Pullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : HasShift.{v_1, u_1, u_3} C B
φ : A →+ B
X : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = (φ : (a : A) → B) a₁
h₂ : b₂ = (φ : (a : A) → B) a₂
h₃ : b₃ = (φ : (a : A) → B) a₃
D : Type u_4
inst_4 : Category.{v_2, u_4} D
inst_5 : HasShift.{v_2, u_4, u_3} D B
F : Functor.{v_1, v_2, u_1, u_4} C D
inst_6 : F.CommShift B
G_1 : Functor.{v_1, v_2, u_1, u_4} C D
inst_7 : G_1.CommShift B
E : Type u_5
inst_8 : Category.{v_3, u_5} E
inst_9 : HasShift.{v_3, u_5, u_3} E B
G : Functor.{v_2, v_3, u_4, u_5} D E
inst_10 : G.CommShift B
x : A
x_1 : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a : G.map (𝟙 (obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x : B)) (F.obj x_1)))
| CategoryStruct.comp (Y :=
    G.obj (obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x) (F.obj x_1)))
    (G.map (app (Iso.inv (pullbackShiftIso D φ x ((φ : (a : A) → B) x) ⋯)) (F.obj x_1)))
    (G.map (app (Iso.hom (pullbackShiftIso D φ x ((φ : (a : A) → B) x) ⋯)) (F.obj x_1)))

Tactic:
rw [← G.map_comp, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app
-- Module: Mathlib.CategoryTheory.Shift.Pullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : HasShift.{v_1, u_1, u_3} C B
φ : A →+ B
X : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = (φ : (a : A) → B) a₁
h₂ : b₂ = (φ : (a : A) → B) a₂
h₃ : b₃ = (φ : (a : A) → B) a₃
D : Type u_4
inst_4 : Category.{v_2, u_4} D
inst_5 : HasShift.{v_2, u_4, u_3} D B
F_1 : Functor.{v_1, v_2, u_1, u_4} C D
inst_6 : F_1.CommShift B
F : Functor.{v_1, v_2, u_1, u_4} C D
G : Functor.{v_2, v_1, u_4, u_1} D C
adj : F ⊣ G
x : PullbackShift.{v_1, u_1, u_2, u_3} C φ
⊢ Eq (α :=
    Quiver.Hom (V := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (Functor.obj (functor φ F) x)
      (Functor.obj (functor φ F) x))
    (Functor.map (functor φ F)
        (NatTrans.app
          (Iso.hom (NatTrans.PullbackShift.natIsoId C φ) ≫
            natTrans φ adj.unit ≫ Iso.hom (NatTrans.PullbackShift.natIsoComp φ F G))
          x) ≫
      NatTrans.app
        (Iso.inv (NatTrans.PullbackShift.natIsoComp φ G F) ≫
          natTrans φ adj.counit ≫ Iso.inv (NatTrans.PullbackShift.natIsoId D φ))
        (Functor.obj (functor φ F) x))
    (𝟙 (Functor.obj (functor φ F) x))

Tactic:
simp [PullbackShift.natTrans, NatTrans.PullbackShift.natIsoComp,
      NatTrans.PullbackShift.natIsoId, PullbackShift.functor]

Premises used: CategoryTheory.NatTrans.PullbackShift.natIsoComp, CategoryTheory.NatTrans.PullbackShift.natIsoId, CategoryTheory.PullbackShift.natTrans, CategoryTheory.PullbackShift.functor
-- Module: Mathlib.CategoryTheory.Shift.Pullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : HasShift.{v_1, u_1, u_3} C B
φ : A →+ B
X : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = (φ : (a : A) → B) a₁
h₂ : b₂ = (φ : (a : A) → B) a₂
h₃ : b₃ = (φ : (a : A) → B) a₃
D : Type u_4
inst_4 : Category.{v_2, u_4} D
inst_5 : HasShift.{v_2, u_4, u_3} D B
F_1 : Functor.{v_1, v_2, u_1, u_4} C D
inst_6 : F_1.CommShift B
F : Functor.{v_1, v_2, u_1, u_4} C D
G : Functor.{v_2, v_1, u_4, u_1} D C
adj : F ⊣ G
x : PullbackShift.{v_2, u_4, u_2, u_3} D φ
⊢ Eq (α :=
    Quiver.Hom (V := PullbackShift.{v_1, u_1, u_2, u_3} C φ) (Functor.obj (functor φ G) x)
      (Functor.obj (functor φ G) x))
    (NatTrans.app
        (Iso.hom (NatTrans.PullbackShift.natIsoId C φ) ≫
          natTrans φ adj.unit ≫ Iso.hom (NatTrans.PullbackShift.natIsoComp φ F G))
        (Functor.obj (functor φ G) x) ≫
      Functor.map (functor φ G)
        (NatTrans.app
          (Iso.inv (NatTrans.PullbackShift.natIsoComp φ G F) ≫
            natTrans φ adj.counit ≫ Iso.inv (NatTrans.PullbackShift.natIsoId D φ))
          x))
    (𝟙 (Functor.obj (functor φ G) x))

Tactic:
simp [PullbackShift.natTrans, NatTrans.PullbackShift.natIsoComp,
      NatTrans.PullbackShift.natIsoId, PullbackShift.functor]

Premises used: CategoryTheory.NatTrans.PullbackShift.natIsoComp, CategoryTheory.NatTrans.PullbackShift.natIsoId, CategoryTheory.PullbackShift.natTrans, CategoryTheory.PullbackShift.functor
-- Module: Mathlib.CategoryTheory.Shift.Pullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : HasShift.{v_1, u_1, u_3} C B
φ : A →+ B
X : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = (φ : (a : A) → B) a₁
h₂ : b₂ = (φ : (a : A) → B) a₂
h₃ : b₃ = (φ : (a : A) → B) a₃
D : Type u_4
inst_4 : Category.{v_2, u_4} D
inst_5 : HasShift.{v_2, u_4, u_3} D B
F : Functor.{v_1, v_2, u_1, u_4} C D
inst_6 : F.CommShift B
G : Functor.{v_2, v_1, u_4, u_1} D C
adj : F ⊣ G
inst_7 : G.CommShift B
inst_8 : adj.CommShift B
⊢ NatTrans.CommShift (C := PullbackShift.{v_1, u_1, u_2, u_3} C φ) (F₂ :=
    Functor.comp (D := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (PullbackShift.functor φ F) (PullbackShift.functor φ G))
    (Iso.hom (NatTrans.PullbackShift.natIsoId C φ) ≫
      PullbackShift.natTrans φ adj.unit ≫ Iso.hom (NatTrans.PullbackShift.natIsoComp φ F G))
    A

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.Pullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst_1 : AddMonoid A
inst_2 : AddMonoid B
inst_3 : HasShift.{v_1, u_1, u_3} C B
φ : A →+ B
X : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = (φ : (a : A) → B) a₁
h₂ : b₂ = (φ : (a : A) → B) a₂
h₃ : b₃ = (φ : (a : A) → B) a₃
D : Type u_4
inst_4 : Category.{v_2, u_4} D
inst_5 : HasShift.{v_2, u_4, u_3} D B
F : Functor.{v_1, v_2, u_1, u_4} C D
inst_6 : F.CommShift B
G : Functor.{v_2, v_1, u_4, u_1} D C
adj : F ⊣ G
inst_7 : G.CommShift B
inst_8 : adj.CommShift B
⊢ NatTrans.CommShift (C := PullbackShift.{v_2, u_4, u_2, u_3} D φ) (F₁ :=
    Functor.comp (D := PullbackShift.{v_1, u_1, u_2, u_3} C φ) (PullbackShift.functor φ G) (PullbackShift.functor φ F))
    (Iso.inv (NatTrans.PullbackShift.natIsoComp φ G F) ≫
      PullbackShift.natTrans φ adj.counit ≫ Iso.inv (NatTrans.PullbackShift.natIsoId D φ))
    A

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
r : HomRel.{u, v} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
inst_3 : r.IsCompatibleWithShift A
X : C
n : A
⊢ Functor.obj.{v, v, u, u} (shiftFunctor (Quotient r) n) ((functor r).obj X) =
    (functor r).obj (Functor.obj.{v, v, u, u} (shiftFunctor C n) X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ Eq (α :=
    (shiftFunctor (Quotient r) a ⋙ lift r F hF).obj ((functor r).obj X) ⟶
      (lift r F hF ⋙ shiftFunctor D a).obj ((functor r).obj X))
    (NatTrans.app (Iso.hom (iso F r hF a)) ((functor r).obj X))
    (CategoryStruct.comp (Y := (lift r F hF).obj ((shiftFunctor C a ⋙ functor r).obj X))
      ((lift r F hF).map (NatTrans.app (Iso.inv (Functor.commShiftIso (functor r) a)) X))
      (NatTrans.app (Iso.hom (Functor.commShiftIso F a)) X))

Tactic:
simp [iso, lift_obj_functor_obj]

Premises used: CategoryTheory.Quotient.LiftCommShift.iso, CategoryTheory.Quotient.lift_obj_functor_obj
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a : A
X : C
⊢ Eq (α :=
    (lift r F hF ⋙ shiftFunctor D a).obj ((functor r).obj X) ⟶
      (shiftFunctor (Quotient r) a ⋙ lift r F hF).obj ((functor r).obj X))
    (NatTrans.app (Iso.inv (iso F r hF a)) ((functor r).obj X))
    (CategoryStruct.comp (Y := (shiftFunctor C a ⋙ F).obj X) (NatTrans.app (Iso.inv (Functor.commShiftIso F a)) X)
      ((lift r F hF).map (NatTrans.app (Iso.hom (Functor.commShiftIso (functor r) a)) X)))

Tactic:
simp [iso, lift_obj_functor_obj]

Premises used: CategoryTheory.Quotient.LiftCommShift.iso, CategoryTheory.Quotient.lift_obj_functor_obj
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
w :
  Eq (α :=
    shiftFunctor.{v, u, w} (Quotient r) (A := A) 0 ⋙ lift r F hF ⟶ lift r F hF ⋙ shiftFunctor.{v', u', w} D (A := A) 0)
    (Iso.hom (LiftCommShift.iso F r hF 0)) (Iso.hom (Functor.CommShift.isoZero (lift r F hF) A))
⊢ Eq (α :=
    shiftFunctor.{v, u, w} (Quotient r) (A := A) 0 ⋙ lift r F hF ≅ lift r F hF ⋙ shiftFunctor.{v', u', w} D (A := A) 0)
    (LiftCommShift.iso F r hF 0) (Functor.CommShift.isoZero (lift r F hF) A)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
w :
  Eq (α :=
    functor r ⋙ shiftFunctor.{v, u, w} (Quotient r) (A := A) 0 ⋙ lift r F hF ⟶
      functor r ⋙ lift r F hF ⋙ shiftFunctor.{v', u', w} D (A := A) 0)
    ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF 0)))
    ((functor r).whiskerLeft (Iso.hom (Functor.CommShift.isoZero (lift r F hF) A)))
⊢ Eq (α :=
    shiftFunctor.{v, u, w} (Quotient r) (A := A) 0 ⋙ lift r F hF ⟶ lift r F hF ⋙ shiftFunctor.{v', u', w} D (A := A) 0)
    (Iso.hom (LiftCommShift.iso F r hF 0)) (Iso.hom (Functor.CommShift.isoZero (lift r F hF) A))

Tactic:
apply natTrans_ext

Premises used: CategoryTheory.Quotient.natTrans_ext
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
w :
  ∀ (X : C),
    Eq (α :=
      (functor r ⋙ shiftFunctor.{v, u, w} (Quotient r) (A := A) 0 ⋙ lift r F hF).obj X ⟶
        (functor r ⋙ lift r F hF ⋙ shiftFunctor.{v', u', w} D (A := A) 0).obj X)
      (NatTrans.app ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF 0))) X)
      (NatTrans.app ((functor r).whiskerLeft (Iso.hom (Functor.CommShift.isoZero (lift r F hF) A))) X)
⊢ Eq (α :=
    functor r ⋙ shiftFunctor.{v, u, w} (Quotient r) (A := A) 0 ⋙ lift r F hF ⟶
      functor r ⋙ lift r F hF ⋙ shiftFunctor.{v', u', w} D (A := A) 0)
    ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF 0)))
    ((functor r).whiskerLeft (Iso.hom (Functor.CommShift.isoZero (lift r F hF) A)))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
w :
  Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) ((lift r F hF).obj ((functor r).obj X)))
    (NatTrans.app (Iso.hom (LiftCommShift.iso F r hF 0)) ((functor r).obj X))
    (NatTrans.app (Iso.hom (Functor.CommShift.isoZero (lift r F hF) A)) ((functor r).obj X))
⊢ Eq (α :=
    (functor r ⋙ shiftFunctor.{v, u, w} (Quotient r) (A := A) 0 ⋙ lift r F hF).obj X ⟶
      (functor r ⋙ lift r F hF ⋙ shiftFunctor.{v', u', w} D (A := A) 0).obj X)
    (NatTrans.app ((functor r).whiskerLeft (Iso.hom (LiftCommShift.iso F r hF 0))) X)
    (NatTrans.app ((functor r).whiskerLeft (Iso.hom (Functor.CommShift.isoZero (lift r F hF) A))) X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
w :
  Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) ((lift r F hF).obj ((functor r).obj X)))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      F.map (𝟙 (Functor.obj.{v, v, u, u} (𝟭 C) X)) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) ((lift r F hF).obj ((functor r).obj X)))
⊢ Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) ((lift r F hF).obj ((functor r).obj X)))
    (NatTrans.app (Iso.hom (LiftCommShift.iso F r hF 0)) ((functor r).obj X))
    (NatTrans.app (Iso.hom (Functor.CommShift.isoZero (lift r F hF) A)) ((functor r).obj X))

Tactic:
rw [LiftCommShift.iso_hom_app, (functor r).commShiftIso_zero,
      Functor.CommShift.isoZero_hom_app, Functor.CommShift.isoZero_inv_app,
      Functor.map_comp, assoc, F.commShiftIso_zero, Functor.CommShift.isoZero_hom_app,
      lift_map_functor_map, ← F.map_comp_assoc, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.CommShift.isoZero_hom_app, CategoryTheory.Quotient.functor, CategoryTheory.Quotient.LiftCommShift.iso_hom_app, CategoryTheory.Quotient.lift_map_functor_map, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.CommShift.isoZero_inv_app, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Functor.CommShift.commShiftIso_zero
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
w :
  Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      F.map (𝟙 X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
⊢ Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) ((lift r F hF).obj ((functor r).obj X)))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      F.map (𝟙 (Functor.obj.{v, v, u, u} (𝟭 C) X)) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) ((lift r F hF).obj ((functor r).obj X)))

Tactic:
dsimp [lift_obj_functor_obj]

Premises used: CategoryTheory.Quotient.lift_obj_functor_obj
-- Module: Mathlib.CategoryTheory.Shift.Quotient
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
r : HomRel.{u, v} C
A : Type w
inst_2 : AddMonoid A
inst_3 : HasShift.{v, u, w} C A
inst_4 : HasShift.{v', u', w} D A
inst_5 : r.IsCompatibleWithShift A
inst_6 : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
w :
  Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      𝟙 (F.obj X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
w₁ w₂ :
  Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
⊢ Eq (α :=
    (lift r F hF).obj (Functor.obj.{v, v, u, u} (shiftFunctor.{v, u, w} (Quotient r) (A := A) 0) ((functor r).obj X)) ⟶
      Functor.obj.{v', v', u', u'} (shiftFunctor.{v', u', w} D (A := A) 0) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      F.map (𝟙 X) ≫ NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))
    ((lift r F hF).map (NatTrans.app (Iso.hom (shiftFunctorZero (Quotient r) A)) ((functor r).obj X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorZero D A)) (F.obj X))

Tactic:
rw [F.map_id, id_comp]

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp