mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Creates

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
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
⊢ IsIso ((Cone.functoriality K F).map f)

Tactic:
this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
⊢ IsIso i.inv
Module: Mathlib.CategoryTheory.Limits.Creates

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
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
⊢ IsIso ((Cocone.functoriality K F).map f)

Tactic:
this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
⊢ IsIso i.hom
Module: Mathlib.Algebra.Category.AlgCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
J : Type u_1
inst✝² : Category.{v_1, u_1} J
F : J ⥤ AlgCat R
inst✝¹ : PreservesColimitsOfShape J (forget RingCat)
c : Cocone (F ⋙ forget₂ (AlgCat R) RingCat)
inst✝ : IsFilteredOrEmpty J
hc : IsColimit c
j : J
⊢ ∀ (c_1 : R) (x : ↑(((Functor.const J).obj c.pt).obj j)),
    ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) c_1 * x =
      x * ((RingCat.Hom.hom (c.ι.app j)).comp (algebraMap R ↑(F.obj j))) c_1

Tactic:
intro r x
    obtain ⟨k, hjk, y, rfl⟩ := Concrete.exists_hom_ι_eq_of_isColimit _ hc x j
    simp [← dsimp% c.w hjk, ← dsimp% (c.ι.app k).hom.map_mul, Algebra.commutes']

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
P : C ⥤ Type w
f : shrinkCoyoneda.{w, v, u}.obj X ⟶ P
g : Y ⟶ X
⊢ (ConcreteCategory.hom (P.map g.unop)) (shrinkCoyonedaEquiv f) =
    shrinkCoyonedaEquiv (shrinkCoyoneda.{w, v, u}.map g ≫ f)

Tactic:
by
  simpa [shrinkCoyonedaEquiv, shrinkYoneda]
    using (f.naturality_apply g.unop ((equivShrink _) (𝟙 _))).symm

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
J : Type v
inst✝ : Category.{t, v} J
F : J ⥤ ModuleCat R
r : R
s : (j : J) → ↑(F.obj j)
sh : s ∈ (F ⋙ forget (ModuleCat R)).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom ((F ⋙ forget (ModuleCat R)).map f)) ((r • s) j) = (r • s) j'

Tactic:
by
      simpa [Functor.sections] using congr_arg (r • ·) (sh f)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: case refine_1
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
x y : ↑s.1
⊢ (ConcreteCategory.hom
        ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
      (x + y) =
    (ConcreteCategory.hom
          ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
        x +
      (ConcreteCategory.hom
          ((Types.Small.limitConeIsLimit (F ⋙ forget (ModuleCat R))).lift ((forget (ModuleCat R)).mapCone s)))
        y

Tactic:
simp [← equivShrink_add]

Goal state after:
case refine_1
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
s : Cone F
x y : ↑s.1
⊢ ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x + (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩ =
    ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ + ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩
Module: Mathlib.Algebra.Category.AlgCat.Limits

Goal state before:
pp: case refine_3
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) 0, ⋯⟩ =
    0

pp: case refine_4
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩

pp: case refine_5
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
⊢ ∀ (r : R),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) ((algebraMap R ↑s.1) r), ⋯⟩ =
      (algebraMap R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt) r

Tactic:
· ext j
    simp
    rfl

Goal state after:
case refine_4
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
⊢ ∀ (x y : ↑s.1),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) (x + y), ⋯⟩ =
      EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) x, ⋯⟩ +
        EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
          ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) y, ⋯⟩

case refine_5
R : Type u
inst✝² : CommRing R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ AlgCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (AlgCat R)).sections
s : Cone F
⊢ ∀ (r : R),
    EquivLike.coe (equivShrink ↑(F ⋙ forget (AlgCat R)).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget (AlgCat R)).mapCone s).π.app j)) ((algebraMap R ↑s.1) r), ⋯⟩ =
      (algebraMap R (Types.Small.limitCone (F ⋙ forget (AlgCat R))).pt) r
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
this :
  L.whiskerLeft h.counit = (L.associator R L).inv ≫ whiskerRight (inv h.unit) L ≫ L.leftUnitor.hom ≫ L.rightUnitor.inv
⊢ IsIso (L.whiskerLeft h.counit)

Tactic:
this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
this :
  L.whiskerLeft h.counit = (L.associator R L).inv ≫ whiskerRight (inv h.unit) L ≫ L.leftUnitor.hom ≫ L.rightUnitor.inv
⊢ IsIso ((L.associator R L).inv ≫ whiskerRight (inv h.unit) L ≫ L.leftUnitor.hom ≫ L.rightUnitor.inv)
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
this :
  whiskerRight h.counit R = (R.associator L R).hom ≫ inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso (whiskerRight h.counit R)

Tactic:
this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Full
inst✝ : L.Faithful
this :
  whiskerRight h.counit R = (R.associator L R).hom ≫ inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv
⊢ IsIso ((R.associator L R).hom ≫ inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv)
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this :
  R.whiskerLeft h.unit = (R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ inv ((R.associator L R).inv ≫ whiskerRight h.counit R)
⊢ IsIso (R.whiskerLeft h.unit)

Tactic:
this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this :
  R.whiskerLeft h.unit = (R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ inv ((R.associator L R).inv ≫ whiskerRight h.counit R)
⊢ IsIso ((R.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ inv ((R.associator L R).inv ≫ whiskerRight h.counit R))
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this :
  whiskerRight h.unit L = (L.leftUnitor.hom ≫ L.rightUnitor.inv) ≫ inv ((L.associator R L).hom ≫ L.whiskerLeft h.counit)
⊢ IsIso (whiskerRight h.unit L)

Tactic:
this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Full
inst✝ : R.Faithful
this :
  whiskerRight h.unit L = (L.leftUnitor.hom ≫ L.rightUnitor.inv) ≫ inv ((L.associator R L).hom ≫ L.whiskerLeft h.counit)
⊢ IsIso ((L.leftUnitor.hom ≫ L.rightUnitor.inv) ≫ inv ((L.associator R L).hom ≫ L.whiskerLeft h.counit))
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ (f ⊗ₘ g) ⊗ₘ h = (α_ X Y Z).hom ≫ (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X' Y' Z').inv

Tactic:
rw [associator_inv_naturality, hom_inv_id_assoc]

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

Goal state before:
pp: C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ 𝟙 (X ⊗ Y) ≫ adj.unit.app (X ⊗ Y) = (adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y) ≫ G.map (μ F X Y)

Tactic:
← unit_app_tensor_comp_map_δ_assoc,

Goal state after:
C : Type u₁
inst✝¹³ : Category.{v₁, u₁} C
inst✝¹² : MonoidalCategory C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : MonoidalCategory D
E : Type u₃
inst✝⁹ : Category.{v₃, u₃} E
inst✝⁸ : MonoidalCategory E
E' : Type u₄
inst✝⁷ : Category.{v₄, u₄} E'
inst✝⁶ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁵ : F₁.LaxMonoidal
inst✝⁴ : F₂.LaxMonoidal
inst✝³ : F₃.LaxMonoidal
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.Monoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : C
⊢ 𝟙 (X ⊗ Y) ≫ adj.unit.app (X ⊗ Y) = adj.unit.app (X ⊗ Y) ≫ G.map (δ F X Y) ≫ G.map (μ F X Y)
Module: Mathlib.Algebra.Category.Ring.Limits

Goal state before:
pp: case refine_4
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
x y : ↑s.1
⊢ EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
      ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) (x + y), ⋯⟩ =
    EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) x, ⋯⟩ +
      EquivLike.coe (equivShrink ↑(F ⋙ forget SemiRingCat).sections)
        ⟨fun j ↦ (ConcreteCategory.hom (((forget SemiRingCat).mapCone s).π.app j)) y, ⋯⟩

Tactic:
simp [← equivShrink_add]

Goal state after:
case refine_4
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ SemiRingCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget SemiRingCat).sections
s : Cone F
x y : ↑s.1
⊢ ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x + (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩ =
    ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) x, ⋯⟩ + ⟨fun j ↦ (ConcreteCategory.hom (s.π.app j)) y, ⋯⟩
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, X ◁ b.π j ≫ X ◁ b.ι j = 𝟙 (X ⊗ b.pt)

Tactic:
[

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, X ◁ b.π j ≫ X ◁ b.ι j = 𝟙 (X ⊗ b.pt)
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, b.π j ▷ X ≫ b.ι j ▷ X = 𝟙 (b.pt ⊗ X)

Tactic:
[

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Finite J
val✝ : Fintype J
f : J → C
b : Bicone f
i : b.IsBilimit
⊢ ∑ j, b.π j ▷ X ≫ b.ι j ▷ X = 𝟙 (b.pt ⊗ X)
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X Y : C
f : J → C
val✝ : Fintype J
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x,
        (𝟙 X ⊗ₘ Y ◁ biproduct.π f x) ≫ (𝟙 X ⊗ₘ biproduct.ι (fun j ↦ Y ⊗ f j) x) ≫ X ◁ biproduct.π (fun j ↦ Y ⊗ f j) j✝
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (X ⊗ Y) ◁ biproduct.π f j✝ ≫ (α_ X Y (f j✝)).hom else 0

Tactic:
[

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X Y : C
f : J → C
val✝ : Fintype J
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x,
        (𝟙 X ⊗ₘ Y ◁ biproduct.π f x) ≫ (𝟙 X ⊗ₘ biproduct.ι (fun j ↦ Y ⊗ f j) x) ≫ X ◁ biproduct.π (fun j ↦ Y ⊗ f j) j✝
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (X ⊗ Y) ◁ biproduct.π f j✝ ≫ (α_ X Y (f j✝)).hom else 0
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y : C
val✝ : Fintype J
j✝ : J
⊢ ∑ x, (biproduct.π f x ▷ X ⊗ₘ 𝟙 Y) ≫ (biproduct.ι (fun j ↦ f j ⊗ X) x ⊗ₘ 𝟙 Y) ≫ biproduct.π (fun j ↦ f j ⊗ X) j✝ ▷ Y =
    (α_ (⨁ f) X Y).hom ≫ biproduct.π f j✝ ▷ (X ⊗ Y) ≫ (α_ (f j✝) X Y).inv

Tactic:
[

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y : C
val✝ : Fintype J
j✝ : J
⊢ ∑ x, (biproduct.π f x ▷ X ⊗ₘ 𝟙 Y) ≫ (biproduct.ι (fun j ↦ f j ⊗ X) x ⊗ₘ 𝟙 Y) ≫ biproduct.π (fun j ↦ f j ⊗ X) j✝ ▷ Y =
    (α_ (⨁ f) X Y).hom ≫ biproduct.π f j✝ ▷ (X ⊗ Y) ≫ (α_ (f j✝) X Y).inv
Module: Mathlib.CategoryTheory.Monoidal.Preadditive

Goal state before:
pp: case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
Y : C
val✝ : Fintype J
j✝ : J
⊢ ∑ x, (X ◁ biproduct.π f x ⊗ₘ 𝟙 Y) ≫ (biproduct.ι (fun j ↦ X ⊗ f j) x ⊗ₘ 𝟙 Y) ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝ ▷ Y =
    ∑ x,
      (α_ X (⨁ f) Y).hom ≫
        (𝟙 X ⊗ₘ biproduct.π f x ▷ Y ≫ biproduct.ι (fun j ↦ f j ⊗ Y) x) ≫
          X ◁ biproduct.π (fun j ↦ f j ⊗ Y) j✝ ≫ (α_ X (f j✝) Y).inv

Tactic:
[

Goal state after:
case intro
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
X : C
f : J → C
Y : C
val✝ : Fintype J
j✝ : J
⊢ ∑ x, (X ◁ biproduct.π f x ⊗ₘ 𝟙 Y) ≫ (biproduct.ι (fun j ↦ X ⊗ f j) x ⊗ₘ 𝟙 Y) ≫ biproduct.π (fun j ↦ X ⊗ f j) j✝ ▷ Y =
    ∑ x,
      (α_ X (⨁ f) Y).hom ≫
        (𝟙 X ⊗ₘ biproduct.π f x ▷ Y ≫ biproduct.ι (fun j ↦ f j ⊗ Y) x) ≫
          X ◁ biproduct.π (fun j ↦ f j ⊗ Y) j✝ ≫ (α_ X (f j✝) Y).inv
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X✝ Y✝ : C
f : X✝ ⟶ Y✝
X' : C
⊢ F.map f ▷ F.obj X' ≫ μ Y✝ X' = μ X✝ X' ≫ F.map (f ▷ X')

Tactic:
[

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X✝ Y✝ : C
f : X✝ ⟶ Y✝
X' : C
⊢ F.map f ▷ F.obj X' ≫ μ Y✝ X' = μ X✝ X' ≫ F.map (f ▷ X')
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X✝ Y✝ X' : C
f : X✝ ⟶ Y✝
⊢ F.obj X' ◁ F.map f ≫ μ X' Y✝ = μ X' X✝ ≫ F.map (X' ◁ f)

Tactic:
[

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X✝ Y✝ X' : C
f : X✝ ⟶ Y✝
⊢ F.obj X' ◁ F.map f ≫ μ X' Y✝ = μ X' X✝ ≫ F.map (X' ◁ f)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X Y Z : C
⊢ μ X Y ▷ F.obj Z ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ Y Z ≫ μ X (Y ⊗ Z)

Tactic:
[

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
ε : 𝟙_ D ⟶ F.obj (𝟙_ C)
μ : (X Y : C) → F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)
μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (F.map f ⊗ₘ F.map g) ≫ μ Y Y' = μ X X' ≫ F.map (f ⊗ₘ g)
associativity :
  ∀ (X Y Z : C),
    (μ X Y ⊗ₘ 𝟙 (F.obj Z)) ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
      (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ (𝟙 (F.obj X) ⊗ₘ μ Y Z) ≫ μ X (Y ⊗ Z)
left_unitality : ∀ (X : C), (λ_ (F.obj X)).hom = (ε ⊗ₘ 𝟙 (F.obj X)) ≫ μ (𝟙_ C) X ≫ F.map (λ_ X).hom
right_unitality : ∀ (X : C), (ρ_ (F.obj X)).hom = (𝟙 (F.obj X) ⊗ₘ ε) ≫ μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
X Y Z : C
⊢ μ X Y ▷ F.obj Z ≫ μ (X ⊗ Y) Z ≫ F.map (α_ X Y Z).hom =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ μ Y Z ≫ μ X (Y ⊗ Z)