awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
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 φ
| 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)))
have 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)))
Tactic: rw [← map_comp, Iso.inv_hom_id_app, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
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 φ
| 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))
have a : F.map
    (NatTrans.app (Iso.hom (pullbackShiftIso C φ x_1 ((φ : (a : A) → B) x_1) sorry))
      (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) sorry)) x_2))
Tactic: rw [← map_comp, (pullbackShiftIso C φ _ _ rfl).hom.naturality, map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
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 φ
| 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)))
have 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)))
Tactic: rw [← map_comp, Iso.inv_hom_id_app, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
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 φ
| 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)))
have 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)))
Tactic: rw [← map_comp, ← map_comp, Iso.inv_hom_id_app, map_id, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
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
⊢ 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)))))
have 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) sorry) 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) sorry))) :
      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: obtain rfl : b = φ a := h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
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 φ
⊢ 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)
have 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)
Tactic: dsimp [PullbackShift.natTrans]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Pullback (goal)
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 φ
| 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)))
have 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)))
Tactic: rw [← G.map_comp, Iso.inv_hom_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
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₂
⊢ 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)
have 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))
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
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₂
⊢ 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))
have 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)))
Tactic: apply natTrans_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
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₂
⊢ 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)))
have 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)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
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
⊢ 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)
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Quotient (goal)
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
⊢ 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))
have 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)))
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]