mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasCoseparator C
⊢ HasSeparator Cᵒᵖ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasCoseparator Cᵒᵖ
⊢ HasSeparator C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasDetector C
⊢ HasCodetector Cᵒᵖ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasDetector Cᵒᵖ
⊢ HasCodetector C

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasCodetector C
⊢ HasDetector Cᵒᵖ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasCodetector Cᵒᵖ
⊢ HasDetector C

Tactic:
by

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
f g : A ⟶ B
h :
  ∀ (h : AddCommGrpCat.of (ULift.{u, 0} ℤ) ⟶ A) (x : ℤ),
    (AddCommGrpCat.Hom.hom f) ((AddCommGrpCat.Hom.hom h) { down := x }) =
      (AddCommGrpCat.Hom.hom g) ((AddCommGrpCat.Hom.hom h) { down := x })
x : ↑A
y z : ULift.{u, 0} ℤ
⊢ (y + z) • x = y • x + z • x

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
⊢ f = g

Tactic:
by

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ ∃ G, IsSeparator G

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
isc : IsColimit
  ((Over.forget c.pt).mapCocone
    (colimit.cocone
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))) :=
  isColimitOfPreserves (Over.forget c.pt)
    (colimit.isColimit
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
i : I
⊢ c.ι.app i ≫
      (hc.coconePointUniqueUpToIso isc).hom ≫
        (colimit
            ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙
              CostructuredArrow.toOver yoneda c.pt)).hom =
    c.ι.app i ≫ (Over.mk (𝟙 c.pt)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ (c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt).Final

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
u₁ u₂ : F.Elementsᵒᵖ
g : u₁ ⟶ u₂
⊢ (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).map g ≫
      ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (unop u₂).snd) =
    (↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) (unop u₁).snd) ≫
      ((const F.Elementsᵒᵖ).obj (F.obj X)).map g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
u : G.ColimitType
x : F.obj X
h : G.descColimitType c u = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u

Tactic:
by

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

Goal state before:
pp: G : GrpCat
inst✝ : Subsingleton ↑G
⊢ IsZero G

Tactic:
by

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

Goal state before:
pp: G : CommGrpCat
inst✝ : Subsingleton ↑G
⊢ IsZero G

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType
hu :
  ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₁ =
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₂
x : c.pt
hx₁ : G.descColimitType c u₁ = x
⊢ G.descColimitType c u₂ = x

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
i j : C
f : { as := i } ⟶ { as := j }
⊢ i = j

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : AddCommGrpCat
⊢ (free.obj X ⟶ Y) ≃ (X ⟶ (forget AddCommGrpCat).obj Y)

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
⊢ ∀ {j j' : Discrete C} (f : j ⟶ j'),
    (fun x ↦
          match j', x with
          | { as := i }, x => ⟨i, x⟩) ∘
        ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
      fun x ↦
      match j, x with
      | { as := i }, x => ⟨i, x⟩

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {X' X : Type u} {Y : AddCommGrpCat} (f : X' ⟶ X) (g : X ⟶ (forget AddCommGrpCat).obj Y),
    (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f ≫ g) =
      free.map f ≫ (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g

Tactic:
by

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

Goal state before:
pp: case right
C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
⊢ Function.Surjective ((Discrete.functor F).descColimitType c)

Tactic:
intro x
      obtain ⟨i, y, rfl⟩ := h₁ x
      exact ⟨(Discrete.functor F).ιColimitType ⟨i⟩ y, rfl⟩

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
h₁ : ∀ (x : c.pt), ∃ i y, c.inj i y = x
h₂ : ∀ (i : C), Function.Injective (c.inj i)
h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j
⊢ Function.Bijective ((Discrete.functor F).descColimitType c)

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
⊢ ∀ (x : (sigma F).pt), ∃ i y, (sigma F).inj i y = x

Tactic:
by

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

Goal state before:
pp: G H : GrpCat
⊢ ∀ {T : GrpCat} (f : T ⟶ G) (g : T ⟶ H)
    (m : T ⟶ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).pt),
    m ≫ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).fst = f →
      m ≫ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).snd = g →
        m = ofHom ((Hom.hom f).prod (Hom.hom g))

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
x✝² : C
x✝¹ x✝ : F x✝²
h : (sigma F).inj x✝² x✝¹ = (sigma F).inj x✝² x✝
⊢ x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : Nonempty X
⊢ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
⊢ Functor.CoconeTypes.IsColimit c ↔ Function.Bijective (fromSigma F c)

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
⊢ Function.Bijective (fromSigma F c)

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
x : F i
⊢ (equivOfIsColimit hc) ((equivOfIsColimit hc).symm (c.inj i x)) = (equivOfIsColimit hc) ⟨i, x⟩

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
x : c.pt
⊢ ∃ i y, c.inj i y = x

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
⊢ Function.Injective (c.inj i)

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
⊢ Function.Injective (c.inj i)

Tactic:
by
  intro y₁ y₂ h
  simpa using (equivOfIsColimit hc).injective (a₁ := ⟨i, y₁⟩) (a₂ := ⟨i, y₂⟩) h

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
x✝ : Mono f
⊢ Mono (free.map f)

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : i₁ = i₂
⊢ F i₁ = F i₂

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
x :
  (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
      (coconeπOpCompShrinkYonedaObj F X)).pt
⊢ ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ιColimitType (op (F.elementsMk X x))
        (shrinkYonedaObjObjEquiv.symm (𝟙 X))) =
    x

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
x✝ : ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
h₁ : i₁ = i₂
h₂ : y₂ = cast ⋯ y₁
⊢ c.inj i₁ y₁ = c.inj i₂ y₂

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
⊢ c.inj i₁ y₁ = c.inj i₂ y₂ ↔ ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
i j : C
f : { as := i } ⟶ { as := j }
⊢ i = j

Tactic:
by

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

Goal state before:
pp: G H : GrpCat
p : ↑G
q : ↑H
⊢ (hom (Functor.LaxMonoidal.μ (forget GrpCat) G H)) (p, q) = (p, q)

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
⊢ ∀ {j j' : Discrete C} (f : j ⟶ j'),
    (match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) j' with
        | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))) ∘
        ⇑(ConcreteCategory.hom ((Discrete.functor F).map f)) =
      match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) j with
      | { as := j } => ⇑(ConcreteCategory.hom (c.inj j))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
⊢ IsColimit (coconeπOpCompShrinkYonedaObj F X)

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
c : Cofan F
⊢ Nonempty (IsColimit c) ↔ Function.Bijective (CofanTypes.fromSigma F c.cofanTypes)

Tactic:
by

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

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
hc : IsColimit c
i j : C
x : F i
y : F j
hij : i = j
⊢ F i = F j

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
x✝ : Cocone (Functor.empty (Type u))
⊢ ∀ (j : Discrete PEmpty.{?u.24 + 1}),
    ({ pt := PEmpty.{u + 1},
                ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.ι.app
          j ≫
        ↾fun x ↦ PEmpty.elim x) =
      x✝.ι.app j

Tactic:
by

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

Goal state before:
pp: G H : AddGrpCat
⊢ ∀ {T : AddGrpCat} (f : T ⟶ G) (g : T ⟶ H)
    (m : T ⟶ (BinaryFan.mk (ofHom (AddMonoidHom.fst ↑G ↑H)) (ofHom (AddMonoidHom.snd ↑G ↑H))).pt),
    m ≫ (BinaryFan.mk (ofHom (AddMonoidHom.fst ↑G ↑H)) (ofHom (AddMonoidHom.snd ↑G ↑H))).fst = f →
      m ≫ (BinaryFan.mk (ofHom (AddMonoidHom.fst ↑G ↑H)) (ofHom (AddMonoidHom.snd ↑G ↑H))).snd = g →
        m = ofHom ((Hom.hom f).prod (Hom.hom g))

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
x✝² : Cocone (Functor.empty (Type u))
x✝¹ :
  { pt := PEmpty.{u + 1},
        ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.pt ⟶
    x✝².pt
x✝ :
  ∀ (j : Discrete PEmpty.{?u.24 + 1}),
    { pt := PEmpty.{u + 1},
                ι := ((Functor.const (Discrete PEmpty.{?u.24 + 1})).obj PEmpty.{u + 1}).uniqueFromEmpty.inv }.ι.app
          j ≫
        x✝¹ =
      x✝².ι.app j
⊢ x✝¹ = ↾fun x ↦ PEmpty.elim x

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {X' X : Type u} {Y : GrpCat} (f : X' ⟶ X) (g : X ⟶ (forget GrpCat).obj Y),
    (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f ≫ g) =
      free.map f ≫ (ConcreteCategory.homEquiv.trans (FreeGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g

Tactic:
by

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

Goal state before:
pp: X : Type u
⊢ Nonempty (IsInitial X) ↔ IsEmpty X

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X₁ X₂ : C
f : X₁ ⟶ X₂
u : F.Elements
⊢ ((shrinkYoneda.{w, v₁, u₁}.map f).app (op u.fst) ≫
      ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd) =
    (↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd) ≫ F.map f

Tactic:
by

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

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
x✝¹ : Cocone (pair X Y)
x✝ : (binaryCoproductCocone X Y).pt ⟶ x✝¹.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x✝ = x✝¹.ι.app j
⊢ x✝ = ↾Sum.elim ⇑(ConcreteCategory.hom (BinaryCofan.inl x✝¹)) ⇑(ConcreteCategory.hom (BinaryCofan.inr x✝¹))

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (X : GrpCat),
    CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (𝟙 X)))) =
      𝟙 (CommGrpCat.of (Abelianization ↑X))

Tactic:
by

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

Goal state before:
pp: G H : AddGrpCat
p : ↑G
q : ↑H
⊢ (hom (Functor.LaxMonoidal.μ (forget AddGrpCat) G H)) (p, q) = (p, q)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u : F.Elementsᵒᵖ
X Y : C
f : X ⟶ Y
⊢ (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).obj u).map f ≫
      (coconeπOpCompShrinkYonedaObj F Y).ι.app u =
    (coconeπOpCompShrinkYonedaObj F X).ι.app u ≫ (((const F.Elementsᵒᵖ).obj F).obj u).map f

Tactic:
by

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

Goal state before:
pp: G H : CommGrpCat
⊢ ∀ {T : CommGrpCat} (f : T ⟶ G) (g : T ⟶ H)
    (m : T ⟶ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).pt),
    m ≫ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).fst = f →
      m ≫ (BinaryFan.mk (ofHom (MonoidHom.fst ↑G ↑H)) (ofHom (MonoidHom.snd ↑G ↑H))).snd = g →
        m = ofHom ((Hom.hom f).prod (Hom.hom g))

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {X Y Z : GrpCat} (f : X ⟶ Y) (g : Y ⟶ Z),
    CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom (f ≫ g)))) =
      CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom f))) ≫
        CommGrpCat.ofHom (Abelianization.lift (Abelianization.of.comp (Hom.hom g)))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u v : F.Elementsᵒᵖ
g : u ⟶ v
⊢ ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).map g ≫
      { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app v, naturality := ⋯ } =
    { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app u, naturality := ⋯ } ≫ ((const F.Elementsᵒᵖ).obj F).map g

Tactic:
by

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

Goal state before:
pp: G H : CommGrpCat
p : ↑G
q : ↑H
⊢ (hom (Functor.LaxMonoidal.μ (forget CommGrpCat) G H)) (p, q) = (p, q)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
inst✝ : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ ∀ (j : F.Elementsᵒᵖ),
    colimit.ι
          (((whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryOfElements.π F).op).obj
            (shrinkYoneda.{w, v₁, u₁}.obj X₁))
          j ≫
        (shrinkYoneda.{w, v₁, u₁} ⋙
                (whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryOfElements.π F).op ⋙ colim).map
            f ≫
          ((colimit.isColimit ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X₂)).coconePointUniqueUpToIso
              (isColimitCoconeπOpCompShrinkYonedaObj F X₂)).hom =
      colimit.ι
          (((whiskeringLeft F.Elementsᵒᵖ Cᵒᵖ (Type w)).obj (CategoryOfElements.π F).op).obj
            (shrinkYoneda.{w, v₁, u₁}.obj X₁))
          j ≫
        ((colimit.isColimit ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X₁)).coconePointUniqueUpToIso
              (isColimitCoconeπOpCompShrinkYonedaObj F X₁)).hom ≫
          F.map f

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {X' X : GrpCat} {Y : CommGrpCat} (f : X' ⟶ X) (g : X ⟶ (forget₂ CommGrpCat GrpCat).obj Y),
    ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm (f ≫ g) =
      abelianize.map f ≫
        ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
inst✝ : HasColimitsOfShape F.Elementsᵒᵖ (Type w)
u : F.Elements
⊢ (ConcreteCategory.hom ((shrinkYonedaCompWhiskeringLeftObjπCompColimIso F).inv.app u.fst)) u.snd =
    (ConcreteCategory.hom (colimit.ι ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj u.fst) (op u)))
      (shrinkYonedaObjObjEquiv.symm (𝟙 (unop ((CategoryOfElements.π F).op.obj (op u)))))

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {X : CommGrpCat} {Y : CommMonCat} {f : (forget₂ CommGrpCat CommMonCat).obj X ⟶ Y},
    { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
          invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y).comp (Hom.hom f)), left_inv := ⋯, right_inv := ⋯ }
        f =
      { app := fun X ↦ ofHom toUnits.toMonoidHom, naturality := ⋯ }.app X ≫ CommMonCat.units.map f

Tactic:
by

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

Goal state before:
pp: G H : AddCommGrpCat
p : ↑G
q : ↑H
⊢ (hom (Functor.LaxMonoidal.μ (forget AddCommGrpCat) G H)) (p, q) = (p, q)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
u : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).Elements
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).map (shrinkYonedaObjObjEquiv u.snd)))
      ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).snd =
    u.snd

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {X : CommGrpCat} {Y : CommMonCat} {g : X ⟶ CommMonCat.units.obj Y},
    { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
            invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y).comp (Hom.hom f)), left_inv := ⋯,
            right_inv := ⋯ }.symm
        g =
      (forget₂ CommGrpCat CommMonCat).map g ≫
        { app := fun X ↦ CommMonCat.ofHom (Units.coeHom ↑X), naturality := ⋯ }.app Y

Tactic:
by

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

Goal state before:
pp: X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
⊢ ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ Set.range ⇑(ConcreteCategory.hom c.inr)

Tactic:
by

Goal state after: