mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
ρ : C₂ ⥤ C₁
i : 𝟭 C₂ ⟶ ρ ⋙ Φ.functor
hi : ∀ (X₂ : C₂), W₂ (i.app X₂)
hW₁ : W₁ = W₂.inverseImage Φ.functor
inst✝³ : Φ.functor.Full
inst✝² : Φ.functor.Faithful
inst✝¹ : W₂.HasTwoOutOfThreeProperty
inst✝ : W₂.IsMultiplicative
X₂ : C₂
⊢ IsConnected (Φ.RightResolution X₂)

Tactic:
have : W₁.IsMultiplicative := by rw [hW₁]; infer_instance
  have : Nonempty (Φ.RightResolution X₂) := ⟨{ hw := hi X₂, .. }⟩
  have : IsPreconnected (Φ.RightResolution X₂) :=
    zigzag_isPreconnected (fun R₀ R₄ ↦
      calc
        Zigzag R₀ { hw := W₂.comp_mem _ _ R₀.hw (hi _), .. } :=
          Zigzag.of_hom { f := (ι i).app R₀.X₁ }
        Zigzag (J := Φ.RightResolution X₂) _ { hw := hi X₂, .. } :=
          Zigzag.of_inv
            { f := ρ.map R₀.w
              comm := (i.naturality R₀.w).symm }
        Zigzag (J := Φ.RightResolution X₂) _ { hw := W₂.comp_mem _ _ R₄.hw (hi _), .. } :=
          Zigzag.of_hom
            { f := ρ.map R₄.w
              comm := (i.naturality R₄.w).symm }
        Zigzag _ R₄ := Zigzag.of_inv { f := (ι i).app R₄.X₁ })
  constructor

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

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
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y : C
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by simp [β_hom_app]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
X : Over I
g : A' ⟶ A
v : A ⟶ (sections I).obj X
⊢ homMk ((β_ A' I).hom ≫ uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯ =
    homMk (g ▷ I) ⋯ ≫
      homMk ((β_ A I).hom ≫ uncurry (v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯

Tactic:
← Over.homMk_comp

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
X : Over I
g : A' ⟶ A
v : A ⟶ (sections I).obj X
⊢ homMk ((β_ A' I).hom ≫ uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯ =
    homMk (g ▷ I ≫ (β_ A I).hom ≫ uncurry (v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
Y Z : Over X
inst✝ : ChosenPullbacksAlong Z.hom
T✝ : Over X
u : T✝ ⟶ Y
v : T✝ ⟶ Z
⊢ Over.Hom.left u ≫ Y.hom = Over.Hom.left v ≫ Z.hom

Tactic:
rw [Over.w u, Over.w v]

Goal state after:
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Over

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
Z : Over X
A : C
f : Z ⟶ (toOver X).obj A
⊢ (Over.forget X).map f ≫ (forgetAdjToOver X).counit.app A = Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X

Tactic:
forgetAdjToOver_counit_app

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
Z : Over X
A : C
f : Z ⟶ (toOver X).obj A
⊢ (Over.forget X).map f ≫ SemiCartesianMonoidalCategory.fst A X =
    Over.Hom.left f ≫ SemiCartesianMonoidalCategory.fst A X
Module: Mathlib.CategoryTheory.Monad.Types

Goal state before:
pp: m : Type u → Type u
inst✝¹ : _root_.Monad m
inst✝ : LawfulMonad m
x✝¹ : Type u
x✝ : (𝟭 (Type u)).obj ((ofTypeFunctor m).obj x✝¹)
⊢ (ConcreteCategory.hom
          ({ app := fun X ↦ ↾pure, naturality := ⋯ }.app ((ofTypeFunctor m).obj x✝¹) ≫
            { app := fun X ↦ ↾joinM, naturality := ⋯ }.app x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (𝟙 ((𝟭 (Type u)).obj ((ofTypeFunctor m).obj x✝¹)))).toFun x✝

Tactic:
exact joinM_pure _

Goal state after:
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
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      (((((adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d) ≫
                adj.unit.app ((L ⋙ R).obj ((ihom d).obj (R.obj c)) ⊗ (L ⋙ R).obj d)) ≫
              inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d)))) ≫
            R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom)) ≫
          R.map (L.map ((ihom.ev d).app (R.obj c)))) ≫
        inv (adj.unit.app (R.1 c)) =
    (ihom.ev d).app (R.obj c)

Tactic:
slice_lhs 2 4 =>
    rw [← adj.unit_naturality_assoc]

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
c : C
d : D
inst✝ : IsIso (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d))
⊢ (β_ d ((ihom d).obj (R.obj c))).hom ≫
      (((adj.unit.app ((ihom d).obj (R.obj c) ⊗ d) ≫
              R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d)) ≫
                inv (R.map (L.map (adj.unit.app ((ihom d).obj (R.obj c)) ⊗ₘ adj.unit.app d)))) ≫
            R.map (L.map (β_ ((ihom d).obj (R.obj c)) d).hom)) ≫
          R.map (L.map ((ihom.ev d).app (R.obj c)))) ≫
        inv (adj.unit.app (R.1 c)) =
    (ihom.ev d).app (R.obj c)
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f = g

Tactic:
rw [← cancel_mono (terminal.from A)]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ terminal.from A = g ≫ terminal.from A
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case e
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
this : IsIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y)) := ofReflective._proof_2 i X Y
⊢ (reflector i ⋙ i).obj (i.obj X ⊗ i.obj Y) ≅ (𝟭 C).obj (i.obj X ⊗ i.obj Y)

Tactic:
exact asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y)) |>.symm

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasZeroObject C
X Y : C
⊢ Unique (X ⟶ Y)

Tactic:
haveI : HasInitial C := HasZeroObject.hasInitial
  apply uniqueHomsetOfInitialIsoUnit _ X Y
  refine ⟨default, (default : 𝟙_ C ⟶ 0) ≫ default, ?_, ?_⟩ <;> simp [eq_iff_true_of_subsingleton]

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
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        ((ihom.adjunction B).homEquiv A (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))).symm
          ((reflectorAdjunction i).unit.app A ≫
            ((ihom.adjunction B).homEquiv (i.obj ((reflector i).obj A))
                (i.obj ((reflector i).obj A ⊗ (reflector i).obj B)))
              ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv B
                      (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))).symm
                  ((reflectorAdjunction i).unit.app B ≫
                    ((ihom.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B))
                        (i.obj ((reflector i).obj A ⊗ (reflector i).obj B)))
                      (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)))) =
    prodComparison (reflector i) A B

Tactic:
erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]

Goal state after:
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
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        uncurry
          ((reflectorAdjunction i).unit.app A ≫
            curry
              ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                uncurry
                  ((reflectorAdjunction i).unit.app B ≫
                    curry (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv)))) =
    prodComparison (reflector i) A B
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h_fst
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
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ fst A B ≫ (reflectorAdjunction i).unit.app A =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫ i.map (fst ((reflector i).obj A) ((reflector i).obj B))

Tactic:
← i.map_comp,

Goal state after:
case h_fst
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
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ fst A B ≫ (reflectorAdjunction i).unit.app A =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B ≫ fst ((reflector i).obj A) ((reflector i).obj B))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h_snd
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
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ snd A B ≫ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫ i.map (snd ((reflector i).obj A) ((reflector i).obj B))

Tactic:
← i.map_comp,

Goal state after:
case h_snd
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
inst✝³ : MonoidalClosed C
inst✝² : CartesianMonoidalCategory D
inst✝¹ : ExponentialIdeal i
inst✝ : BraidedCategory C
A B : C
⊢ snd A B ≫ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B ≫ snd ((reflector i).obj A) ((reflector i).obj B))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ 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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H F
inst✝⁵ : DayConvolution G (H ⊛ F)
inst✝⁴ : DayConvolution (G ⊛ H) F
inst✝³ : DayConvolution G F
inst✝² : DayConvolution (G ⊛ F) H
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution G (F ⊛ H)
⊢ (associator F G H).hom ≫ (braiding F (G ⊛ H)).hom ≫ (associator G H F).hom =
    map (braiding F G).hom (𝟙 H) ≫ (associator G F H).hom ≫ map (𝟙 G) (braiding F H).hom

Tactic:
by
  apply Functor.hom_ext_of_isLeftKanExtension ((F ⊛ G) ⊛ H) (unit _ H)
  apply Functor.hom_ext_of_isLeftKanExtension ((F ⊛ G) ⊠ H)
    (ExternalProduct.extensionUnitLeft (F ⊛ G) (unit F G) H)
  ext ⟨⟨x, y⟩, z⟩
  dsimp
  simp only [whiskerLeft_id, Category.comp_id, associator_hom_unit_unit_assoc,
    externalProductBifunctor_obj_obj, tensor_obj, NatTrans.naturality_assoc,
    NatTrans.naturality, unit_app_braiding_hom_app_assoc,
    BraidedCategory.braiding_tensor_left_hom, Functor.map_comp, Category.assoc,
    Iso.map_hom_inv_id, BraidedCategory.braiding_naturality_right_assoc,
    BraidedCategory.braiding_tensor_right_hom, Iso.map_inv_hom_id_assoc,
    Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, unit_app_map_app_assoc,
    NatTrans.id_app, tensorHom_id]
  simp only [← comp_whiskerRight_assoc, ← whiskerLeft_comp_assoc,
    unit_app_braiding_hom_app]
  simp only [whiskerLeft_comp, ← Functor.map_comp, Category.assoc,
    Functor.comp_obj, tensor_obj, comp_whiskerRight,
    whiskerRight_comp_unit_app_assoc, NatTrans.naturality_assoc,
    NatTrans.naturality, associator_hom_unit_unit_assoc,
    externalProductBifunctor_obj_obj, unit_app_map_app_assoc, NatTrans.id_app,
    id_tensorHom]
  rw [← BraidedCategory.hexagon_reverse, ← whiskerLeft_comp_assoc]
  have := unit_app_braiding_hom_app F H x z =≫ (H ⊛ F).map (β_ z x).inv
  dsimp at this
  simp only [Category.assoc, Iso.map_hom_inv_id, Category.comp_id] at this
  rw [← this, whiskerLeft_comp_assoc]
  simp [← Functor.map_comp]

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

Goal state before:
pp: case e_a
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ 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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
this :
  ((unit F H).app (x, z) ≫ (braiding F H).hom.app (x ⊗ z)) ≫ (H ⊛ F).map (β_ z x).inv =
    ((β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x) ≫ (H ⊛ F).map (β_ z x).hom) ≫ (H ⊛ F).map (β_ z x).inv
⊢ ((β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x)) ▷ G.obj y ≫
      (unit (H ⊛ F) G).app (z ⊗ x, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ z x y).hom ≫ (β_ z (x ⊗ y)).hom ≫ (α_ x y z).hom) =
    (unit F H).app (x, z) ▷ G.obj y ≫
      (braiding F H).hom.app (x ⊗ z) ▷ G.obj y ≫
        (unit (H ⊛ F) G).app (x ⊗ z, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ x z y).hom ≫ x ◁ (β_ z y).hom)

Tactic:
simp only [Category.assoc, Iso.map_hom_inv_id, Category.comp_id] at this

Goal state after:
case e_a
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ 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)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
this :
  (unit F H).app (x, z) ≫ (braiding F H).hom.app (x ⊗ z) ≫ (H ⊛ F).map (β_ z x).inv =
    (β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x)
⊢ ((β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x)) ▷ G.obj y ≫
      (unit (H ⊛ F) G).app (z ⊗ x, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ z x y).hom ≫ (β_ z (x ⊗ y)).hom ≫ (α_ x y z).hom) =
    (unit F H).app (x, z) ▷ G.obj y ≫
      (braiding F H).hom.app (x ⊗ z) ▷ G.obj y ≫
        (unit (H ⊛ F) G).app (x ⊗ z, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ x z y).hom ≫ x ◁ (β_ z y).hom)
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
this : (ρ_ (𝟙_ C)).inv ≫ η ▷ 𝟙_ C ≫ A ◁ η ≫ 𝒮 ▷ A ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η

Tactic:
← rightUnitor_inv_naturality_assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ (ρ_ A).inv ≫ A ◁ η ≫ 𝒮 ▷ A ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η
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
this : η ≫ (ρ_ A).inv ≫ 𝒮 ▷ 𝟙_ C ≫ A ◁ η ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η

Tactic:
← rightUnitor_inv_naturality_assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
this : η ≫ 𝒮 ≫ (ρ_ A).inv ≫ A ◁ η ≫ μ = η ≫ ε ≫ η
⊢ η ≫ 𝒮 = η
Module: Mathlib.CategoryTheory.Monoidal.Limits.Basic

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F G H : J ⥤ C
j : J
⊢ ((limit.lift (F ⊗ G)
            { pt := limit F ⊗ limit G, π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π G j, naturality := ⋯ } } ⊗ₘ
          𝟙 (lim.obj H)) ≫
        limit.lift ((F ⊗ G) ⊗ H)
            { pt := limit (F ⊗ G) ⊗ limit H,
              π := { app := fun j ↦ limit.π (F ⊗ G) j ⊗ₘ limit.π H j, naturality := ⋯ } } ≫
          lim.map (α_ F G H).hom) ≫
      limit.π (F ⊗ G ⊗ H) j =
    ((α_ (lim.obj F) (lim.obj G) (lim.obj H)).hom ≫
        (𝟙 (lim.obj F) ⊗ₘ
            limit.lift (G ⊗ H)
              { pt := limit G ⊗ limit H, π := { app := fun j ↦ limit.π G j ⊗ₘ limit.π H j, naturality := ⋯ } }) ≫
          limit.lift (F ⊗ G ⊗ H)
            { pt := limit F ⊗ limit (G ⊗ H),
              π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π (G ⊗ H) j, naturality := ⋯ } }) ≫
      limit.π (F ⊗ G ⊗ H) j

Tactic:
dsimp
      simp only [tensorHom_id, limit.lift_map, Category.assoc, limit.lift_π,
        id_tensorHom]
      dsimp
      conv_lhs => rw [tensorHom_def, Category.assoc, ← comp_whiskerRight_assoc,
        limit.lift_π, tensor_whiskerLeft, Category.assoc, Category.assoc,
        Iso.inv_hom_id, Category.comp_id,
        ← associator_naturality_right, ← tensorHom_def_assoc]
      dsimp
      conv_rhs => rw [tensorHom_def, ← whisker_exchange,
        ← whiskerLeft_comp_assoc, limit.lift_π,
        whisker_exchange, ← associator_naturality_left_assoc]
      dsimp only
      conv_rhs => rw [tensorHom_def, whiskerLeft_comp,
        ← associator_naturality_middle_assoc,
        ← associator_naturality_right, ← comp_whiskerRight_assoc,
        ← tensorHom_def, ← tensorHom_def_assoc]

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

Goal state before:
pp: J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    ((𝟙 (limit F) ⊗ₘ
          limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } }) ≫
        limit.lift (F ⊗ 𝟙_ (J ⥤ C))
            { pt := limit F ⊗ limit (𝟙_ (J ⥤ C)),
              π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π (𝟙_ (J ⥤ C)) j, naturality := ⋯ } } ≫
          limMap (ρ_ F).hom) ≫
      limit.π F j

Tactic:
simp only [id_tensorHom, limit.lift_map, Category.assoc, limit.lift_π]

Goal state after:
J : Type w
inst✝³ : SmallCategory J
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : MonoidalCategory C
F : J ⥤ C
j : J
⊢ (ρ_ (limit F)).hom ≫ limit.π F j =
    limit F ◁
        limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun x ↦ 𝟙 (𝟙_ C), naturality := ⋯ } } ≫
      ((Cone.postcompose (ρ_ F).hom).obj
              { pt := limit F ⊗ limit (𝟙_ (J ⥤ C)),
                π := { app := fun j ↦ limit.π F j ⊗ₘ limit.π (𝟙_ (J ⥤ C)) j, naturality := ⋯ } }).π.app
        j
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).inv ▷ Y ⊗≫ Y ◁ (β_ X Y).hom =
    𝟙 ((X ⊗ Y) ⊗ Y) ⊗≫ X ◁ (β_ Y Y).hom ⊗≫ (β_ X Y).hom ▷ Y ⊗≫ Y ◁ (β_ Y X).inv ⊗≫ (β_ Y Y).inv ▷ X ⊗≫ 𝟙 (Y ⊗ Y ⊗ X)

pp: case 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 ⊗≫ 𝟙 Y = ⊗𝟙.hom ≫ Y ◁ ε_ X Y ⊗≫ 𝟙 Y

Tactic:
on_goal 2 => simp [monoidalComp]

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).inv ▷ Y ⊗≫ Y ◁ (β_ X Y).hom =
    𝟙 ((X ⊗ Y) ⊗ Y) ⊗≫ X ◁ (β_ Y Y).hom ⊗≫ (β_ X Y).hom ▷ Y ⊗≫ Y ◁ (β_ Y X).inv ⊗≫ (β_ Y Y).inv ▷ X ⊗≫ 𝟙 (Y ⊗ Y ⊗ X)
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.ind f
hg : P.ind g
T : C
p : X ⟶ T
u : T ⟶ Z
⊢ isFinitelyPresentable C p → p ≫ u = f ≫ g → ∃ W u_1 v, u_1 ≫ v = u ∧ P (p ≫ u_1)

Tactic:
hp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
P : MorphismProperty C
inst✝⁴ : ∀ (X : C), IsFinitelyAccessibleCategory (Under X)
inst✝³ : HasPushouts C
inst✝² : P.IsStableUnderComposition
inst✝¹ : P.IsStableUnderCobaseChange
inst✝ : P.PreIndSpreads
H : P ≤ isFinitelyPresentable C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : P.ind f
hg : P.ind g
T : C
p : X ⟶ T
u : T ⟶ Z
hp : isFinitelyPresentable C p
⊢ p ≫ u = f ≫ g → ∃ W u_1 v, u_1 ≫ v = u ∧ P (p ≫ u_1)
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst✝¹ : Mono i
inst✝ : IsNoetherianObject Y
⊢ IsNoetherianObject X

Tactic:
by
  rw [isNoetherianObject_iff_monotone_chain_condition]
  intro f
  obtain ⟨n, hn⟩ := monotone_chain_condition_of_isNoetherianObject
    ⟨_, (Subobject.map i).monotone.comp f.2⟩
  exact ⟨n, fun m hm ↦ Subobject.map_obj_injective i (hn m hm)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
α β : A₁ ⟶ A₂
⊢ F.map (α.f + β.f) ≫ A₂.str = A₁.str ≫ (α.f + β.f)

Tactic:
by simp only [Functor.map_add, add_comp, Endofunctor.Algebra.Hom.h, comp_add]

Goal state after: