mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Over I
A : C
u : (toOver I).obj A ⟶ X
⊢ (β_ I A).hom ≫ ((toOver I).obj A).hom = SemiCartesianMonoidalCategory.fst I A

Tactic:
simp [braiding_hom_snd]

Goal state after:
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✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this : HasCoequalizerOfIsSplitPair G
⊢ ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], PreservesColimit (parallelPair f g) G

Tactic:
intros

Goal state after:
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✝¹ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this : HasCoequalizerOfIsSplitPair G
A✝ B✝ : D
f✝ g✝ : A✝ ⟶ B✝
inst✝ : G.IsSplitPair f✝ g✝
⊢ PreservesColimit (parallelPair f✝ g✝) G
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✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this✝ : HasCoequalizerOfIsSplitPair G
this : PreservesColimitOfIsSplitPair G
⊢ ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], ReflectsColimit (parallelPair f g) G

Tactic:
intros

Goal state after:
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✝¹ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this✝ : HasCoequalizerOfIsSplitPair G
this : PreservesColimitOfIsSplitPair G
A✝ B✝ : D
f✝ g✝ : A✝ ⟶ B✝
inst✝ : G.IsSplitPair f✝ g✝
⊢ ReflectsColimit (parallelPair f✝ g✝) G
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:
have e := congrArg (fun t ↦ t.unmop.app d) <|
      Functor.OplaxMonoidal.associativity F c₁ c₂ c₃

Goal state after:
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
e :
  (Functor.OplaxMonoidal.δ F (c₁ ⊗ c₂) c₃ ≫
            Functor.OplaxMonoidal.δ F c₁ c₂ ▷ F.obj c₃ ≫ (α_ (F.obj c₁) (F.obj c₂) (F.obj c₃)).hom).unmop.app
      d =
    (F.map (α_ c₁ c₂ c₃).hom ≫
            Functor.OplaxMonoidal.δ F c₁ (c₂ ⊗ c₃) ≫ F.obj c₁ ◁ Functor.OplaxMonoidal.δ F c₂ c₃).unmop.app
      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
Module: Mathlib.CategoryTheory.Monoidal.Braided.Transport

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
e : C ≌ D
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : Transported e
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    simp +instances [Transported.instBraidedCategory, BraidedCategory.ofFaithful,
      fromInducedCoreMonoidal, Functor.CoreMonoidal.toLaxMonoidal]

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
this : μ ⊵ₗ Y ≫ (e₁.inv ⊙ₗₘ e₂.inv) = ((e₁.inv ⊗ₘ e₁.inv) ⊙ₗₘ e₂.inv) ≫ μ ⊵ₗ X
⊢ (αₗ N M X).inv ≫ (e₁.inv ▷ M) ⊵ₗ X ≫ (αₗ M M X).hom ≫ M ⊴ₗ γ = N ⊴ₗ γ ≫ e₁.inv ⊵ₗ X

Tactic:
rw [← actionHomLeft_action_assoc, action_exchange]

Goal state after:
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
R S T : Mon C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| P.X ◁ (Q.X ◁ μ ≫ Q.actRight)

pp: case a.a
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₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

pp: case a
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₁} (tensorRight X)
| (α_ P.X Q.X (T.X ⊗ T.X)).hom

Tactic:
right_assoc,

Goal state after:
case a.a
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₁} (tensorRight X)
| P.X ◁ ((α_ Q.X T.X T.X).inv ≫ Q.actRight ▷ T.X ≫ Q.actRight)

case a.a
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₁} (tensorRight X)
| coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)

case a
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₁} (tensorRight X)
| (α_ P.X Q.X (T.X ⊗ T.X)).hom
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
⊢ (P.tensorBimod Q).actRight ▷ L.X ≫ homAux P Q L =
    ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫ homAux P Q L

Tactic:
dsimp [homAux]
      refine (cancel_epi ((tensorRight _ ⋙ tensorRight _).map (coequalizer.π _ _))).1 ?_
      dsimp [TensorBimod.X]
      slice_lhs 1 2 => rw [← comp_whiskerRight, TensorBimod.π_tensor_id_actRight,
        comp_whiskerRight, comp_whiskerRight]
      slice_lhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
      slice_lhs 2 3 => rw [associator_naturality_middle]
      slice_lhs 3 4 =>
        rw [← whiskerLeft_comp, coequalizer.condition,
          whiskerLeft_comp, whiskerLeft_comp]
      slice_rhs 1 2 => rw [associator_naturality_left]
      slice_rhs 2 3 => rw [← whisker_exchange]
      slice_rhs 3 5 => rw [π_tensor_id_preserves_coequalizer_inv_desc]
      simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ 𝒮 ≫ ε = ε

Tactic:
by
  have := (rfl : Δ[A] ≫ (𝒮[A] ▷ A) ≫ μ[A] ≫ ε[A] = _)
  conv at this =>
    rhs
    rw [antipode_left_assoc]
  rw [Bimon.mul_counit, tensorHom_def', Category.assoc, ← whisker_exchange_assoc] at this
  simpa [unitors_equal]

Goal state after:
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
R S : Mon C
P : Bimod R S
⊢ P.actRight ▷ S.X ≫ P.actRight = (α_ P.X S.X S.X).hom ≫ P.X ◁ μ ≫ P.actRight

Tactic:
right_assoc,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
A B : Mon C
M : Bimod A B
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ P.actRight ▷ S.X ≫ P.actRight = (α_ P.X S.X S.X).hom ≫ (α_ P.X S.X S.X).inv ≫ P.actRight ▷ S.X ≫ P.actRight
Module: Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
P : ι → MorphismProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hP : ∀ (i : ι), (P i).HasCardinalLT κ
hι : HasCardinalLT ι κ
⊢ HasCardinalLT (↑(⨆ i, P i).toSet) κ

Tactic:
toSet_iSup

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
P : ι → MorphismProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hP : ∀ (i : ι), (P i).HasCardinalLT κ
hι : HasCardinalLT ι κ
⊢ HasCardinalLT (↑(⋃ i, (P i).toSet)) κ
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F : C ⥤ CommMon D
X : C
⊢ ((β_ ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X
              ((monFunctorCategoryEquivalence C D).inverse.obj (F ⋙ CommMon.forget₂Mon D)).X).hom ≫
          μ).app
      X =
    μ.app X

Tactic:
exact IsCommMonObj.mul_comm (F.obj X).X

Goal state after:
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✝
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
inst✝ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
d d' : D
⊢ ∀ ⦃X Y : C × C⦄ (f : X ⟶ Y),
    ((ι C V D).obj d ⊠ (ι C V D).obj d').map f ≫ convolutionUnitApp V d d' Y.1 Y.2 =
      convolutionUnitApp V d d' X.1 X.2 ≫ (tensor C ⋙ (ι C V D).obj (tensorObj C V d d')).map f

Tactic:
intros

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✝
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁴ : Category.{v₂, u₂} V
inst✝³ : MonoidalCategory C
inst✝² : MonoidalCategory V
D : Type u₃
inst✝¹ : Category.{v₃, u₃} D
inst✝ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
d d' : D
X✝ Y✝ : C × C
f✝ : X✝ ⟶ Y✝
⊢ ((ι C V D).obj d ⊠ (ι C V D).obj d').map f✝ ≫ convolutionUnitApp V d d' Y✝.1 Y✝.2 =
    convolutionUnitApp V d d' X✝.1 X✝.2 ≫ (tensor C ⋙ (ι C V D).obj (tensorObj C V d d')).map f✝
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✝
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
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)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
⊢ ∀ {d₁ d₁' : D} (f₁ : d₁ ⟶ d₁') (d₂ : D) (x y : C),
    (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₂)).app (x, y) ≫ ((ι C V D).map (f₁ ▷ d₂)).app (x ⊗ y) =
      ((ι C V D).map f₁).app x ▷ ((ι C V D).obj d₂).obj y ≫
        (DayConvolution.unit ((ι C V D).obj d₁') ((ι C V D).obj d₂)).app (x, y)

Tactic:
intros

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✝
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
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)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
d₁✝ d₁'✝ : D
f₁✝ : d₁✝ ⟶ d₁'✝
d₂✝ : D
x✝ y✝ : C
⊢ (DayConvolution.unit ((ι C V D).obj d₁✝) ((ι C V D).obj d₂✝)).app (x✝, y✝) ≫
      ((ι C V D).map (f₁✝ ▷ d₂✝)).app (x✝ ⊗ y✝) =
    ((ι C V D).map f₁✝).app x✝ ▷ ((ι C V D).obj d₂✝).obj y✝ ≫
      (DayConvolution.unit ((ι C V D).obj d₁'✝) ((ι C V D).obj d₂✝)).app (x✝, y✝)
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✝
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
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)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
x✝¹ : D
x✝ : C
⊢ DayConvolutionUnit.can ▷ ((ι C V D).obj x✝¹).obj x✝ ≫
      (DayConvolution.unit ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj x✝¹)).app (𝟙_ C, x✝) ≫
        (DayConvolutionUnit.leftUnitor ((ι C V D).obj (tensorUnit C V D)) ((ι C V D).obj x✝¹)).hom.app (𝟙_ C ⊗ x✝) =
    (λ_ (((ι C V D).obj x✝¹).obj x✝)).hom ≫ ((ι C V D).obj x✝¹).map (λ_ x✝).inv

Tactic:
apply DayConvolutionUnit.leftUnitor_hom_unit_app

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasZeroObject C
⊢ isNoetherianObject 0

Tactic:
rw [← isNoetherianObject.is_iff]
    exact isNoetherianObject_of_isZero (isZero_zero C)

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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
⊢ ∀ (X Y : D),
    Functor.LaxMonoidal.μ (Functor.pi' F) X Y ≫ (Functor.pi' F).map (β_ X Y).hom =
      (β_ ((Functor.pi' F).obj X) ((Functor.pi' F).obj Y)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi' F) Y X

Tactic:
intros

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : MonoidalCategory D
inst✝¹ : BraidedCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
X✝ Y✝ : D
⊢ Functor.LaxMonoidal.μ (Functor.pi' F) X✝ Y✝ ≫ (Functor.pi' F).map (β_ X✝ Y✝).hom =
    (β_ ((Functor.pi' F).obj X✝) ((Functor.pi' F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi' F) Y✝ X✝
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : I → Type u₂
inst✝³ : (i : I) → Category.{v₂, u₂} (D i)
inst✝² : (i : I) → MonoidalCategory (D i)
inst✝¹ : (i : I) → BraidedCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
⊢ ∀ (X Y : (i : I) → D i),
    Functor.LaxMonoidal.μ (Functor.pi F) X Y ≫ (Functor.pi F).map (β_ X Y).hom =
      (β_ ((Functor.pi F).obj X) ((Functor.pi F).obj Y)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi F) Y X

Tactic:
intros

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : I → Type u₂
inst✝³ : (i : I) → Category.{v₂, u₂} (D i)
inst✝² : (i : I) → MonoidalCategory (D i)
inst✝¹ : (i : I) → BraidedCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
X✝ Y✝ : (i : I) → D i
⊢ Functor.LaxMonoidal.μ (Functor.pi F) X✝ Y✝ ≫ (Functor.pi F).map (β_ X✝ Y✝).hom =
    (β_ ((Functor.pi F).obj X✝) ((Functor.pi F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi F) Y✝ X✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ ∀ (i : W✝.ι) (j : Z✝.ι), (f.comp g).comp h i j = f.comp (g.comp h) i j

Tactic:
intros

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
W✝ X✝ Y✝ Z✝ : Mat_ C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
i✝ : W✝.ι
j✝ : Z✝.ι
⊢ (f.comp g).comp h i✝ j✝ = f.comp (g.comp h) i✝ j✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
⊢ (∑ j,
      (fun x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
        if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }

Tactic:
ext1 ⟨i, j⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
⊢ ∀ (j_1 : { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.ι),
    (∑ j,
          (fun x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
            if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0)
        ⟨i, j⟩ j_1 =
      𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ j_1
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type u
inst✝ : Semiring R
⊢ ∀ {W X Y Z : Mat R} (f : Matrix W.obj X.obj R) (g : Matrix X.obj Y.obj R) (h : Matrix Y.obj Z.obj R),
    ((have this :=
          (have this := f;
            this) *
            have this := g;
            this;
        this) *
        have this := h;
        this) =
      (have this := f;
        this) *
        have this :=
          (have this := g;
            this) *
            have this := h;
            this;
        this

Tactic:
intros

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type u
inst✝ : Semiring R
W✝ X✝ Y✝ Z✝ : Mat R
f✝ : Matrix W✝.obj X✝.obj R
g✝ : Matrix X✝.obj Y✝.obj R
h✝ : Matrix Y✝.obj Z✝.obj R
⊢ ((have this :=
        (have this := f✝;
          this) *
          have this := g✝;
          this;
      this) *
      have this := h✝;
      this) =
    (have this := f✝;
      this) *
      have this :=
        (have this := g✝;
          this) *
          have this := h✝;
          this;
      this
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id : D.W (𝟙 e)
h₁ : ∀ ⦃j : J⦄, D.P j → ∃ lift, D.W lift
h₂ : ∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂
h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j), D.W f → ∃ li lj, D.W li ∧ D.W lj ∧ f ≫ lj = li
i✝ j✝ : J
x✝ : i✝ ⟶ j✝
hf : D.W x✝
li : i✝ ⟶ e
lj : j✝ ⟶ e
hli : D.W li
hlj : D.W lj
fac : x✝ ≫ lj = li
⊢ x✝ ≫ lj = li

Tactic:
fac

Goal state after:
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
prop_id : D.W (𝟙 e)
h₁ : ∀ ⦃j : J⦄, D.P j → ∃ lift, D.W lift
h₂ : ∀ ⦃j : J⦄, D.P j → ∀ (l₁ l₂ : j ⟶ e), D.W l₁ → D.W l₂ → l₁ = l₂
h₃ : ∀ ⦃i j : J⦄ (f : i ⟶ j), D.W f → ∃ li lj, D.W li ∧ D.W lj ∧ f ≫ lj = li
i✝ j✝ : J
x✝ : i✝ ⟶ j✝
hf : D.W x✝
li : i✝ ⟶ e
lj : j✝ ⟶ e
hli : D.W li
hlj : D.W lj
fac : x✝ ≫ lj = li
⊢ li = li
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ : Mat_ (SingleObj Rᵐᵒᵖ)
a₁✝ a₂✝ : X✝ ⟶ Y✝
w : (equivalenceSingleObjInverse R).map a₁✝ = (equivalenceSingleObjInverse R).map a₂✝
i✝ : X✝.ι
j✝ : Y✝.ι
⊢ MulOpposite.unop (a₁✝ i✝ j✝) = MulOpposite.unop (a₂✝ i✝ j✝)

Tactic:
exact congr_fun (congr_fun w _) _

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h : κ₁ ≤ κ₂
inst✝ : IsCardinalAccessibleCategory (CardinalDirectedPoset κ₁) κ₂
X : Type w
hX : HasCardinalLT X κ₂
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ₂
p : (isCardinalPresentable (CardinalDirectedPoset κ₁) κ₂).ColimitOfShape J (setCardinalLT κ₁ X)
this✝ : IsCardinalFiltered J κ₁
hp : ∀ (j : J), HasCardinalLT (↑(p.diag.obj j).obj) κ₂
j : X → J
y : (x : X) → ToType (p.diag.obj (j x))
hy : ∀ (x : X), (ConcreteCategory.hom (p.ι.app (j x))) (y x) = SetCardinalLT.singleton κ₁ x
j' : J := IsCardinalFiltered.max j hX
y' : X → ↑(p.diag.obj j').obj := fun x ↦ (ConcreteCategory.hom (p.diag.map (IsCardinalFiltered.toMax j hX x))) (y x)
hy' : ∀ (x : X), (ConcreteCategory.hom (p.ι.app j')) (y' x) = SetCardinalLT.singleton κ₁ x
x✝ : SetCardinalLT κ₁ X
B : Set X
hB : HasCardinalLT (↑B) κ₁
j'' : ↑(p.diag.obj j').obj := IsCardinalFiltered.max (fun b ↦ y' ↑b) hB
b : X
hb : b ∈ ↑⟨B, hB⟩
this : y' b ≤ j''
⊢ ↑((PartOrdEmb.Hom.hom (p.ι.app j').hom) (y' b)) = {b}

Tactic:
exact Subtype.ext_iff.1 (hy' b)

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
hf : (D₂ D hι u).W f
⊢ f = 𝟙 m

Tactic:
simp only [D₂_W] at hf

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
hf :
  (((⨆ i, (D i).W) ⊔ MorphismProperty.ofHoms fun x ↦ 𝟙 m) ⊔
      MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst)
    f
⊢ f = 𝟙 m