mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g

Tactic:
← G.map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
⊢ G.map (h ≫ f) = G.map k ≫ G.map g
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
⊢ G.map (h ≫ f) = G.map k ≫ G.map g

Tactic:
← G.map_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst✝ : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
⊢ G.map (h ≫ f) = G.map (k ≫ g)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map
        ((adj.unit.app (𝟙_ C) ▷ G.obj X ≫ G.map (η F) ▷ G.obj X) ≫
          (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X) ≫
              G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
            G.map (λ_ X).hom) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    (F.map (adj.unit.app (𝟙_ C) ▷ G.obj X ≫ G.map (η F) ▷ G.obj X) ≫
        F.map
          ((adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X) ≫
              G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
            G.map (λ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    (F.map (adj.unit.app (𝟙_ C) ▷ G.obj X ≫ G.map (η F) ▷ G.obj X) ≫
        F.map
          ((adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X) ≫
              G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
            G.map (λ_ X).hom)) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫ F.map (G.map (η F) ▷ G.obj X)) ≫
        F.map
          ((adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X) ≫
              G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
            G.map (λ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫ F.map (G.map (η F) ▷ G.obj X)) ≫
        F.map
          ((adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X) ≫
              G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
            G.map (λ_ X).hom)) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫ F.map (G.map (η F) ▷ G.obj X)) ≫
        F.map
            (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X) ≫
              G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
          F.map (G.map (λ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫ F.map (G.map (η F) ▷ G.obj X)) ≫
        F.map
            (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X) ≫
              G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
          F.map (G.map (λ_ X).hom)) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫ F.map (G.map (η F) ▷ G.obj X)) ≫
        (F.map (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X)) ≫
            F.map (G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X)))) ≫
          F.map (G.map (λ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫ F.map (G.map (η F) ▷ G.obj X)) ≫
        (F.map (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X)) ≫
            F.map (G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X)))) ≫
          F.map (G.map (λ_ X).hom)) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫ F.map (G.map (η F) ▷ G.obj X)) ≫
        (F.map (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X)) ≫
            F.map (G.map (δ F (G.obj (𝟙_ D)) (G.obj X)) ≫ G.map (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
          F.map (G.map (λ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫ F.map (G.map (η F) ▷ G.obj X)) ≫
        (F.map (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X)) ≫
            F.map (G.map (δ F (G.obj (𝟙_ D)) (G.obj X)) ≫ G.map (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
          F.map (G.map (λ_ X).hom)) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (adj.unit.app (𝟙_ C) ▷ G.obj X) ≫ F.map (G.map (η F) ▷ G.obj X)) ≫
        (F.map (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X)) ≫
            F.map (G.map (δ F (G.obj (𝟙_ D)) (G.obj X))) ≫ F.map (G.map (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
          F.map (G.map (λ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map
        ((G.obj X ◁ adj.unit.app (𝟙_ C) ≫ G.obj X ◁ G.map (η F)) ≫
          (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D)) ≫
              G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
            G.map (ρ_ X).hom) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    (F.map (G.obj X ◁ adj.unit.app (𝟙_ C) ≫ G.obj X ◁ G.map (η F)) ≫
        F.map
          ((adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D)) ≫
              G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
            G.map (ρ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    (F.map (G.obj X ◁ adj.unit.app (𝟙_ C) ≫ G.obj X ◁ G.map (η F)) ≫
        F.map
          ((adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D)) ≫
              G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
            G.map (ρ_ X).hom)) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫ F.map (G.obj X ◁ G.map (η F))) ≫
        F.map
          ((adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D)) ≫
              G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
            G.map (ρ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫ F.map (G.obj X ◁ G.map (η F))) ≫
        F.map
          ((adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D)) ≫
              G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
            G.map (ρ_ X).hom)) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫ F.map (G.obj X ◁ G.map (η F))) ≫
        F.map
            (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D)) ≫
              G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
          F.map (G.map (ρ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫ F.map (G.obj X ◁ G.map (η F))) ≫
        F.map
            (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D)) ≫
              G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
          F.map (G.map (ρ_ X).hom)) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫ F.map (G.obj X ◁ G.map (η F))) ≫
        (F.map (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D))) ≫
            F.map (G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D))))) ≫
          F.map (G.map (ρ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫ F.map (G.obj X ◁ G.map (η F))) ≫
        (F.map (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D))) ≫
            F.map (G.map (δ F (G.obj X) (G.obj (𝟙_ D)) ≫ (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D))))) ≫
          F.map (G.map (ρ_ X).hom)) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫ F.map (G.obj X ◁ G.map (η F))) ≫
        (F.map (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D))) ≫
            F.map (G.map (δ F (G.obj X) (G.obj (𝟙_ D))) ≫ G.map (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
          F.map (G.map (ρ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫ F.map (G.obj X ◁ G.map (η F))) ≫
        (F.map (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D))) ≫
            F.map (G.map (δ F (G.obj X) (G.obj (𝟙_ D))) ≫ G.map (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
          F.map (G.map (ρ_ X).hom)) ≫
      adj.counit.app X

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    ((F.map (G.obj X ◁ adj.unit.app (𝟙_ C)) ≫ F.map (G.obj X ◁ G.map (η F))) ≫
        (F.map (adj.unit.app (G.obj X ⊗ G.obj (𝟙_ D))) ≫
            F.map (G.map (δ F (G.obj X) (G.obj (𝟙_ D)))) ≫ F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
          F.map (G.map (ρ_ X).hom)) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ (PushoutCocone.unop (colimit.cocone (span f.op g.op))).π.app WalkingCospan.left = (pushout.inl f.op g.op).unop

Tactic:
by simp [unop_id (X := { unop := X })]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
    μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫
      G.map
        ((F.map (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫
              F.map (μ G (F.obj X) (F.obj Y)) ≫ adj.counit.app (F.obj X ⊗ F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom)

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
    μ G (F.obj (X ⊗ Y)) (F.obj Z) ≫
      G.map
          ((F.map (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫
              F.map (μ G (F.obj X) (F.obj Y)) ≫ adj.counit.app (F.obj X ⊗ F.obj Y)) ▷
            F.obj Z) ≫
        G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
    G.map
          (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫
            F.map (μ G (F.obj X) (F.obj Y)) ≫ adj.counit.app (F.obj X ⊗ F.obj Y)) ▷
        G.obj (F.obj Z) ≫
      μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
    (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
          G.map (F.map (μ G (F.obj X) (F.obj Y)) ≫ adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
        G.obj (F.obj Z) ≫
      μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
    (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
          G.map (F.map (μ G (F.obj X) (F.obj Y)) ≫ adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
        G.obj (F.obj Z) ≫
      μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (adj.unit.app (X ⊗ Y) ⊗ₘ adj.unit.app Z) ≫
    (G.map (F.map (adj.unit.app X ⊗ₘ adj.unit.app Y)) ≫
          G.map (F.map (μ G (F.obj X) (F.obj Y))) ≫ G.map (adj.counit.app (F.obj X ⊗ F.obj Y))) ▷
        G.obj (F.obj Z) ≫
      μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (α_ X Y Z).hom ≫
    (adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫
      G.obj (F.obj X) ◁
          G.map
            (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫
              F.map (μ G (F.obj Y) (F.obj Z)) ≫ adj.counit.app (F.obj Y ⊗ F.obj Z)) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
map_comp,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (α_ X Y Z).hom ≫
    (adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫
      G.obj (F.obj X) ◁
          (G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
            G.map (F.map (μ G (F.obj Y) (F.obj Z)) ≫ adj.counit.app (F.obj Y ⊗ F.obj Z))) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)