mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (WithTerminal J) F
K✝ : J ⥤ Over X
coneK : Cone K✝
isLimitConeK : IsLimit coneK
isLimitConeD : IsLimit ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK)))
⊢ ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).π.app WithTerminal.star =
    (Iso.refl ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).pt).hom ≫
      (coneEquiv.functor.obj ((Over.post F).mapCone coneK)).π.app WithTerminal.star

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (WithTerminal J) F
K✝ : J ⥤ Over X
coneK : Cone K✝
isLimitConeK : IsLimit coneK
isLimitConeD : IsLimit ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK)))
a : J
⊢ ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).π.app (of a) =
    (Iso.refl ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).pt).hom ≫
      (coneEquiv.functor.obj ((Over.post F).mapCone coneK)).π.app (of a)

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (WithInitial J) F
K✝ : J ⥤ Under X
coconeK : Cocone K✝
isColimitCoconeK : IsColimit coconeK
isColimitCoconeD :
  IsColimit ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK)))
⊢ ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).ι.app
        WithInitial.star ≫
      (Iso.refl
          ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).pt).hom =
    (coconeEquiv.functor.obj ((Under.post F).mapCocone coconeK)).ι.app WithInitial.star

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasCoproducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : C ⥤ A
x : C
⊢ (Sigma.desc fun x_1 ↦ 𝟙 (F.obj (((incl C).obj x).obj x_1))) ≫ Sigma.ι (fun x_1 ↦ F.obj x) PUnit.unit =
    𝟙 (((eval C A ⋙ (whiskeringLeft C (FormalCoproduct C) A).obj (incl C)).obj F).obj x)

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (WithInitial J) F
K✝ : J ⥤ Under X
coconeK : Cocone K✝
isColimitCoconeK : IsColimit coconeK
isColimitCoconeD :
  IsColimit ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK)))
a : J
⊢ ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).ι.app (of a) ≫
      (Iso.refl
          ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).pt).hom =
    (coconeEquiv.functor.obj ((Under.post F).mapCocone coconeK)).ι.app (of a)

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasProducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : Cᵒᵖ ⥤ A
x : Cᵒᵖ
⊢ (Pi.π (fun i ↦ F.obj (op ((unop ((incl C).op.obj x)).obj i))) PUnit.unit ≫
      Pi.lift fun x_1 ↦ 𝟙 (((𝟭 (Cᵒᵖ ⥤ A)).obj F).obj x)) =
    𝟙 (((evalOp C A ⋙ (whiskeringLeft Cᵒᵖ (FormalCoproduct C)ᵒᵖ A).obj (incl C).op).obj F).obj x)

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasProducts A
J : Type w
f : J → FormalCoproduct C
F : Cᵒᵖ ⥤ A
s : Cone ((Discrete.functor fun x ↦ op (f x)) ⋙ (evalOp C A).obj F)
m : s.pt ⟶ (((evalOp C A).obj F).mapCone (cofan J f).op).pt
h : ∀ (j : Discrete J), m ≫ (((evalOp C A).obj F).mapCone (cofan J f).op).π.app j = s.π.app j
x✝ : (unop (cofan J f).op.pt).I
i₁ : J
i₂ : (f i₁).I
⊢ m ≫ Pi.π (fun i ↦ F.obj (op ((unop (cofan J f).op.pt).obj i))) ⟨i₁, i₂⟩ =
    (Pi.lift fun i ↦
        s.π.app { as := i.fst } ≫
          Pi.π (fun i_1 ↦ F.obj (op ((unop ((Discrete.functor fun x ↦ op (f x)).obj { as := i.fst })).obj i_1)))
            i.snd) ≫
      Pi.π (fun i ↦ F.obj (op ((unop (cofan J f).op.pt).obj i))) ⟨i₁, i₂⟩

Tactic:
by simp [← h, cofan]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ ∀ (s : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)),
    ((lift fun b ↦
          if h : P b then s.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
          else s.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
        map' Subtype.val fun x ↦ 𝟙 (X ↑x)) =
      s.fst

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ ∀ (s : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)),
    ((lift fun b ↦
          if h : P b then s.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
          else s.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
        map' Subtype.val fun x ↦ 𝟙 (X ↑x)) =
      s.snd

Tactic:
by aesop

Goal state after:
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
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom (P.map (F.map g))) (shrinkYonedaEquiv (c'.ι.app (op X) ≫ f)) =
    shrinkYonedaEquiv (c'.ι.app (op X') ≫ f)

Tactic:
← dsimp% c'.w g.op,

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
f : c'.pt ⟶ P
X X' : J
g : X ⟶ X'
⊢ (ConcreteCategory.hom (P.map (F.map g))) (shrinkYonedaEquiv (c'.ι.app (op X) ≫ f)) =
    shrinkYonedaEquiv ((shrinkYoneda.{w, v, u}.map (F.map g).unop ≫ c'.ι.app (op X)) ≫ f)
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
⊢ ∃ a, (fun g ↦ f ≫ g) a = g

Tactic:
let c : Cocone hf.F :=
        { pt := Z
          ι.app j := σ.1 (op j)
          ι.naturality _ _ f := by
            dsimp
            simpa only [Category.comp_id] using! σ.2 f.op }

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
c : Cocone hf.F := { pt := Z, ι := { app := fun j ↦ ↑σ (op j), naturality := ⋯ } }
⊢ ∃ a, (fun g ↦ f ≫ g) a = g
Module: Mathlib.CategoryTheory.Localization.BousfieldTransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
P : ObjectProperty C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
x✝ : P.isLocal.transfiniteCompositionsOfShape J f
Z : C
hZ : P Z
hf : P.isLocal.TransfiniteCompositionOfShape J f
g : X ⟶ Z
d : (hf.F.op ⋙ yoneda.obj Z).WellOrderInductionData := Functor.WellOrderInductionData.ofExists ⋯ ⋯
σ : ↑(hf.F.op ⋙ yoneda.obj Z).sections := d.sectionsMk (hf.isoBot.hom ≫ g)
c : Cocone hf.F := { pt := Z, ι := { app := fun j ↦ ↑σ (op j), naturality := ⋯ } }
⊢ (fun g ↦ f ≫ g) (hf.isColimit.desc c) = g

Tactic:
simp only [← hf.fac, Category.assoc, hf.isColimit.fac c ⊥, c, σ,
          d.sectionsMk_val_op_bot, Iso.inv_hom_id_assoc]

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
⊢ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm (g ≫ v) =
    (toOver I).map g ≫ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ }.symm v

Tactic:
dsimp [sectionsCurry, sectionsUncurry, curryRightUnitorHom]

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))) ⋯ =
    (toOver I).map g ≫
      homMk ((β_ A I).hom ≫ uncurry (v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))) ⋯
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 : C
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } (u ≫ g) =
    { toFun := sectionsCurry, invFun := sectionsUncurry, left_inv := ⋯, right_inv := ⋯ } u ≫ (sections I).map g

Tactic:
dsimp [sectionsCurry, sectionsUncurry, curryRightUnitorHom]

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
X' X : Over I
u : (toOver I).obj A ⟶ X'
g : X' ⟶ X
⊢ ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯ =
    ChosenPullbacksAlong.lift (curry ((β_ I A).hom ≫ Hom.left u)) (toUnit A) ⋯ ≫ (sections I).map g
Module: Mathlib.CategoryTheory.Monad.Kleisli

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
T : Monad C
W✝ X✝ Y✝ Z✝ : Kleisli T
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ { of := { of := f.of ≫ T.map g.of ≫ T.μ.app Y✝.of }.of ≫ T.map h.of ≫ T.μ.app Z✝.of } =
    { of := f.of ≫ T.map { of := g.of ≫ T.map h.of ≫ T.μ.app Z✝.of }.of ≫ T.μ.app Z✝.of }

Tactic:
by
    simp [Monad.assoc, T.mu_naturality_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Action.End

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ (D ⥤ D)ᴹᵒᵖ
inst✝ : F.Monoidal
c₁ c₂ c₃ : C
d : D
⊢ (F.map (α_ c₁ c₂ c₃).hom).unmop.app d ≫
      ((Functor.Monoidal.μIso F c₁ (c₂ ⊗ c₃)).unmop.app d).symm.hom ≫
        (F.obj c₁).unmop.map ((Functor.Monoidal.μIso F c₂ c₃).unmop.app d).symm.hom =
    ((Functor.Monoidal.μIso F (c₁ ⊗ c₂) c₃).unmop.app d).symm.hom ≫
      ((Functor.Monoidal.μIso F c₁ c₂).unmop.app ((F.obj c₃).unmop.obj d)).symm.hom

Tactic:
by
    have e := congrArg (fun t ↦ t.unmop.app d) <|
      Functor.OplaxMonoidal.associativity F c₁ c₂ c₃
    dsimp at e
    simp only [Category.comp_id] at e
    simp [e]

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' N' O' : D
A✝¹ : C
inst✝⁸ : MonObj A✝¹
M✝¹ N O : D
inst✝⁷ : ModObj A✝¹ M✝¹
inst✝⁶ : ModObj A✝¹ N
inst✝⁵ : ModObj A✝¹ O
A✝ : C
inst✝⁴ : MonObj A✝
M✝ : Mod D A✝
A B : C
inst✝³ : MonObj A
inst✝² : MonObj B
f : A ⟶ B
inst✝¹ : IsMonHom f
M : D
inst✝ : ModObj B M
⊢ μ ⊵ₗ M ≫ f ⊵ₗ M ≫ γ = (αₗ A A M).hom ≫ A ⊴ₗ (f ⊵ₗ M ≫ γ) ≫ f ⊵ₗ M ≫ γ

Tactic:
by
    -- oh, for homotopy.io in a widget!
    slice_rhs 2 3 => rw [action_exchange]
    simp only [actionHomLeft_action_assoc, Category.assoc, Iso.hom_inv_id_assoc,
      actionHomRight_comp]
    slice_rhs 4 6 => rw [ModObj.assoc_flip]
    slice_rhs 2 4 => rw [← whiskerLeft_actionHomLeft]
    slice_rhs 1 2 => rw [← comp_actionHomLeft]
    rw [← comp_actionHomLeft, Category.assoc, ← comp_actionHomLeft_assoc,
      IsMonHom.mul_hom, tensorHom_def, Category.assoc]

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

Goal state before:
pp: D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    ((𝟭 (D ⥤ C)).obj G).map f ≫ (ihom.coev (F.obj Y)).app (G.obj Y) =
      (ihom.coev (F.obj X)).app (G.obj X) ≫ ((tensorLeft F ⋙ F.closedIhom).obj G).map f

Tactic:
intro X Y f

Goal state after:
D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ ((𝟭 (D ⥤ C)).obj G).map f ≫ (ihom.coev (F.obj Y)).app (G.obj Y) =
    (ihom.coev (F.obj X)).app (G.obj X) ≫ ((tensorLeft F ⋙ F.closedIhom).obj G).map f
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid

Goal state before:
pp: D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
⊢ ∀ ⦃X Y : D⦄ (f : X ⟶ Y),
    ((F.closedIhom ⋙ tensorLeft F).obj G).map f ≫ (ihom.ev (F.obj Y)).app (G.obj Y) =
      (ihom.ev (F.obj X)).app (G.obj X) ≫ ((𝟭 (D ⥤ C)).obj G).map f

Tactic:
intro X Y f

Goal state after:
D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ ((F.closedIhom ⋙ tensorLeft F).obj G).map f ≫ (ihom.ev (F.obj Y)).app (G.obj Y) =
    (ihom.ev (F.obj X)).app (G.obj X) ≫ ((𝟭 (D ⥤ C)).obj G).map f
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
f₂ : F₂ ⟶ F₂'
g : F₂' ⟶ functorEnrichedHom C F₁ F₃
⊢ homEquiv.symm (f₂ ≫ g) = F₁ ◁ f₂ ≫ homEquiv.symm g

Tactic:
dsimp [homEquiv]
  ext j
  simp [← uncurry_natural_left]

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
η : 𝟭 C ⟶ L ⋙ i := ir.unit
ε : i ⋙ L ⟶ 𝟭 D := ir.counit
B : D
A : C
⊢ i.obj (L.obj (A ⟹ i.obj B)) ⟶ A ⟹ i.obj B

Tactic:
apply MonoidalClosed.curry (ir.homEquiv _ _ _)
    apply _ ≫ (ir.homEquiv _ _).symm ((ihom.ev A).app (i.obj B))
    exact prodComparison L A _ ≫ (_ ◁ (ε.app _)) ≫ inv (prodComparison _ _ _)

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

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  (MonoidalClosed.pre (F.map φ)).app (G.obj (j' ⊗ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ihom (F.obj j')).map (f.app (j' ⊗ c)) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))
⊢ ℌ.π c j ≫ (ihom (F.obj j)).map (G.map (φ ▷ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ℌ.π c j' ≫ (ihom (F.obj j')).map (f.app (j' ⊗ c))) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))

Tactic:
reassoc_of% ℌ.hπ

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
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c j j' : C
φ : j ⟶ j'
this :
  (MonoidalClosed.pre (F.map φ)).app (G.obj (j' ⊗ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ihom (F.obj j')).map (f.app (j' ⊗ c)) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))
⊢ ℌ.π c j' ≫ (MonoidalClosed.pre (F.map φ)).app (G.obj (j' ⊗ c)) ≫ (ihom (F.obj j)).map (f.app (j' ⊗ c)) =
    (ℌ.π c j' ≫ (ihom (F.obj j')).map (f.app (j' ⊗ c))) ≫ (MonoidalClosed.pre (F.map φ)).app (G'.obj (j' ⊗ c))
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

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
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
          (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯ ≫
        Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j =
    Wedge.IsLimit.lift (ℌ.isLimitWedge c) (fun c' ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c', c))) ⋯ ≫
      Multifork.ι (Wedge.mk (H.obj c) (ℌ.π c) ⋯) j ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))

Tactic:
Wedge.IsLimit.lift_ι_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
inst✝¹ : MonoidalClosed V
F G✝ H G : C ⥤ V
inst✝ : DayConvolution F G
ℌ : DayConvolutionInternalHom F (F ⊛ G) H
c c' : C
f : c ⟶ c'
j : C
⊢ G.map f ≫
      Wedge.IsLimit.lift (ℌ.isLimitWedge c')
          (fun c'_1 ↦ MonoidalClosed.curry ((DayConvolution.unit F G).app (c'_1, c'))) ⋯ ≫
        Multifork.ι (Wedge.mk (H.obj c') (ℌ.π c') ⋯) j =
    MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c)) ≫ (ihom (F.obj j)).map ((F ⊛ G).map (j ◁ f))
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro X Y f

Goal state after:
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
⊢ (tensorFunc C).map f ≫ (normalizeIsoAux C Y).hom = (normalizeIsoAux C X).hom ≫ (normalize' C).map f
Module: Mathlib.CategoryTheory.Monoidal.Free.Coherence

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro X Y f

Goal state after:
C : Type u
X Y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
f : X ⟶ Y
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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
| R.X ◁
      coequalizer.π (P.actRight ▷ coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))
        ((α_ P.X S.X (coequalizer (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft))).hom ≫
          P.X ◁ TensorBimod.actLeft Q L) ≫
    TensorBimod.actLeft P (Q.tensorBimod L)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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
| R.X ◁ (α_ P.X Q.X L.X).hom

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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
| R.X ◁ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)

Tactic:
erw [TensorBimod.whiskerLeft_π_actLeft P (Q.tensorBimod L)]

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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
| (α_ R.X P.X (Q.tensorBimod L).X).inv ≫
    P.actLeft ▷ (Q.tensorBimod L).X ≫
      coequalizer.π (P.actRight ▷ (Q.tensorBimod L).X)
        ((α_ P.X S.X (Q.tensorBimod L).X).hom ≫ P.X ◁ (Q.tensorBimod L).actLeft)

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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
| R.X ◁ (α_ P.X Q.X L.X).hom

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
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
| R.X ◁ P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ f ≫ 𝒮 * f = 1

Tactic:
Conv.mul_eq,

Goal state after:
case hba
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : BraidedCategory C
A B : C
inst✝² : HopfObj A
inst✝¹ : HopfObj B
f : A ⟶ B
inst✝ : IsBimonHom f
⊢ Δ ≫ (f ≫ 𝒮) ▷ A ≫ B ◁ f ≫ μ = 1