mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.PreservesLimit

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ (F.leftOp ⋙ shrinkYoneda.{w, v, u}).map f ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    shrinkYonedaEquiv.symm (↑s (unop j₁)) ≫ ((Functor.const Jᵒᵖ).obj P).map f

Tactic:
← s.property f.unop

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : LocallySmall.{w, v, u} C
F : J ⥤ Cᵒᵖ
c : Cone F
c' : Cocone (F.leftOp ⋙ shrinkYoneda.{w, v, u})
hc : IsLimit c
hc' : IsColimit c'
P : Cᵒᵖ ⥤ Type w
s : ↑(F ⋙ P).sections
j₁ j₂ : Jᵒᵖ
f : j₁ ⟶ j₂
⊢ (F.leftOp ⋙ shrinkYoneda.{w, v, u}).map f ≫ shrinkYonedaEquiv.symm (↑s (unop j₂)) =
    shrinkYonedaEquiv.symm ((ConcreteCategory.hom ((F ⋙ P).map f.unop)) (↑s (unop j₂))) ≫
      ((Functor.const Jᵒᵖ).obj P).map f
Module: Mathlib.CategoryTheory.Localization.LocallySmall

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : LocallySmall.{w, v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
this✝³ : LocallySmall.{w, v₂, u₁} (InducedCategory D L.obj)
L' : C ⥤ InducedCategory D L.obj :=
  { obj := fun X ↦ X, map := fun {X Y} f ↦ InducedCategory.homMk (L.map f), map_id := ⋯, map_comp := ⋯ }
this✝² : L.EssSurj
this✝¹ : (inducedFunctor L.obj).EssSurj
this✝ : (inducedFunctor L.obj).IsEquivalence
e : InducedCategory D L.obj ≌ D := (inducedFunctor L.obj).asEquivalence
e' : (L' ⋙ e.functor) ⋙ e.inverse ≅ L' :=
  L'.associator e.functor e.inverse ≪≫ L'.isoWhiskerLeft e.unitIso.symm ≪≫ L'.rightUnitor
this : L'.IsLocalization W
⊢ W.HasLocalization

Tactic:
exact hasLocalizationOfLocallySmall.{w} W L'

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
x y : F ⊡ G
f : x ⟶ y
inst✝ : IsIso f
⊢ f.snd ≫ (inv f).snd = 𝟙 x.snd

Tactic:
simp [← comp_snd]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ F.obj Y₁ ◁ F.map e₂.hom ≫
      F.map e₁.hom ▷ F.obj (L.obj X₂) ≫
        ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫
        (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫
          F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv)) ≫ F.map (Y₁ ◁ e₂.hom) ≫ F.map (e₁.hom ▷ L.obj X₂)

Tactic:
← tensorHom_def'_assoc,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  F.obj Y₁ ◁ F.map e₂.hom ≫ ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app (L.obj X₂) =
    ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ ≫ F.map (Y₁ ◁ e₂.hom)
h₂ :
  ∀ (X : D),
    F.map e₁.hom ▷ F.obj X ≫ ((curriedTensorPreIsoPost L W F G).hom.app (L.obj X₁)).app X =
      ((curriedTensorPreIsoPost L W F G).hom.app Y₁).app X ≫ F.map (e₁.hom ▷ X)
⊢ (F.map e₁.hom ⊗ₘ F.map e₂.hom) ≫
      ((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
        μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫ F.map (δ L X₁ X₂) =
    (F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      μ G X₁ X₂ ≫
        (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ≫
          F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv)) ≫ F.map (Y₁ ◁ e₂.hom) ≫ F.map (e₁.hom ▷ L.obj X₂)
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : C
inst✝¹ : ChosenPullbacksAlong (𝟙 I)
inst✝ : ExponentiableMorphism (𝟙 I)
⊢ (pullbackPushforwardAdj (𝟙 I)).unit ≫ (pullback (𝟙 I)).whiskerLeft (pushforwardId I).hom =
    (pullbackPushforwardAdj (𝟙 I)).unit

Tactic:
rw [pushforwardId, Adjunction.unit_rightAdjointUniq_hom]

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
⊢ ∀ {X : C} {Y Y' : Over I} (f : (toOver I).obj X ⟶ Y) (g : Y ⟶ Y'),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } f ≫ (sections I).map g

Tactic:
intro A

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 : C
⊢ ∀ {Y Y' : Over I} (f : (toOver I).obj A ⟶ Y) (g : Y ⟶ Y'),
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (f ≫ g) =
      { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } f ≫ (sections I).map g
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: case refine_2
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))
⊢ ∀ (X : adj.toMonad.Algebra) (Y Y' : D) (g : Y ⟶ Y') (h : comparisonLeftAdjointObj adj X ⟶ Y),
    (comparisonLeftAdjointHomEquiv adj X Y') (h ≫ g) =
      (comparisonLeftAdjointHomEquiv adj X Y) h ≫ (comparison adj).map g

Tactic:
intro A

Goal state after:
case refine_2
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
⊢ ∀ (Y Y' : D) (g : Y ⟶ Y') (h : comparisonLeftAdjointObj adj A ⟶ Y),
    (comparisonLeftAdjointHomEquiv adj A Y') (h ≫ g) =
      (comparisonLeftAdjointHomEquiv adj A Y) h ≫ (comparison adj).map g
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M : Grp C
Y Y' : Cᵒᵖ
g : Y ⟶ Y'
f : unop Y ⟶ M.X
⊢ (ConcreteCategory.hom ((shrinkYonedaGrp.{w, v, u}.obj M).map g)) (shrinkYonedaGrpObjObjEquiv.symm f) =
    shrinkYonedaGrpObjObjEquiv.symm (g.unop ≫ f)

Tactic:
by
  simp [shrinkYonedaGrp, shrinkYonedaGrpObjObjEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : CartesianMonoidalCategory C
M M' : Grp C
Y : Cᵒᵖ
f : unop Y ⟶ M.X
g : M ⟶ M'
⊢ (ConcreteCategory.hom ((shrinkYonedaGrp.{w, v, u}.map g).app Y)) (shrinkYonedaGrpObjObjEquiv.symm f) =
    shrinkYonedaGrpObjObjEquiv.symm (f ≫ g.hom.hom)

Tactic:
by
  simp [shrinkYonedaGrp, shrinkYonedaGrpObjObjEquiv]

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

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ η ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X = 𝟙_ C ⊴ₗ e₂.inv ≫ η ⊵ₗ X ≫ e₁.inv ⊵ₗ X

Tactic:
action_exchange_assoc

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalLeftAction C D
M : C
inst✝³ : MonObj M
X : D
N : C
inst✝² : MonObj N
e₁ : M ≅ N
inst✝¹ : IsMonHom e₁.hom
Y : D
e₂ : X ≅ Y
inst✝ : ModObj M X
⊢ η ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X = η ⊵ₗ Y ≫ N ⊴ₗ e₂.inv ≫ e₁.inv ⊵ₗ X
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete

Goal state before:
pp: I : Type u₂
inst✝⁴ : Category.{v₂, u₂} I
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : ∀ (F : Discrete I ⥤ C), (Discrete.functor _root_.id).HasRightKanExtension F
A✝ B✝ : I ⥤ C
f : A✝ ⟶ B✝
h : IsIso (((whiskeringLeft (Discrete I) I C).obj (incl I)).map f)
⊢ IsIso f

Tactic:
by
    simp only [NatTrans.isIso_iff_isIso_app] at *
    intro X
    exact h ⟨X⟩

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✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
⊢ ExponentialIdeal i

Tactic:
let η : 𝟭 C ⟶ L ⋙ i := ir.unit

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✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) (reflector i)
ir : reflector i ⊣ i := reflectorAdjunction i
L : C ⥤ D := reflector i
η : 𝟭 C ⟶ L ⋙ i := ir.unit
⊢ ExponentialIdeal i
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 ◁ (reflectorAdjunction i).unit.app B ≫
        (reflectorAdjunction i).unit.app A ▷ i.obj ((reflector i).obj B) ≫
          (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv) =
    prodComparison (reflector i) A B

Tactic:
← tensorHom_def'_assoc,

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
      (((reflectorAdjunction i).unit.app A ⊗ₘ (reflectorAdjunction i).unit.app B) ≫
        (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv) =
    prodComparison (reflector i) A B
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
⊢ (β_ (F.obj x) (H.obj z)).hom ▷ G.obj y ≫
      (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:
← comp_whiskerRight_assoc

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
⊢ ((β_ (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.DayConvolution.DayFunctor

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
F G : C ⊛⥤ V
α β : F ⟶ G
h : α.natTrans = β.natTrans
⊢ α = β

Tactic:
cases α

Goal state after:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
V : Type u₂
inst✝² : Category.{v₂, u₂} V
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalCategory V
F G : C ⊛⥤ V
β : F ⟶ G
natTrans✝ : F.functor ⟶ G.functor
h : { natTrans := natTrans✝ }.natTrans = β.natTrans
⊢ { natTrans := natTrans✝ } = β
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
⊢ (tensorLeft P.X).map (Q.actRight ▷ L.X) ≫
      (α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
            ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) =
    (tensorLeft P.X).map ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
      (α_ P.X Q.X L.X).inv ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ L.X ≫
          coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
            ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft)

Tactic:
by
        dsimp; dsimp [TensorBimod.X]
        slice_lhs 1 2 => rw [associator_inv_naturality_middle]
        rw [← Iso.inv_hom_id_assoc (α_ _ _ _) (P.X ◁ Q.actRight), comp_whiskerRight]
        slice_lhs 3 4 =>
          rw [← comp_whiskerRight, Category.assoc, ← TensorBimod.π_tensor_id_actRight,
            comp_whiskerRight]
        slice_lhs 4 5 => rw [coequalizer.condition]
        slice_lhs 3 4 => rw [associator_naturality_left]
        slice_rhs 1 2 => rw [whiskerLeft_comp]
        slice_rhs 2 3 => rw [associator_inv_naturality_right]
        slice_rhs 3 4 => rw [whisker_exchange]
        simp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
⊢ MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A) =
    (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom

Tactic:
ext : 1
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` did not pick up `TensorProduct.ext`
    refine TensorProduct.ext <| LinearMap.ext_ring <| LinearMap.ext fun x => ?_
    rw [compr₂ₛₗ_apply, compr₂ₛₗ_apply, hom_comp, LinearMap.comp_apply]
    -- Porting note: this `dsimp` does nothing
    -- dsimp [AlgCat.id_apply, TensorProduct.mk_apply, Algebra.linearMap_apply,
    --    LinearMap.compr₂_apply, Function.comp_apply, RingHom.map_one,
    --    ModuleCat.MonoidalCategory.tensorHom_tmul, AlgCat.hom_comp,
    --    ModuleCat.MonoidalCategory.leftUnitor_hom_apply]
    -- Porting note: because `dsimp` is not effective, `rw` needs to be changed to `erw`
    dsimp
    erw [LinearMap.mul'_apply, MonoidalCategory.leftUnitor_hom_apply, ← Algebra.smul_def]
    dsimp

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ x * y * z =
    LinearMap.id ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).1 *
      (Hom.hom (↟(mul' R ↑A))) ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).2

Tactic:
LinearMap.id_apply,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ x * y * z =
    ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).1 *
      (Hom.hom (↟(mul' R ↑A))) ((x, y).1, (x, y).2 ⊗ₜ[R] (x ⊗ₜ[R] y, z).2).2
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft =
    R.X ◁ coequalizer.π (μ ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ≫
      R.X ◁ coequalizer.desc P.actLeft ⋯ ≫ P.actLeft

Tactic:
slice_rhs 1 2 => rw [← whiskerLeft_comp, coequalizer.π_desc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ R.X R.X P.X).inv ≫ (α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft = R.X ◁ P.actLeft ≫ P.actLeft
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : MonoidalCategory C
M : Cᴹᵒᵖ
inst✝² : MonObj M
N : Cᴹᵒᵖ
inst✝¹ : MonObj N
f : M ⟶ N
inst✝ : IsMonHom f
⊢ MonObj.mul ≫ f.unmop = (f.unmop ⊗ₘ f.unmop) ≫ MonObj.mul

Tactic:
apply mopEquiv C |>.fullyFaithfulFunctor.map_injective
    simpa [-IsMonHom.mul_hom] using! IsMonHom.mul_hom f

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ R.X P.X S.X).inv ≫ (α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight ≫ P.actLeft =
    R.X ◁ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ μ) ≫
      R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft

Tactic:
slice_rhs 1 2 => rw [← whiskerLeft_comp, coequalizer.π_desc]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
⊢ (α_ R.X P.X S.X).inv ≫ (α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight ≫ P.actLeft = R.X ◁ P.actRight ≫ P.actLeft
Module: Mathlib.CategoryTheory.ObjectProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
h : P ≤ isFinitelyPresentable C
inst✝ : LocallySmall.{w, v, u} C
⊢ P.ind.ind = P.ind

Tactic:
refine le_antisymm (fun X h ↦ ?_) (le_ind P.ind)
  choose J Jc Jf pres K Kc Kf pres' hp using h
  have (j : J) (i : K j) : IsFinitelyPresentable ((pres' j).diag.obj i) := h _ (hp _ _)
  have := IsFiltered.of_equivalence (ShrinkHoms.equivalence (ColimitPresentation.Total pres'))
  exact ⟨_, inferInstance, inferInstance,
    (pres.bind pres').reindex (ShrinkHoms.equivalence _).inverse, fun k ↦ by simp [hp]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
i : X ⟶ Y
inst✝¹ : Mono i
inst✝ : IsArtinianObject Y
f : ℕ →o (Subobject X)ᵒᵈ
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      { toFun := fun n ↦ (Subobject.map i).obj (f n), monotone' := ⋯ } n =
        { toFun := fun n ↦ (Subobject.map i).obj (f n), monotone' := ⋯ } m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
exact ⟨n, fun m hm ↦ Subobject.map_obj_injective i (hn m hm)⟩

Goal state after:
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
f : ℕ →o Subobject X
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      { toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := ⋯ } n =
        { toFun := (Subobject.map i).obj ∘ f.toFun, monotone' := ⋯ } m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
exact ⟨n, fun m hm ↦ Subobject.map_obj_injective i (hn m hm)⟩

Goal state after:
Module: Mathlib.GroupTheory.EckmannHilton

Goal state before:
pp: X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ m₁ = m₂

Tactic:
funext a b

Goal state after:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₂ a b
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
hl : ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl
f : X ⟶ Y
⊢ leftAdd X Y f 0 = f

Tactic:
simp [hl f, leftAdd, Category.assoc, Category.comp_id, biprod.inl_desc]

Goal state after: