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₃
rw :
  𝟙
      (Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ ⋙
          shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
        X) =
    𝟙
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁) X))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₃) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ ⋙
          shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
        X)
    (NatTrans.app (Iso.hom (shiftFunctorAdd' (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ a₂ a₃ h)) X)
    (NatTrans.app (Iso.hom (pullbackShiftIso C φ a₃ b₃ h₃)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) X ≫
        NatTrans.app (Iso.inv (pullbackShiftIso C φ a₂ b₂ h₂))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b₁) X) ≫
          Functor.map (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
            (NatTrans.app (Iso.inv (pullbackShiftIso C φ a₁ b₁ h₁)) X))

Tactic:
rw [← cancel_epi ((shiftFunctorAdd' _ a₁ a₂ a₃ h).inv.app X), Iso.inv_hom_id_app,
    pullbackShiftFunctorAdd'_inv_app φ X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃, assoc, assoc, assoc,
    Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app_assoc, Iso.hom_inv_id_app_assoc,
    ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.shiftFunctorAdd', CategoryTheory.Iso.hom_inv_id_app, CategoryTheory.Iso.hom_inv_id_app_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Iso.inv, CategoryTheory.pullbackShiftFunctorAdd'_inv_app, CategoryTheory.NatTrans.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₃
⊢ 𝟙
      (Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ ⋙
          shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
        X) =
    𝟙
      (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
        (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁) X))

Tactic:
rfl
-- 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
w :
  ∀ (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 φ)
        (obj
          (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0 ⋙ PullbackShift.functor φ F)
          x)
        (obj
          (PullbackShift.functor φ F ⋙ shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0)
          x))
      (NatTrans.app
        (Iso.hom
          (Iso.trans (Y := shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B) ⋙ F)
            (isoWhiskerRight (pullbackShiftIso C φ 0 ((φ : (a : A) → B) 0) ⋯) F :
              shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0 ⋙ F ≅
                shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B) ⋙ F)
            (Iso.trans (Y := F ⋙ shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) 0 : B))
                (commShiftIso F ((φ : (a : A) → B) 0))
                (F.isoWhiskerLeft (Iso.symm (pullbackShiftIso D φ 0 ((φ : (a : A) → B) 0) ⋯))) :
              shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B) ⋙ F ≅
                PullbackShift.functor φ F ⋙
                  shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0)))
        x)
      (NatTrans.app (Iso.hom (CommShift.isoZero (PullbackShift.functor φ F) A)) x)
⊢ Eq (α :=
    Iso (C :=
      Functor.{v_1, v_2, u_1, u_4} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (PullbackShift.{v_2, u_4, u_2, u_3} D φ))
      (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0 ⋙ PullbackShift.functor φ F)
      (PullbackShift.functor φ F ⋙ shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0))
    (Iso.trans (Y := shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B) ⋙ F)
      (isoWhiskerRight (pullbackShiftIso C φ 0 ((φ : (a : A) → B) 0) ⋯) F :
        shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0 ⋙ F ≅
          shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B) ⋙ F)
      (Iso.trans (Y := F ⋙ shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) 0 : B))
          (commShiftIso F ((φ : (a : A) → B) 0))
          (F.isoWhiskerLeft (Iso.symm (pullbackShiftIso D φ 0 ((φ : (a : A) → B) 0) ⋯))) :
        shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B) ⋙ F ≅
          PullbackShift.functor φ F ⋙ shiftFunctor.{v_2, u_4, u_2} (PullbackShift.{v_2, u_4, u_2, u_3} D φ) (A := A) 0))
    (CommShift.isoZero (PullbackShift.functor φ F) A)

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
x : PullbackShift.{v_1, u_1, u_2, u_3} C φ
rw rw₁ : Eq.{u_3 + 1} (α := B) 0 0
⊢ Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) 0 : B) (0 : B)

Tactic:
rw [map_zero]

Premises used: map_zero
-- 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
x x_1 : A
x_2 : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a :
  𝟙
    (obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
      (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_2)))
| CategoryStruct.comp (Y :=
    obj.{v_2, v_2, u_4, u_4} (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
      (obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x) (F.obj x_2)))
    (map (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
      (NatTrans.app (Iso.inv (pullbackShiftIso D φ x ((φ : (a : A) → B) x) ⋯)) (F.obj x_2)))
    (map (shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) x_1 : B))
      (NatTrans.app (Iso.hom (pullbackShiftIso D φ x ((φ : (a : A) → B) x) ⋯)) (F.obj x_2)))

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

Premises used: CategoryTheory.Functor.map_id, 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 : Functor.{v_1, v_2, u_1, u_4} C D
inst_6 : F.CommShift B
x x_1 : A
x_2 : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a :
  F.map
      (NatTrans.app (Iso.hom (pullbackShiftIso C φ x_1 ((φ : (a : A) → B) x_1) ⋯))
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)) ≫
    F.map
      (map (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B))
        (NatTrans.app (Iso.inv (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_2))
| F.map
      (map (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x_1)
        (NatTrans.app (Iso.inv (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_2)) ≫
    F.map
      (NatTrans.app (Iso.hom (pullbackShiftIso C φ x_1 ((φ : (a : A) → B) x_1) ⋯))
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_2))

Tactic:
rw [← map_comp, (pullbackShiftIso C φ _ _ rfl).hom.naturality, map_comp]

Premises used: CategoryTheory.pullbackShiftIso, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom, rfl
-- 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
x x_1 : A
x_2 : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a :
  𝟙
    (F.obj
      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B))
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))
| CategoryStruct.comp (Y :=
    F.obj
      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x_1)
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))
    (F.map
      (NatTrans.app (Iso.inv (pullbackShiftIso C φ x_1 ((φ : (a : A) → B) x_1) ⋯))
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))
    (F.map
      (NatTrans.app (Iso.hom (pullbackShiftIso C φ x_1 ((φ : (a : A) → B) x_1) ⋯))
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))

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

Premises used: CategoryTheory.Functor.map_id, 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 : Functor.{v_1, v_2, u_1, u_4} C D
inst_6 : F.CommShift B
x x_1 : A
x_2 : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a :
  𝟙
    (F.obj
      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B))
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x : B)) x_2)))
| CategoryStruct.comp (Y :=
    F.obj
      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B))
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_2)))
    (F.map
      (map (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B))
        (NatTrans.app (Iso.inv (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_2)))
    (F.map
      (map (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) x_1 : B))
        (NatTrans.app (Iso.hom (pullbackShiftIso C φ x ((φ : (a : A) → B) x) ⋯)) x_2)))

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

Premises used: CategoryTheory.Functor.map_id, 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
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
a : A
b : B
h : b = (φ : (a : A) → B) a
⊢ b = (φ : (a : A) → B) a

Tactic:
h
-- 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
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
a : A
b : B
h : b = (φ : (a : A) → B) a
obtain :
  Eq (α :=
    Iso (C :=
      Functor.{v_1, v_2, u_1, u_4} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (PullbackShift.{v_2, u_4, u_2, u_3} D φ))
      (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a ⋙ PullbackShift.functor φ F)
      (PullbackShift.functor φ F ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) a))
    (commShiftIso (PullbackShift.functor φ F) a)
    (Iso.trans (Y := shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a : B) ⋙ F)
      (isoWhiskerRight (pullbackShiftIso C φ a ((φ : (a : A) → B) a) ⋯) F :
        shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a ⋙ F ≅
          shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a : B) ⋙ F)
      (Iso.trans (Y := F ⋙ shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) a : B))
          (commShiftIso F ((φ : (a : A) → B) a))
          (F.isoWhiskerLeft (Iso.symm (pullbackShiftIso D φ a ((φ : (a : A) → B) a) ⋯))) :
        shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a : B) ⋙ F ≅
          F ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) a))
⊢ Eq (α :=
    Iso (C :=
      Functor.{v_1, v_2, u_1, u_4} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (PullbackShift.{v_2, u_4, u_2, u_3} D φ))
      (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a ⋙ PullbackShift.functor φ F)
      (PullbackShift.functor φ F ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) a))
    (commShiftIso (PullbackShift.functor φ F) a)
    (Iso.trans (Y := shiftFunctor C b ⋙ F) (isoWhiskerRight (pullbackShiftIso C φ a b h) F)
      (Iso.trans (Y := F ⋙ shiftFunctor D b) (commShiftIso F b)
        (F.isoWhiskerLeft (Iso.symm (pullbackShiftIso D φ a b h)))))

Tactic:
obtain rfl : b = φ a := h

Premises used: DFunLike.coe, rfl
-- 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
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
a : A
⊢ Eq (α :=
    Iso (C :=
      Functor.{v_1, v_2, u_1, u_4} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (PullbackShift.{v_2, u_4, u_2, u_3} D φ))
      (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a ⋙ PullbackShift.functor φ F)
      (PullbackShift.functor φ F ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) a))
    (commShiftIso (PullbackShift.functor φ F) a)
    (Iso.trans (Y := shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a : B) ⋙ F)
      (isoWhiskerRight (pullbackShiftIso C φ a ((φ : (a : A) → B) a) ⋯) F :
        shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a ⋙ F ≅
          shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a : B) ⋙ F)
      (Iso.trans (Y := F ⋙ shiftFunctor.{v_2, u_4, u_3} D (A := B) ((φ : (a : A) → B) a : B))
          (commShiftIso F ((φ : (a : A) → B) a))
          (F.isoWhiskerLeft (Iso.symm (pullbackShiftIso D φ a ((φ : (a : A) → B) a) ⋯))) :
        shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a : B) ⋙ F ≅
          F ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) a))

Tactic:
rfl
-- 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
τ : F ⟶ G
inst_8 : CommShift τ B
x : A
w :
  ∀ (x_1 : PullbackShift.{v_1, u_1, u_2, u_3} C φ),
    Eq (α :=
      Quiver.Hom (V := PullbackShift.{v_2, u_4, u_2, u_3} D φ)
        (obj (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x ⋙ PullbackShift.functor φ F) x_1)
        (obj (PullbackShift.functor φ G ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x) x_1))
      (app
        (Iso.hom (commShiftIso (PullbackShift.functor φ F) x) ≫
          whiskerRight (PullbackShift.natTrans φ τ) (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x))
        x_1)
      (app
        (whiskerLeft (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) (PullbackShift.natTrans φ τ) ≫
          Iso.hom (commShiftIso (PullbackShift.functor φ G) x))
        x_1)
⊢ Eq (α :=
    Quiver.Hom (V :=
      Functor.{v_1, v_2, u_1, u_4} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (PullbackShift.{v_2, u_4, u_2, u_3} D φ))
      (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x ⋙ PullbackShift.functor φ F)
      (PullbackShift.functor φ G ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x))
    (Iso.hom (commShiftIso (PullbackShift.functor φ F) x) ≫
      whiskerRight (PullbackShift.natTrans φ τ) (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x))
    (whiskerLeft (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) (PullbackShift.natTrans φ τ) ≫
      Iso.hom (commShiftIso (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 : Functor.{v_1, v_2, u_1, u_4} C D
inst_7 : G.CommShift B
τ : F ⟶ G
inst_8 : CommShift τ B
x : A
x_1 : PullbackShift.{v_1, u_1, u_2, u_3} C φ
w :
  Eq (α :=
    Quiver.Hom (V := PullbackShift.{v_2, u_4, u_2, u_3} D φ)
      (obj (PullbackShift.functor φ F)
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_1))
      (obj.{v_2, v_2, u_4, u_4} (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x)
        (obj (PullbackShift.functor φ G) x_1)))
    (app (Iso.hom (commShiftIso (PullbackShift.functor φ F) x)) x_1 ≫
      map (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x) (τ.app x_1))
    (τ.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) x_1) ≫
      app (Iso.hom (commShiftIso (PullbackShift.functor φ G) x)) x_1)
⊢ Eq (α :=
    Quiver.Hom (V := PullbackShift.{v_2, u_4, u_2, u_3} D φ)
      (obj (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x ⋙ PullbackShift.functor φ F) x_1)
      (obj (PullbackShift.functor φ G ⋙ shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x) x_1))
    (app
      (Iso.hom (commShiftIso (PullbackShift.functor φ F) x) ≫
        whiskerRight (PullbackShift.natTrans φ τ) (shiftFunctor (PullbackShift.{v_2, u_4, u_2, u_3} D φ) x))
      x_1)
    (app
      (whiskerLeft (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x) (PullbackShift.natTrans φ τ) ≫
        Iso.hom (commShiftIso (PullbackShift.functor φ G) x))
      x_1)

Tactic:
dsimp [PullbackShift.natTrans]

Premises used: CategoryTheory.PullbackShift.natTrans
-- 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
w :
  ∀ (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)
⊢ Eq (α :=
    Quiver.Hom (V :=
      Functor.{v_1, v_1, u_1, u_1} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (PullbackShift.{v_1, u_1, u_2, u_3} C φ))
      (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x ⋙ 𝟭 (PullbackShift.{v_1, u_1, u_2, u_3} C φ))
      (PullbackShift.functor φ (𝟭 C) ⋙ shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) x))
    (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))
    (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))

Tactic:
ext