Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: case a.a.a.a.a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (s m₃).map ((i (m₁ + m₂)).inv.app X) ≫ (s m₃).map ((i (m₁ + m₂)).hom.app X)

pp: case a.a.a.a.a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (s m₃).map (F.map ((shiftFunctorAdd C m₁ m₂).hom.app X))

pp: case a.a.a.a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X))

pp: case a.a.a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (s m₃).map ((s m₂).map ((i m₁).inv.app X))

pp: case a.a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (s m₃).map ((s m₂).map ((i m₁).hom.app X))

pp: case a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (i (m₁ + m₂ + m₃)).hom.app X

pp: case a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X)

pp: case a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (i m₃).inv.app ((shiftFunctor C (m₁ + m₂)).obj X)

Tactic:
erw [← Functor.map_comp, Iso.inv_hom_id_app, Functor.map_id]

Goal state after:
case a.a.a.a.a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| 𝟙 ((s m₃).obj (F.obj ((shiftFunctor C (m₁ + m₂)).obj X)))

case a.a.a.a.a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (s m₃).map (F.map ((shiftFunctorAdd C m₁ m₂).hom.app X))

case a.a.a.a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X))

case a.a.a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (s m₃).map ((s m₂).map ((i m₁).inv.app X))

case a.a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (s m₃).map ((s m₂).map ((i m₁).hom.app X))

case a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (i (m₁ + m₂ + m₃)).hom.app X

case a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X)

case a.a.a
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
| (i m₃).inv.app ((shiftFunctor C (m₁ + m₂)).obj X)