awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F_1 F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
x : OppositeShift.{v_2, u_2, u_3} D A
simp :
  Eq.{v_1 + 1} (α := Opposite.op (G.obj (Opposite.unop x)) ⟶ Opposite.op (G.obj (Opposite.unop x)))
    (Quiver.Hom.op (G.map (adj.counit.app (Opposite.unop x))) ≫ Quiver.Hom.op (adj.unit.app (G.obj (Opposite.unop x))))
    (𝟙 (Opposite.op (G.obj (Opposite.unop x))))
⊢ Eq.{v_1 + 1} (α := Opposite.op (G.obj (Opposite.unop x)) ⟶ Opposite.op (G.obj (Opposite.unop x)))
    ((G.map
          (𝟙 x ≫
              Quiver.Hom.op (adj.counit.app (Opposite.unop x)) ≫
                𝟙 (Opposite.op (F.obj (G.obj (Opposite.unop x))))).unop).op ≫
      𝟙 (Opposite.op (G.obj (F.obj (G.obj (Opposite.unop x))))) ≫
        Quiver.Hom.op (adj.unit.app (G.obj (Opposite.unop x))) ≫ 𝟙 (Opposite.op (G.obj (Opposite.unop x))))
    (𝟙 (Opposite.op (G.obj (Opposite.unop x))))

Tactic:
simp only [comp_id, id_comp, Quiver.Hom.unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F_1 F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
x : OppositeShift.{v_2, u_2, u_3} D A
rw :
  Eq.{v_1 + 1} (α := Opposite.op (G.obj (Opposite.unop x)) ⟶ Opposite.op (G.obj (Opposite.unop x)))
    (Quiver.Hom.op (𝟙 (G.obj (Opposite.unop x)))) (𝟙 (Opposite.op (G.obj (Opposite.unop x))))
⊢ Eq.{v_1 + 1} (α := Opposite.op (G.obj (Opposite.unop x)) ⟶ Opposite.op (G.obj (Opposite.unop x)))
    (Quiver.Hom.op (G.map (adj.counit.app (Opposite.unop x))) ≫ Quiver.Hom.op (adj.unit.app (G.obj (Opposite.unop x))))
    (𝟙 (Opposite.op (G.obj (Opposite.unop x))))

Tactic:
rw [← op_comp, adj.right_triangle_components]

Premises used: CategoryTheory.op_comp, CategoryTheory.Adjunction.right_triangle_components
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F_1 F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
x : OppositeShift.{v_2, u_2, u_3} D A
⊢ Eq.{v_1 + 1} (α := Opposite.op (G.obj (Opposite.unop x)) ⟶ Opposite.op (G.obj (Opposite.unop x)))
    (Quiver.Hom.op (𝟙 (G.obj (Opposite.unop x)))) (𝟙 (Opposite.op (G.obj (Opposite.unop x))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F_1 F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
x : OppositeShift.{v_1, u_1, u_3} C A
dsimp :
  Eq.{v_2 + 1} (α := Opposite.op (F.obj (Opposite.unop x)) ⟶ Opposite.op (F.obj (Opposite.unop x)))
    ((𝟙 (Opposite.op (F.obj (Opposite.unop x))) ≫
        Quiver.Hom.op (adj.counit.app (F.obj (Opposite.unop x))) ≫
          𝟙 (Opposite.op (F.obj (G.obj (F.obj (Opposite.unop x)))))) ≫
      (F.map
          (𝟙 (Opposite.op (G.obj (F.obj (Opposite.unop x)))) ≫
              Quiver.Hom.op (adj.unit.app (Opposite.unop x)) ≫ 𝟙 x).unop).op)
    (𝟙 (Opposite.op (F.obj (Opposite.unop x))))
⊢ Eq (α :=
    Quiver.Hom (V := OppositeShift.{v_2, u_2, u_3} D A) (Functor.obj (functor A F) x) (Functor.obj (functor A F) x))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := OppositeShift.{v_1, u_1, u_3} C A) (functor A F)
        (Functor.obj (C := OppositeShift.{v_2, u_2, u_3} D A) (functor A G) (Functor.obj (functor A F) x)))
      (NatTrans.app
        (Iso.hom (NatTrans.OppositeShift.natIsoId D A) ≫
          natTrans A adj.counit ≫ Iso.hom (NatTrans.OppositeShift.natIsoComp A G F))
        (Functor.obj (functor A F) x))
      (Functor.map (functor A F)
        (NatTrans.app
          (Iso.inv (NatTrans.OppositeShift.natIsoComp A F G) ≫
            natTrans A adj.unit ≫ Iso.inv (NatTrans.OppositeShift.natIsoId C A))
          x)))
    (𝟙 (Functor.obj (functor A F) x))

Tactic:
dsimp [OppositeShift.natTrans, NatTrans.OppositeShift.natIsoComp,
      NatTrans.OppositeShift.natIsoId, OppositeShift.functor]

Premises used: CategoryTheory.OppositeShift.natTrans, CategoryTheory.NatTrans.OppositeShift.natIsoComp, CategoryTheory.OppositeShift.functor, CategoryTheory.NatTrans.OppositeShift.natIsoId
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F_1 F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
x : OppositeShift.{v_1, u_1, u_3} C A
simp :
  Eq.{v_2 + 1} (α := Opposite.op (F.obj (Opposite.unop x)) ⟶ Opposite.op (F.obj (Opposite.unop x)))
    (Quiver.Hom.op (adj.counit.app (F.obj (Opposite.unop x))) ≫ Quiver.Hom.op (F.map (adj.unit.app (Opposite.unop x))))
    (𝟙 (Opposite.op (F.obj (Opposite.unop x))))
⊢ Eq.{v_2 + 1} (α := Opposite.op (F.obj (Opposite.unop x)) ⟶ Opposite.op (F.obj (Opposite.unop x)))
    ((𝟙 (Opposite.op (F.obj (Opposite.unop x))) ≫
        Quiver.Hom.op (adj.counit.app (F.obj (Opposite.unop x))) ≫
          𝟙 (Opposite.op (F.obj (G.obj (F.obj (Opposite.unop x)))))) ≫
      (F.map
          (𝟙 (Opposite.op (G.obj (F.obj (Opposite.unop x)))) ≫
              Quiver.Hom.op (adj.unit.app (Opposite.unop x)) ≫ 𝟙 x).unop).op)
    (𝟙 (Opposite.op (F.obj (Opposite.unop x))))

Tactic:
simp only [comp_id, id_comp, Quiver.Hom.unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F_1 F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
x : OppositeShift.{v_1, u_1, u_3} C A
rw :
  Eq.{v_2 + 1} (α := Opposite.op (F.obj (Opposite.unop x)) ⟶ Opposite.op (F.obj (Opposite.unop x)))
    (Quiver.Hom.op (𝟙 (F.obj (Opposite.unop x)))) (𝟙 (Opposite.op (F.obj (Opposite.unop x))))
⊢ Eq.{v_2 + 1} (α := Opposite.op (F.obj (Opposite.unop x)) ⟶ Opposite.op (F.obj (Opposite.unop x)))
    (Quiver.Hom.op (adj.counit.app (F.obj (Opposite.unop x))) ≫ Quiver.Hom.op (F.map (adj.unit.app (Opposite.unop x))))
    (𝟙 (Opposite.op (F.obj (Opposite.unop x))))

Tactic:
rw [← op_comp, adj.left_triangle_components]

Premises used: CategoryTheory.op_comp, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F_1 F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
x : OppositeShift.{v_1, u_1, u_3} C A
⊢ Eq.{v_2 + 1} (α := Opposite.op (F.obj (Opposite.unop x)) ⟶ Opposite.op (F.obj (Opposite.unop x)))
    (Quiver.Hom.op (𝟙 (F.obj (Opposite.unop x)))) (𝟙 (Opposite.op (F.obj (Opposite.unop x))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
⊢ NatTrans.CommShift (C := OppositeShift.{v_2, u_2, u_3} D A) (F₂ :=
    Functor.comp (D := OppositeShift.{v_1, u_1, u_3} C A) (OppositeShift.functor A G) (OppositeShift.functor A F))
    (Iso.hom (NatTrans.OppositeShift.natIsoId D A) ≫
      OppositeShift.natTrans A adj.counit ≫ Iso.hom (NatTrans.OppositeShift.natIsoComp A G F))
    A

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Shift.Opposite
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
inst_4 : HasShift.{v_2, u_2, u_3} D A
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_5 : F.CommShift A
inst_6 : G.CommShift A
inst_7 : adj.CommShift A
⊢ NatTrans.CommShift (C := OppositeShift.{v_1, u_1, u_3} C A) (F₁ :=
    Functor.comp (D := OppositeShift.{v_2, u_2, u_3} D A) (OppositeShift.functor A F) (OppositeShift.functor A G))
    (Iso.inv (NatTrans.OppositeShift.natIsoComp A F G) ≫
      OppositeShift.natTrans A adj.unit ≫ Iso.inv (NatTrans.OppositeShift.natIsoId C A))
    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
inst_4 : HasZeroObject.{v_1, u_1} C
⊢ HasZeroObject.{v_1, u_1} (PullbackShift.{v_1, u_1, u_2, u_3} C φ)

Tactic:
inferInstanceAs <| HasZeroObject C

Premises used: _private.0.CategoryTheory.instHasZeroObjectPullbackShift._proof_1
-- 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
inst_4 : Preadditive.{v_1, u_1} C
a : A
inst_5 : Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a : B))
⊢ Functor.Additive.{v_1, u_1, v_1, u_1} (C := PullbackShift.{v_1, u_1, u_2, u_3} C φ)
    (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a)

Tactic:
inferInstanceAs (shiftFunctor C (φ a)).Additive

Premises used: _private.0.CategoryTheory.instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom._proof_1
-- 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
a : A
b : B
h : b = (φ : (a : A) → B) a
subst :
  Eq (α :=
    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 φ) a)
    (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a : B))
⊢ Eq (α :=
    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 φ) a) (shiftFunctor C b)

Tactic:
subst 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
a : A
⊢ Eq (α :=
    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 φ) a)
    (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a : B))

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₃
⊢ Eq.{u_3 + 1} (α := B) (0 : B) ((φ : (a : A) → B) 0 : B)

Tactic:
simp
-- 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 φ
change :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)))
        X)
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) 0) X)
      (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X)
      (NatTrans.app (Functor.map (shiftMonoidalFunctor C B) (Functor.LaxMonoidal.ε (Discrete.addMonoidalFunctor φ))) X))
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) 0) X)
      (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X) (NatTrans.app (Iso.inv (pullbackShiftIso C φ 0 0 ⋯)) X))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 (PullbackShift.{v_1, u_1, u_2, u_3} C φ)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero (PullbackShift.{v_1, u_1, u_2, u_3} C φ) A)) X)
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) 0) X)
      (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X) (NatTrans.app (Iso.inv (pullbackShiftIso C φ 0 0 ⋯)) X))

Tactic:
change (shiftFunctorZero C B).inv.app X ≫ _ = _

Premises used: CategoryTheory.shiftFunctorZero, CategoryTheory.Iso.inv, 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 φ
dsimp :
  Eq.{v_1 + 1} (α :=
    X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          ((Discrete.addMonoidalFunctor φ).obj
            (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))))
        X)
    (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X ≫
      NatTrans.app (Functor.map (shiftMonoidalFunctor C B) (eqToHom ⋯)) X)
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) 0) X)
      (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X) (NatTrans.app (Iso.inv (pullbackShiftIso C φ 0 0 ⋯)) X))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)))
        X)
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) 0) X)
      (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X)
      (NatTrans.app (Functor.map (shiftMonoidalFunctor C B) (Functor.LaxMonoidal.ε (Discrete.addMonoidalFunctor φ))) X))
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) 0) X)
      (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X) (NatTrans.app (Iso.inv (pullbackShiftIso C φ 0 0 ⋯)) X))

Tactic:
dsimp [Discrete.eqToHom, Discrete.addMonoidalFunctor_ε]

Premises used: CategoryTheory.Discrete.eqToHom, CategoryTheory.Discrete.addMonoidalFunctor_ε
-- 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 φ
e_a :
  Eq (α :=
    NatTrans.{v_1, v_1, u_1, u_1}
      (Functor.obj (shiftMonoidalFunctor C B)
        (MonoidalCategoryStruct.tensorUnit (Discrete B) (𝒞 := discreteCategory B)))
      (Functor.obj (shiftMonoidalFunctor C B)
        ((Discrete.addMonoidalFunctor φ).obj
          (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)))))
    (Functor.map (shiftMonoidalFunctor C B) (eqToHom ⋯)) (Iso.inv (pullbackShiftIso C φ 0 0 ⋯))
⊢ Eq.{v_1 + 1} (α :=
    X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          ((Discrete.addMonoidalFunctor φ).obj
            (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A))))
        X)
    (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X ≫
      NatTrans.app (Functor.map (shiftMonoidalFunctor C B) (eqToHom ⋯)) X)
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) 0) X)
      (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X) (NatTrans.app (Iso.inv (pullbackShiftIso C φ 0 0 ⋯)) X))

Tactic:
congr 2
-- 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 φ
⊢ Eq (α :=
    NatTrans.{v_1, v_1, u_1, u_1}
      (Functor.obj (shiftMonoidalFunctor C B)
        (MonoidalCategoryStruct.tensorUnit (Discrete B) (𝒞 := discreteCategory B)))
      (Functor.obj (shiftMonoidalFunctor C B)
        ((Discrete.addMonoidalFunctor φ).obj
          (MonoidalCategoryStruct.tensorUnit (Discrete A) (𝒞 := discreteCategory A)))))
    (Functor.map (shiftMonoidalFunctor C B) (eqToHom ⋯)) (Iso.inv (pullbackShiftIso C φ 0 0 ⋯))

Tactic:
apply eqToHom_map

Premises used: CategoryTheory.eqToHom_map
-- 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 φ
rw :
  𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 (PullbackShift.{v_1, u_1, u_2, u_3} C φ)) X) =
    𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X)
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0)
        X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 (PullbackShift.{v_1, u_1, u_2, u_3} C φ)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero (PullbackShift.{v_1, u_1, u_2, u_3} C φ) A)) X)
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) 0) X)
      (NatTrans.app (Iso.hom (pullbackShiftIso C φ 0 0 ⋯)) X) (NatTrans.app (Iso.hom (shiftFunctorZero C B)) X))

Tactic:
rw [← cancel_epi ((shiftFunctorZero _ A).inv.app X), Iso.inv_hom_id_app,
    pullbackShiftFunctorZero_inv_app, assoc, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.pullbackShiftFunctorZero_inv_app, CategoryTheory.shiftFunctorZero, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Iso.inv, 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 φ
⊢ 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 (PullbackShift.{v_1, u_1, u_2, u_3} C φ)) X) =
    𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) 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₃
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 φ
rw :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 (PullbackShift.{v_1, u_1, u_2, u_3} C φ)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0) X)
    (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) 0) X)
      (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X) (NatTrans.app (Iso.inv (pullbackShiftIso C φ 0 0 ⋯)) X))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) X)
      (NatTrans.app (Iso.inv (shiftFunctorZero' C ((φ : (a : A) → B) 0) ⋯)) X :
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) X)
      (NatTrans.app (Iso.inv (pullbackShiftIso C φ 0 ((φ : (a : A) → B) 0) ⋯)) X :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) X ⟶
          Functor.obj.{v_1, v_1, u_1, u_1}
            (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0) X))
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 (PullbackShift.{v_1, u_1, u_2, u_3} C φ)) X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero (PullbackShift.{v_1, u_1, u_2, u_3} C φ) A)) X)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) X)
      (NatTrans.app (Iso.inv (shiftFunctorZero' C ((φ : (a : A) → B) 0) ⋯)) X :
        Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 C) X ⟶
          Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) X)
      (NatTrans.app (Iso.inv (pullbackShiftIso C φ 0 ((φ : (a : A) → B) 0) ⋯)) X :
        Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) 0 : B)) X ⟶
          Functor.obj.{v_1, v_1, u_1, u_1}
            (shiftFunctor.{v_1, u_1, u_2} (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (A := A) 0) X))

Tactic:
rw [pullbackShiftFunctorZero_inv_app]

Premises used: CategoryTheory.pullbackShiftFunctorZero_inv_app