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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| (e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    F.map ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫ (e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'

Tactic:
rhs

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
| F.map ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g)) ≫ (e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv = (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i

Tactic:
by
  simp [← cancel_epi (f ◁ (α_ g h i).inv)]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
⊢ (ρ_ (𝟙 a)).hom ▷ 𝟙 a ≫ (ρ_ (𝟙 a)).hom = ((α_ (𝟙 a) (𝟙 a) (𝟙 a)).hom ≫ 𝟙 a ◁ (ρ_ (𝟙 a)).hom) ≫ (ρ_ (𝟙 a)).hom

Tactic:
←
      rightUnitor_comp,

Goal state after:
B : Type u
inst✝ : Bicategory B
a : B
⊢ (ρ_ (𝟙 a)).hom ▷ 𝟙 a ≫ (ρ_ (𝟙 a)).hom = (ρ_ (𝟙 a ≫ 𝟙 a)).hom ≫ (ρ_ (𝟙 a)).hom
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type v₁
f g : P ⟶ Q
h : ∀ (X : C) (p : yoneda.obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj X
⊢ (ConcreteCategory.hom (f.app X)).toFun x = (ConcreteCategory.hom (g.app X)).toFun x

Tactic:
simpa only [yonedaEquiv_comp, Equiv.apply_symm_apply]
    using! congr_arg (yonedaEquiv) (h _ (yonedaEquiv.symm x))

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : C) (p : uliftYoneda.{w, v₁, u₁}.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g

Tactic:
ext X x
  simpa [-op_unop, uliftYonedaEquiv_comp] using
    congr_arg uliftYonedaEquiv.{w} (h _ (uliftYonedaEquiv.symm x))

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type u₂
X : Type u₂
inst✝ : Unique X
τ : (const C).obj X ⟶ F
⊢ ↑F.sections

Tactic:
by
    refine ⟨fun j ↦ τ.app _ (default : X), fun φ ↦ ?_⟩
    simp [-const_obj_obj, ← comp_apply, -types_comp_apply, ← NatTrans.naturality]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
h : Retract X Y
⊢ h.r.op ≫ h.i.op = 𝟙 (Opposite.op X)

Tactic:
simp [← op_comp, h.retract]

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✝ : J ⥤ C
G F : C ⥤ D
inst✝ : F.ReflectsIsomorphisms
K : J ⥤ C
⊢ (functoriality K F).ReflectsIsomorphisms

Tactic:
by
  constructor
  intro A B f _
  have : IsIso (F.map f.hom) :=
    (forget (K ⋙ F)).map_isIso ((functoriality K F).map f)
  have := ReflectsIsomorphisms.reflects F f.hom
  apply cone_iso_of_hom_iso

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
⊢ HasLiftingProperty g z

Tactic:
by
      constructor
      intro u v sq
      have h₀ : (f ≫ u) ≫ z = (f ≫ g) ≫ v := by simp only [Category.assoc, sq.w]
      exact
        CommSq.HasLift.mk'
          ⟨(CommSq.mk h₀).lift, by
            simp only [← cancel_mono z, Category.assoc, CommSq.fac_right, sq.w], by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi (F.map f) → Epi f

Tactic:
exact F.epi_of_epi_map

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)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
⊢ pre F E ≫ pre (E ⋙ F) D = pre F (D ⋙ E)

Tactic:
have : HasLimit ((D ⋙ E) ⋙ F) := h
  ext j; erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]; rfl

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := left } ≫ desc (inl t) (inr t) = t.ι.app { as := left }

Tactic:
exact hd₁ _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
⊢ ∀ (j : Discrete WalkingPair), I.lift (BinaryFan.swap t) ≫ s.swap.π.app j = t.π.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
⊢ I.lift (BinaryFan.swap t) ≫ s.swap.π.app { as := WalkingPair.left } = t.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P : C
s : BinaryFan X Y
t✝ : BinaryFan Y X
I : IsLimit s
t : Cone (pair Y X)
⊢ I.lift (BinaryFan.swap t) ≫ s.swap.π.app { as := WalkingPair.right } = t.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ ∀ (j : Discrete WalkingPair), R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.left } =
    t.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.right } =
    t.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ ∀ (j : Discrete WalkingPair),
    (R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.right }) ≫ sYZ.π.app j =
      t.π.app { as := WalkingPair.right } ≫ sYZ.π.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case right.left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ (R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.right }) ≫
      sYZ.π.app { as := WalkingPair.left } =
    t.π.app { as := WalkingPair.right } ≫ sYZ.π.app { as := WalkingPair.left }

case right.right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
⊢ (R.lift (BinaryFan.assocInv P t) ≫ (BinaryFan.assoc Q s).π.app { as := WalkingPair.right }) ≫
      sYZ.π.app { as := WalkingPair.right } =
    t.π.app { as := WalkingPair.right } ≫ sYZ.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ ∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ m ≫ s.π.app { as := WalkingPair.left } = (BinaryFan.assocInv P t).π.app { as := WalkingPair.left }

case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ m ≫ s.π.app { as := WalkingPair.right } = (BinaryFan.assocInv P t).π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ ∀ (j : Discrete WalkingPair),
    (m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app j =
      (BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case left.left
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ (m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app { as := WalkingPair.left } =
    (BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app { as := WalkingPair.left }

case left.right
C : Type u
inst✝ : Category.{v, u} C
X Y Z P✝ : C
sXY : BinaryFan X Y
sYZ : BinaryFan Y Z
P : IsLimit sXY
Q : IsLimit sYZ
s : BinaryFan sXY.pt Z
R : IsLimit s
t : Cone (pair X sYZ.pt)
m : t.pt ⟶ (BinaryFan.assoc Q s).pt
w : ∀ (j : Discrete WalkingPair), m ≫ (BinaryFan.assoc Q s).π.app j = t.π.app j
h :
  (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.assocInv P t).π.app j) → m = R.lift (BinaryFan.assocInv P t)
⊢ (m ≫ s.π.app { as := WalkingPair.left }) ≫ sXY.π.app { as := WalkingPair.right } =
    (BinaryFan.assocInv P t).π.app { as := WalkingPair.left } ≫ sXY.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ ∀ (j : Discrete WalkingPair),
    (t.snd ≫
          Q.lift
            (mk (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } })
              (𝟙 { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }.pt))) ≫
        t.π.app j =
      𝟙 t.pt ≫ t.π.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ (t.snd ≫
        Q.lift
          (mk (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } })
            (𝟙 { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }.pt))) ≫
      t.π.app { as := WalkingPair.left } =
    𝟙 t.pt ≫ t.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ (t.snd ≫
        Q.lift
          (mk (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } })
            (𝟙 { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }.pt))) ≫
      t.π.app { as := WalkingPair.right } =
    𝟙 t.pt ≫ t.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan s.pt X
Q : IsLimit t
⊢ ∀ (j : Discrete PEmpty.{1}),
    ((t.snd ≫
            Q.lift
              (mk (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } })
                (𝟙 { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }.pt))) ≫
          t.π.app { as := WalkingPair.left }) ≫
        s.π.app j =
      (𝟙 t.pt ≫ t.π.app { as := WalkingPair.left }) ≫ s.π.app j

Tactic:
rintro ⟨⟨⟩⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ ∀ (j : Discrete WalkingPair),
    (t.fst ≫ Q.lift (mk (𝟙 X) (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }))) ≫ t.π.app j =
      𝟙 t.pt ≫ t.π.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ (t.fst ≫ Q.lift (mk (𝟙 X) (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }))) ≫
      t.π.app { as := WalkingPair.left } =
    𝟙 t.pt ≫ t.π.app { as := WalkingPair.left }

case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ (t.fst ≫ Q.lift (mk (𝟙 X) (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }))) ≫
      t.π.app { as := WalkingPair.right } =
    𝟙 t.pt ≫ t.π.app { as := WalkingPair.right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y Z P✝ X : C
s : Cone (Functor.empty C)
P : IsLimit s
t : BinaryFan X s.pt
Q : IsLimit t
⊢ ∀ (j : Discrete PEmpty.{1}),
    ((t.fst ≫ Q.lift (mk (𝟙 X) (P.lift { pt := X, π := { app := fun x ↦ x.as.elim, naturality := ⋯ } }))) ≫
          t.π.app { as := WalkingPair.right }) ≫
        s.π.app j =
      (𝟙 t.pt ≫ t.π.app { as := WalkingPair.right }) ≫ s.π.app j

Tactic:
rintro ⟨⟨⟩⟩

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

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
F : T ⥤ D
inst✝ : F.Faithful
A B : Over X
f g : A ⟶ B
h : (post F).map f = (post F).map g
⊢ Hom.left f = Hom.left g

Tactic:
exact F.map_injective (congrArg CommaMorphism.left h)

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 : D
S : C ⥤ D
x y : CostructuredArrow S T
hl : x.left = y.left
hh : S.map (eqToHom hl) ≫ y.hom = x.hom
⊢ x = y

Tactic:
by
  cases x
  cases y
  cases hl
  cat_disch

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
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
X✝ Y✝ : CostructuredArrow (snd L R) b
f : X✝ ⟶ Y✝
⊢ L.map f.left.left ≫ (CostructuredArrow.mk (Y✝.left.hom ≫ R.map Y✝.hom)).hom =
    (CostructuredArrow.mk (X✝.left.hom ≫ R.map X✝.hom)).hom

Tactic:
dsimp
    rw [reassoc_of% f.left.w, ← R.map_comp, dsimp% CostructuredArrow.w f]

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
s : Cofork f g
W : C
k l : s.pt ⟶ W
h : s.π ≫ k = s.π ≫ l
⊢ s.ι.app zero ≫ k = s.ι.app zero ≫ l

Tactic:
by simp only [s.app_zero_eq_comp_π_left, Category.assoc, h]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : f = 0
⊢ IsZero Y

Tactic:
subst h
  apply of_epi_zero X Y

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:
simp [← cancel_epi p, ← reassoc_of% w]

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
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
F : J → C
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
X✝ Y✝ : Bicone F
f : X✝ ⟶ Y✝
j : J
⊢ { pt := G.obj X✝.pt, π := fun j ↦ G.map (X✝.π j), ι := fun j ↦ G.map (X✝.ι j), ι_π := ⋯ }.ι j ≫ G.map f.hom =
    { pt := G.obj Y✝.pt, π := fun j ↦ G.map (Y✝.π j), ι := fun j ↦ G.map (Y✝.ι j), ι_π := ⋯ }.ι j

Tactic:
by simp [-BiconeMorphism.wι, ← f.wι j]

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
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map h ≫ G.map f = 0

Tactic:
by simp only [← G.map_comp, w, Functor.map_zero]

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

Goal state before:
pp: case isFalse
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
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
j✝¹ j✝ : J
h✝ : ¬j✝ = j✝¹
⊢ 0 ≫ p j✝¹ = Sigma.ι f j✝ ≫ Sigma.map p ≫ Sigma.desc (ι g) ≫ π g j✝¹

Tactic:
· simp_all

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
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ G.map f ≫ G.map h = 0

Tactic:
by simp only [← G.map_comp, w, Functor.map_zero]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryProducts C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝ : F.PreservesZeroMorphisms
⊢ F.Additive

Tactic:
by
  have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts
  have := preservesBinaryBiproducts_of_preservesBinaryProducts F
  exact Functor.additive_of_preservesBinaryBiproducts F

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

Goal state before:
pp: case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cocone (Discrete.functor f)
as✝ : J
⊢ b.toCocone.ι.app { as := as✝ } ≫ ∑ j, b.π j ≫ s.ι.app { as := j } = s.ι.app { as := as✝ }

Tactic:
simp only [comp_sum, ← Category.assoc, Bicone.toCocone_ι_app, b.ι_π, dite_comp]

Goal state after:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cocone (Discrete.functor f)
as✝ : J
⊢ (∑ x, if h : as✝ = x then eqToHom ⋯ ≫ s.ι.app { as := x } else 0 ≫ s.ι.app { as := x }) = s.ι.app { as := as✝ }
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
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
⊢ ι f j ≫ toSubtype f p = if h : p j then ι (Subtype.restrict p f) ⟨j, h⟩ else 0

Tactic:
classical
  ext i
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π]
  by_cases h : p j
  · rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
  · rw [dif_neg h, dif_neg (show j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ ∀ (j : Discrete WalkingPair), t.inl ≫ t.toCone.π.app j = (BinaryFan.mk (𝟙 X) 0).π.app j

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.inl ≫ t.toCone.π.app { as := WalkingPair.left } = (BinaryFan.mk (𝟙 X) 0).π.app { as := WalkingPair.left }

case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.inl ≫ t.toCone.π.app { as := WalkingPair.right } = (BinaryFan.mk (𝟙 X) 0).π.app { as := WalkingPair.right }