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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
⊢ whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit = F.leftUnitor.hom ≫ F.rightUnitor.inv

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
⊢ G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G = G.rightUnitor.hom ≫ G.leftUnitor.inv

Tactic:
ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.RepresentableBy X
⊢ (fun R ↦ R.ofIsoObj e.symm) ((fun R ↦ R.ofIsoObj e) x✝) = x✝

Tactic:
ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.RepresentableBy Y
⊢ (fun R ↦ R.ofIsoObj e) ((fun R ↦ R.ofIsoObj e.symm) x✝) = x✝

Tactic:
ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.CorepresentableBy X
⊢ (fun R ↦ R.ofIsoObj e.symm) ((fun R ↦ R.ofIsoObj e) x✝) = x✝

Tactic:
ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type w
X Y : C
e : Y ≅ X
x✝ : F.CorepresentableBy Y
⊢ (fun R ↦ R.ofIsoObj e) ((fun R ↦ R.ofIsoObj e.symm) x✝) = x✝

Tactic:
ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.map g.op)) (yonedaEquiv f) = (ConcreteCategory.hom (f.app (op Y))) g

Tactic:
rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
⊢ ∀ (a : ThinSkeleton C), Quotient.lift₂ (fun X Y ↦ Nonempty (X ⟶ Y)) ⋯ a a

Tactic:
refine Quotient.ind fun a => ?_
    exact ⟨𝟙 _⟩

Goal state after:
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton C
⊢ (𝟭 (ThinSkeleton C)).obj X ⟶ (map L ⋙ map R).obj X

Tactic:
letI := isIsomorphicSetoid C

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton C
this : Setoid C := isIsomorphicSetoid C
⊢ (𝟭 (ThinSkeleton C)).obj X ⟶ (map L ⋙ map R).obj X
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: case fst.mk
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
fst✝ : Cᵒᵖ
snd✝ : (const J).obj (unop fst✝) ⟶ F
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := unop c.fst, π := c.snd }) ≫ ↾fun c ↦ ⟨op c.pt, c.π⟩)).toFun
        ⟨fst✝, snd✝⟩).fst =
    ((ConcreteCategory.hom (𝟙 ((X : Cᵒᵖ) × ((const J).obj (unop X) ⟶ F)))).toFun ⟨fst✝, snd✝⟩).fst

pp: 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

Tactic:
all_goals rfl

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

Goal state before:
pp: case fst.mk
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
fst✝ : C
snd✝ : F.cocones.obj fst✝
⊢ ((ConcreteCategory.hom ((↾fun c ↦ { pt := c.fst, ι := c.snd }) ≫ ↾fun c ↦ ⟨c.pt, c.ι⟩)).toFun ⟨fst✝, snd✝⟩).fst =
    ((ConcreteCategory.hom (𝟙 ((X : C) × F.cocones.obj X))).toFun ⟨fst✝, snd✝⟩).fst

pp: 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

Tactic:
all_goals rfl

Goal state after:
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
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
⊢ lift F c ≫ pre F E = lift (E ⋙ F) (Cone.whisker E c)

Tactic:
ext; simp

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

Goal state before:
pp: case some
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
val✝ : J
⊢ g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app (some val✝) =
    (WidePullbackShape.mkCone f fs w).π.app (some val✝)

Tactic:
· apply h1

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

Goal state before:
pp: case some
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
val✝ : J
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val✝) =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val✝)

Tactic:
· apply h1

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

Goal state before:
pp: case some
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
val✝ : J
⊢ (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app (some val✝) ≫ g =
    (WidePushoutShape.mkCocone f fs w).ι.app (some val✝)

Tactic:
· apply h1

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
⊢ (map fun a ↦ 𝟙 (f a)) = 𝟙 (∏ᶜ f)

Tactic:
ext; simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
⊢ map q ≫ map q' = map fun a ↦ q a ≫ q' a

Tactic:
ext; simp

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

Goal state before:
pp: case some
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
val✝ : J
⊢ colimit.ι (WidePushoutShape.wideSpan B objs arrows) (some val✝) ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) (some val✝) ≫ g2

Tactic:
· apply h1

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
⊢ (map' id fun a ↦ 𝟙 (f a)) = 𝟙 (∏ᶜ f)

Tactic:
ext; simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
p' : γ → β
q : (b : β) → f (p b) ⟶ g b
q' : (c : γ) → g (p' c) ⟶ h c
⊢ map' p q ≫ map' p' q' = map' (p ∘ p') fun c ↦ q (p' c) ≫ q' c

Tactic:
ext; simp

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → g b ⟶ h b
⊢ map' p q ≫ map q' = map' p fun b ↦ q b ≫ q' b

Tactic:
ext; simp

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (a : α) → f a ⟶ g a
q' : (b : β) → g (p b) ⟶ h b
⊢ map q ≫ map' p q' = map' p fun b ↦ q (p b) ≫ q' b

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F) = 𝟙 (limit F)

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F) = 𝟙 (limit F)

Tactic:
ext; simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
⊢ (map fun a ↦ 𝟙 (f a)) = 𝟙 (∐ f)

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
⊢ colimit.desc F (coconeOfDiagramTerminal I F) ≫ colimit.ι F j = 𝟙 (colimit F)

Tactic:
ext; simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
⊢ map q ≫ map q' = map fun a ↦ q a ≫ q' a

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = 𝟙 (colimit F)

Tactic:
ext; simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
⊢ (map' id fun a ↦ 𝟙 (f a)) = 𝟙 (∐ f)

Tactic:
ext; simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
⊢ map' p q ≫ map' p' q' = map' (p' ∘ p) fun a ↦ q a ≫ q' (p a)

Tactic:
ext; simp

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h b
⊢ map' p q ≫ map q' = map' p fun a ↦ q a ≫ q' (p a)

Tactic:
ext; simp

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h (p a)
⊢ map q ≫ map' p q' = map' p fun a ↦ q a ≫ q' a

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryCoproduct W Y
inst✝ : HasBinaryCoproduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ desc (g ≫ inl) (g' ≫ inr) = map g g'

Tactic:
by
  rw [← coprod.map_desc]; simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (leftUnitor X).inv ≫ map (𝟙 (⊤_ C)) f = f ≫ (leftUnitor Y).inv

Tactic:
by
  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
X Y : C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F✝ : C ⥤ D
A✝ A' B B' : C
inst✝⁵ : HasBinaryCoproduct A✝ B
inst✝⁴ : HasBinaryCoproduct A' B'
inst✝³ : HasBinaryCoproduct (F✝.obj A✝) (F✝.obj B)
inst✝² : HasBinaryCoproduct (F✝.obj A') (F✝.obj B')
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasBinaryCoproducts D
F : C ⥤ D
A f : C
⊢ ∀ ⦃Y : C⦄ (f_1 : f ⟶ Y),
    (F ⋙ coprod.functor.obj (F.obj A)).map f_1 ≫ coprodComparison F A Y =
      coprodComparison F A f ≫ (coprod.functor.obj A ⋙ F).map f_1

Tactic:
simp [coprodComparison_natural]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ { obj := fun j ↦ (data.factorizationData (X✝.hom.app j)).Z,
            map := fun {X Y} φ ↦ data.mapZ (Arrow.homMk (X✝.left.map φ) (X✝.right.map φ) ⋯), map_id := ⋯,
            map_comp := ⋯ }.map
        x✝ ≫
      data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯) ≫
      { obj := fun j ↦ (data.factorizationData (Y✝.hom.app j)).Z,
            map := fun {X Y} φ ↦ data.mapZ (Arrow.homMk (Y✝.left.map φ) (Y✝.right.map φ) ⋯), map_id := ⋯,
            map_comp := ⋯ }.map
        x✝

Tactic:
by
        dsimp
        rw [← data.mapZ_comp, ← data.mapZ_comp]
        congr 1
        ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
⊢ HasZeroObject C

Tactic:
by
  refine ⟨⟨⊤_ C, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, by cat_disch⟩⟩⟩⟩
  calc
    f = 𝟙 _ ≫ f := (Category.id_comp _).symm
    _ = 0 ≫ f := by congr!; subsingleton
    _ = 0 := zero_comp

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
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ IsColimit c

Tactic:
by
    apply IsColimit.precomposeHomEquiv h c (isColimitOfReflects F _)
    apply ((IsColimit.precomposeHomEquiv (Functor.isoWhiskerRight h F :) _).symm t).ofIsoColimit _
    exact Cocone.ext (Iso.refl _)

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

Goal state before:
pp: 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 : C ⥤ᵣ D
G : D ⥤ᵣ E
⊢ rightExactFunctor C E (F.obj ⋙ G.obj)

Tactic:
exact comp_preservesFiniteColimits _ _

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

Goal state before:
pp: 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 : D ⥤ᵣ E
G : C ⥤ᵣ D
⊢ rightExactFunctor C E (G.obj ⋙ F.obj)

Tactic:
exact comp_preservesFiniteColimits _ _

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

Goal state before:
pp: 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 : C ⥤ₑ D
G : D ⥤ₑ E
⊢ rightExactFunctor C E (F.obj ⋙ G.obj)

Tactic:
exact comp_preservesFiniteColimits _ _

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

Goal state before:
pp: 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 : D ⥤ₑ E
G : C ⥤ₑ D
⊢ rightExactFunctor C E (G.obj ⋙ F.obj)

Tactic:
exact comp_preservesFiniteColimits _ _

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
W : C
h : 0 ≫ f = 0
⊢ lift f 0 h = 0

Tactic:
ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ ((F.mapBiproduct f).hom ≫ desc fun j ↦ F.map (g j)) = F.map (desc g)

Tactic:
rw [← biproduct.mapBiproduct_inv_map_desc, Iso.hom_inv_id_assoc]

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✝ : HasCokernel f
W : C
h : f ≫ 0 = 0
⊢ desc f 0 h = 0

Tactic:
ext; 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 : X ⟶ Y
inst✝³ : HasCokernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝² : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
inst✝¹ : Epi p
inst✝ : IsIso q
⊢ f' ≫ inv q ≫ cokernel.π f = 0

Tactic:
by simp [← cancel_epi p, ← reassoc_of% w]

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✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
s : CokernelCofork (f ≫ g)
⊢ f ≫ g ≫ Cofork.π s = 0

Tactic:
rw [← Category.assoc, CokernelCofork.condition]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : Discrete J
⊢ colimit.ι (Discrete.functor f) j ≫ (isoCoproduct f).inv = colimit.ι (Discrete.functor f) j ≫ Sigma.desc (ι f)

Tactic:
simp [biproduct.isoCoproduct]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (j : J) → f j ⟶ g j
P : C
k : (j : J) → g j ⟶ P
⊢ map p ≫ desc k = desc fun j ↦ p j ≫ k j

Tactic:
ext; simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
P : C
k : (j : J) → P ⟶ f j
p : (j : J) → f j ⟶ g j
⊢ lift k ≫ map p = lift fun j ↦ k j ≫ p j

Tactic:
ext; simp

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
⊢ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv ≫
      (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).hom =
    𝟙 (X ⊞ Y)

Tactic:
Iso.inv_hom_id

Goal state after:
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
⊢ 𝟙 (X ⊞ Y) = 𝟙 (X ⊞ Y)
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

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✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv ≫ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).hom = 𝟙 (⨁ f)

Tactic:
Iso.inv_hom_id

Goal state after:
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✝
F : J✝¹ → C✝¹
J✝ : Type w
K : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ 𝟙 (⨁ f) = 𝟙 (⨁ f)
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M✝ N✝ x✝ M N : ModuleCat S
s₀ : S₀
f : x✝ ⟶ M
g : M ⟶ N
⊢ (s₀ • f) ≫ g = s₀ • f ≫ g

Tactic:
ext; simp

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝ : LE α
⊢ insertNthOrderIso (fun x ↦ α) (last n) = snocOrderIso fun x ↦ α

Tactic:
ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂
inst✝ : IsIso (biprod.inl ≫ f ≫ biprod.fst)
⊢ (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
    (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×' (g₂₂ : X₂ ⟶ Y₂) ×' L.hom ≫ f ≫ R.hom = biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂

Tactic:
let :=
    Biprod.gaussian' (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd)
      (biprod.inr ≫ f ≫ biprod.fst) (biprod.inr ≫ f ≫ biprod.snd)
  rwa [Biprod.ofComponents_eq] at this

Goal state after: