awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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)))
    ((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))))
have 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))))
Tactic: simp only [comp_id, id_comp, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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.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))))
have 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))))
Tactic: rw [← op_comp, adj.right_triangle_components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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 (α :=
    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))
have 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))))
Tactic: dsimp [OppositeShift.natTrans, NatTrans.OppositeShift.natIsoComp,
      NatTrans.OppositeShift.natIsoId, OppositeShift.functor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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)))
    ((𝟙 (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))))
have 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))))
Tactic: simp only [comp_id, id_comp, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Opposite (goal)
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 (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))))
have 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))))
Tactic: rw [← op_comp, adj.left_triangle_components]
-- 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
a : A
b : B
h : b = (φ : (a : A) → B) 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 C b)
have 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))
Tactic: subst 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 φ
⊢ 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))
have 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 sorry)) X))
Tactic: change (shiftFunctorZero C B).inv.app X ≫ _ = _
-- 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 φ
⊢ 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))
have 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 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) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero C B)) X) (NatTrans.app (Iso.inv (pullbackShiftIso C φ 0 0 sorry)) X))
Tactic: dsimp [Discrete.eqToHom, 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 φ
⊢ 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))
have 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 sorry)) (Iso.inv (pullbackShiftIso C φ 0 0 sorry))
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 φ
⊢ 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))
have 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)
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]
-- 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.{u_3 + 1} (α := B) ((φ : (a : A) → B) 0 : B) (0 : B)
have rw : Eq.{u_3 + 1} (α := B) 0 0
Tactic: rw [map_zero]
-- 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 φ
⊢ 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))
have 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 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) 0 : B)) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero' C ((φ : (a : A) → B) 0) sorry)) 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) sorry)) 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]
-- 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 φ
⊢ 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))
have 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 sorry))
  (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 sorry ≫
      𝟙
        (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]
-- 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 φ
⊢ 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)))
have 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 sorry))
  (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 sorry))
Tactic: erw [comp_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 φ
⊢ 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))
have 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)
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]
-- 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₃
⊢ b₁ + b₂ = b₃
have rw : HAdd.hAdd (α := B) ((φ : (a : A) → B) a₁ : B) b₂ = 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₃
rw : HAdd.hAdd (α := B) ((φ : (a : A) → B) a₁ : B) b₂ = b₃
⊢ b₁ + b₂ = b₃
have rw₁ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = 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₃
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₃
⊢ b₁ + b₂ = b₃
have rw₂ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) a₃
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₃
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₃
⊢ b₁ + b₂ = b₃
have rw₃ : HAdd.hAdd (α := B) (β := B) ((φ : (a : A) → B) a₁ : B) ((φ : (a : A) → B) a₂ : B) = (φ : (a : A) → B) (a₁ + a₂)
Tactic: rw [h₁, h₂, h₃, ← h, φ.map_add]