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₃
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₂)
⊢ b₁ + b₂ = b₃
have 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)
Tactic: rw [h₁, h₂, h₃, ← h, φ.map_add]
-- 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₃
⊢ 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)
have 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₂) sorry)) 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₁) sorry)) 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₂) sorry))
          (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₃ sorry)) X)
          (NatTrans.app (Iso.inv (pullbackShiftIso C φ (a₁ + a₂) b₃ h₃)) X)))
Tactic: subst h₁ h₂ h
Cleared hypotheses: a₃, h, b₁, b₂, h₁, h₂, 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
b₃ : B
h₃ : b₃ = (φ : (a : A) → B) (a₁ + a₂)
⊢ b₃ = HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)
have rw : (φ : (a : A) → B) (a₁ + a₂) = HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)
Tactic: rw [h₃, φ.map_add]
-- 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
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)
⊢ b₃ = HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B)
have 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)
Tactic: rw [h₃, φ.map_add]
-- 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
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
⊢ 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))
have 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))
Tactic: change _ ≫ _ = _
-- 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
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
⊢ 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))
have 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)
Tactic: congr 1
-- 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
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + 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)
have 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 sorry)) 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_μ]
-- 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
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + 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)
have 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 sorry)) 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]
-- 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
h₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + 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)
have 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 sorry))
  (Iso.inv
    (pullbackShiftIso C φ (a₁ + a₂) (HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B))
      h₃))
Tactic: congr 2
-- 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₃
⊢ 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))
have 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))
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]
-- 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
⊢ 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)
have 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) sorry) 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) sorry))) :
            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)
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
x : PullbackShift.{v_1, u_1, u_2, u_3} C φ
⊢ Eq.{u_3 + 1} (α := B) ((φ : (a : A) → B) 0 : B) (0 : B)
have rw : Eq.{u_3 + 1} (α := B) 0 0
Tactic: rw [map_zero]