mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasLimitsOfShape J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
j : J
⊢ (f ≫ (limitObjIsoLimitCompEvaluation H k).hom) ≫ limit.π (H ⋙ (evaluation K C).obj k) j =
    (g ≫ (limitObjIsoLimitCompEvaluation H k).hom) ≫ limit.π (H ⋙ (evaluation K C).obj k) j

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasLimitsOfShape J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
j : J
⊢ f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasLimitsOfShape J C
j : J
⊢ (limitCompWhiskeringLeftIsoCompLimit F G).hom ≫ G.whiskerLeft (limit.π F j) =
    limit.π (F ⋙ (whiskeringLeft D K C).obj G) j

Tactic:
ext d
  simp [limitCompWhiskeringLeftIsoCompLimit]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
P : Cᵒᵖ ⥤ Type w
f : shrinkYoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.op)) (shrinkYonedaEquiv f) = shrinkYonedaEquiv (shrinkYoneda.{w, v, u}.map g ≫ f)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : C
P : Cᵒᵖ ⥤ Type w
f : shrinkYoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (f.app (op X))) ((equivShrink (X ⟶ X)) (𝟙 X))) =
    (ConcreteCategory.hom (f.app (op Y))) ((equivShrink (Y ⟶ X)) g)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
j : J
⊢ colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ f =
    colimit.ι (H ⋙ (evaluation K C).obj k) j ≫ (colimitObjIsoColimitCompEvaluation H k).inv ≫ g

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasColimitsOfShape J C
k : K
W : C
f g : (colimit H).obj k ⟶ W
w : ∀ (j : J), (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
j : J
⊢ (colimit.ι H j).app k ≫ f = (colimit.ι H j).app k ≫ g
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X✝ Y✝ : C
g : X✝ ⟶ Y✝
⊢ uliftYoneda.{w', v, u}.map g ≫
      (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso) ⋯).hom =
    (NatIso.ofComponents (fun Y ↦ (Equiv.ulift.trans shrinkYonedaObjObjEquiv.symm).toIso) ⋯).hom ≫
      shrinkYoneda.{max w' v, v, u}.map g

Tactic:
ext
      exact (shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
τ : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
Y : C
f : (yoneda.obj Y).obj X
⊢ (ConcreteCategory.hom
          (((fun x ↦
                  { app := fun Y ↦ ↾fun f ↦ (ConcreteCategory.hom (P.map ((equivShrink (unop X ⟶ Y)).symm f))) x,
                    naturality := ⋯ })
                ((fun τ ↦
                    (ConcreteCategory.hom (τ.app (unop X))) ((equivShrink ((yoneda.obj (unop X)).obj X)) (𝟙 (unop X))))
                  τ)).app
            Y)).toFun
      ((equivShrink ((yoneda.obj Y).obj X)) f) =
    (ConcreteCategory.hom (τ.app Y)).toFun ((equivShrink ((yoneda.obj Y).obj X)) f)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : Cᵒᵖ
P : C ⥤ Type w
τ : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
Y : C
f : (yoneda.obj Y).obj X
⊢ (ConcreteCategory.hom (P.map f))
      ((ConcreteCategory.hom (τ.app (unop X))) ((equivShrink (unop X ⟶ unop X)) (𝟙 (unop X)))) =
    (ConcreteCategory.hom (τ.app Y)) ((equivShrink (unop X ⟶ Y)) f)
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
P : C ⥤ Type w
f : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.unop)) (shrinkCoyonedaEquiv f) =
    shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map g ≫ f)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
P : C ⥤ Type w
f : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.unop))
      ((ConcreteCategory.hom (f.app (unop X))) ((equivShrink (unop X ⟶ unop X)) (𝟙 (unop X)))) =
    (ConcreteCategory.hom (f.app (unop Y))) ((equivShrink (unop X ⟶ unop Y)) g.unop)
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
r : R
s : (j : J) → ↑(F.obj j)
sh : s ∈ (F ⋙ forget (ModuleCat R)).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((F ⋙ forget (ModuleCat R)).map f)) ((r • s) j) = (r • s) j'

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
r : R
s : (j : J) → ↑(F.obj j)
sh : s ∈ (F ⋙ forget (ModuleCat R)).sections
j j' : J
f : j ⟶ j'
⊢ r • (ConcreteCategory.hom (F.map f)) (s j) = r • s j'
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
⊢ (((bifunctorComp₁₂FunctorObj F₁₂).obj G).obj X₁).map f ≫
      { app := fun X₃ ↦ (G.map ((φ.app X₁).app Y₂)).app X₃, naturality := ⋯ } =
    { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ } ≫
      (((bifunctorComp₁₂FunctorObj F₁₂').obj G).obj X₁).map f

Tactic:
by
            ext X₃
            dsimp
            simp only [← NatTrans.comp_app, NatTrans.naturality, ← G.map_comp]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
⊢ Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections → HasLimit F

Tactic:
· intro
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
⊢ Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections → HasLimit F

Tactic:
· intro
    infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : L.Faithful
X Y : C
f g : Y ⟶ (𝟭 C).obj X
hfg : f ≫ h.unit.app X = g ≫ h.unit.app X
⊢ (h.homEquiv Y (L.obj X)) (L.map f) = (h.homEquiv Y (L.obj X)) (L.map g)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : L.Faithful
X Y : C
f g : Y ⟶ (𝟭 C).obj X
hfg : f ≫ h.unit.app X = g ≫ h.unit.app X
⊢ f ≫ h.unit.app X = g ≫ h.unit.app X
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ (h.homEquiv X (L.obj Y)).symm (f ≫ h.unit.app Y) = (h.homEquiv X (L.obj Y)).symm (g ≫ h.unit.app Y)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), Mono (h.unit.app X)
X Y : C
f g : X ⟶ Y
hfg : L.map f = L.map g
⊢ L.map f = L.map g
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ (h.homEquiv (R.obj X) Y) (h.counit.app X ≫ f) = (h.homEquiv (R.obj X) Y) (h.counit.app X ≫ g)

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : D), Epi (h.counit.app X)
X Y : D
f g : X ⟶ Y
hfg : R.map f = R.map g
⊢ R.map f = R.map g
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ (X ⊗ Y) ◁ f = (α_ X Y Z).hom ≫ X ◁ Y ◁ f ≫ (α_ X Y Z').inv

Tactic:
simp only [← id_tensorHom]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ 𝟙 (X ⊗ Y) ⊗ₘ f = (α_ X Y Z).hom ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ f) ≫ (α_ X Y Z').inv
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
h : f ▷ 𝟙_ C = g ▷ 𝟙_ C
⊢ f = g

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
h : f ▷ 𝟙_ C = g ▷ 𝟙_ C
⊢ f = g
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
h : ((curriedTensor C).obj (𝟙_ C)).map f = ((curriedTensor C).obj (𝟙_ C)).map g
⊢ f = g

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X✝ Y✝ Z X Y : C
f g : X ⟶ Y
h : ((curriedTensor C).obj (𝟙_ C)).map f = ((curriedTensor C).obj (𝟙_ C)).map g
⊢ f = g
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X Y : J
f : X ⟶ Y
X' : J
⊢ F.map f ▷ G.obj X' ≫ (α.app Y ⊗ₘ β.app X') = (α.app X ⊗ₘ β.app X') ≫ F'.map f ▷ G'.obj X'

Tactic:
simpa using

Goal state after:
J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X Y : J
f : X ⟶ Y
X' : J
⊢ F.map f ▷ G.obj X' ≫ (α.app Y ⊗ₘ β.app X') = (α.app X ⊗ₘ β.app X') ≫ F'.map f ▷ G'.obj X'
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X' Y' : J
f : X' ⟶ Y'
X : J
⊢ F.obj X ◁ G.map f ≫ (α.app X ⊗ₘ β.app Y') = (α.app X ⊗ₘ β.app X') ≫ F'.obj X ◁ G'.map f

Tactic:
simpa using

Goal state after:
J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : MonoidalCategory C
F G F' G' : J ⥤ C
α : F ⟶ F'
β : G ⟶ G'
X' Y' : J
f : X' ⟶ Y'
X : J
⊢ F.obj X ◁ G.map f ≫ (α.app X ⊗ₘ β.app Y') = (α.app X ⊗ₘ β.app X') ≫ F'.obj X ◁ G'.map f
Module: Mathlib.CategoryTheory.Linear.LinearFunctor

Goal state before:
pp: R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
r : R
X' Y' : C
eX : F.obj X' ≅ X
eY : F.obj Y' ≅ Y
f' : X' ⟶ Y'
⊢ G.map (r • eX.inv ≫ F.map f' ≫ eY.hom) = r • G.map (eX.inv ≫ F.map f' ≫ eY.hom)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹³ : Semiring R
C : Type u_2
D : Type u_3
inst✝¹² : Category.{v_1, u_2} C
inst✝¹¹ : Category.{v_2, u_3} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryTheory.Linear R C
inst✝⁷ : CategoryTheory.Linear R D
F : C ⥤ D
inst✝⁶ : Linear R F
E : Type u_4
inst✝⁵ : Category.{v_3, u_4} E
inst✝⁴ : Preadditive E
inst✝³ : CategoryTheory.Linear R E
G : D ⥤ E
inst✝² : F.Full
inst✝¹ : F.EssSurj
inst✝ : Linear R (F ⋙ G)
X Y : D
r : R
X' Y' : C
eX : F.obj X' ≅ X
eY : F.obj Y' ≅ Y
f' : X' ⟶ Y'
⊢ G.map (r • eX.inv ≫ F.map f' ≫ eY.hom) = r • G.map (eX.inv ≫ F.map f' ≫ eY.hom)
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
j : J
⊢ X ◁ biproduct.ι f j ≫ (leftDistributor X f).hom = biproduct.ι (fun j ↦ X ⊗ f j) j

Tactic:
by
  classical
  cases nonempty_fintype J
  simp [leftDistributor_hom, Preadditive.comp_sum, ← whiskerLeft_comp_assoc,
    biproduct.ι_π, whiskerLeft_dite, dite_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (F ⋙ G).map x✝¹ ▷ (F ⋙ G).obj x✝ ≫ μ G (F.obj Y✝) (F.obj x✝) ≫ G.map (μ F Y✝ x✝) =
    (μ G (F.obj X✝) (F.obj x✝) ≫ G.map (μ F X✝ x✝)) ≫ (F ⋙ G).map (x✝¹ ▷ x✝)

Tactic:
comp_obj,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : C
⊢ (F ⋙ G).map x✝¹ ▷ G.obj (F.obj x✝) ≫ μ G (F.obj Y✝) (F.obj x✝) ≫ G.map (μ F Y✝ x✝) =
    (μ G (F.obj X✝) (F.obj x✝) ≫ G.map (μ F X✝ x✝)) ≫ (F ⋙ G).map (x✝¹ ▷ x✝)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ (F ⋙ G).obj x✝¹ ◁ (F ⋙ G).map x✝ ≫ μ G (F.obj x✝¹) (F.obj Y✝) ≫ G.map (μ F x✝¹ Y✝) =
    (μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (μ F x✝¹ X✝)) ≫ (F ⋙ G).map (x✝¹ ◁ x✝)

Tactic:
comp_obj,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ G.obj (F.obj x✝¹) ◁ (F ⋙ G).map x✝ ≫ μ G (F.obj x✝¹) (F.obj Y✝) ≫ G.map (μ F x✝¹ Y✝) =
    (μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (μ F x✝¹ X✝)) ≫ (F ⋙ G).map (x✝¹ ◁ x✝)
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ MonoidalLinear R (ModuleCat R)

Tactic:
refine ⟨?_, ?_⟩
  · intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp [ModuleCat.hom_whiskerLeft]
  · intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp [ModuleCat.hom_whiskerRight]

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

Goal state before:
pp: case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ = μ F x✝¹ x✝

Tactic:
rw [← cancel_mono (μIso F _ _).inv]

Goal state after:
case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ ≫ (μIso F x✝¹ x✝).inv = μ F x✝¹ x✝ ≫ (μIso F x✝¹ x✝).inv
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
⊢ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') =
    (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
⊢ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') =
    (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
⊢ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y') =
    (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X' Y' X : D
g : X' ⟶ Y'
⊢ F.obj (G.obj X) ◁ F.map (G.map g) ≫ (adj.counit.app X ⊗ₘ adj.counit.app Y') =
    (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ X ◁ g
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ G.map c.fst ≫ G.map f = G.map c.snd ≫ G.map g

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : C ⥤ D
⊢ G.map c.fst ≫ G.map f = G.map c.snd ≫ G.map g
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : C ⥤ D
⊢ G.map f ≫ G.map c.inl = G.map g ≫ G.map c.inr

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : C ⥤ D
⊢ G.map f ≫ G.map c.inl = G.map g ≫ G.map c.inr
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W : Set (MorphismProperty C)
h : ∀ W' ∈ W, W'.IsStableUnderComposition
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : InfSet.sInf W f
hg : InfSet.sInf W g
⊢ InfSet.sInf W (f ≫ g)

Tactic:
by
    rw [sInf_iff] at hf hg ⊢
    exact fun W' hW' ↦ (h W' hW').comp_mem _ _ (hf _ hW') (hg _ hW')

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

Goal state before:
pp: case of_comp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
g' : x✝ ⟶ y✝
f : y✝ ⟶ z✝
hg' : W g'
hf : W.multiplicativeClosure' f
h_rec : ∀ (g : z✝ ⟶ Z✝), W.multiplicativeClosure' g → W.multiplicativeClosure' (f ≫ g)
g : z✝ ⟶ Z✝
hg : W.multiplicativeClosure' g
⊢ W.multiplicativeClosure' ((g' ≫ f) ≫ g)

Tactic:
rw [Category.assoc]
      exact .of_comp g' (f ≫ g) hg' (h_rec g hg)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝ W' : MorphismProperty C
h : x✝ ≤ W'
⊢ x✝.multiplicativeClosure ≤ W'.multiplicativeClosure

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x✝ W' : MorphismProperty C
h : x✝ ≤ W'
⊢ x✝ ≤ W'.multiplicativeClosure
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case of_comp
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
x y : C
f✝ : x ⟶ y
x✝ y✝ z✝ : C
f : x✝ ⟶ y✝
g : y✝ ⟶ z✝
hf : W f
hg : W.multiplicativeClosure' g
hr : W.multiplicativeClosure g
⊢ W.multiplicativeClosure (f ≫ g)

Tactic:
| of_comp f g hf hg hr =>

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

Goal state before:
pp: case map.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
x : C
⊢ (W.strictMap F).multiplicativeClosure (F.map (𝟙 x))

Tactic:
simpa using

Goal state after:
case map.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
x : C
⊢ (W.strictMap F).multiplicativeClosure (𝟙 (F.obj x))
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case map.comp_of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf : W.multiplicativeClosure f✝
hg : W g✝
h : (W.strictMap F).multiplicativeClosure (F.map f✝)
⊢ (W.strictMap F).multiplicativeClosure (F.map (f✝ ≫ g✝))

Tactic:
simpa using

Goal state after:
case map.comp_of
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
X✝¹ Y✝¹ : D
f : X✝¹ ⟶ Y✝¹
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf : W.multiplicativeClosure f✝
hg : W g✝
h : (W.strictMap F).multiplicativeClosure (F.map f✝)
⊢ (W.strictMap F).multiplicativeClosure (F.map f✝ ≫ F.map g✝)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hg : IsIso g
hfg : IsIso (f ≫ g)
⊢ isomorphisms C f

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hg : IsIso g
hfg : IsIso (f ≫ g)
⊢ IsIso f