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 φ
simp :
  Eq.{v_1 + 1} (α :=
    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) (eqToHom ⋯))
    (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)
      (eqToHom ⋯ ≫
        𝟙
          (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.{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))

Tactic:
simp only [Functor.id_obj, pullbackShiftIso, eqToIso.inv, eqToHom_app, shiftFunctorZero',
    Iso.trans_inv, NatTrans.comp_app, eqToIso_refl, Iso.refl_inv, NatTrans.id_app, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_app, CategoryTheory.pullbackShiftIso, CategoryTheory.eqToIso_refl, CategoryTheory.shiftFunctorZero', CategoryTheory.Iso.refl_inv, CategoryTheory.Functor.id_obj, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Iso.trans_inv, CategoryTheory.eqToIso.inv
-- 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 φ
erw erw₁ :
  Eq.{v_1 + 1} (α :=
    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) (eqToHom ⋯))
    (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) (eqToHom ⋯))
⊢ Eq.{v_1 + 1} (α :=
    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) (eqToHom ⋯))
    (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)
      (eqToHom ⋯ ≫
        𝟙
          (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:
erw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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) ((φ : (a : A) → B) 0 : B)) X)
      (NatTrans.app (Iso.hom (pullbackShiftIso C φ 0 ((φ : (a : A) → B) 0) ⋯)) 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 ⟶
          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.hom (shiftFunctorZero' C ((φ : (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} (𝟭 C) 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.shiftFunctorZero, CategoryTheory.pullbackShiftFunctorZero'_inv_app, 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 φ
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 : HAdd.hAdd (α := B) ((φ : (a : A) → B) a₁ : B) b₂ = b₃
rw₁ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = b₃
rw₂ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) a₃
rw₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
rw₄ rw₅ :
  HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) =
    HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)
⊢ b₁ + b₂ = b₃

Tactic:
rw [h₁, h₂, h₃, ← h, φ.map_add]

Premises used: AddMonoidHom.map_add
-- 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₃
subst :
  ∀ (h₃ : b₃ = (φ : (a : A) → B) (a₁ + a₂)),
    Eq (α :=
      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₁ + a₂)) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd' (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ a₂ (a₁ + a₂) ⋯)) X)
      (Functor.map (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
          (NatTrans.app (Iso.hom (pullbackShiftIso C φ a₁ ((φ : (a : A) → B) 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) a₂ : B))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₁ : B)) X))
          (NatTrans.app (Iso.hom (pullbackShiftIso C φ a₂ ((φ : (a : A) → B) a₂) ⋯))
            (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor.{v_1, u_1, u_3} C (A := B) ((φ : (a : A) → B) a₁ : B)) X))
          (CategoryStruct.comp (Y := Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b₃) X)
            (NatTrans.app (Iso.inv (shiftFunctorAdd' C ((φ : (a : A) → B) a₁) ((φ : (a : A) → B) a₂) b₃ ⋯)) X)
            (NatTrans.app (Iso.inv (pullbackShiftIso C φ (a₁ + a₂) b₃ h₃)) X)))
⊢ Eq (α :=
    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₃) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd' (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ a₂ a₃ h)) X)
    (Functor.map (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₂)
        (NatTrans.app (Iso.hom (pullbackShiftIso C φ a₁ b₁ h₁)) X) ≫
      NatTrans.app (Iso.hom (pullbackShiftIso C φ a₂ b₂ h₂)) (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C b₁) X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C b₁ b₂ b₃ ⋯)) X ≫
          NatTrans.app (Iso.inv (pullbackShiftIso C φ a₃ b₃ h₃)) X)

Tactic:
subst h₁ h₂ 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
X : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a₁ a₂ : A
b₃ : B
h₃ : b₃ = (φ : (a : A) → B) (a₁ + a₂)
rw : (φ : (a : A) → B) (a₁ + a₂) = HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)
rw₁ rw₂ :
  HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) =
    HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)
⊢ b₃ = HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)

Tactic:
rw [h₃, φ.map_add]

Premises used: AddMonoidHom.map_add
-- 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
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
change :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
          (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B) { as := a₁ : Discrete A })
          (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B) { as := a₂ : Discrete A }))
        X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
            { as := a₂ : Discrete A }))
        X)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory B)
            ((Discrete.addMonoidalFunctor φ).obj { as := a₁ : Discrete A })
            ((Discrete.addMonoidalFunctor φ).obj { as := a₂ : Discrete A })))
        X)
      (NatTrans.app
        (Functor.LaxMonoidal.μ (shiftMonoidalFunctor C B) ((Discrete.addMonoidalFunctor φ).obj { as := a₁ })
          ((Discrete.addMonoidalFunctor φ).obj { as := a₂ }))
        X)
      (NatTrans.app
        (Functor.map (shiftMonoidalFunctor C B)
          (Functor.LaxMonoidal.μ (Discrete.addMonoidalFunctor φ) { as := a₁ } { as := a₂ }))
        X))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor C (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B))) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd C ((φ : (a : A) → B) a₁) ((φ : (a : A) → B) a₂))) X)
      (NatTrans.app
        (Iso.inv
          (pullbackShiftIso C φ (a₁ + a₂)
            (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
        X))
⊢ Eq.{v_1 + 1} (α :=
    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) ⟶
      Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor (PullbackShift.{v_1, u_1, u_2, u_3} C φ) (a₁ + a₂)) X)
    (NatTrans.app (Iso.inv (shiftFunctorAdd (PullbackShift.{v_1, u_1, u_2, u_3} C φ) a₁ a₂)) X)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor C (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B))) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd C ((φ : (a : A) → B) a₁) ((φ : (a : A) → B) a₂))) X)
      (NatTrans.app
        (Iso.inv
          (pullbackShiftIso C φ (a₁ + a₂)
            (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
        X))

Tactic:
change _ ≫ _ = _
-- 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
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
e_a :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory B)
            ((Discrete.addMonoidalFunctor φ).obj { as := a₁ : Discrete A })
            ((Discrete.addMonoidalFunctor φ).obj { as := a₂ : Discrete A })))
        X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
            { as := a₂ : Discrete A }))
        X)
    (NatTrans.app
      (Functor.map (shiftMonoidalFunctor C B)
        (Functor.LaxMonoidal.μ (Discrete.addMonoidalFunctor φ) { as := a₁ } { as := a₂ }))
      X)
    (NatTrans.app
      (Iso.inv
        (pullbackShiftIso C φ (a₁ + a₂)
          (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
      X)
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (MonoidalCategoryStruct.tensorObj (𝒞 := Functor.category)
          (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B) { as := a₁ : Discrete A })
          (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B) { as := a₂ : Discrete A }))
        X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
            { as := a₂ : Discrete A }))
        X)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory B)
            ((Discrete.addMonoidalFunctor φ).obj { as := a₁ : Discrete A })
            ((Discrete.addMonoidalFunctor φ).obj { as := a₂ : Discrete A })))
        X)
      (NatTrans.app
        (Functor.LaxMonoidal.μ (shiftMonoidalFunctor C B) ((Discrete.addMonoidalFunctor φ).obj { as := a₁ })
          ((Discrete.addMonoidalFunctor φ).obj { as := a₂ }))
        X)
      (NatTrans.app
        (Functor.map (shiftMonoidalFunctor C B)
          (Functor.LaxMonoidal.μ (Discrete.addMonoidalFunctor φ) { as := a₁ } { as := a₂ }))
        X))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, v_1, u_1, u_1}
        (shiftFunctor C (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B))) X)
      (NatTrans.app (Iso.inv (shiftFunctorAdd C ((φ : (a : A) → B) a₁) ((φ : (a : A) → B) a₂))) X)
      (NatTrans.app
        (Iso.inv
          (pullbackShiftIso C φ (a₁ + a₂)
            (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
        X))

Tactic:
congr 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
X : PullbackShift.{v_1, u_1, u_2, u_3} C φ
a₁ a₂ : A
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
e_a :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory B)
            ((Discrete.addMonoidalFunctor φ).obj { as := a₁ : Discrete A })
            ((Discrete.addMonoidalFunctor φ).obj { as := a₂ : Discrete A })))
        X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
            { as := a₂ : Discrete A }))
        X)
    (NatTrans.app (Functor.map (shiftMonoidalFunctor C B) (Discrete.eqToHom ⋯)) X)
    (NatTrans.app
      (Iso.inv
        (pullbackShiftIso C φ (a₁ + a₂)
          (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
      X)
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory B)
            ((Discrete.addMonoidalFunctor φ).obj { as := a₁ : Discrete A })
            ((Discrete.addMonoidalFunctor φ).obj { as := a₂ : Discrete A })))
        X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
            { as := a₂ : Discrete A }))
        X)
    (NatTrans.app
      (Functor.map (shiftMonoidalFunctor C B)
        (Functor.LaxMonoidal.μ (Discrete.addMonoidalFunctor φ) { as := a₁ } { as := a₂ }))
      X)
    (NatTrans.app
      (Iso.inv
        (pullbackShiftIso C φ (a₁ + a₂)
          (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
      X)

Tactic:
rw [Discrete.addMonoidalFunctor_μ]

Premises used: 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 φ
a₁ a₂ : A
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
e_a :
  Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory B) { as := (φ : (a : A) → B) a₁ : Discrete B }
            { as := (φ : (a : A) → B) a₂ : Discrete B }))
        X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          ((Discrete.addMonoidalFunctor φ).obj
            (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
              { as := a₂ : Discrete A })))
        X)
    (NatTrans.app (Functor.map (shiftMonoidalFunctor C B) (eqToHom ⋯)) X)
    (NatTrans.app
      (Iso.inv
        (pullbackShiftIso C φ (a₁ + a₂)
          (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
      X)
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory B)
            ((Discrete.addMonoidalFunctor φ).obj { as := a₁ : Discrete A })
            ((Discrete.addMonoidalFunctor φ).obj { as := a₂ : Discrete A })))
        X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (Discrete.addMonoidalFunctor φ ⋙ shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
            { as := a₂ : Discrete A }))
        X)
    (NatTrans.app (Functor.map (shiftMonoidalFunctor C B) (Discrete.eqToHom ⋯)) X)
    (NatTrans.app
      (Iso.inv
        (pullbackShiftIso C φ (a₁ + a₂)
          (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
      X)

Tactic:
dsimp [Discrete.eqToHom]

Premises used: CategoryTheory.Discrete.eqToHom
-- 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
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
e_a :
  Eq (α :=
    NatTrans.{v_1, v_1, u_1, u_1}
      (Functor.obj (shiftMonoidalFunctor C B)
        (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory B) { as := (φ : (a : A) → B) a₁ }
          { as := (φ : (a : A) → B) a₂ }))
      (Functor.obj (shiftMonoidalFunctor C B)
        ((Discrete.addMonoidalFunctor φ).obj
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
            { as := a₂ : Discrete A }))))
    (Functor.map (shiftMonoidalFunctor C B) (eqToHom ⋯))
    (Iso.inv
      (pullbackShiftIso C φ (a₁ + a₂)
        (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory B) { as := (φ : (a : A) → B) a₁ : Discrete B }
            { as := (φ : (a : A) → B) a₂ : Discrete B }))
        X ⟶
      Functor.obj.{v_1, v_1, u_1, u_1}
        (Functor.obj (shiftMonoidalFunctor C B)
          ((Discrete.addMonoidalFunctor φ).obj
            (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
              { as := a₂ : Discrete A })))
        X)
    (NatTrans.app (Functor.map (shiftMonoidalFunctor C B) (eqToHom ⋯)) X)
    (NatTrans.app
      (Iso.inv
        (pullbackShiftIso C φ (a₁ + a₂)
          (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))
      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 φ
a₁ a₂ : A
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
⊢ Eq (α :=
    NatTrans.{v_1, v_1, u_1, u_1}
      (Functor.obj (shiftMonoidalFunctor C B)
        (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory B) { as := (φ : (a : A) → B) a₁ }
          { as := (φ : (a : A) → B) a₂ }))
      (Functor.obj (shiftMonoidalFunctor C B)
        ((Discrete.addMonoidalFunctor φ).obj
          (MonoidalCategoryStruct.tensorObj (𝒞 := discreteCategory A) { as := a₁ : Discrete A }
            { as := a₂ : Discrete A }))))
    (Functor.map (shiftMonoidalFunctor C B) (eqToHom ⋯))
    (Iso.inv
      (pullbackShiftIso C φ (a₁ + a₂)
        (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)) h₃))

Tactic:
apply eqToHom_map

Premises used: CategoryTheory.eqToHom_map