mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
        (α_ X Y X).inv) ≫
      (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
← assoc

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
          (α_ X Y X).inv) ≫
        (β_ Y X).inv ▷ X) ≫
      (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
          (α_ X Y X).inv) ≫
        (β_ Y X).inv ▷ X) ≫
      (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
← assoc

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
            (α_ X Y X).inv) ≫
          (β_ Y X).inv ▷ X) ≫
        (α_ Y X X).hom) ≫
      Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
            (α_ X Y X).inv) ≫
          (β_ Y X).inv ▷ X) ≫
        (α_ Y X X).hom) ≫
      Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
← assoc

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
              (α_ X Y X).inv) ≫
            (β_ Y X).inv ▷ X) ≫
          (α_ Y X X).hom) ≫
        Y ◁ (β_ X X).inv) ≫
      (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
              (α_ X Y X).inv) ≫
            (β_ Y X).inv ▷ X) ≫
          (α_ Y X X).hom) ≫
        Y ◁ (β_ X X).inv) ≫
      (α_ Y X X).inv

Tactic:
← assoc

Goal state after:
case e_g.e_f
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
              (α_ X Y X).inv) ≫
            (β_ Y X).inv ▷ X) ≫
          (α_ Y X X).hom) ≫
        Y ◁ (β_ X X).inv) ≫
      (α_ Y X X).inv
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    inv (α_ Y X Y).hom ≫
      inv ((β_ Y X).inv ▷ Y) ≫
        (α_ X Y Y).hom ≫
          X ◁ (β_ Y Y).hom ≫
            (α_ X Y Y).inv ≫
              (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
← assoc

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫
      (α_ X Y Y).hom ≫
        X ◁ (β_ Y Y).hom ≫
          (α_ X Y Y).inv ≫
            (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫
      (α_ X Y Y).hom ≫
        X ◁ (β_ Y Y).hom ≫
          (α_ X Y Y).inv ≫
            (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
← assoc

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    ((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫
      X ◁ (β_ Y Y).hom ≫
        (α_ X Y Y).inv ≫
          (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    ((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫
      X ◁ (β_ Y Y).hom ≫
        (α_ X Y Y).inv ≫
          (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
← assoc

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫
      (α_ X Y Y).inv ≫
        (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫
      (α_ X Y Y).inv ≫
        (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
← assoc

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    ((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
      (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    ((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
      (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
← assoc

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
        (β_ X Y).hom ▷ Y) ≫
      (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
        (β_ X Y).hom ▷ Y) ≫
      (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
← assoc

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    ((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
          (β_ X Y).hom ▷ Y) ≫
        (α_ Y X Y).hom) ≫
      Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    ((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
          (β_ X Y).hom ▷ Y) ≫
        (α_ Y X Y).hom) ≫
      Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
← assoc

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
            (β_ X Y).hom ▷ Y) ≫
          (α_ Y X Y).hom) ≫
        Y ◁ (β_ Y X).inv) ≫
      (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
            (β_ X Y).hom ▷ Y) ≫
          (α_ Y X Y).hom) ≫
        Y ◁ (β_ Y X).inv) ≫
      (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
← assoc

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    ((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
              (β_ X Y).hom ▷ Y) ≫
            (α_ Y X Y).hom) ≫
          Y ◁ (β_ Y X).inv) ≫
        (α_ Y Y X).inv) ≫
      (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    ((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
              (β_ X Y).hom ▷ Y) ≫
            (α_ Y X Y).hom) ≫
          Y ◁ (β_ Y X).inv) ≫
        (α_ Y Y X).inv) ≫
      (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
← assoc

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
                (β_ X Y).hom ▷ Y) ≫
              (α_ Y X Y).hom) ≫
            Y ◁ (β_ Y X).inv) ≫
          (α_ Y Y X).inv) ≫
        (β_ Y Y).inv ▷ X) ≫
      (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
                (β_ X Y).hom ▷ Y) ≫
              (α_ Y X Y).hom) ≫
            Y ◁ (β_ Y X).inv) ≫
          (α_ Y Y X).inv) ≫
        (β_ Y Y).inv ▷ X) ≫
      (α_ Y Y X).hom

Tactic:
← assoc

Goal state after:
case e_g.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
                (β_ X Y).hom ▷ Y) ≫
              (α_ Y X Y).hom) ≫
            Y ◁ (β_ Y X).inv) ≫
          (α_ Y Y X).inv) ≫
        (β_ Y Y).inv ▷ X) ≫
      (α_ Y Y X).hom
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X : C
⊢ { hom := A.map (𝟙 X), isMonHom_hom := ⋯ } = 𝟙 (functorObjObj A X)

Tactic:
by ext; dsimp; rw [CategoryTheory.Functor.map_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X : C
⊢ { hom := A.map (𝟙 X), isComonHom_hom := ⋯ } = 𝟙 (functorObjObj A X)

Tactic:
by ext; dsimp; rw [CategoryTheory.Functor.map_id]

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

Goal state before:
pp: C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹³ : Category.{v₂, u₂} V
inst✝¹² : MonoidalCategory C
inst✝¹¹ : MonoidalCategory V
inst✝¹⁰ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝⁸ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝⁷ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝⁶ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
F G U : C ⥤ V
inst✝⁵ : DayConvolutionUnit U
inst✝⁴ : DayConvolution F U
inst✝³ : DayConvolution U G
inst✝² : DayConvolution F (U ⊛ G)
inst✝¹ : DayConvolution (F ⊛ U) G
inst✝ : DayConvolution F G
⊢ unit (F ⊛ U) G ≫ (tensor C).whiskerLeft ((associator F U G).hom ≫ map (𝟙 F) (DayConvolutionUnit.leftUnitor U G).hom) =
    unit (F ⊛ U) G ≫ (tensor C).whiskerLeft (map (DayConvolutionUnit.rightUnitor U F).hom (𝟙 G))

Tactic:
apply Functor.hom_ext_of_isLeftKanExtension
    (α := extensionUnitLeft (F ⊛ U) (DayConvolution.unit F U) G)

Goal state after:
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹³ : Category.{v₂, u₂} V
inst✝¹² : MonoidalCategory C
inst✝¹¹ : MonoidalCategory V
inst✝¹⁰ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝⁸ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝⁷ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝⁶ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
F G U : C ⥤ V
inst✝⁵ : DayConvolutionUnit U
inst✝⁴ : DayConvolution F U
inst✝³ : DayConvolution U G
inst✝² : DayConvolution F (U ⊛ G)
inst✝¹ : DayConvolution (F ⊛ U) G
inst✝ : DayConvolution F G
⊢ extensionUnitLeft (F ⊛ U) (unit F U) G ≫
      ((tensor C).prod (𝟭 C)).whiskerLeft
        (unit (F ⊛ U) G ≫
          (tensor C).whiskerLeft ((associator F U G).hom ≫ map (𝟙 F) (DayConvolutionUnit.leftUnitor U G).hom)) =
    extensionUnitLeft (F ⊛ U) (unit F U) G ≫
      ((tensor C).prod (𝟭 C)).whiskerLeft
        (unit (F ⊛ U) G ≫ (tensor C).whiskerLeft (map (DayConvolutionUnit.rightUnitor U F).hom (𝟙 G)))
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : ObjectProperty D
e : C ≌ D
inst✝ : P.IsClosedUnderIsomorphisms
X : D
⊢ (P.inverseImage e.functor).ind (e.inverse.obj X) ↔ P.ind X

Tactic:
by
  dsimp only [ObjectProperty.ind]
  congr!
  refine ⟨fun ⟨pres, h⟩ ↦ ?_, fun ⟨pres, h⟩ ↦ ?_⟩
  · exact ⟨.ofIso (pres.map e.functor) (e.counitIso.app X), fun i ↦ h i⟩
  · exact ⟨pres.map e.inverse, fun i ↦ P.prop_of_iso ((e.counitIso.app _).symm) (h i)⟩

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
x✝ : P.ind f
J : Type u_1
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
⊢ IsColimit { pt := Z, ι := s ≫ (Functor.const J).map i }

Tactic:
exact (IsColimit.equivIsoColimit (Cocone.ext (asIso i))) hs

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Comma

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
f : Comma F₁ F₂
hf : P₁ f.left ∧ P₂ f.right
⊢ (comma F₁ F₂ Q₁ Q₂).isoClosure f

Tactic:
obtain ⟨X₁, hX₁, ⟨e₁⟩⟩ := h₁' _ hf.1

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
Q₁ : ObjectProperty C₁
w✝¹ : ObjectProperty.Small.{w, v_1, u_1} Q₁
h₁ : Q₁ ≤ P₁
h₁' : P₁ ≤ Q₁.isoClosure
Q₂ : ObjectProperty C₂
w✝ : ObjectProperty.Small.{w, v_2, u_2} Q₂
h₂ : Q₂ ≤ P₂
h₂' : P₂ ≤ Q₂.isoClosure
f : Comma F₁ F₂
hf : P₁ f.left ∧ P₂ f.right
X₁ : C₁
hX₁ : Q₁ X₁
e₁ : f.left ≅ X₁
⊢ (comma F₁ F₂ Q₁ Q₂).isoClosure f
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case isSuccLimit
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : Order.IsSuccLimit j
hj' : ∀ b < j, HasCardinalLT (↑(transfiniteIterate (φ Y m) b A)) κ₂
⊢ HasCardinalLT (↑(⨆ x, transfiniteIterate (φ Y m) (↑x) A)) κ₂

Tactic:
Set.iSup_eq_iUnion

Goal state after:
case isSuccLimit
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : Order.IsSuccLimit j
hj' : ∀ b < j, HasCardinalLT (↑(transfiniteIterate (φ Y m) b A)) κ₂
⊢ HasCardinalLT (↑(⋃ x, transfiniteIterate (φ Y m) (↑x) A)) κ₂
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
F' : Cᵒᵖ ⥤ Type w
e : F ≅ F'
⊢ ∃ R, R.homEquiv (𝟙 X) = (ConcreteCategory.hom (e.hom.app (op X))) x

Tactic:
use h.representableBy.ofIso e

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
h : F.IsRepresentedBy x
F' : Cᵒᵖ ⥤ Type w
e : F ≅ F'
⊢ (h.representableBy.ofIso e).homEquiv (𝟙 X) = (ConcreteCategory.hom (e.hom.app (op X))) x
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck = coherentTopology C

Tactic:
ext B S

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
⊢ S ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck B ↔ S ∈ (coherentTopology C) B
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_1.top
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
X✝ : C
⊢ ⊤ ∈ (coherentTopology C) X✝

Tactic:
apply Coverage.Saturate.top

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_2.top
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
X✝ : C
⊢ ⊤ ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck X✝

Tactic:
apply Coverage.Saturate.top

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
b : P.obj (op X)
hb : b ∈ {x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (P.map π.op)) a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a
⊢ ∀ (y : (fun X ↦ X) (P.obj (op B))),
    (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a

Tactic:
intro y

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
b : P.obj (op X)
hb : b ∈ {x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (P.map π.op)) a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a
y : P.obj (op B)
⊢ (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) y → y = a