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

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝² : Category.{v₂, u₂} K✝
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F✝ : J ⥤ C
t✝ : Cone F✝
D : Type u₄
inst✝ : Category.{v₄, u₄} D
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (G.mapCone c)

Tactic:
apply postcomposeInvEquiv (isoWhiskerLeft K h :) (mapCone G c) _

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝² : Category.{v₂, u₂} K✝
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
F✝ : J ⥤ C
t✝ : Cone F✝
D : Type u₄
inst✝ : Category.{v₄, u₄} D
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj (G.mapCone c))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : F.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ e.homEquiv f = (ConcreteCategory.hom (F.map f)) (e.homEquiv (𝟙 X))

Tactic:
conv_lhs => rw [← Category.id_comp f, e.homEquiv_comp]

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
⊢ ((↾fun c ↦ ⟨op c.pt, c.π⟩) ≫ ↾fun c ↦ { pt := unop c.fst, π := c.snd }) = 𝟙 (Cone F)

Tactic:
ext X

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : Cone F
⊢ (ConcreteCategory.hom ((↾fun c ↦ ⟨op c.pt, c.π⟩) ≫ ↾fun c ↦ { pt := unop c.fst, π := c.snd })).toFun X =
    (ConcreteCategory.hom (𝟙 (Cone F))).toFun X
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
⊢ ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩) = 𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F))

Tactic:
ext X

Goal state after:
case fst
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : (X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩)).toFun X).fst =
    ((ConcreteCategory.hom (𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)))).toFun X).fst

case snd
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : (X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩)).toFun X).snd ≍
    ((ConcreteCategory.hom (𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)))).toFun X).snd
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
⊢ ((↾fun c ↦ ⟨c.pt, c.ι⟩) ≫ ↾fun c ↦ { pt := c.fst, ι := c.snd }) = 𝟙 (Cocone F)

Tactic:
ext X

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : Cocone F
⊢ (ConcreteCategory.hom ((↾fun c ↦ ⟨c.pt, c.ι⟩) ≫ ↾fun c ↦ { pt := c.fst, ι := c.snd })).toFun X =
    (ConcreteCategory.hom (𝟙 (Cocone F))).toFun X
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
⊢ ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩) = 𝟙 ((X : C) × F.cocones.obj X)

Tactic:
ext X

Goal state after:
case fst
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : (X : C) × F.cocones.obj X
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩)).toFun X).fst =
    ((ConcreteCategory.hom (𝟙 ((X : C) × F.cocones.obj X))).toFun X).fst

case snd
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F✝ F : J ⥤ C
X : (X : C) × F.cocones.obj X
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩)).toFun X).snd ≍
    ((ConcreteCategory.hom (𝟙 ((X : C) × F.cocones.obj X))).toFun X).snd
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cone F
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
cases f
  cases g
  congr

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
⊢ Unique (x ⟶ y)

Tactic:
suffices sub : Subsingleton (x ⟶ y) from uniqueOfSubsingleton f

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
⊢ Subsingleton (x ⟶ y)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
e : K ≌ J
inst✝ : HasColimit (e.functor ⋙ F)
this : HasColimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasColimit F

Tactic:
apply hasColimit_of_iso (e.invFunIdAssoc F).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ : Over A
k : X✝ ⟶ Y✝
g : Over A
⊢ coprod.map (Hom.left k) (𝟙 g.left) ≫ coprod.desc Y✝.hom g.hom = coprod.desc X✝.hom g.hom

Tactic:
rw [coprod.map_desc, Category.id_comp, Over.w k]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : F✝ ⋙ U ⟶ S ⋙ G✝
β✝ : G✝.obj T ⟶ V
F : C ≌ A
G : D ≌ B
α : F.functor ⋙ U ⟶ S ⋙ G.functor
α' : F.inverse ⋙ S ⟶ U ⋙ G.inverse
hα'α :
  S.leftUnitor.hom ≫ S.rightUnitor.inv ≫ S.whiskerLeft G.unitIso.hom ≫ (S.associator G.functor G.inverse).inv =
    Functor.whiskerRight F.unitIso.hom S ≫
      (F.functor.associator F.inverse S).hom ≫
        F.functor.whiskerLeft α' ≫ (F.functor.associator U G.inverse).inv ≫ Functor.whiskerRight α G.inverse
hαα' :
  F.inverse.whiskerLeft α ≫
      (F.inverse.associator S G.functor).inv ≫
        Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom ≫ U.whiskerLeft G.counitIso.hom =
    (F.inverse.associator F.functor U).inv ≫
      Functor.whiskerRight F.counitIso.hom U ≫ U.leftUnitor.hom ≫ U.rightUnitor.inv
β : G.functor.obj T ⟶ V
β' : G.inverse.obj V ⟶ T
hββ' : G.inverse.map β ≫ β' = G.unitIso.inv.app T
hβ'β : G.functor.map β' ≫ β = G.counitIso.hom.app V
⊢ (S.leftUnitor.hom ≫ S.rightUnitor.inv) ≫ S.whiskerLeft G.unitIso.hom =
    Functor.whiskerRight F.unitIso.hom S ≫
      (F.functor.associator F.inverse S).hom ≫
        F.functor.whiskerLeft α' ≫
          (F.functor.associator U G.inverse).inv ≫
            Functor.whiskerRight α G.inverse ≫ (S.associator G.functor G.inverse).hom

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : F✝ ⋙ U ⟶ S ⋙ G✝
β✝ : G✝.obj T ⟶ V
F : C ≌ A
G : D ≌ B
α : F.functor ⋙ U ⟶ S ⋙ G.functor
α' : F.inverse ⋙ S ⟶ U ⋙ G.inverse
hα'α :
  S.leftUnitor.hom ≫ S.rightUnitor.inv ≫ S.whiskerLeft G.unitIso.hom ≫ (S.associator G.functor G.inverse).inv =
    Functor.whiskerRight F.unitIso.hom S ≫
      (F.functor.associator F.inverse S).hom ≫
        F.functor.whiskerLeft α' ≫ (F.functor.associator U G.inverse).inv ≫ Functor.whiskerRight α G.inverse
hαα' :
  F.inverse.whiskerLeft α ≫
      (F.inverse.associator S G.functor).inv ≫
        Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom ≫ U.whiskerLeft G.counitIso.hom =
    (F.inverse.associator F.functor U).inv ≫
      Functor.whiskerRight F.counitIso.hom U ≫ U.leftUnitor.hom ≫ U.rightUnitor.inv
β : G.functor.obj T ⟶ V
β' : G.inverse.obj V ⟶ T
hββ' : G.inverse.map β ≫ β' = G.unitIso.inv.app T
hβ'β : G.functor.map β' ≫ β = G.counitIso.hom.app V
X : C
⊢ ((S.leftUnitor.hom ≫ S.rightUnitor.inv) ≫ S.whiskerLeft G.unitIso.hom).app X =
    (Functor.whiskerRight F.unitIso.hom S ≫
          (F.functor.associator F.inverse S).hom ≫
            F.functor.whiskerLeft α' ≫
              (F.functor.associator U G.inverse).inv ≫
                Functor.whiskerRight α G.inverse ≫ (S.associator G.functor G.inverse).hom).app
      X
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : F✝ ⋙ U ⟶ S ⋙ G✝
β✝ : G✝.obj T ⟶ V
F : C ≌ A
G : D ≌ B
α : F.functor ⋙ U ⟶ S ⋙ G.functor
α' : F.inverse ⋙ S ⟶ U ⋙ G.inverse
hα'α :
  S.leftUnitor.hom ≫ S.rightUnitor.inv ≫ S.whiskerLeft G.unitIso.hom ≫ (S.associator G.functor G.inverse).inv =
    Functor.whiskerRight F.unitIso.hom S ≫
      (F.functor.associator F.inverse S).hom ≫
        F.functor.whiskerLeft α' ≫ (F.functor.associator U G.inverse).inv ≫ Functor.whiskerRight α G.inverse
hαα' :
  F.inverse.whiskerLeft α ≫
      (F.inverse.associator S G.functor).inv ≫
        Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom ≫ U.whiskerLeft G.counitIso.hom =
    (F.inverse.associator F.functor U).inv ≫
      Functor.whiskerRight F.counitIso.hom U ≫ U.leftUnitor.hom ≫ U.rightUnitor.inv
β : G.functor.obj T ⟶ V
β' : G.inverse.obj V ⟶ T
hββ' : G.inverse.map β ≫ β' = G.unitIso.inv.app T
hβ'β : G.functor.map β' ≫ β = G.counitIso.hom.app V
⊢ ((F.inverse.associator F.functor U).hom ≫
        F.inverse.whiskerLeft α ≫
          (F.inverse.associator S G.functor).inv ≫
            Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom) ≫
      U.whiskerLeft G.counitIso.hom =
    Functor.whiskerRight F.counitIso.hom U ≫ U.leftUnitor.hom ≫ U.rightUnitor.inv

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
U : A ⥤ B
V : B
F✝ : C ⥤ A
G✝ : D ⥤ B
α✝ : F✝ ⋙ U ⟶ S ⋙ G✝
β✝ : G✝.obj T ⟶ V
F : C ≌ A
G : D ≌ B
α : F.functor ⋙ U ⟶ S ⋙ G.functor
α' : F.inverse ⋙ S ⟶ U ⋙ G.inverse
hα'α :
  S.leftUnitor.hom ≫ S.rightUnitor.inv ≫ S.whiskerLeft G.unitIso.hom ≫ (S.associator G.functor G.inverse).inv =
    Functor.whiskerRight F.unitIso.hom S ≫
      (F.functor.associator F.inverse S).hom ≫
        F.functor.whiskerLeft α' ≫ (F.functor.associator U G.inverse).inv ≫ Functor.whiskerRight α G.inverse
hαα' :
  F.inverse.whiskerLeft α ≫
      (F.inverse.associator S G.functor).inv ≫
        Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom ≫ U.whiskerLeft G.counitIso.hom =
    (F.inverse.associator F.functor U).inv ≫
      Functor.whiskerRight F.counitIso.hom U ≫ U.leftUnitor.hom ≫ U.rightUnitor.inv
β : G.functor.obj T ⟶ V
β' : G.inverse.obj V ⟶ T
hββ' : G.inverse.map β ≫ β' = G.unitIso.inv.app T
hβ'β : G.functor.map β' ≫ β = G.counitIso.hom.app V
X : A
⊢ (((F.inverse.associator F.functor U).hom ≫
            F.inverse.whiskerLeft α ≫
              (F.inverse.associator S G.functor).inv ≫
                Functor.whiskerRight α' G.functor ≫ (U.associator G.inverse G.functor).hom) ≫
          U.whiskerLeft G.counitIso.hom).app
      X =
    (Functor.whiskerRight F.counitIso.hom U ≫ U.leftUnitor.hom ≫ U.rightUnitor.inv).app X
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: ⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    (𝟭 WalkingParallelPair).map f ≫ (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map f

Tactic:
rintro _ _ (_ | _ | _) <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map f

Tactic:
rintro _ _ (_ | _ | _) <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    ((Functor.const WalkingParallelPair).obj t.pt).map f ≫ t.π.app Y ≫ eqToHom ⋯ =
      (t.π.app X ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map f

Tactic:
rintro _ _ (_ | _ | _) <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
H : C ⥤ D
⊢ η ≫ 0 = 0

Tactic:
ext X

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
H : C ⥤ D
X : C
⊢ (η ≫ 0).app X = NatTrans.app 0 X
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    (parallelPair (F.map left) (F.map right)).map f ≫ eqToHom ⋯ ≫ t.ι.app Y =
      (eqToHom ⋯ ≫ t.ι.app X) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map f

Tactic:
rintro _ _ (_ | _ | _) <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
⊢ 0 ≫ η = 0

Tactic:
ext X

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
X : C
⊢ (0 ≫ η).app X = NatTrans.app 0 X
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
β : Type w
inst✝¹ : DecidableEq β
f : β → C
inst✝ : HasProduct f
b c : β
h : b ≠ c
⊢ ι f b ≫ π f c = 0

Tactic:
simp [Pi.ι, Function.update_of_ne h.symm]

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

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
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso ((Cone.functoriality F G).map ((limit.isLimit F).liftConeMorphism c))

Tactic:
exact t.hom_isIso (isLimitOfPreserves G (limit.isLimit F)) _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
⊢ (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure

Tactic:
ext X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
⊢ (P ⊔ Q).isoClosure X ↔ (P.isoClosure ⊔ Q.isoClosure) X
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ⊤.map P.ι = P.isoClosure

Tactic:
ext X

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ ⊤.map P.ι X ↔ P.isoClosure X
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this✝ : m₁.toMulOneClass = m₂.toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : NPow.npow = NPow.npow
⊢ m₁ = m₂

Tactic:
rcases m₁ with @⟨@⟨⟨_⟩⟩, ⟨_⟩, _, _, ⟨_⟩⟩

Goal state after:
M : Type u
m₂ : Monoid M
mul✝ : M → M → M
mul_assoc✝ : ∀ (a b c : M), a * b * c = a * (b * c)
one✝ : M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
npow✝ : ℕ → M → M
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
h_mul : HMul.hMul = HMul.hMul
this✝ :
  { mul := mul✝, mul_assoc := mul_assoc✝, one := one✝, one_mul := one_mul✝, mul_one := mul_one✝, npow := npow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝ }.toMulOneClass =
    m₂.toMulOneClass
h₁ : One.one = One.one
f : M →* M := { toFun := id, map_one' := h₁, map_mul' := ⋯ }
this : NPow.npow = NPow.npow
⊢ { mul := mul✝, mul_assoc := mul_assoc✝, one := one✝, one_mul := one_mul✝, mul_one := mul_one✝, npow := npow✝,
      npow_zero := npow_zero✝, npow_succ := npow_succ✝ } =
    m₂
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon : m₁.toMonoid = m₂.toMonoid
⊢ m₁ = m₂

Tactic:
have h₁ : m₁.one = m₂.one := congr_arg (·.one) h_mon

Goal state after:
M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
h_mon : m₁.toMonoid = m₂.toMonoid
h₁ : One.one = One.one
⊢ m₁ = m₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f g h : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasKernel g
inst✝ : HasKernel h
w₁ : f = g
w₂ : g = h
⊢ kernelIsoOfEq w₁ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq ⋯

Tactic:
by
  cases w₁; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f g h : X ⟶ Y
inst✝² : HasCokernel f
inst✝¹ : HasCokernel g
inst✝ : HasCokernel h
w₁ : f = g
w₂ : g = h
⊢ cokernelIsoOfEq w₁ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq ⋯

Tactic:
by
  cases w₁; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
c c' : Bicone F
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
cases f
  cases g
  congr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasImage f
inst✝ : HasKernel (factorThruImage f)
⊢ (kernelFactorThruImage f).hom ≫ kernel.ι f = kernel.ι (factorThruImage f)

Tactic:
by
  simp [kernelFactorThruImage]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝² : HasKernel f
inst✝¹ : HasImage f
inst✝ : HasKernel (factorThruImage f)
⊢ (kernelFactorThruImage f).inv ≫ kernel.ι (factorThruImage f) = kernel.ι f

Tactic:
by
  simp [kernelFactorThruImage]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι f ≫ f) = 0

Tactic:
kernel.condition,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι f) ≫ G.map f = 0

Tactic:
by rw [← G.map_comp, kernel.condition, G.map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι g ≫ g) = 0

Tactic:
kernel.condition,

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁴ : G.PreservesZeroMorphisms
X' Y' : C
inst✝³ : HasKernel f
inst✝² : HasKernel (G.map f)
g : X' ⟶ Y'
inst✝¹ : HasKernel g
inst✝ : HasKernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map (kernel.ι g) ≫ G.map g = 0

Tactic:
by rw [← G.map_comp, kernel.condition, G.map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
P Q : C
c c' : BinaryBicone P Q
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
cases f
  cases g
  congr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁴ : Category.{uC', uC} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ lift b.fst b.snd ≫ desc b.inl b.inr = 𝟙 b.pt

Tactic:
by
    rw [← biprod.conePointUniqueUpToIso_hom X Y hb, ←
      biprod.conePointUniqueUpToIso_inv X Y hb, Iso.hom_inv_id]

Goal state after: