awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (hypothesis)
Goal:
C : Type u_3
D : Type u_1
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_3, u_1} C D
A : Type u_2
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_3, u_2} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a b : A
X : C
⊢ (add F s i a b).hom.app (F.obj X) =
    NatTrans.app (Iso.hom (i (a + b))) X ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C a b)) X) ≫
        (i b).inv.app (obj.{v_1, v_1, u_3, u_3} (shiftFunctor C a) X) ≫ (s b).map ((i a).inv.app X)
have h : F.whiskerLeft (add F s i a b).hom =
  (i (a + b) ≪≫
      isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
        associator (shiftFunctor C a) (shiftFunctor C b) F ≪≫
          isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫
            Iso.symm (associator (shiftFunctor C a) F (s b)) ≪≫
              isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom
Tactic: have h : whiskerLeft F (add F s i a b).hom = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (hypothesis)
Goal:
C : Type u_2
D : Type u_1
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} D
F : Functor.{v_1, v_2, u_2, u_1} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_2, u_3} C A
s : A → Functor.{v_2, v_2, u_1, u_1} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_1, u_1} D D) (obj (whiskeringLeft C D D) F)
a b : A
X : C
⊢ (add F s i a b).inv.app (F.obj X) =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app (obj.{v_1, v_1, u_2, u_2} (shiftFunctor C a) X) ≫
        F.map (NatTrans.app (Iso.inv (shiftFunctorAdd C a b)) X) ≫ NatTrans.app (Iso.inv (i (a + b))) X
have h : F.whiskerLeft (add F s i a b).inv =
  (i (a + b) ≪≫
      isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
        associator (shiftFunctor C a) (shiftFunctor C b) F ≪≫
          isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫
            Iso.symm (associator (shiftFunctor C a) F (s b)) ≪≫
              isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv
Tactic: have h : whiskerLeft F (add F s i a b).inv = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (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
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
⊢ s (m₁ + m₂ + m₃) = s (m₁ + (m₂ + m₃))
have rw : s (m₁ + (m₂ + m₃)) = s (m₁ + (m₂ + m₃))
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (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
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
⊢ ∀ (X : D),
    NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) X ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫
        NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) X ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj X)
have suffices : Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
  eqToHom sorry ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom
Tactic: suffices (Induced.add F s i (m₁ + m₂) m₃).hom ≫
            whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
            eqToHom (by rw [add_assoc]) ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫
              whiskerLeft (s m₁) (Induced.add F s i m₂ m₃).hom by
          intro X
          simpa using NatTrans.congr_app this X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (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
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
⊢ Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
    eqToHom ⋯ ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom
have a : Eq (α :=
  obj (obj (whiskeringLeft C D D) F) (s (m₁ + m₂ + m₃)) ⟶ obj (obj (whiskeringLeft C D D) F) ((s m₁ ⋙ s m₂) ⋙ s m₃))
  (map (obj (whiskeringLeft C D D) F)
    (Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃)))
  (map (obj (whiskeringLeft C D D) F)
    (eqToHom sorry ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom))
Tactic: apply ((whiskeringLeft C D D).obj F).map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (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
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
⊢ Eq (α :=
    obj (obj (whiskeringLeft C D D) F) (s (m₁ + m₂ + m₃)) ⟶ obj (obj (whiskeringLeft C D D) F) ((s m₁ ⋙ s m₂) ⋙ s m₃))
    (map (obj (whiskeringLeft C D D) F)
      (Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃)))
    (map (obj (whiskeringLeft C D D) F)
      (eqToHom ⋯ ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom))
have a : ∀ (X : C),
  Eq (α :=
    (obj (obj (whiskeringLeft C D D) F) (s (m₁ + m₂ + m₃))).obj X ⟶
      (obj (obj (whiskeringLeft C D D) F) ((s m₁ ⋙ s m₂) ⋙ s m₃)).obj X)
    (NatTrans.app
      (map (obj (whiskeringLeft C D D) F)
        (Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃)))
      X)
    (NatTrans.app
      (map (obj (whiskeringLeft C D D) F)
        (eqToHom sorry ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (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
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
⊢ Eq (α :=
    (obj (obj (whiskeringLeft C D D) F) (s (m₁ + m₂ + m₃))).obj X ⟶
      (obj (obj (whiskeringLeft C D D) F) ((s m₁ ⋙ s m₂) ⋙ s m₃)).obj X)
    (NatTrans.app
      (map (obj (whiskeringLeft C D D) F)
        (Iso.hom (Induced.add F s i (m₁ + m₂) m₃) ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃)))
      X)
    (NatTrans.app
      (map (obj (whiskeringLeft C D D) F)
        (eqToHom ⋯ ≫ Iso.hom (Induced.add F s i m₁ (m₂ + m₃)) ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom))
      X)
have a : NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
    (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X)) =
  NatTrans.app (eqToHom sorry) (F.obj X) ≫
    NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
      (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
⊢ NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
      (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X)) =
    NatTrans.app (eqToHom ⋯) (F.obj X) ≫
      NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
        (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))
have eq : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
    F.obj
      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)))
  (F.map
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C (m₁ + m₂) m₃ (m₁ + m₂ + m₃) sorry)) X ≫
      map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) sorry)) X)))
  (F.map
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) sorry)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) sorry)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
Tactic: have eq := F.congr_map (shiftFunctorAdd'_assoc_hom_app
          m₁ m₂ m₃ _ _ (m₁ + m₂ + m₃) rfl rfl rfl X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C (m₁ + m₂) m₃ (m₁ + m₂ + m₃) ⋯)) X ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ m₂ (m₁ + m₂) ⋯)) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd' C m₂ m₃ (m₂ + m₃) ⋯)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
⊢ NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
      (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X)) =
    NatTrans.app (eqToHom ⋯) (F.obj X) ≫
      NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
        (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))
have eq₁ : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
    F.obj
      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)))
  (F.map
    (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X ≫
      map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
  (F.map
    (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) sorry)) X ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
Tactic: simp only [shiftFunctorAdd'_eq_shiftFunctorAdd] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁ ⋙ shiftFunctor C m₂) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X ≫
        map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map
      (NatTrans.app (Iso.hom (shiftFunctorAdd' C m₁ (m₂ + m₃) (m₁ + m₂ + m₃) ⋯)) X ≫
        NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
⊢ NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
      (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X)) =
    NatTrans.app (eqToHom ⋯) (F.obj X) ≫
      NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
        (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))
have eq₁ : Eq (α :=
  F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
    F.obj
      (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
  (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
    F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
  (F.map (eqToHom sorry) ≫
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
Tactic: simp only [Functor.comp_obj, Functor.map_comp, shiftFunctorAdd',
          Iso.trans_hom, eqToIso.hom, NatTrans.comp_app, eqToHom_app,
          Category.assoc] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (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
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
⊢ NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
      (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X)) =
    NatTrans.app (eqToHom ⋯) (F.obj X) ≫
      NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
        (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))
have a : (NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
      (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X))) ≫
    (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
  (NatTrans.app (eqToHom sorry) (F.obj X) ≫
      NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
        (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))) ≫
    (s m₃).map ((s m₂).map ((i m₁).hom.app X))
Tactic: rw [← cancel_mono ((s m₃).map ((s m₂).map ((i m₁).hom.app X)))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (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
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
⊢ (NatTrans.app (Iso.hom (Induced.add F s i (m₁ + m₂) m₃)) (F.obj X) ≫
        (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X))) ≫
      (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
    (NatTrans.app (eqToHom ⋯) (F.obj X) ≫
        NatTrans.app (Iso.hom (Induced.add F s i m₁ (m₂ + m₃))) (F.obj X) ≫
          (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))) ≫
      (s m₃).map ((s m₂).map ((i m₁).hom.app X))
have a : Eq (α := (s (m₁ + m₂ + m₃)).obj (F.obj X) ⟶ (s m₃).obj ((s m₂).obj ((shiftFunctor C m₁ ⋙ F).obj X)))
  (NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      (i m₃).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂)) X) ≫
        (s m₃).map (NatTrans.app (Iso.inv (i (m₁ + m₂))) X) ≫
          (s m₃).map (NatTrans.app (Iso.hom (i (m₁ + m₂))) X) ≫
            (s m₃).map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)) ≫
              (s m₃).map ((i m₂).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)) ≫
                (s m₃).map ((s m₂).map ((i m₁).inv.app X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X)))
  (NatTrans.app (eqToHom sorry) (F.obj X) ≫
    NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        NatTrans.app (Iso.inv (i (m₂ + m₃))) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X) ≫
          (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
            (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X)))
Tactic: simp only [Induced.add_hom_app_obj, Category.assoc, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (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
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
| (s m₃).map (NatTrans.app (Iso.inv (i (m₁ + m₂))) X) ≫ (s m₃).map (NatTrans.app (Iso.hom (i (m₁ + m₂))) X)
have a : 𝟙 ((s m₃).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂)) X)))
Tactic: erw [← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Shift.Induced (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
F : Functor.{v_1, v_2, u_1, u_2} C D
A : Type u_3
inst_2 : AddMonoid A
inst_3 : HasShift.{v_1, u_1, u_3} C A
s : A → Functor.{v_2, v_2, u_2, u_2} D D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst_4 : Full (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
inst_5 : Faithful (C := Functor.{v_2, v_2, u_2, u_2} D D) (obj (whiskeringLeft C D D) F)
m₁ m₂ m₃ : A
X : C
eq :
  Eq (α :=
    F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂ + m₃)) X) ⟶
      F.obj
        (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₃)
          (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₂) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))))
    (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      F.map (map (shiftFunctor C m₃) (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)))
    (F.map (eqToHom ⋯) ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₂ m₃)) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X)))
⊢ NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
        (i m₃).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂)) X) ≫
          (((𝟙 ((s m₃).obj (F.obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂)) X))) ≫
                  (s m₃).map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X))) ≫
                (s m₃).map ((i m₂).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))) ≫
              (s m₃).map ((s m₂).map ((i m₁).inv.app X))) ≫
            (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
    NatTrans.app (eqToHom ⋯) (F.obj X) ≫
      NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
        F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
          NatTrans.app (Iso.inv (i (m₂ + m₃))) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))
have a : NatTrans.app (Iso.hom (i (m₁ + m₂ + m₃))) X ≫
    F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C (m₁ + m₂) m₃)) X) ≫
      (i m₃).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (m₁ + m₂)) X) ≫
        (((s m₃).map (F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ m₂)) X)) ≫
              (s m₃).map ((i m₂).inv.app (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X))) ≫
            (s m₃).map ((s m₂).map ((i m₁).inv.app X))) ≫
          (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
  NatTrans.app (eqToHom sorry) (F.obj X) ≫
    NatTrans.app (Iso.hom (i (m₁ + (m₂ + m₃)))) X ≫
      F.map (NatTrans.app (Iso.hom (shiftFunctorAdd C m₁ (m₂ + m₃))) X) ≫
        NatTrans.app (Iso.inv (i (m₂ + m₃))) (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C m₁) X) ≫
          (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
            (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))
Tactic: erw [Category.id_comp]