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

Goal state before:
pp: J : Type w
inst✝⁴ : Finite J
C : J → Type u₁
D : J → Type u₂
inst✝³ : (j : J) → Category.{v₁, u₁} (C j)
inst✝² : (j : J) → Category.{v₂, u₂} (D j)
L : (j : J) → C j ⥤ D j
W : (j : J) → MorphismProperty (C j)
inst✝¹ : ∀ (j : J), (W j).ContainsIdentities
inst✝ : ∀ (j : J), (L j).IsLocalization (W j)
⊢ (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
by
  revert J
  apply Finite.induction_empty_option
  · intro J₁ J₂ e hJ₁ C₂ D₂ _ _ L₂ W₂ _ _
    let L₁ := fun j => (L₂ (e j))
    let E := Pi.equivalenceOfEquiv C₂ e
    let E' := Pi.equivalenceOfEquiv D₂ e
    have : CatCommSq E.functor (Functor.pi L₁) (Functor.pi L₂) E'.functor :=
      (CatCommSq.hInvEquiv E (Functor.pi L₁) (Functor.pi L₂) E').symm ⟨Iso.refl _⟩
    refine IsLocalization.of_equivalences (Functor.pi L₁)
      (MorphismProperty.pi (fun j => (W₂ (e j)))) (Functor.pi L₂)
      (MorphismProperty.pi W₂) E E' ?_
      (MorphismProperty.IsInvertedBy.pi _ _ (fun _ => Localization.inverts _ _))
    intro _ _ f hf
    refine ⟨_, _, E.functor.map f, fun i => ?_, ⟨Iso.refl _⟩⟩
    have H : ∀ {j j' : J₂} (h : j = j') {X Y : C₂ j} (g : X ⟶ Y) (_ : W₂ j g),
        W₂ j' ((Pi.eqToEquivalence C₂ h).functor.map g) := by
      rintro j _ rfl _ _ g hg
      exact hg
    exact H (e.apply_symm_apply i) _ (hf (e.symm i))
  · intro C D _ _ L W _ _
    have : ∀ j, IsEquivalence (L j) := by rintro ⟨⟩
    refine IsLocalization.of_isEquivalence _ _ (fun _ _ _ _ => ?_)
    rw [MorphismProperty.isomorphisms.iff, isIso_pi_iff]
    rintro ⟨⟩
  · intro J _ hJ C D _ _ L W _ _
    let L₁ := (L none).prod (Functor.pi (fun j => L (some j)))
    have : CatCommSq (Pi.optionEquivalence C).symm.functor L₁ (Functor.pi L)
      (Pi.optionEquivalence D).symm.functor :=
        ⟨NatIso.pi' (by rintro (_ | i) <;> apply Iso.refl)⟩
    refine IsLocalization.of_equivalences L₁
      ((W none).prod (MorphismProperty.pi (fun j => W (some j)))) (Functor.pi L) _
      (Pi.optionEquivalence C).symm (Pi.optionEquivalence D).symm ?_ ?_
    · intro ⟨X₁, X₂⟩ ⟨Y₁, Y₂⟩ f ⟨hf₁, hf₂⟩
      refine ⟨_, _, (Pi.optionEquivalence C).inverse.map f, ?_, ⟨Iso.refl _⟩⟩
      rintro (_ | i)
      · exact hf₁
      · apply hf₂
    · apply MorphismProperty.IsInvertedBy.pi
      rintro (_ | i) <;> apply Localization.inverts

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

Goal state before:
pp: case whiskerRight
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)
Y✝ Z✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f✝ f'✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
X✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
a✝ : HomEquiv f✝ f'✝
hf : projectMapAux f✝¹ f✝ = projectMapAux f✝¹ f'✝
⊢ projectMapAux f✝¹ (f✝.whiskerRight X✝) = projectMapAux f✝¹ (f'✝.whiskerRight X✝)

Tactic:
| whiskerRight _ _ _ _ hf =>

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
I J K : C
f : I ⟶ J
g : J ⟶ K
inst✝⁴ : ChosenPullbacksAlong f
inst✝³ : ChosenPullbacksAlong g
inst✝² : ChosenPullbacksAlong (f ≫ g)
inst✝¹ : ExponentiableMorphism f
inst✝ : ExponentiableMorphism g
⊢ pushforward (f ≫ g) = pushforward f ⋙ pushforward g

Tactic:
by
  dsimp +instances only [comp]

Goal state after:
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
⊢ T✝.hom = Over.Hom.left v ≫ Z.hom

Tactic:
Over.w v

Goal state after:
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
⊢ T✝.hom = T✝.hom
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
⊢ ((comparisonAdjunction adj).unit.app A).f = (beckCoequalizer A).desc (unitCofork A)

Tactic:
apply Limits.Cofork.IsColimit.hom_ext (beckCoequalizer A)
  rw [Cofork.IsColimit.π_desc]
  dsimp only [beckCofork_π, unitCofork_π]
  rw [comparisonAdjunction_unit_f_aux, ← adj.homEquiv_naturality_left A.a, coequalizer.condition,
    adj.homEquiv_naturality_right, adj.homEquiv_unit, Category.assoc]
  apply adj.right_triangle_components_assoc

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

Goal state before:
pp: case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ X₁.right ◁ X₂.left ◁ Arrow.Hom.right f₃ ≫
      (α_ X₁.right X₂.left Y₃.right).inv ≫
        Arrow.Hom.right f₁ ▷ X₂.left ▷ Y₃.right ≫
          (α_ Y₁.right X₂.left Y₃.right).hom ≫
            Y₁.right ◁ Arrow.Hom.left f₂ ▷ Y₃.right ≫ Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) =
    X₁.right ◁ Arrow.Hom.left f₂ ▷ X₃.right ≫
      X₁.right ◁ Y₂.left ◁ Arrow.Hom.right f₃ ≫
        X₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) ≫
          Arrow.Hom.right f₁ ▷ pushout (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom)

Tactic:
← MonoidalCategory.whiskerLeft_comp_assoc,

Goal state after:
case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ X₁.right ◁ X₂.left ◁ Arrow.Hom.right f₃ ≫
      (α_ X₁.right X₂.left Y₃.right).inv ≫
        Arrow.Hom.right f₁ ▷ X₂.left ▷ Y₃.right ≫
          (α_ Y₁.right X₂.left Y₃.right).hom ≫
            Y₁.right ◁ Arrow.Hom.left f₂ ▷ Y₃.right ≫ Y₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) =
    X₁.right ◁ (Arrow.Hom.left f₂ ▷ X₃.right ≫ Y₂.left ◁ Arrow.Hom.right f₃) ≫
      X₁.right ◁ pushout.inr (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom) ≫
        Arrow.Hom.right f₁ ▷ pushout (Y₂.hom ▷ Y₃.left) (Y₂.left ◁ Y₃.hom)
Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
⊢ (tensorRight Y.right).map
        (pushout.inl (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((α_ X (𝟙_ (Arrow C)) Y).hom ≫ X ◁ (λ_ Y).hom) =
    (tensorRight Y.right).map
        (pushout.inl (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((ρ_ X).hom ▷ Y)

pp: case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
⊢ (tensorRight Y.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((α_ X (𝟙_ (Arrow C)) Y).hom ≫ X ◁ (λ_ Y).hom) =
    (tensorRight Y.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((ρ_ X).hom ▷ Y)

Tactic:
· apply (initialIsInitial.ofIso ((initialIsoIsInitial ?_) ≪≫ (mulZero ?_).symm)).hom_ext <;>
    exact initialIsInitial.ofIso (zeroMul initialIsInitial).symm

Goal state after:
case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X Y : Arrow C
⊢ (tensorRight Y.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((α_ X (𝟙_ (Arrow C)) Y).hom ≫ X ◁ (λ_ Y).hom) =
    (tensorRight Y.right).map
        (pushout.inr (((curriedTensor C).map X.hom).app (𝟙_ (Arrow C)).left)
          (((curriedTensor C).obj X.left).map (𝟙_ (Arrow C)).hom)) ≫
      pushout.inr (((curriedTensor C).map (X ⊗ 𝟙_ (Arrow C)).hom).app Y.left)
          (((curriedTensor C).obj (X ⊗ 𝟙_ (Arrow C)).left).map Y.hom) ≫
        Arrow.Hom.left ((ρ_ X).hom ▷ Y)
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 T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ (α_ (R.X ⊗ R.X) P.X Q.X).inv ≫
      ((α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (((α_ R.X R.X (P.X ⊗ Q.X)).hom ≫
          R.X ◁ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫
        R.X ◁ actLeft P Q) ≫
      actLeft P Q

Tactic:
slice_rhs 2 3 =>
    rw [← whiskerLeft_comp, whiskerLeft_π_actLeft,
      whiskerLeft_comp, whiskerLeft_comp]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ (α_ (R.X ⊗ R.X) P.X Q.X).inv ≫
      ((α_ R.X R.X P.X).hom ▷ Q.X ≫ (R.X ◁ P.actLeft) ▷ Q.X ≫ P.actLeft ▷ Q.X) ≫
        coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) =
    (α_ R.X R.X (P.X ⊗ Q.X)).hom ≫
      (R.X ◁ (α_ R.X P.X Q.X).inv ≫
          R.X ◁ P.actLeft ▷ Q.X ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫
        actLeft P Q
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: case refine_1
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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ δ L (R.obj c) (R.obj X✝) ≫
      L.obj (R.obj c) ◁ L.map (R.map x✝) ≫ L.obj (R.obj c) ◁ adj.counit.app Y✝ ≫ adj.counit.app c ▷ Y✝ =
    δ L (R.obj c) (R.obj X✝) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X✝) ≫ c ◁ x✝

Tactic:
← MonoidalCategory.whiskerLeft_comp_assoc,

Goal state after:
case refine_1
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
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
c X✝ Y✝ : C
x✝ : X✝ ⟶ Y✝
⊢ δ L (R.obj c) (R.obj X✝) ≫ L.obj (R.obj c) ◁ (L.map (R.map x✝) ≫ adj.counit.app Y✝) ≫ adj.counit.app c ▷ Y✝ =
    δ L (R.obj c) (R.obj X✝) ≫ (adj.counit.app c ⊗ₘ adj.counit.app X✝) ≫ c ◁ x✝
Module: Mathlib.CategoryTheory.Monoidal.Closed.Functor

Goal state before:
pp: case e'_3.e'_6
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v, u'} D
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝² : MonoidalClosed C
inst✝¹ : MonoidalClosed D
inst✝ : Limits.PreservesLimitsOfShape (Discrete Limits.WalkingPair) F
A B : C
e_1✝ :
  (F.obj A ⊗ (ihom A ⋙ F).obj B ⟶ (𝟭 D).obj (F.obj B)) =
    (((curriedTensor D).obj (F.obj A)).obj ((ihom A ⋙ F).obj B) ⟶ (𝟭 D).obj (F.obj B))
e_3✝ : F.obj A ⊗ F.obj ((ihom A).obj B) = (F ⋙ (curriedTensor D).obj (F.obj A)).obj ((ihom A).obj B)
e_4✝ : F.obj (A ⊗ (ihom A).obj B) = ((curriedTensor C).obj A ⋙ F).obj ((ihom A).obj B)
⊢ prodComparison F A ((ihom A).obj B) ≫ (prodComparisonNatIso F A).inv.app ((ihom A).obj B) =
    𝟙 (F.obj (A ⊗ (ihom A).obj B))

Tactic:
simp only [prodComparisonNatTrans_app, prodComparisonNatIso_inv, NatIso.isIso_inv_app,
    IsIso.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: case e_a
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
g : F₂ ⟶ functorEnrichedHom C F₁ F₃
j j' : J
φ : j ⟶ j'
α : Under.mk (𝟙 j) ⟶ (Under.map φ).obj (Under.mk (𝟙 j')) := Under.homMk φ ⋯
⊢ enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) ((Under.map φ).obj (Under.mk (𝟙 j'))) ≫
      eHomWhiskerRight C (F₁.map φ) (F₃.obj j') =
    enrichedHomπ C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) (Under.mk (𝟙 j)) ≫
      eHomWhiskerLeft C (F₁.obj j) (F₃.map φ)

Tactic:
exact (enrichedHom_condition C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃) α).symm

Goal state after:
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₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        (ρ_ (((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k)).inv ≫
          ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
              ((Enriched.FunctorCategory.homEquiv C) f₃ ≫ precompEnrichedHom C F₃ F₃' (Under.forget j)) ≫
            ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
                end_.π (diagram C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) k ≫
              eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
                ((Under.forget j ⋙ F₃').obj k)

Tactic:
← MonoidalCategory.whiskerLeft_comp_assoc,

Goal state after:
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₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right ≫ f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        (ρ_ (((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k)).inv ≫
          ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k)).obj k ◁
              (((Enriched.FunctorCategory.homEquiv C) f₃ ≫ precompEnrichedHom C F₃ F₃' (Under.forget j)) ≫
                end_.π (diagram C (Under.forget j ⋙ F₃) (Under.forget j ⋙ F₃')) k) ≫
            eComp C (Opposite.unop ((Under.forget j ⋙ F₁).op.obj (Opposite.op k))) ((Under.forget j ⋙ F₃).obj k)
              ((Under.forget j ⋙ F₃').obj k)
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✝ : MonoidalClosed C
B : Subterminals C
A : C
⊢ (subterminalInclusion C).essImage (A ⟹ (subterminalInclusion C).obj B)

Tactic:
refine ⟨⟨A ⟹ B.1, fun Z g h => ?_⟩, ⟨Iso.refl _⟩⟩

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✝ : MonoidalClosed C
B : Subterminals C
A Z : C
g h : Z ⟶ A ⟹ B.obj
⊢ g = h
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
this : HasFiniteProducts D
⊢ i.essImage (i.obj X ⊗ i.obj Y)

Tactic:
use Limits.prod X Y

Goal state after:
case h
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 : HasFiniteProducts D
⊢ Nonempty (i.obj (X ⨯ Y) ≅ i.obj X ⊗ i.obj Y)
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case h₂
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
⊢ BinaryFan.snd
      ((Cone.postcompose (pairComp X Y i).hom).obj
        (i.mapCone
          (BinaryFan.mk ((reflector i).map (fst (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app X)
            ((reflector i).map (snd (i.obj X) (i.obj Y)) ≫ (reflectorAdjunction i).counit.app Y)))) =
    (_root_.id (asIso ((reflectorAdjunction i).unit.app (i.obj X ⊗ i.obj Y))).symm).hom ≫
      (BinaryFan.mk (fst (i.obj X) (i.obj Y)) (snd (i.obj X) (i.obj Y))).snd

Tactic:
simp only [BinaryFan.snd, Cone.postcompose, pairComp]
          simp [← Functor.comp_map, ← NatTrans.naturality_assoc]

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

Goal state before:
pp: C : Type u
X Y X✝ Y✝ Z✝ : F C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
ihf :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ f ≫ (normalizeIsoApp' C Y✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)
ihg :
  ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ g ≫ (normalizeIsoApp' C Z✝ n).hom = (normalizeIsoApp' C Y✝ n).hom ≫ inclusion.map (eqToHom ⋯)
⊢ ∀ (n : NormalMonoidalObject C),
    inclusionObj n ◁ (f ≫ g) ≫ (normalizeIsoApp' C Z✝ n).hom = (normalizeIsoApp' C X✝ n).hom ≫ inclusion.map (eqToHom ⋯)

Tactic:
simp [ihg, reassoc_of% (ihf _)]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : ModuleCat R
inst✝ : MonObj A
x : ↑A
⊢ (ConcreteCategory.hom μ) (0 ⊗ₜ[R] x) = 0

Tactic:
rw [TensorProduct.zero_tmul, map_zero]

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 G H : J ⥤ C
j : J
| limit.π F j ▷ limit G ▷ limit H ≫ (α_ (F.obj j) (limit G) (limit H)).hom ≫ F.obj j ◁ (limit.π G j ⊗ₘ limit.π H j)

Tactic:
rw [tensorHom_def, whiskerLeft_comp,
        ← associator_naturality_middle_assoc,
        ← associator_naturality_right, ← comp_whiskerRight_assoc,
        ← tensorHom_def, ← tensorHom_def_assoc]

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 G H : J ⥤ C
j : J
| ((limit.π F j ⊗ₘ limit.π G j) ⊗ₘ limit.π H j) ≫ (α_ (F.obj j) (G.obj j) (H.obj j)).hom
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
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ▷ H.obj x✝.2 ≫
      (F'.obj x✝.1.1 ⊗ G'.obj x✝.1.2) ◁ h.app x✝.2 ≫
        (α_ (F'.obj x✝.1.1) ((G', H').1.obj (x✝.1.2, x✝.2).1) ((G', H').2.obj (x✝.1.2, x✝.2).2)).hom ≫
          F'.obj x✝.1.1 ◁ (unit G' H').app (x✝.1.2, x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
              (F' ⊛ G' ⊛ H').map (α_ (x✝.1.1, x✝.1.2 ⊗ x✝.2).1 x✝.1.2 x✝.2).inv =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      f.app x✝.1.1 ▷ (G.obj x✝.1.2 ⊗ H.obj x✝.2) ≫
        F'.obj x✝.1.1 ◁ (unit G H).app (x✝.1.2, x✝.2) ≫
          F'.obj x✝.1.1 ◁ (map g h).app (x✝.1.2 ⊗ x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv

Tactic:
← MonoidalCategory.whiskerLeft_comp_assoc,

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
F G : C ⥤ V
inst✝⁹ : DayConvolution F G
H : C ⥤ V
inst✝⁸ : DayConvolution G H
inst✝⁷ : DayConvolution F (G ⊛ H)
inst✝⁶ : DayConvolution (F ⊛ G) H
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)
F' G' H' : C ⥤ V
inst✝³ : DayConvolution F' G'
inst✝² : DayConvolution G' H'
inst✝¹ : DayConvolution F' (G' ⊛ H')
inst✝ : DayConvolution (F' ⊛ G') H'
f : F ⟶ F'
g : G ⟶ G'
h : H ⟶ H'
x✝ : (C × C) × C
⊢ (f.app x✝.1.1 ⊗ₘ g.app x✝.1.2) ▷ H.obj x✝.2 ≫
      (F'.obj x✝.1.1 ⊗ G'.obj x✝.1.2) ◁ h.app x✝.2 ≫
        (α_ (F'.obj x✝.1.1) ((G', H').1.obj (x✝.1.2, x✝.2).1) ((G', H').2.obj (x✝.1.2, x✝.2).2)).hom ≫
          F'.obj x✝.1.1 ◁ (unit G' H').app (x✝.1.2, x✝.2) ≫
            (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫
              (F' ⊛ G' ⊛ H').map (α_ (x✝.1.1, x✝.1.2 ⊗ x✝.2).1 x✝.1.2 x✝.2).inv =
    (α_ (F.obj x✝.1.1) (G.obj x✝.1.2) (H.obj x✝.2)).hom ≫
      f.app x✝.1.1 ▷ (G.obj x✝.1.2 ⊗ H.obj x✝.2) ≫
        F'.obj x✝.1.1 ◁ ((unit G H).app (x✝.1.2, x✝.2) ≫ (map g h).app (x✝.1.2 ⊗ x✝.2)) ≫
          (unit F' (G' ⊛ H')).app (x✝.1.1, x✝.1.2 ⊗ x✝.2) ≫ (F' ⊛ G' ⊛ H').map (α_ x✝.1.1 x✝.1.2 x✝.2).inv
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalAccessibleCategory C κ
⊢ (isCardinalPresentable C κ).IsCardinalFilteredGenerator κ

Tactic:
by
  obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ
  refine hP.of_le_isoClosure ?_ le_rfl
  rw [ObjectProperty.isoClosure_eq_self]
  exact hP.le_isCardinalPresentable

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

Goal state before:
pp: case of_limitPresentation
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddGroup A
inst✝² : HasShift C A
α : Type u_3
J : α → Type u_4
inst✝¹ : (i : α) → Category.{u_5, u_4} (J i)
inst✝ : P.IsStableUnderShift A
a : A
X X✝ : C
a✝ : α
pres : Limits.LimitPresentation (J a✝) X✝
h : ∀ (j : J a✝), P.limitsClosure J (pres.diag.obj j)
h' : ∀ (j : J a✝), (P.limitsClosure J).shift a (pres.diag.obj j)
⊢ (P.limitsClosure J).shift a X✝

Tactic:
| of_limitPresentation pres h h' =>

Goal state after: