mathlib-initiative/mathlib-tactics huggingface dataset:
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
D : Type u₃
inst✝⁴ : Category.{v₃, u₃} D
inst✝³ : MonoidalCategoryStruct D
inst✝² : LawfulDayConvolutionMonoidalCategoryStruct C V D
d d' d'' : 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)
⊢ (ι C V D).map (α_ d d' d'').hom =
    (DayConvolution.associator ((ι C V D).obj d) ((ι C V D).obj d') ((ι C V D).obj d'')).hom

Tactic:
apply corepresentableBy₂'
    (ι C V D |>.obj d) (ι C V D |>.obj d') (ι C V D |>.obj d'') |>.homEquiv.injective

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
D : Type u₃
inst✝⁴ : Category.{v₃, u₃} D
inst✝³ : MonoidalCategoryStruct D
inst✝² : LawfulDayConvolutionMonoidalCategoryStruct C V D
d d' d'' : 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)
⊢ (corepresentableBy₂' ((ι C V D).obj d) ((ι C V D).obj d') ((ι C V D).obj d'')).homEquiv
      ((ι C V D).map (α_ d d' d'').hom) =
    (corepresentableBy₂' ((ι C V D).obj d) ((ι C V D).obj d') ((ι C V D).obj d'')).homEquiv
      (DayConvolution.associator ((ι C V D).obj d) ((ι C V D).obj d') ((ι C V D).obj d'')).hom
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
X✝ Y✝ : C
f' : X✝ ⟶ Y✝
hf' : sourceLocalClosure K P f'
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g' : U✝ ⟶ X✝
hg' : R g'
ih : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h : IsPullback fst snd (g' ≫ f') g
⊢ snd ≫ g = (fst ≫ g') ≫ f'

Tactic:
by simp [h.w.symm]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Z : Under X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
W : C
u : Z.right ⟶ W
v : W ⟶ Y
huv : u ≫ v = Under.Hom.right g
hW : P (Z.hom ≫ u)
⊢ CategoryTheory.Under.homMk u ⋯ ≫ CategoryTheory.Under.homMk v ⋯ = g

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Z : Under X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
W : C
u : Z.right ⟶ W
v : W ⟶ Y
huv : u ≫ v = Under.Hom.right g
hW : P (Z.hom ≫ u)
⊢ Under.Hom.right (CategoryTheory.Under.homMk u ⋯ ≫ CategoryTheory.Under.homMk v ⋯) = Under.Hom.right g
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ⊤.localEpi = MorphismProperty.epimorphisms C

Tactic:
ext

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ⊤.localEpi f✝ ↔ MorphismProperty.epimorphisms C 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
⊢ whiskerRight (f ≫ g) Q = whiskerRight f Q ≫ whiskerRight g Q

Tactic:
ext

Goal state after:
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
⊢ (whiskerRight (f ≫ g) Q).hom = (whiskerRight f Q ≫ whiskerRight g Q).hom
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsArtinianObject X
h : ¬IsZero X
this : Nontrivial (Subobject X)
Y : Subobject X
s : IsAtom Y ∧ Y ≤ ⊤
⊢ ∃ Y, Simple (underlying.obj Y)

Tactic:
exact ⟨Y, (subobject_simple_iff_isAtom _).mpr s.1⟩

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
⊢ whiskerRight f
      { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
        middle_assoc := ⋯ } =
    (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯).hom ≫
      f ≫
        (isoOfIso { hom := RightUnitorBimod.hom N, inv := RightUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).inv

Tactic:
ext

Goal state after:
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
⊢ (whiskerRight f
        { X := Y.X, actLeft := μ, one_actLeft := ⋯, left_assoc := ⋯, actRight := μ, actRight_one := ⋯, right_assoc := ⋯,
          middle_assoc := ⋯ }).hom =
    ((isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).hom ≫
        f ≫
          (isoOfIso { hom := RightUnitorBimod.hom N, inv := RightUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).inv).hom
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)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
⊢ whiskerRight f
      { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯,
        actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ } =
    (isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯).inv ≫
      whiskerRight (whiskerRight f N) P ≫
        (isoOfIso
            { hom := AssociatorBimod.hom M' N P, inv := AssociatorBimod.inv M' N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).hom

Tactic:
ext

Goal state after:
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)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
⊢ (whiskerRight f
        { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯,
          actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }).hom =
    ((isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ }
            ⋯ ⋯).inv ≫
        whiskerRight (whiskerRight f N) P ≫
          (isoOfIso
              { hom := AssociatorBimod.hom M' N P, inv := AssociatorBimod.inv M' N P, hom_inv_id := ⋯, inv_hom_id := ⋯ }
              ⋯ ⋯).hom).hom
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 : u ⟶ v
inst✝ : IsIso (Hom.right f)
Z✝ : RightFreyd V
g₁ g₂ : v ⟶ Z✝.as
eq : (quotient V).map f ≫ (quotient V).map g₁ = (quotient V).map f ≫ (quotient V).map g₂
h : RightHomotopy (f ≫ g₁) (f ≫ g₂) := homotopyOfEq (f ≫ g₁) (f ≫ g₂) eq
⊢ Hom.right g₁ - Hom.right g₂ = (inv (Hom.right f) ≫ h.hom) ≫ Z✝.as.hom

Tactic:
simp [dsimp% h.comm]

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
⊢ (λ_ ((Functor.pi' F).obj X)).inv =
    (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

Tactic:
ext

Goal state after:
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✝
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
⊢ (ρ_ ((Functor.pi' F).obj X)).inv =
    (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)

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

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

Tactic:
ext

Goal state after:
case h₁
V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
w : Arrow V
g : v ⟶ w
h : RightHomotopy (f ≫ g) 0
⊢ Hom.left (π f ≫ desc f g h) = Hom.left g

case h₂
V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
inst✝ : HasBinaryBiproducts V
u v : Arrow V
f : u ⟶ v
w : Arrow V
g : v ⟶ w
h : RightHomotopy (f ≫ g) 0
⊢ Hom.right (π f ≫ desc f g h) = Hom.right g
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
i : I
⊢ (Functor.LaxMonoidal.μ (Functor.pi' F) X✝ Y✝ ≫ (Functor.pi' F).map (β_ X✝ Y✝).hom) i =
    ((β_ ((Functor.pi' F).obj X✝) ((Functor.pi' F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi' F) Y✝ X✝) i

Tactic:
exact Functor.LaxBraided.braided _ _

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
⊢ (λ_ ((Functor.pi F).obj X)).inv =
    (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

Tactic:
ext

Goal state after:
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✝
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
⊢ (ρ_ ((Functor.pi F).obj X)).inv =
    (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)

Tactic:
ext

Goal state after:
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✝
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
x✝² x✝¹ x✝ : u ⟶ v
⊢ x✝² + x✝¹ + x✝ = x✝² + (x✝¹ + x✝)

Tactic:
ext

Goal state after:
case h₁
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
x✝² x✝¹ x✝ : u ⟶ v
⊢ (x✝² + x✝¹ + x✝).left = (x✝² + (x✝¹ + x✝)).left

case h₂
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
x✝² x✝¹ x✝ : u ⟶ v
⊢ (x✝² + x✝¹ + x✝).right = (x✝² + (x✝¹ + x✝)).right
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
i : I
⊢ (Functor.LaxMonoidal.μ (Functor.pi F) X✝ Y✝ ≫ (Functor.pi F).map (β_ X✝ Y✝).hom) i =
    ((β_ ((Functor.pi F).obj X✝) ((Functor.pi F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi F) Y✝ X✝) i

Tactic:
exact Functor.LaxBraided.braided _ _

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)
⊢ o.matrixDecomposition.toFun (w + z) = o.matrixDecomposition.toFun w + o.matrixDecomposition.toFun z

Tactic:
ext

Goal state after:
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✝})
⊢ o.matrixDecomposition.toFun (w + z) x✝ i✝ j✝ =
    (o.matrixDecomposition.toFun w + o.matrixDecomposition.toFun z) x✝ i✝ j✝
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
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := (x✝¹ + 1) • x✝.left, right := (x✝¹ + 1) • x✝.right, w := ⋯ } =
    { left := x✝¹ • x✝.left, right := x✝¹ • x✝.right, w := ⋯ } + x✝

Tactic:
ext

Goal state after:
case h₁
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
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := (x✝¹ + 1) • x✝.left, right := (x✝¹ + 1) • x✝.right, w := ⋯ }.left =
    ({ left := x✝¹ • x✝.left, right := x✝¹ • x✝.right, w := ⋯ } + x✝).left

case h₂
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
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := (x✝¹ + 1) • x✝.left, right := (x✝¹ + 1) • x✝.right, w := ⋯ }.right =
    ({ left := x✝¹ • x✝.left, right := x✝¹ • x✝.right, w := ⋯ } + x✝).right
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)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ whiskerRight (M.whiskerLeft f) P =
    (isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯).hom ≫
      M.whiskerLeft (whiskerRight f P) ≫
        (isoOfIso
            { hom := AssociatorBimod.hom M N' P, inv := AssociatorBimod.inv M N' P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).inv

Tactic:
ext

Goal state after:
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)
W X Y Z : Mon C
M : Bimod W X
N N' : Bimod X Y
f : N ⟶ N'
P : Bimod Y Z
⊢ (whiskerRight (M.whiskerLeft f) P).hom =
    ((isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ }
            ⋯ ⋯).hom ≫
        M.whiskerLeft (whiskerRight f P) ≫
          (isoOfIso
              { hom := AssociatorBimod.hom M N' P, inv := AssociatorBimod.inv M N' P, hom_inv_id := ⋯, inv_hom_id := ⋯ }
              ⋯ ⋯).inv).hom
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
x✝¹ x✝ : u ⟶ v
⊢ x✝¹ - x✝ = x✝¹ + -x✝

Tactic:
ext

Goal state after:
case h₁
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
x✝¹ x✝ : u ⟶ v
⊢ (x✝¹ - x✝).left = (x✝¹ + -x✝).left

case h₂
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
x✝¹ x✝ : u ⟶ v
⊢ (x✝¹ - x✝).right = (x✝¹ + -x✝).right
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
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := ↑x✝¹.succ • x✝.left, right := ↑x✝¹.succ • x✝.right, w := ⋯ } =
    { left := ↑x✝¹ • x✝.left, right := ↑x✝¹ • x✝.right, w := ⋯ } + x✝

Tactic:
ext

Goal state after:
case h₁
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
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := ↑x✝¹.succ • x✝.left, right := ↑x✝¹.succ • x✝.right, w := ⋯ }.left =
    ({ left := ↑x✝¹ • x✝.left, right := ↑x✝¹ • x✝.right, w := ⋯ } + x✝).left

case h₂
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
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := ↑x✝¹.succ • x✝.left, right := ↑x✝¹.succ • x✝.right, w := ⋯ }.right =
    ({ left := ↑x✝¹ • x✝.left, right := ↑x✝¹ • x✝.right, w := ⋯ } + x✝).right