mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case of.star
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
i : J
⊢ ∀ (f : WithTerminal.of i ⟶ WithTerminal.star),
    (WithTerminal.liftFromOver.obj c).map f ≫
        (WithTerminal.casesOn WithTerminal.star
            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
      (WithTerminal.casesOn (WithTerminal.of i)
            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
        (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map f

Tactic:
(try rintro ⟨⟩)

Goal state after:
case of.star
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
i : J
⊢ (WithTerminal.liftFromOver.obj c).map PUnit.unit ≫
      (WithTerminal.casesOn WithTerminal.star
          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
    (WithTerminal.casesOn (WithTerminal.of i)
          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
      (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map PUnit.unit
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case star.of
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
j : J
⊢ ∀ (f : WithTerminal.star ⟶ WithTerminal.of j),
    (WithTerminal.liftFromOver.obj c).map f ≫
        (WithTerminal.casesOn (WithTerminal.of j)
            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
      (WithTerminal.casesOn WithTerminal.star
            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
        (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map f

Tactic:
(try rintro ⟨⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: case star.star
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ ∀ (f : WithTerminal.star ⟶ WithTerminal.star),
    (WithTerminal.liftFromOver.obj c).map f ≫
        (WithTerminal.casesOn WithTerminal.star
            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
      (WithTerminal.casesOn WithTerminal.star
            (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
        (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map f

Tactic:
(try rintro ⟨⟩)

Goal state after:
case star.star
J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ (WithTerminal.liftFromOver.obj c).map PUnit.unit ≫
      (WithTerminal.casesOn WithTerminal.star
          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
    (WithTerminal.casesOn WithTerminal.star
          (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
          (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
      (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map PUnit.unit
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.EquifiberedLimits

Goal state before:
pp: J : Type u_1
K : Type u_2
C : Type u_3
D : Type u_4
ι : Type u_5
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_3} C
inst✝² : Category.{v_3, u_2} K
inst✝¹ : Category.{v_4, u_4} D
F : C ⥤ D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
this :
  ∀ {J : Type u_1} [inst : Category.{v_1, u_1} J],
    IsConnected J → IsClosedUnderLimitsOfShape (fun f ↦ Equifibered f.hom) J
hJ : ¬IsConnected J
G : Over F
x✝ : limitsOfShape (fun f ↦ Equifibered f.hom) J G
U V : C
f : U ⟶ V
c : J ⥤ Over F
α : (const J).obj G ⟶ c
hc : IsLimit { pt := G, π := α }
H : ∀ (j : J), Equifibered ({ diag := c, π := α, isLimit := hc }.diag.obj j).hom
hα : ∀ (i j : J) (f : i ⟶ j), α.app i ≫ c.map f = α.app j
hc' : IsLimit (WithTerminal.coneEquiv.functor.obj { pt := G, π := α })
inst : IsConnected (WithTerminal J)
⊢ ∀ {X Y : WithTerminal J} (f : X ⟶ Y),
    (WithTerminal.liftFromOver.obj c).map f ≫
        (WithTerminal.casesOn Y (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom =
      (WithTerminal.casesOn X (fun x ↦ Iso.refl ((WithTerminal.liftFromOver.obj c).obj (WithTerminal.of x)))
            (Iso.refl ((WithTerminal.liftFromOver.obj c).obj WithTerminal.star))).hom ≫
        (WithTerminal.liftToTerminal c Over.mkIdTerminal ⋙ Over.forget F).map f

Tactic:
rintro (i | _) (j | _) <;> (try rintro ⟨⟩) <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ #(md → (X ⟶ Y)) = #(X ⟶ yp)

Tactic:
rw [Cardinal.eq]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
⊢ Nonempty ((md → (X ⟶ Y)) ≃ (X ⟶ yp))
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ #(X ⟶ yp) ≤ α

Tactic:
apply Cardinal.mk_le_of_injective _
      · intro f
        exact ⟨_, _, f⟩
      · rintro f g k
        cases k
        rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: case l_naturality
C : Type u
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : MonoidalCategory D
f✝¹ : C → D
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f g : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ Y✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ projectMapAux f✝¹ ((Hom.whiskerLeft unit f✝).comp (l_hom Y✝)) = projectMapAux f✝¹ ((l_hom X✝).comp f✝)

Tactic:
dsimp only [projectMapAux, projectObj]
        rw [MonoidalCategory.leftUnitor_naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ (adj.homEquiv (adj.toMonad.obj A.A) (coequalizer (F.map A.a) (adj.counit.app (F.obj A.A))))
      (adj.counit.app (F.obj A.A) ≫ coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))

Tactic:
adj.homEquiv_naturality_right,

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : ∀ (A : adj.toMonad.Algebra), HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
A : adj.toMonad.Algebra
⊢ (adj.homEquiv (adj.toMonad.obj A.A) (F.obj A.A)) (adj.counit.app (F.obj A.A)) ≫
      G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A))) =
    G.map (coequalizer.π (F.map A.a) (adj.counit.app (F.obj A.A)))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
⊢ Function.Bijective ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c))

Tactic:
w₁

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
h : ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
d d' : D
c : C
w₁ :
  ⇑(ConcreteCategory.hom ((coyoneda.map (L.map (adj.unit.app d ▷ d')).op).app c)) =
    ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c)
⊢ Function.Bijective
    (⇑(adj.homEquiv (Opposite.unop (Opposite.op ((𝟭 D).obj d ⊗ d'))) c).symm ∘
      ⇑(ConcreteCategory.hom ((coyoneda.map (adj.unit.app d ▷ d').op).app (R.obj c))) ∘
        ⇑(adj.homEquiv (Opposite.unop (Opposite.op ((L ⋙ R).obj d ⊗ d'))) c))
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ F₂.map k₁.hom ≫ curry (f.app k₁.right) ≫ (ihom (F₁.obj k₁.right)).map (F₃.map (Under.Hom.right φ)) =
    F₂.map k₂.hom ≫ curry (f.app k₂.right) ≫ (pre (F₁.map (Under.Hom.right φ))).app (F₃.obj k₂.right)

Tactic:
rw [← curry_natural_left_assoc, ← curry_natural_left_assoc,
            ← curry_natural_right, curry_pre_app, Category.assoc,
            ← f.naturality φ.right, Monoidal.tensorObj_map, tensorHom_def_assoc,
            ← Under.w φ, Functor.map_comp, MonoidalCategory.whiskerLeft_comp_assoc,
            whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : Reflective i
X Y : D
⊢ IsIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))

Tactic:
by
            apply Functor.essImage.unit_isIso
            have := reflective_products i
            use Limits.prod X Y
            constructor
            apply Limits.PreservesLimitPair.iso i _ _ |>.trans
            refine Limits.IsLimit.conePointUniqueUpToIso (limit.isLimit (pair (i.obj X) (i.obj Y)))
              (tensorProductIsBinaryProduct _ _)

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      (((((((A ◁ Δ ≫ A ◁ Δ ▷ A ≫ A ◁ (α_ A A A).hom) ≫ A ◁ A ◁ 𝒮 ▷ A) ≫ A ◁ (α_ A A A).inv) ≫ A ◁ μ ▷ A) ≫
              A ◁ (β_ A A).hom) ≫
            A ◁ 𝒮 ▷ A) ≫
          (α_ A A A).inv) ≫
        μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
slice_lhs 3 7 =>
    simp only [← whiskerLeft_comp]
    rw [← associator_naturality_middle_assoc, Iso.hom_inv_id_assoc]
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
    simp only [whiskerLeft_comp]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ A ◁ Δ ≫ ((((A ◁ ε ▷ A ≫ A ◁ η ▷ A) ≫ A ◁ (β_ A A).hom) ≫ A ◁ 𝒮 ▷ A) ≫ (α_ A A A).inv) ≫ μ ▷ A =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ Δ ▷ A ≫ A ◁ (α_ A A A).hom ≫ A ◁ A ◁ 𝒮 ▷ A ≫ A ◁ (α_ A A A).inv ≫ A ◁ μ ▷ A

pp: case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ μ

pp: case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ 𝒮

Tactic:
simp only [← whiskerLeft_comp]
    rw [associator_inv_naturality_middle_assoc, Iso.hom_inv_id_assoc]
    simp only [← comp_whiskerRight]
    rw [antipode_right]
    simp only [comp_whiskerRight]
    simp only [whiskerLeft_comp]

Goal state after:
case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ ε ▷ A ≫ A ◁ η ▷ A

case a.a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ μ

case a.a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| μ

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (β_ A A).hom

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ 𝒮
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided

Goal state before:
pp: 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 ⊗≫ X ◁ η_ X Y ⊗≫ (X ◁ (β_ Y X).inv ⊗≫ (β_ X Y).hom ▷ X) ⊗≫ ε_ X Y ▷ X ⊗≫ 𝟙 X =
    𝟙 X ⊗≫
      X ◁ η_ X Y ⊗≫
        (𝟙 (X ⊗ X ⊗ Y) ⊗≫
            (β_ X X).hom ▷ Y ⊗≫ X ◁ (β_ X Y).hom ⊗≫ (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ 𝟙 ((Y ⊗ X) ⊗ X)) ⊗≫
          ε_ X Y ▷ X ⊗≫ 𝟙 X

Tactic:
by
      congr 3
      simp only [monoidalComp, MonoidalCoherence.assoc'_iso, MonoidalCoherence.whiskerRight_iso,
        MonoidalCoherence.refl_iso, whiskerRightIso_refl, Iso.refl_trans, Iso.symm_hom,
        MonoidalCoherence.assoc_iso, Iso.trans_refl, comp_id, id_comp]
      rw [← IsIso.eq_inv_comp]
      repeat rw [← assoc]
      iterate 5 rw [← IsIso.comp_inv_eq]
      simpa using yang_baxter X Y X

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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : MonoidalCategoryStruct D
inst✝¹ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d : D
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
⊢ (((ι C V D).obj d ⊠ (ι C V D).obj (𝟙_ D)).homEquivOfIsLeftKanExtension
        (ExternalProduct.extensionUnitRight ((ι C V D).obj (𝟙_ D)) (φ ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
        (tensor C ⋙ (ι C V D).obj d))
      ((((ι C V D).obj d ⊛ (ι C V D).obj (𝟙_ D)).homEquivOfIsLeftKanExtension
          (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
        ((ι C V D).map (ρ_ d).hom)) =
    (((ι C V D).obj d ⊠ (ι C V D).obj (𝟙_ D)).homEquivOfIsLeftKanExtension
        (ExternalProduct.extensionUnitRight ((ι C V D).obj (𝟙_ D)) (φ ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
        (tensor C ⋙ (ι C V D).obj d))
      ((((ι C V D).obj d ⊛ (ι C V D).obj (𝟙_ D)).homEquivOfIsLeftKanExtension
          (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
        (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom)

Tactic:
ext ⟨x, _⟩

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
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : MonoidalCategoryStruct D
inst✝¹ : LawfulDayConvolutionMonoidalCategoryStruct C V D
d : D
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
x : C
snd✝ : Discrete PUnit.{1}
⊢ ((((ι C V D).obj d ⊠ (ι C V D).obj (𝟙_ D)).homEquivOfIsLeftKanExtension
            (ExternalProduct.extensionUnitRight ((ι C V D).obj (𝟙_ D)) (φ ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
            (tensor C ⋙ (ι C V D).obj d))
          ((((ι C V D).obj d ⊛ (ι C V D).obj (𝟙_ D)).homEquivOfIsLeftKanExtension
              (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
            ((ι C V D).map (ρ_ d).hom))).app
      (x, snd✝) =
    ((((ι C V D).obj d ⊠ (ι C V D).obj (𝟙_ D)).homEquivOfIsLeftKanExtension
            (ExternalProduct.extensionUnitRight ((ι C V D).obj (𝟙_ D)) (φ ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
            (tensor C ⋙ (ι C V D).obj d))
          ((((ι C V D).obj d ⊛ (ι C V D).obj (𝟙_ D)).homEquivOfIsLeftKanExtension
              (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj (𝟙_ D))) ((ι C V D).obj d))
            (DayConvolutionUnit.rightUnitor ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj d)).hom)).app
      (x, snd✝)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.ind f
J : Type w
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
j : J
⊢ ((Under.lift D t).obj j).hom ≫ s.app j = (((Functor.const J).obj (CategoryTheory.Under.mk f)).obj j).hom

Tactic:
simp [hst]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.ind f
J : Type w
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
this : Nonempty J
⊢ ∀ (j : J), t.app j ≫ { pt := Y, ι := s }.ι.app j = f

Tactic:
simp [hst]

Goal state after: