mathlib-initiative/mathlib-tactics huggingface dataset:
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)))) ≫ F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
          F.map (G.map (ρ_ X).hom)) ≫
        adj.counit.app X

Tactic:
assoc,

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.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)))) ≫
                F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
            F.map (G.map (ρ_ X).hom)) ≫
          adj.counit.app X

Tactic:
assoc,

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.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)))) ≫ F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
          F.map (G.map (ρ_ X).hom) ≫ adj.counit.app X

Tactic:
assoc,

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.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)))) ≫ F.map (G.map (adj.counit.app X ⊗ₘ adj.counit.app (𝟙_ D)))) ≫
            F.map (G.map (ρ_ X).hom) ≫ adj.counit.app X

Tactic:
assoc,

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.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 (G.obj X) (𝟙_ C) ≫
      F.obj (G.obj X) ◁ F.map (adj.unit.app (𝟙_ C)) ≫
        F.obj (G.obj X) ◁ F.map (G.map (η F)) ≫
          (adj.counit.app X ▷ F.obj (G.obj (𝟙_ D)) ≫ X ◁ adj.counit.app (𝟙_ D)) ≫ (ρ_ X).hom

Tactic:
assoc,

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 (G.obj X) (𝟙_ C) ≫
      F.obj (G.obj X) ◁ F.map (adj.unit.app (𝟙_ C)) ≫
        F.obj (G.obj X) ◁ F.map (G.map (η F)) ≫
          adj.counit.app X ▷ F.obj (G.obj (𝟙_ D)) ≫ X ◁ adj.counit.app (𝟙_ D) ≫ (ρ_ X).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✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    δ F (G.obj X) (𝟙_ C) ≫
      F.obj (G.obj X) ◁ ((F.map (adj.unit.app (𝟙_ C)) ≫ F.map (G.map (η F))) ≫ adj.counit.app (𝟙_ D)) ≫
        adj.counit.app X ▷ 𝟙_ D ≫ (ρ_ X).hom

Tactic:
assoc,

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 (G.obj X) (𝟙_ C) ≫
      F.obj (G.obj X) ◁ (F.map (adj.unit.app (𝟙_ C)) ≫ F.map (G.map (η F)) ≫ adj.counit.app (𝟙_ D)) ≫
        adj.counit.app X ▷ 𝟙_ D ≫ (ρ_ X).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✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    δ F (G.obj X) (𝟙_ C) ≫
      F.obj (G.obj X) ◁ η F ≫ ((ρ_ (F.obj (G.obj X))).hom ≫ adj.counit.app X ≫ (ρ_ X).inv) ≫ (ρ_ X).hom

Tactic:
assoc,

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 (G.obj X) (𝟙_ C) ≫
      F.obj (G.obj X) ◁ η F ≫ (ρ_ (F.obj (G.obj X))).hom ≫ (adj.counit.app X ≫ (ρ_ X).inv) ≫ (ρ_ X).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✝ : F.OplaxMonoidal
X : D
⊢ F.map (ρ_ (G.obj X)).hom ≫ adj.counit.app X =
    δ F (G.obj X) (𝟙_ C) ≫
      F.obj (G.obj X) ◁ η F ≫ (ρ_ (F.obj (G.obj X))).hom ≫ (adj.counit.app X ≫ (ρ_ X).inv) ≫ (ρ_ X).hom

Tactic:
assoc,

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 (G.obj X) (𝟙_ C) ≫
      F.obj (G.obj X) ◁ η F ≫ (ρ_ (F.obj (G.obj X))).hom ≫ adj.counit.app X ≫ (ρ_ X).inv ≫ (ρ_ X).hom
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
f : Arrow (Type u)
x₁ x₂ :
  (fun X ↦ X)
    ({ obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
          map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
          map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
          map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.obj
      f)
h :
  (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₁ =
    (hom ({ app := fun x ↦ ↾fun y ↦ ↑y, naturality := functorialSurjectiveInjectiveFactorizationData._proof_5 }.app f))
      x₂
⊢ x₁ = x₂

Tactic:
by
    rw [Subtype.ext_iff]
    exact h

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✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (adj.homEquiv (X✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
      (((adj.unit.app X✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj X✝) (F.obj x✝)) ≫ G.map (F.map x✝¹ ▷ F.obj x✝)) =
    (adj.homEquiv (X✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
      (x✝¹ ▷ x✝ ≫ (adj.unit.app Y✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj Y✝) (F.obj x✝))

Tactic:
assoc,

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✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (adj.homEquiv (X✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
      ((adj.unit.app X✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj X✝) (F.obj x✝) ≫ G.map (F.map x✝¹ ▷ F.obj x✝)) =
    (adj.homEquiv (X✝ ⊗ x✝) (F.obj Y✝ ⊗ F.obj x✝)).symm
      (x✝¹ ▷ x✝ ≫ (adj.unit.app Y✝ ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj Y✝) (F.obj 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✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
      (((adj.unit.app x✝¹ ⊗ₘ adj.unit.app X✝) ≫ μ G (F.obj x✝¹) (F.obj X✝)) ≫ G.map (F.obj x✝¹ ◁ F.map x✝)) =
    (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
      (x✝¹ ◁ x✝ ≫ (adj.unit.app x✝¹ ⊗ₘ adj.unit.app Y✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝))

Tactic:
assoc,

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✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
      ((adj.unit.app x✝¹ ⊗ₘ adj.unit.app X✝) ≫ μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (F.obj x✝¹ ◁ F.map x✝)) =
    (adj.homEquiv (x✝¹ ⊗ X✝) (F.obj x✝¹ ⊗ F.obj Y✝)).symm
      (x✝¹ ◁ x✝ ≫ (adj.unit.app x✝¹ ⊗ₘ adj.unit.app Y✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝))
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
        ((adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm
              ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
            F.obj Z ≫
          (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) =
    (α_ X Y Z).hom ≫
      ((adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
        G.map
          (F.obj X ◁
            (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))

Tactic:
assoc,

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
          ((adj.homEquiv (X ⊗ Y) (F.obj X ⊗ F.obj Y)).symm
                ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷
              F.obj Z ≫
            (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) =
    (α_ X Y Z).hom ≫
      ((adj.unit.app X ⊗ₘ adj.unit.app (Y ⊗ Z)) ≫ μ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
        G.map
          (F.obj X ◁
            (adj.homEquiv (Y ⊗ Z) (F.obj Y ⊗ F.obj Z)).symm
              ((adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ μ G (F.obj Y) (F.obj Z)))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
⊢ HasPushout f.op g.op

Tactic:
rwa [hasPushout_op_iff_hasPullback]

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 ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      (G.obj (F.obj X) ◁ (adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫ G.obj (F.obj X) ◁ μ G (F.obj Y) (F.obj Z)) ≫
        μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
assoc,

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 ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      G.obj (F.obj X) ◁ (adj.unit.app Y ⊗ₘ adj.unit.app Z) ≫
        G.obj (F.obj X) ◁ μ G (F.obj Y) (F.obj Z) ≫ μ G (F.obj X) (F.obj Y ⊗ F.obj Z)
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✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (λ_ x✝).inv ≫
      ((adj.unit.app (𝟙_ C) ⊗ₘ adj.unit.app x✝) ≫ μ G (F.obj (𝟙_ C)) (F.obj x✝)) ≫
        G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G) ▷ F.obj x✝)

Tactic:
assoc,

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✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (λ_ x✝).inv ≫
      (adj.unit.app (𝟙_ C) ⊗ₘ adj.unit.app x✝) ≫
        μ G (F.obj (𝟙_ C)) (F.obj x✝) ≫ G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G) ▷ F.obj 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✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (λ_ x✝).inv ≫
      (adj.unit.app (𝟙_ C) ⊗ₘ adj.unit.app x✝) ≫
        G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G)) ▷ G.obj (F.obj x✝) ≫ μ G (𝟙_ D) (F.obj x✝)

Tactic:
← tensorHom_id,

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✝ : C
⊢ (adj.homEquiv x✝ (𝟙_ D ⊗ F.obj x✝)) (λ_ (F.obj x✝)).inv =
    (λ_ x✝).inv ≫
      (adj.unit.app (𝟙_ C) ⊗ₘ adj.unit.app x✝) ≫
        (G.map ((adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G)) ⊗ₘ 𝟙 (G.obj (F.obj x✝))) ≫ μ G (𝟙_ D) (F.obj 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✝ : G.LaxMonoidal
x✝ : C
⊢ (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D)) (ρ_ (F.obj x✝)).inv =
    (ρ_ x✝).inv ≫
      ((adj.unit.app x✝ ⊗ₘ adj.unit.app (𝟙_ C)) ≫ μ G (F.obj x✝) (F.obj (𝟙_ C))) ≫
        G.map (F.obj x✝ ◁ (adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G))

Tactic:
assoc,

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✝ : C
⊢ (adj.homEquiv x✝ (F.obj x✝ ⊗ 𝟙_ D)) (ρ_ (F.obj x✝)).inv =
    (ρ_ x✝).inv ≫
      (adj.unit.app x✝ ⊗ₘ adj.unit.app (𝟙_ C)) ≫
        μ G (F.obj x✝) (F.obj (𝟙_ C)) ≫ G.map (F.obj x✝ ◁ (adj.homEquiv (𝟙_ C) (𝟙_ D)).symm (ε G))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case e_a
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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ (i.inv.app X ⊗ₘ i.inv.app Y) ▷ G.obj Z ≫
      (α_ (F.obj X) (F.obj Y) (G.obj Z)).hom ≫
        F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫ F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫ (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z)

Tactic:
← tensorHom_id,

Goal state after:
case e_a
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 G : C ⥤ D
inst✝ : F.Monoidal
i : F ≅ G
X Y Z : C
⊢ ((i.inv.app X ⊗ₘ i.inv.app Y) ⊗ₘ 𝟙 (G.obj Z)) ≫
      (α_ (F.obj X) (F.obj Y) (G.obj Z)).hom ≫
        F.obj X ◁ F.obj Y ◁ i.inv.app Z ≫ F.obj X ◁ LaxMonoidal.μ F Y Z ≫ LaxMonoidal.μ F X (Y ⊗ Z) =
    (α_ (G.obj X) (G.obj Y) (G.obj Z)).hom ≫
      G.obj X ◁ (i.inv.app Y ⊗ₘ i.inv.app Z) ≫
        G.obj X ◁ LaxMonoidal.μ F Y Z ≫
          G.obj X ◁ i.hom.app (Y ⊗ Z) ≫ (i.inv.app X ⊗ₘ i.inv.app (Y ⊗ Z)) ≫ LaxMonoidal.μ F X (Y ⊗ Z)
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
⊢ Quot F →+ Quot (F ⋙ uliftFunctor)

Tactic:
by
  refine QuotientAddGroup.lift (Relations F) (DFinsupp.sumAddHom (fun j ↦ (Quot.ι _ j).comp
    AddEquiv.ulift.symm.toAddMonoidHom)) ?_
  rw [AddSubgroup.closure_le]
  intro _ hx
  obtain ⟨j, j', u, a, rfl⟩ := hx
  rw [SetLike.mem_coe, AddMonoidHom.mem_ker, map_sub, DFinsupp.sumAddHom_single,
    DFinsupp.sumAddHom_single]
  change Quot.ι (F ⋙ uliftFunctor) j' ((F ⋙ uliftFunctor).map u (AddEquiv.ulift.symm a)) - _ = _
  rw [Quot.map_ι]
  dsimp
  rw [sub_self]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X✝ : C
⊢ (α.natTrans.app X✝ ≫ H.map (L₁.map (adj₁.unit.app X✝))) ≫ H.map (adj₁.counit.app (L₁.obj X✝)) = α.natTrans.app X✝

Tactic:
assoc,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X✝ : C
⊢ α.natTrans.app X✝ ≫ H.map (L₁.map (adj₁.unit.app X✝)) ≫ H.map (adj₁.counit.app (L₁.obj X✝)) = α.natTrans.app X✝