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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝ : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
h : { obj := obj, map := map, map_id := map_id✝, map_comp := map_comp✝ }.toPrefunctor = G.toPrefunctor
⊢ { obj := obj, map := map, map_id := map_id✝, map_comp := map_comp✝ } = G

Tactic:
obtain ⟨obj', map', _, _⟩ := G

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝¹ : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
obj' : C → D
map' : {X Y : C} → (X ⟶ Y) → (obj' X ⟶ obj' Y)
map_id✝ : ∀ (X : C), map' (𝟙 X) = 𝟙 (obj' X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map' (f ≫ g) = map' f ≫ map' g
h :
  { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ }.toPrefunctor =
    { obj := obj', map := map', map_id := map_id✝, map_comp := map_comp✝ }.toPrefunctor
⊢ { obj := obj, map := map, map_id := map_id✝¹, map_comp := map_comp✝¹ } =
    { obj := obj', map := map', map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
⊢ inv (𝟙 X) = 𝟙 X

Tactic:
apply inv_eq_of_hom_inv_id
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
h : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso h
⊢ inv (f ≫ h) = inv h ≫ inv f

Tactic:
apply inv_eq_of_hom_inv_id
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ inv (inv f) = f

Tactic:
apply inv_eq_of_hom_inv_id
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ inv f.inv = f.hom

Tactic:
apply inv_eq_of_hom_inv_id
  simp

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case refine_1
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ ∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1

Tactic:
have h_len : p.length = (p.length - 1) + 1 := by lia

Goal state after:
case refine_1
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
h_len : p.length = p.length - 1 + 1
⊢ ∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
t : V
C : Path a t
D : t ⟶ x✝
h : c = t ∧ p.toList = C.toList
⊢ p.cons f = C.cons D

Tactic:
obtain ⟨rfl, hAC⟩ := h

Goal state after:
V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
C : Path a c
D : c ⟶ x✝
hAC : p.toList = C.toList
⊢ p.cons f = C.cons D
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u₁
inst✝ : Quiver V
a b✝¹ b b✝ : V
q : Path a b✝
e : b✝ ⟶ b
⊢ (𝟭q V).mapPath (q.cons e) = q.cons e

Tactic:
by dsimp; rw [mapPath_id q]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : F.ReflectsIsomorphisms
X Y : C ⥤ D
f : X ⟶ Y
x✝ : IsIso (((whiskeringRight C D E).obj F).map f)
⊢ IsIso f

Tactic:
by
    rw [NatTrans.isIso_iff_isIso_app]
    intro Z
    rw [← isIso_iff_of_reflects_iso _ F]
    change IsIso ((((whiskeringRight C D E).obj F).map f).app Z)
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

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 G : C ⥤ D
X Y : C
f : X ⟶ Y
H : D ⥤ E
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hmap : F.map f ≍ G.map f
⊢ (F ⋙ H).map f ≍ (G ⋙ H).map f

Tactic:
dsimp
  congr

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

Goal state before:
pp: α✝ : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
α : Type u₁
β : Type u₂
h : Discrete α ≌ Discrete β
a : β
⊢ (as ∘ h.functor.obj ∘ mk) ((as ∘ h.inverse.obj ∘ mk) a) = a

Tactic:
by simpa using eq_of_hom (h.counitIso.app (Discrete.mk a)).1

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₂
inst✝¹ : (i : I) → Category.{v₂, u₂} (D i)
F✝ G✝ : (i : I) → C i ⥤ D i
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F G : E ⥤ ((i : I) → C i)
τ : (i : I) → F ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i
x✝¹ x✝ : E
f : x✝¹ ⟶ x✝
⊢ (F.map f ≫ fun i ↦ (τ i).app x✝) = (fun i ↦ (τ i).app x✝¹) ≫ G.map f

Tactic:
by
    ext i
    exact (τ i).naturality f

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

Goal state before:
pp: I : Type w₀
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (i : I), IsIso (f i)

Tactic:
by
  constructor
  · intro _ i
    exact (Pi.isoApp (asIso f) i).isIso_hom
  · intro
    exact ⟨fun i => inv (f i), by cat_disch, by cat_disch⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.inverseImage E.functor = P.map E.inverse

Tactic:
by
  apply le_antisymm
  · intro X Y f hf
    refine ⟨_, _, _, hf, ⟨?_⟩⟩
    exact ((Functor.mapArrowFunctor _ _).mapIso E.unitIso.symm).app (Arrow.mk f)
  · rw [map_le_iff]
    intro X Y f hf
    exact (P.arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf

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

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ F.map (L.map φ.left) ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right

Tactic:
← F.map_comp_assoc,

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ F.map (L.map φ.left ≫ Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ F.map (L.map φ.left ≫ Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ F.map (R.map φ.right) ≫ β.app Y.right

Tactic:
← F.map_comp_assoc,

Goal state after:
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ F.map (L.map φ.left ≫ Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map (X.hom ≫ R.map φ.right) ≫ β.app Y.right
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
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G.obj Y
⊢ (e X' Y).symm (f ≫ g) = (leftAdjointOfEquiv e he).map f ≫ (e X Y).symm g

Tactic:
have {X : C} {Y Y' : D} (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
            (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g := by
          rw [Equiv.symm_apply_eq, he]; simp
        simp [← this, ← he]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)

Tactic:
rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
⊢ sq.HasLift

Tactic:
CommSq.HasLift.iff_op

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : Cᵒᵖ
i : A ⟶ B
p : X ⟶ Y
h : HasLiftingProperty i p
f : Opposite.unop Y ⟶ Opposite.unop B
g : Opposite.unop X ⟶ Opposite.unop A
sq : CommSq f p.unop i.unop g
⊢ ⋯.HasLift
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1}) → Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit.{w + 1})

Tactic:
· rintro ⟨h⟩
    refine ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro ?_⟩
    let f : x ⟶ y := by
      have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert! h.unit.app x
      have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert! h.unitInv.app y
      exact hx ≫ hy
    suffices sub : Subsingleton (x ⟶ y) from uniqueOfSubsingleton f
    have : ∀ z, z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y := by
      simp
    apply Subsingleton.intro
    intro a b
    rw [this a, this b]
    simp only [Functor.comp_map]
    congr 3
    apply ULift.ext
    simp [eq_iff_true_of_subsingleton]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit.{w + 1})
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f = hi.inv ≫ hi.hom ≫ f

pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    c₁.ι.app j ≫ hi.hom ≫ f = { pt := c.pt, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.ι.app j

Tactic:
· simp only [Iso.inv_hom_id_assoc]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    c₁.ι.app j ≫ hi.hom ≫ f = { pt := c.pt, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.ι.app j
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (isoLimitCone t).hom ≫ t.cone.π.app j = π F j

Tactic:
dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (Cone.forget F).map ((isLimit F).uniqueUpToIso t.isLimit).hom ≫ t.cone.π.app j = π F j
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (isoLimitCone t).inv ≫ π F j = t.cone.π.app j

Tactic:
dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (Cone.forget F).map ((isLimit F).uniqueUpToIso t.isLimit).inv ≫ π F j = t.cone.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X : Over A
⊢ { app := fun g ↦ homMk (coprod.map (Hom.left (𝟙 X)) (𝟙 g.left)) ⋯, naturality := ⋯ } = 𝟙 X.coprodObj

Tactic:
by
    ext
    simp

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✝ Z✝ : Over A
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { app := fun g_1 ↦ homMk (coprod.map (Hom.left (f ≫ g)) (𝟙 g_1.left)) ⋯, naturality := ⋯ } =
    { app := fun g ↦ homMk (coprod.map (Hom.left f) (𝟙 g.left)) ⋯, naturality := ⋯ } ≫
      { app := fun g_1 ↦ homMk (coprod.map (Hom.left g) (𝟙 g_1.left)) ⋯, naturality := ⋯ }

Tactic:
by
    ext
    simp

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)
m : t.pt ⟶ s.swap.pt
w : ∀ (j : Discrete WalkingPair), m ≫ s.swap.π.app j = t.π.app j
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
j : WalkingPair
⊢ m ≫ s.π.app { as := j } = (BinaryFan.swap t).π.app { as := j }

Tactic:
specialize w ⟨WalkingPair.swap j⟩

Goal state after:
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)
m : t.pt ⟶ s.swap.pt
h : (∀ (j : Discrete WalkingPair), m ≫ s.π.app j = (BinaryFan.swap t).π.app j) → m = I.lift (BinaryFan.swap t)
j : WalkingPair
w : m ≫ s.swap.π.app { as := WalkingPair.swap j } = t.π.app { as := WalkingPair.swap j }
⊢ m ≫ s.π.app { as := j } = (BinaryFan.swap t).π.app { as := j }
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
F : D ⥤ T
X : T
Y : Over X
X✝ Y✝ : CostructuredArrow F Y.left
f : X✝ ⟶ Y✝
⊢ (toOver F X).map (homMk f.left ⋯) ≫ (mk (Over.homMk Y✝.hom ⋯)).hom = (mk (Over.homMk X✝.hom ⋯)).hom

Tactic:
by ext; exact CostructuredArrow.w f

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 : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
⊢ ∃ a, (post F).map a = f

Tactic:
obtain ⟨a, ha⟩ := F.map_surjective f.right

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ ∃ a, (post F).map a = f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ pullback.snd f g = pullback.fst f g ≫ f ≫ inv g

Tactic:
pullback.condition_assoc,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ pullback.snd f g = pullback.snd f g ≫ g ≫ inv g
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ F.map WalkingParallelPairHom.left ≫ (WalkingParallelPair.casesOn WalkingParallelPair.one zero one).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero zero one).hom ≫ G.map WalkingParallelPairHom.left

Tactic:
simp [left, right]

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

Goal state before:
pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ F.map WalkingParallelPairHom.right ≫ (WalkingParallelPair.casesOn WalkingParallelPair.one zero one).hom =
    (WalkingParallelPair.casesOn WalkingParallelPair.zero zero one).hom ≫ G.map WalkingParallelPairHom.right

Tactic:
simp [left, right]

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

Goal state before:
pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (WalkingParallelPair.casesOn X✝ zero one).hom =
    (WalkingParallelPair.casesOn X✝ zero one).hom ≫ G.map (WalkingParallelPairHom.id X✝)

Tactic:
simp [left, right]

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
i : IsZero Y
inst✝ : Mono 0
⊢ IsZero X

Tactic:
exact IsZero.of_mono_zero X Y

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
O : C
hO : IsZero O
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ 0 = 0

Tactic:
change f ≫ (hO.from_ Y ≫ hO.to_ Z) = hO.from_ X ≫ hO.to_ Z

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
O : C
hO : IsZero O
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ hO.from_ Y ≫ hO.to_ Z = hO.from_ X ≫ hO.to_ Z
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
inst✝¹ : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
⊢ π f g ≫ colimMap (parallelPairHom f g f' g' p q wf wg) ≫ desc h wh = q ≫ h

Tactic:
by
  rw [ι_colimMap_assoc, parallelPairHom_app_one, coequalizer.π_desc]

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

Goal state before:
pp: case calc_1
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ F.map 0 = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y)

Tactic:
Adjunction.left_triangle_components

Goal state after:
case calc_1
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.IsLeftAdjoint
X Y : C
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ F.map 0 = F.map 0 ≫ 𝟙 (F.obj Y)
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
β : Type u'
inst✝¹ : HasZeroMorphisms C
f : β → C
inst✝ : HasColimit (Discrete.functor f)
b : β
⊢ IsSplitMono (Sigma.ι f b)

Tactic:
exact IsSplitMono.mk' { retraction := Sigma.desc <| Pi.single b (𝟙 _) }

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0 = 0

Tactic:
by simp only [zero_of_to_zero i.hom, zero_comp, comp_zero]

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
⊢ G.map f.hom ≫ { pt := G.obj Y✝.pt, π := fun j ↦ G.map (Y✝.π j), ι := fun j ↦ G.map (Y✝.ι j), ι_π := ⋯ }.π j =
    { pt := G.obj X✝.pt, π := fun j ↦ G.map (X✝.π j), ι := fun j ↦ G.map (X✝.ι j), ι_π := ⋯ }.π j

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

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
inst✝¹ : G.Full
inst✝ : G.Faithful
X✝ Y✝ : Bicone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
j : J
⊢ G.map (X✝.ι j ≫ G.preimage t.hom) = G.map (Y✝.ι j)

Tactic:
simpa using! t.wι j

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

Goal state before:
pp: case refine_3
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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : c.IsBilimit
⊢ IsLimit (c.whisker g).toCone

Tactic:
apply IsLimit.ofIsoLimit _ (Bicone.whiskerToCone c g).symm
    apply (IsLimit.postcomposeHomEquiv (Discrete.functorComp f g).symm _).symm _
    exact IsLimit.whiskerEquivalence hc.isLimit (Discrete.equivalence g)

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
⊢ t.inr = BinaryFan.IsLimit.lift ht 0 (𝟙 Y)

Tactic:
apply ht.uniq (BinaryFan.mk 0 (𝟙 Y)); rintro ⟨⟨⟩⟩ <;> simp

Goal state after: