mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
M : Cᴹᵒᵖ
inst✝ : MonObj M
⊢ (mopEquiv C).functor.map (M.unmop ◁ MonObj.one.unmop ≫ MonObj.mul.unmop) = (mopEquiv C).functor.map (ρ_ M.unmop).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Opposite.Mon

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
M : Cᴹᵒᵖ
inst✝ : MonObj M
⊢ (mopEquiv C).functor.map (MonObj.mul.unmop ▷ M.unmop ≫ MonObj.mul.unmop) =
    (mopEquiv C).functor.map ((α_ M.unmop M.unmop M.unmop).hom ≫ M.unmop ◁ MonObj.mul.unmop ≫ MonObj.mul.unmop)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N P Q : Bimod Y Z
f : N ⟶ P
g : P ⟶ Q
⊢ coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (M.whiskerLeft (f ≫ g)).hom =
    coequalizer.π (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ≫ (M.whiskerLeft f ≫ M.whiskerLeft g).hom

Tactic:
simp

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
U : C ⥤ V
inst✝ : DayConvolutionUnit U
c : C
v : V
g h : U.obj c ⟶ v
e : ∀ (f : 𝟙_ C ⟶ c), can ≫ U.map f ≫ g = can ≫ U.map f ≫ h
⊢ ∀ (j : CostructuredArrow (fromPUnit (𝟙_ C)) c),
    ((LeftExtension.mk U { app := fun x ↦ can, naturality := ⋯ }).coconeAt c).ι.app j ≫ g =
      ((LeftExtension.mk U { app := fun x ↦ can, naturality := ⋯ }).coconeAt c).ι.app j ≫ h

Tactic:
intro j

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
U : C ⥤ V
inst✝ : DayConvolutionUnit U
c : C
v : V
g h : U.obj c ⟶ v
e : ∀ (f : 𝟙_ C ⟶ c), can ≫ U.map f ≫ g = can ≫ U.map f ≫ h
j : CostructuredArrow (fromPUnit (𝟙_ C)) c
⊢ ((LeftExtension.mk U { app := fun x ↦ can, naturality := ⋯ }).coconeAt c).ι.app j ≫ g =
    ((LeftExtension.mk U { app := fun x ↦ can, naturality := ⋯ }).coconeAt c).ι.app j ≫ h
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
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
x : C
⊢ (λ_ (F.obj x)).inv ≫
      ((prod.leftInverseUnitor C).whiskerLeft
              (((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ U ⊛ F))
                (((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) (U ⊛ F)) (𝟙 (U ⊛ F))))).app
          x ≫
        (U ⊛ F).map (λ_ x).hom =
    (λ_ (F.obj x)).inv ≫ can ▷ F.obj x ≫ (DayConvolution.unit U F).app (𝟙_ C, x) ≫ (U ⊛ F).map (λ_ x).hom

Tactic:
simp

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
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝ : DayConvolution F U
x : C
⊢ (ρ_ (F.obj x)).inv ≫
      ((prod.rightInverseUnitor C).whiskerLeft
              (((F ⊠ U).homEquivOfIsLeftKanExtension (extensionUnitRight U (φ U) F) (tensor C ⋙ F ⊛ U))
                (((F ⊛ U).homEquivOfIsLeftKanExtension (DayConvolution.unit F U) (F ⊛ U)) (𝟙 (F ⊛ U))))).app
          x ≫
        (F ⊛ U).map (ρ_ x).hom =
    (ρ_ (F.obj x)).inv ≫ F.obj x ◁ can ≫ (DayConvolution.unit F U).app (x, 𝟙_ C) ≫ (F ⊛ U).map (ρ_ x).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        (α_ (𝟙_ C) X.X N.X).inv ≫ (λ_ X.X).hom ▷ N.X ≫ coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J✝ : Type u_1
I✝ : J✝ → Type u_2
inst✝⁶ : Category.{v_1, u_1} J✝
inst✝⁵ : (j : J✝) → Category.{?u.14, u_2} (I✝ j)
D✝ : J✝ ⥤ C
P✝ : (j : J✝) → ColimitPresentation (I✝ j) (D✝.obj j)
J : Type w
I : J → Type w
inst✝⁴ : SmallCategory J
inst✝³ : (j : J) → SmallCategory (I j)
D : J ⥤ C
P : (j : J) → ColimitPresentation (I j) (D.obj j)
inst✝² : IsFiltered J
inst✝¹ : ∀ (j : J), IsFiltered (I j)
inst✝ : ∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)
k l : Total P
f g : k ⟶ l
a : J := IsFiltered.coeq f.base g.base
a' : I (IsFiltered.coeq f.base g.base)
u : Total.mk P l.fst l.snd ⟶ Total.mk P (IsFiltered.coeq f.base g.base) a'
hu : u.base = IsFiltered.coeqHom f.base g.base
⊢ (P k.fst).ι.app k.snd ≫ D.map (g.base ≫ IsFiltered.coeqHom f.base g.base) =
    (P k.fst).ι.app k.snd ≫ D.map g.base ≫ D.map (IsFiltered.coeqHom f.base g.base)

Tactic:
simp

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✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct 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) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
x y : D
fst✝ snd✝ : C
⊢ (unit ((ι C V D).obj x) ((ι C V D).obj y)).app (fst✝, snd✝) =
    (unit ((ι C V D).obj x) ((ι C V D).obj y)).app (fst✝, snd✝) ≫ 𝟙 (((ι C V D).obj (x ⊗ y)).obj (fst✝ ⊗ snd✝))

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
⊢ P f → P.ind f

Tactic:
hf

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P f
⊢ P.ind 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✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct 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) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
fst✝ snd✝ : C
⊢ ((corepresentableBy ((ι C V D).obj X₁✝) ((ι C V D).obj X₂✝)).homEquiv
          (map ((ι C V D).map x✝³) ((ι C V D).map x✝²) ≫ map ((ι C V D).map x✝¹) ((ι C V D).map x✝))).app
      (fst✝, snd✝) =
    ((corepresentableBy ((ι C V D).obj X₁✝) ((ι C V D).obj X₂✝)).homEquiv
          (map ((ι C V D).map x✝³ ≫ (ι C V D).map x✝¹) ((ι C V D).map x✝² ≫ (ι C V D).map x✝))).app
      (fst✝, snd✝)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X Y : C
f : X ⟶ Y
⊢ sourceLocalClosure K P f → Q f

Tactic:
hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
h : P ≤ Q
inst✝ : Q.IsLocalAtSource K
X Y : C
f : X ⟶ Y
hf : sourceLocalClosure K P f
⊢ Q f
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: case refine_2.refine_5
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.underObj.ind (CategoryTheory.Under.mk f)
J : Type w
w✝¹ : SmallCategory J
w✝ : IsFiltered J
pres : ColimitPresentation J (CategoryTheory.Under.mk f)
hpres : ∀ (i : J), P.underObj (pres.diag.obj i)
j : J
⊢ { app := fun j ↦ (pres.diag.obj j).hom, naturality := ⋯ }.app j ≫
      (Functor.whiskerRight pres.ι (CategoryTheory.Under.forget X)).app j =
    f

Tactic:
simp

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✝
⊢ (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj d')).app X✝ ≫
      (tensor C ⋙ DayConvolution.convolution ((ι C V D).obj d) ((ι C V D).obj d')).map f✝ ≫
        (tensorObjIsoConvolution C V d d').inv.app (Y✝.1 ⊗ Y✝.2) =
    (DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj d')).app (X✝.1, X✝.2) ≫
      (tensorObjIsoConvolution C V d d').inv.app (X✝.1 ⊗ X✝.2) ≫ (tensor C ⋙ (ι C V D).obj (tensorObj C V d d')).map f✝

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ⊤.localEpi f✝ ↔ MorphismProperty.epimorphisms C f✝

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
⊢ P.localEpi f → P.isoClosure.localEpi f

Tactic:
hf

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
hf : P.localEpi f
⊢ P.isoClosure.localEpi f
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: 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)
X Y Z : Mon C
M N P : Bimod X Y
f : M ⟶ N
g : N ⟶ P
Q : Bimod Y Z
⊢ coequalizer.π (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ≫ (whiskerRight (f ≫ g) Q).hom =
    coequalizer.π (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ≫
      (whiskerRight f Q ≫ whiskerRight g Q).hom

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : G.Faithful
inst✝ : G.Full
X Y : C
f : X ⟶ Y
⊢ Epi (F.map f) ↔ (MorphismProperty.epimorphisms D).inverseImage F f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : ι → C
κ : Cardinal.{w}
h : HasCardinalLT ι κ
i : ι
⊢ ofObj X (X i)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ f.hom ▷ Y.X ≫ colimit.ι (parallelPair (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ μ)) WalkingParallelPair.one =
    f.hom ▷ Y.X ≫
      (ρ_ (N.X ⊗ Y.X)).inv ≫
        (α_ N.X Y.X (𝟙_ C)).hom ≫ N.X ◁ (ρ_ Y.X).hom ≫ coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ μ)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
K L : Precoverage C
⊢ ∀ {X : C} {R : Presieve X}, R ∈ K.coverings X → ∀ {Y : C} (f : Y ⟶ X), R f → ⊤ X → ⊤ Y

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
K L : Precoverage C
⊢ ∀ {X : C} {R : Presieve X}, R ∈ K.coverings X → (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → ⊤ Y) → ⊤ X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v✝ : Arrow V
f✝ g✝ : u✝ ⟶ v✝
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
w : Arrow V
g : v ⟶ w
h : RightHomotopy (f ≫ g) 0
⊢ biprod.inl ≫ biprod.desc (Hom.left g) h.hom ≫ w.hom = biprod.inl ≫ (cokernel f).hom ≫ Hom.right g

Tactic:
simp

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)
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : D
i✝ : I
⊢ (λ_ ((Functor.pi' F).obj X)).inv i✝ =
    ((Functor.pi' F).map (λ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) (𝟙_ D) X) ≫
          (fun i ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi' F).obj X)
      i✝

Tactic:
simp

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)
D : Type u_1
inst✝² : Category.{v_1, u_1} D
inst✝¹ : MonoidalCategory D
F : (i : I) → D ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : D
i✝ : I
⊢ (ρ_ ((Functor.pi' F).obj X)).inv i✝ =
    ((Functor.pi' F).map (ρ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) X (𝟙_ D)) ≫
          (Functor.pi' F).obj X ◁ fun i ↦ Functor.OplaxMonoidal.η (F i))
      i✝

Tactic:
simp

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)
D : I → Type u₂
inst✝² : (i : I) → Category.{v₂, u₂} (D i)
inst✝¹ : (i : I) → MonoidalCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
i✝ : I
⊢ (λ_ ((Functor.pi F).obj X)).inv i✝ =
    ((Functor.pi F).map (λ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) ((𝟙_ ((i : I) → D i)) i) (X i)) ≫
          (fun i ↦ Functor.OplaxMonoidal.η (F i)) ▷ (Functor.pi F).obj X)
      i✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
α β : u ⟶ v
⊢ L.map (α.left + β.left) ≫ v.hom = u.hom ≫ R.map (α.right + β.right)

Tactic:
simp

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)
D : I → Type u₂
inst✝² : (i : I) → Category.{v₂, u₂} (D i)
inst✝¹ : (i : I) → MonoidalCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
i✝ : I
⊢ (ρ_ ((Functor.pi F).obj X)).inv i✝ =
    ((Functor.pi F).map (ρ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) (X i) ((𝟙_ ((i : I) → D i)) i)) ≫
          (Functor.pi F).obj X ◁ fun i ↦ Functor.OplaxMonoidal.η (F i))
      i✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
α β : u ⟶ v
⊢ L.map (α.left - β.left) ≫ v.hom = u.hom ≫ R.map (α.right - β.right)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
k : α
j : ↑(g ⁻¹' {f k})
⊢ s (f k) = s (f ↑⟨k, ⋯⟩)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : ↑(f ⁻¹' {g j})
⊢ s (g ↑⟨j, ⋯⟩) = s (g j)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : α
k : β
h : f j = g k
⊢ j ∈ f ⁻¹' {f j}

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : α
h : f k = g j
⊢ (eqToHom ⋯ ≫ biproduct.components z k j ≫ eqToHom ⋯) ≫ eqToHom ⋯ =
    biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j

Tactic:
simp

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
j : β
k : α
h : f k = g j
⊢ biproduct.components z k j = biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : f k = g j
⊢ (z (f k) ⟨j, ⋯⟩ ⟨k, ⋯⟩ ≫ eqToHom ⋯) ≫ eqToHom ⋯ = z (f k) ⟨j, w⟩ ⟨k, ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : Preadditive C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
w z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
x✝ : ι
i✝ : ↑(g ⁻¹' {x✝})
j✝ : ↑(f ⁻¹' {x✝})
⊢ eqToHom ⋯ ≫ (biproduct.ι (fun a ↦ s (f a)) ↑j✝ ≫ (w + z) ≫ biproduct.π (fun b ↦ s (g b)) ↑i✝) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (biproduct.ι (fun a ↦ s (f a)) ↑j✝ ≫ w ≫ biproduct.π (fun b ↦ s (g b)) ↑i✝) ≫ eqToHom ⋯ +
      eqToHom ⋯ ≫ (biproduct.ι (fun a ↦ s (f a)) ↑j✝ ≫ z ≫ biproduct.π (fun b ↦ s (g b)) ↑i✝) ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case pos.refl
C : Type u
inst✝³ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
o : HomOrthogonal s
α : Type
inst✝ : Finite α
f : α → ι
b : α
j_property✝ : b ∈ f ⁻¹' {f b}
j_property : f b = f b
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) b ≫ biproduct.π (fun b ↦ s (f b)) b = 𝟙 (s (f b))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case w
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ ∀ (x : β) (hx : x ∈ g ⁻¹' {h c}),
    eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun b ↦ s (g b)) x ≫ biproduct.ι (fun b ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun b ↦ s (h b)) c =
      eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun b ↦ s (g b)) ↑⟨x, hx⟩ ≫
              biproduct.ι (fun a ↦ s (g a)) ↑⟨x, hx⟩ ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (fun x x_1 x_2 ↦ g (f x_2)) i✝ j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ (M + N).map (fun i j ↦ ⇑f) i✝ j✝ = ((M.map fun i j ↦ ⇑f) + N.map fun i j ↦ ⇑f) i✝ j✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ (M - N).map (fun i j ↦ ⇑f) i✝ j✝ = ((M.map fun i j ↦ ⇑f) - N.map fun i j ↦ ⇑f) i✝ j✝

Tactic:
simp

Goal state after: