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

Goal state before:
pp: α β : Type u
f : α ⟶ β
⊢ ∀ {X Y : Type u} (f : X ⟶ Y), HasImage f

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: case step
F : ℕᵒᵖ ⥤ Type u
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
a : F.obj (Opposite.op 0)
n m p : ℕ
h : m.le p
ih :
  (ConcreteCategory.hom (F.map (Opposite.op { down := { down := h } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)
⊢ (ConcreteCategory.hom (F.map (Opposite.op { down := { down := ⋯ } })))
      ((fun x ↦
          match x with
          | Opposite.op n => preimage hF a n)
        (Opposite.op p.succ)) =
    (fun x ↦
        match x with
        | Opposite.op n => preimage hF a n)
      (Opposite.op m)

Tactic:
| @step p h ih =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Images

Goal state before:
pp: case hf
F : ℕᵒᵖ ⥤ Type u
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op))
i : c.pt ≅ (limitCone F).pt := hc.conePointUniqueUpToIso (limitConeIsLimit F)
this : c.π.app (Opposite.op 0) = i.hom ≫ (limitCone F).π.app (Opposite.op 0)
⊢ Epi i.hom

Tactic:
infer_instance

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case neg.inl
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi hjs : i ∈ s
hji : ¬i < i
⊢ s.piecewise a v i - b i = a i - b i

Tactic:
s.piecewise_eq_of_mem _ _ hi

Goal state after:
case neg.inl
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi hjs : i ∈ s
hji : ¬i < i
⊢ a i - b i = a i - b i
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: case inr
J : Type v
inst✝² : SmallCategory J
F : J ⥤ CommRingCat
inst✝¹ : IsFilteredOrEmpty J
inst✝ : ∀ (i : J), Nontrivial ↑(F.obj i)
c : Cocone F
hc : IsColimit c
h✝ : Nonempty J
i : J
h : (ConcreteCategory.hom (c.ι.app i)) 0 = (ConcreteCategory.hom (c.ι.app i)) 1
⊢ False

Tactic:
have : IsFiltered J := ⟨⟩

Goal state after:
case inr
J : Type v
inst✝² : SmallCategory J
F : J ⥤ CommRingCat
inst✝¹ : IsFilteredOrEmpty J
inst✝ : ∀ (i : J), Nontrivial ↑(F.obj i)
c : Cocone F
hc : IsColimit c
h✝ : Nonempty J
i : J
h : (ConcreteCategory.hom (c.ι.app i)) 0 = (ConcreteCategory.hom (c.ι.app i)) 1
this : IsFiltered J
⊢ False
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 i.inv

Tactic:
infer_instance

Goal state after:
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
⊢ IsColimit d

Tactic:
let i : F.mapCocone d' ≅ F.mapCocone d :=
          (h (F.mapCocone d) hd).toLiftableCocone.validLift

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
⊢ IsColimit d
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 i.hom

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Cᵒᵖ
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (coyoneda.obj K)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : C
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (yoneda.obj K)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Cᵒᵖ
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)} (coyoneda.obj K ⋙ uliftFunctor.{w', v})

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Yoneda

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : C
⊢ PreservesLimitsOfSize.{t, w, v, max w' v, u, max (w' + 1) (v + 1)} (yoneda.obj K ⋙ uliftFunctor.{w', v})

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : (forget C).IsCorepresentable
J : Type w
inst✝¹ : Category.{t, w} J
G : J ⥤ C
inst✝ : HasLimit G
⊢ HasLimit (G ⋙ forget C)

Tactic:
infer_instance

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 : C
x✝ : Cᵒᵖ
⊢ Small.{w, v} (unop x✝ ⟶ X)

Tactic:
infer_instance

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 : Cᵒᵖ
x✝ : C
⊢ Small.{w, v} (unop X ⟶ x✝)

Tactic:
infer_instance

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

Goal state before:
pp: case refine_2.refine_1
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
⊢ (s : Cone F) →
    s.pt ⟶
      {
            liftedCone :=
              { pt := of (Types.Small.limitCone (F ⋙ forget MonCat)).pt,
                π := { app := fun j ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ } },
            validLift :=
              Cone.ext ((Types.isLimitEquivSections t).trans (equivShrink ↑(F ⋙ forget MonCat).sections)).symm.toIso
                ⋯ }.liftedCone.pt

Tactic:
intro _
    refine ofHom
      { toFun := (Types.Small.limitConeIsLimit.{v, u} _).lift ((forget MonCat).mapCone _),
        map_one' := by simp; rfl, map_mul' := ?_ }
    · intro x y
      simp only [Types.Small.limitCone_pt, Functor.comp_obj, Functor.mapCone_pt,
        Types.Small.limitConeIsLimit_lift, Functor.const_obj_obj, Functor.mapCone_π_app,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, map_mul]
      rw [← equivShrink_mul]
      rfl

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ CommMonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget CommMonCat).sections
c' : Cone (F ⋙ forget₂ CommMonCat MonCat)
t : IsLimit c'
⊢ (forget₂ CommMonCat MonCat).mapCone
      { pt := of (Types.Small.limitCone (F ⋙ forget CommMonCat)).pt,
        π := { app := fun j ↦ ofHom (limitπMonoidHom (F ⋙ forget₂ CommMonCat MonCat) j), naturality := ⋯ } } ≅
    c'

Tactic:
apply IsLimit.uniqueUpToIso (MonCat.HasLimits.limitConeIsLimit _) t

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

Goal state before:
pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
⊢ Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections → HasLimit F

Tactic:
intro

Goal state after:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
a✝ : Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections
⊢ HasLimit F
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ GrpCat
a✝ : Small.{u, max u v} ↑(F ⋙ forget GrpCat).sections
⊢ HasLimit F

Tactic:
infer_instance

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

Goal state before:
pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
⊢ Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections → HasLimit F

Tactic:
intro

Goal state after:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
a✝ : Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections
⊢ HasLimit F
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
a✝ : Small.{u, max u v} ↑(F ⋙ forget CommGrpCat).sections
⊢ HasLimit F

Tactic:
infer_instance

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ CommGrpCat
f : ℕ → AddCommGrpCat
⊢ HasProduct f

Tactic:
infer_instance

Goal state after:
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.associator R L).inv ≫ whiskerRight (inv h.unit) L ≫ L.leftUnitor.hom ≫ L.rightUnitor.inv)

Tactic:
infer_instance

Goal state after:
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 ((R.associator L R).hom ≫ inv (R.whiskerLeft h.unit) ≫ R.rightUnitor.hom ≫ R.leftUnitor.inv)

Tactic:
infer_instance

Goal state after:
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.rightUnitor.hom ≫ R.leftUnitor.inv) ≫ inv ((R.associator L R).inv ≫ whiskerRight h.counit R))

Tactic:
infer_instance

Goal state after:
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 ((L.leftUnitor.hom ≫ L.rightUnitor.inv) ≫ inv ((L.associator R L).hom ≫ L.whiskerLeft h.counit))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: case mp
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.Faithful
inst✝ : L.Full
X : D
⊢ IsIso (h.counit.app X) → L.essImage X

Tactic:
intro

Goal state after:
case mp
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.Faithful
inst✝ : L.Full
X : D
a✝ : IsIso (h.counit.app X)
⊢ L.essImage X
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: case mpr
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.Faithful
inst✝ : L.Full
X : D
w✝ : C
i : L.obj w✝ ≅ X
⊢ IsIso (h.counit.app (L.obj w✝))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: case mp
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.Faithful
inst✝ : R.Full
Y : C
⊢ IsIso (h.unit.app Y) → R.essImage Y

Tactic:
intro

Goal state after:
case mp
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.Faithful
inst✝ : R.Full
Y : C
a✝ : IsIso (h.unit.app Y)
⊢ R.essImage Y
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: case mpr
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.Faithful
inst✝ : R.Full
Y : C
w✝ : D
i : R.obj w✝ ≅ Y
⊢ IsIso (h.unit.app (R.obj w✝))

Tactic:
infer_instance

Goal state after:
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.IsEquivalence
this : R.IsEquivalence
⊢ IsIso h.unit

Tactic:
infer_instance

Goal state after:
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.IsEquivalence
this : L.IsEquivalence
⊢ IsIso h.counit

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
⊢ 𝟙 X ⊗ₘ f = X ◁ f

Tactic:
simp [tensorHom_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ f ⊗ₘ 𝟙 Y = f ▷ Y

Tactic:
simp [tensorHom_def]

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

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

Tactic:
simp [tensorHom_def]

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

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

Tactic:
simp [tensorHom_def]

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

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

Tactic:
simp [tensorHom_def]

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

Goal state before:
pp: case refl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ X ◁ eqToHom ⋯ = eqToHom ⋯

Tactic:
simp only [whiskerLeft_id, eqToHom_refl]

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
G₁ : D ⥤ E
inst✝¹ : G₁.LaxMonoidal
inst✝ : IsMonoidal τ
⊢ IsMonoidal (τ ◫ 𝟙 G₁)

Tactic:
infer_instance

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

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

Tactic:
simp [tensorHom_def]

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
G₁ G₂ : D ⥤ E
inst✝² : G₁.LaxMonoidal
inst✝¹ : G₂.LaxMonoidal
τ' : G₁ ⟶ G₂
inst✝ : IsMonoidal τ'
⊢ IsMonoidal (𝟙 F₁ ◫ τ')

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ (g ⊗ₘ 𝟙 W) ≫ (𝟙 Z ⊗ₘ f) = g ⊗ₘ f

Tactic:
simp [tensorHom_def]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : MonoidalCategory C
W X Y Z : C
C₁ : Type u₁
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : MonoidalCategory C₁
C₂ : Type u₂
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : MonoidalCategory C₂
⊢ ∀ {X₁ Y₁ X₂ Y₂ : C₁ × C₂} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    (f.1 ⊗ₘ g.1) ×ₘ f.2 ⊗ₘ g.2 = (f.1 ▷ X₂.1 ×ₘ f.2 ▷ X₂.2) ≫ (Y₁.1 ◁ g.1 ×ₘ Y₁.2 ◁ g.2)

Tactic:
simp [tensorHom_def]

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
⊢ ε (G ⋙ F) ≫ adj.counit.app (𝟙_ D) = ε (𝟭 D)

Tactic:
dsimp
    rw [assoc, map_ε_comp_counit_app_unit adj, ε_η]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
⊢ F.CoreMonoidal

Tactic:
letI := induced F fData
  exact
    { εIso := fData.εIso
      μIso := fData.μIso
      μIso_hom_natural_left := fun _ ↦ by simp [fData.whiskerRight_eq]
      μIso_hom_natural_right := fun _ ↦ by simp [fData.whiskerLeft_eq]
      associativity := fun _ _ _ ↦ by simp [fData.associator_eq]
      left_unitality := fun _ ↦ by simp [fData.leftUnitor_eq]
      right_unitality := fun _ ↦ by simp [fData.rightUnitor_eq] }

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ (equivalenceTransported e).inverse.Monoidal

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ (equivalenceTransported e).symm.IsMonoidal

Tactic:
infer_instance

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
X✝ Y✝ Z✝ : LaxMonoidalFunctor C D
α : X✝.Hom Y✝
β : Y✝.Hom Z✝
this✝ : NatTrans.IsMonoidal α.hom
this : NatTrans.IsMonoidal β.hom
⊢ NatTrans.IsMonoidal (α.hom ≫ β.hom)

Tactic:
infer_instance

Goal state after:
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
W X Y Z : C
f : W ⟶ X
⊢ f ⊗ₘ 0 = 0

Tactic:
simp [tensorHom_def]

Goal state after:
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
W X Y Z : C
f : Y ⟶ Z
⊢ 0 ⊗ₘ f = 0

Tactic:
simp [tensorHom_def]

Goal state after:
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
W X Y Z : C
f : W ⟶ X
g h : Y ⟶ Z
⊢ f ⊗ₘ (g + h) = f ⊗ₘ g + f ⊗ₘ h

Tactic:
simp [tensorHom_def]

Goal state after:
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
W X Y Z : C
f g : W ⟶ X
h : Y ⟶ Z
⊢ (f + g) ⊗ₘ h = f ⊗ₘ h + g ⊗ₘ h

Tactic:
simp [tensorHom_def]

Goal state after:
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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (F.map f ⊗ₘ F.map g) ≫ μ F Y Y' = μ F X X' ≫ F.map (f ⊗ₘ g)

Tactic:
simp [tensorHom_def]

Goal state after:
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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
Y : D
f : Y ⟶ F.obj X
⊢ (f ⊗ₘ ε F) ≫ μ F X (𝟙_ C) = f ▷ 𝟙_ D ≫ (ρ_ (F.obj X)).hom ≫ F.map (ρ_ X).inv

Tactic:
simp [tensorHom_def]

Goal state after:
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
F : C ⥤ D
inst✝ : F.LaxMonoidal
X : C
Y : D
f : Y ⟶ F.obj X
⊢ f ▷ 𝟙_ D ≫ (ρ_ (F.obj X)).hom = (f ⊗ₘ ε F) ≫ μ F X (𝟙_ C) ≫ F.map (ρ_ X).hom

Tactic:
simp [tensorHom_def]

Goal state after:
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ δ F X X' ≫ (F.map f ⊗ₘ F.map g) = F.map (f ⊗ₘ g) ≫ δ F Y Y'

Tactic:
simp [tensorHom_def]

Goal state after:
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
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X : C
Y : D
f : F.obj X ⟶ Y
⊢ δ F (𝟙_ C) X ≫ (η F ⊗ₘ f) = F.map (λ_ X).hom ≫ (λ_ (F.obj X)).inv ≫ 𝟙_ D ◁ f

Tactic:
simp [tensorHom_def]

Goal state after: