mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Basic

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
f : X ⟶ Y
hX : X = X'
hY : Y = Y'
X'' Y'' : V
hX' : X' = X''
hY' : Y' = Y''
⊢ homOfEq (homOfEq f hX hY) hX' hY' = homOfEq f ⋯ ⋯

Tactic:
subst hX hY hX' hY'
  rfl

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α✝
f : α✝ → β
α : Type u_4
z : Sym2 α
⊢ Multiset α

Tactic:
refine Sym2.lift ?_ z

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α✝
f : α✝ → β
α : Type u_4
z : Sym2 α
⊢ { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : s(x✝, y✝).IsDiag
⊢ #s(x✝, y✝).toFinset = 1

Tactic:
rw [Sym2.mk_isDiag_iff] at h

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : x✝ = y✝
⊢ #s(x✝, y✝).toFinset = 1
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : ¬s(x✝, y✝).IsDiag
⊢ #s(x✝, y✝).toFinset = 2

Tactic:
rw [Sym2.mk_isDiag_iff] at h

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
x✝ y✝ : α
h : ¬x✝ = y✝
⊢ #s(x✝, y✝).toFinset = 2
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f f' : X ⟶ Y
g : Y ≅ Z
⊢ f ≫ g.hom = f' ≫ g.hom ↔ f = f'

Tactic:
simp only [cancel_mono]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝¹ Y✝¹ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
G : C ⥤ D
e : F ≅ G
X✝ Y✝ : C
f : G.obj X✝ ⟶ G.obj Y✝
⊢ G.map (hF.preimage (e.hom.app X✝ ≫ f ≫ e.inv.app Y✝)) = f

Tactic:
simp [← NatIso.naturality_1 e]

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
F G : C ⥤ D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), map✝¹ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝¹ (f ≫ g) = map✝¹ f ≫ map✝¹ g
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (G_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
h_obj :
  ∀ (X : C),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.obj X =
      { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ (X Y : C) (f : X ⟶ Y),
    { obj := F_obj, map := map✝¹, map_id := map_id✝¹, map_comp := map_comp✝¹ }.map f =
      eqToHom ⋯ ≫ { obj := G_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ eqToHom ⋯
⊢ F_obj = G_obj

Tactic:
by
      ext X
      apply h_obj

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
F G : C ⥤ D
h : F = G
X : C
⊢ (eqToHom h).app X = eqToHom ⋯

Tactic:
by subst h; rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D✝ : Type u₂
inst✝¹ : Category.{v₂, u₂} D✝
C : Type u_2
D : Type u_3
inst✝ : Category.{?u.12, u_3} D
F : C → D
X Y : InducedCategory D F
h : X = Y
⊢ F X = F Y

Tactic:
by subst h; rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C✝ : Type u₁
inst✝² : Category.{v₁, u₁} C✝
β : Sort u_1
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
C : Type u_2
inst✝ : Category.{?u.11, u_2} C
P : ObjectProperty C
X Y : P.FullSubcategory
h : X = Y
⊢ X.obj = Y.obj

Tactic:
by subst h; rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X Y : C × D
h : X = Y
⊢ (eqToHom h).1 = eqToHom ⋯

Tactic:
by subst h; rfl

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

Goal state before:
pp: C : Type u₁
inst✝¹ : CategoryStruct.{v₁, u₁} C
D : Type u₂
inst✝ : CategoryStruct.{v₂, u₂} D
X Y : C × D
h : X = Y
⊢ (eqToHom h).2 = eqToHom ⋯

Tactic:
by subst h; rfl

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)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((comap C g ⋙ comap (C ∘ g) f).map f' ≫ fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫ (comap C (g ∘ f)).map f'

Tactic:
simp only [comap, Function.comp]

Goal state after:
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ (({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
        f' ≫
      fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫ fun i ↦ f' (g (f i))
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)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((comap C (g ∘ f)).map f' ≫ fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫ (comap C g ⋙ comap (C ∘ g) f).map f'

Tactic:
simp only [comap, Function.comp]

Goal state after:
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((fun i ↦ f' (g (f i))) ≫ fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫
      ({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
        f'
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)
i j : I
h : i = j
⊢ C i ≌ C j

Tactic:
by subst h; rfl

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)
i j : I
h : i = j
⊢ eval C i ⋙ (eqToEquivalence C h).functor = eval C j

Tactic:
by subst h; rfl

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)
f : J → I
i' j' : J
h : i' = j'
⊢ (eqToEquivalence C ⋯).functor = (eqToEquivalence (fun i' ↦ C (f i')) h).functor

Tactic:
by subst h; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {X Y : (C ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (C ⥤ D)ᵒᵖ).map f ≫ (unop Y).opUnopIso.op.hom = (unop X).opUnopIso.op.hom ≫ (opHom C D ⋙ opInv C D).map f

Tactic:
intro F

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (C ⥤ D)ᵒᵖ
⊢ ∀ {Y : (C ⥤ D)ᵒᵖ} (f : F ⟶ Y),
    (𝟭 (C ⥤ D)ᵒᵖ).map f ≫ (unop Y).opUnopIso.op.hom = (unop F).opUnopIso.op.hom ≫ (opHom C D ⋙ opInv C D).map f
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X Y : C
f f' : X ⟶ Y
⊢ f ≫ e.unit.app Y = f' ≫ e.unit.app Y ↔ f = f'

Tactic:
simp only [cancel_mono]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X Y : C
f f' : X ⟶ e.inverse.obj (e.functor.obj Y)
⊢ f ≫ e.unitInv.app Y = f' ≫ e.unitInv.app Y ↔ f = f'

Tactic:
simp only [cancel_mono]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X Y : D
f f' : X ⟶ e.functor.obj (e.inverse.obj Y)
⊢ f ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f'

Tactic:
simp only [cancel_mono]

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X Y : D
f f' : X ⟶ Y
⊢ f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f'

Tactic:
simp only [cancel_mono]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {X Y : (Cᵒᵖ ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map f ≫ (unop Y).rightOpLeftOpIso.op.hom =
      (unop X).rightOpLeftOpIso.op.hom ≫
        ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯,
                map_comp := ⋯ }).map
          f

Tactic:
intro F

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (Cᵒᵖ ⥤ D)ᵒᵖ
⊢ ∀ {Y : (Cᵒᵖ ⥤ D)ᵒᵖ} (f : F ⟶ Y),
    (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map f ≫ (unop Y).rightOpLeftOpIso.op.hom =
      (unop F).rightOpLeftOpIso.op.hom ≫
        ({ obj := fun F ↦ (unop F).rightOp, map := fun {X Y} η ↦ NatTrans.rightOp η.unop, map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun F ↦ op F.leftOp, map := fun {X Y} η ↦ (NatTrans.leftOp η).op, map_id := ⋯,
                map_comp := ⋯ }).map
          f
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ Hom.left (eqToHom h) = eqToHom ⋯

Tactic:
by subst h; rfl

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
X Y : Arrow T
h : X = Y
⊢ Hom.right (eqToHom h) = eqToHom ⋯

Tactic:
by subst h; rfl

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 C
⊢ ∀ {F G : C ⥤ D} (x : F ≅ G), P.map F ≤ P.map G

Tactic:
intro F

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
⊢ ∀ {G : C ⥤ D} (x : F ≅ G), P.map F ≤ P.map G
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 : CoreUnitCounit F G
X : C
this : (whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit).app = (NatTrans.id (𝟭 C ⋙ F)).app
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
funext_iff

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
adj : CoreUnitCounit F G
X : C
this :
  ∀ (x : C),
    (whiskerRight adj.unit F ≫ (F.associator G F).hom ≫ F.whiskerLeft adj.counit).app x = (NatTrans.id (𝟭 C ⋙ F)).app x
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X)
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 : CoreUnitCounit F G
Y : D
this : (G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G).app = (NatTrans.id (G ⋙ 𝟭 C)).app
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)

Tactic:
funext_iff

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
adj : CoreUnitCounit F G
Y : D
this :
  ∀ (x : D),
    (G.whiskerLeft adj.unit ≫ (G.associator F G).inv ≫ whiskerRight adj.counit G).app x = (NatTrans.id (G ⋙ 𝟭 C)).app x
⊢ adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y)
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 G : C ⥤ D
H : D ⥤ C
adj : F ⊣ H
iso : F ≅ G
X : C
⊢ G.map ((adj.unit ≫ whiskerRight iso.hom H).app X) ≫ (H.whiskerLeft iso.inv ≫ adj.counit).app (G.obj X) = 𝟙 (G.obj X)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, NatTrans.comp_app, Functor.whiskerRight_app,
      Functor.map_comp, Functor.whiskerLeft_app, Category.assoc, NatTrans.naturality_assoc]

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
F G : C ⥤ D
H : D ⥤ C
adj : F ⊣ H
iso : F ≅ G
X : C
⊢ iso.inv.app X ≫ F.map (adj.unit.app X) ≫ F.map (H.map (iso.hom.app X)) ≫ adj.counit.app (G.obj X) = 𝟙 (G.obj X)
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✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
⊢ lift s ≫ t.π.app j = s.π.app j

Tactic:
apply G.map_injective; rw [G.map_comp, h]; apply ht.fac

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ StrongEpi f ↔ StrongEpi g

Tactic:
constructor <;> intro
  exacts [StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm]

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

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
inst✝¹ : F.PreservesMonomorphisms
inst✝ : G.PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
h : Mono f
⊢ Mono (G.map (F.map f))

Tactic:
exact inferInstance

Goal state after:
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
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ autoParam (∀ (F : J' ⥤ C), HasLimit F) HasLimitsOfShape.has_limit._autoParam

Tactic:
intro F

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
F : J' ⥤ C
⊢ HasLimit F
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
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ autoParam (∀ (F : J' ⥤ C), HasColimit F) HasColimitsOfShape.has_colimit._autoParam

Tactic:
intro F

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
F : J' ⥤ C
⊢ HasColimit F
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X Y : C
s : BinaryFan X Y
⊢ fst ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone s)) =
    (Iso.refl ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone s)).pt).hom ≫ (map F s).fst

Tactic:
simp [fst]

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} 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')
f : A ⟶ A'
g : B ⟶ B'
⊢ coprod.desc (F.map (coprod.inl ≫ coprod.map f g)) (F.map coprod.inr ≫ F.map (coprod.map f g)) =
    coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr))

Tactic:
coprod.inl_map,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} 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')
f : A ⟶ A'
g : B ⟶ B'
⊢ coprod.desc (F.map (f ≫ coprod.inl)) (F.map coprod.inr ≫ F.map (coprod.map f g)) =
    coprod.desc (F.map (f ≫ coprod.inl)) (F.map (g ≫ coprod.inr))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ f ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ f''

Tactic:
rw [reassoc_of% e₁, e₃, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ f ≫ i₂ ≫ j₂ = (i₁ ≫ j₁) ≫ f''

Tactic:
rw [reassoc_of% e₁, e₃, Category.assoc]

Goal state after:
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 f
⊢ pullback.fst f g = pullback.snd f g ≫ g ≫ inv f

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 f
⊢ pullback.fst f g = pullback.fst f g ≫ f ≫ inv f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.fst f f = 𝟙 (pullback f f) ≫ pullback.fst f f

Tactic:
simp [fst_eq_snd_of_mono_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom ≫ pullback.snd f f = 𝟙 (pullback f f) ≫ pullback.snd f f

Tactic:
simp [fst_eq_snd_of_mono_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ (t.fst ≫ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯) ≫ t.snd = 𝟙 t.pt ≫ t.snd

Tactic:
simp [fst_eq_snd_of_mono_eq]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
F✝ F'✝ : MonoFactorisation f✝
hF✝ : IsImage F✝
hF' : IsImage F'✝
f g : Arrow C
F : MonoFactorisation f.hom
hF : IsImage F
sq : f ⟶ g
inst✝ : IsIso sq
F' : MonoFactorisation g.hom
⊢ hF.lift (F'.ofArrowIso (inv sq)) ≫ F'.m = (F.ofArrowIso sq).m

Tactic:
simpa only [MonoFactorisation.ofArrowIso_m, Arrow.inv_right, ← Category.assoc,
      IsIso.comp_inv_eq] using hF.lift_fac (F'.ofArrowIso (inv sq))

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
⊢ g = h

Tactic:
have t₀ : v ≫ q ≫ image.ι f = image.ι f := image.lift_fac F'

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ g = h
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_from.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ G ⟶ F

pp: case unique_from.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : G ⟶ F), a = default

Tactic:
· refine
      { app := fun X => (hF _).from_ _
        naturality := ?_ }
    intros
    exact (hF _).eq_of_tgt _ _

Goal state after:
case unique_from.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ ∀ (a : G ⟶ F), a = default
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

Tactic:
rw [← Category.id_comp f, h, zero_comp]

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)
m : cokernel (?m.116 s) ⟶ ?m.118 s
w : Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
⊢ m = cokernel.desc f (g ≫ Cofork.π s) ⋯

Tactic:
by
            simp_rw [← w]
            apply coequalizer.hom_ext
            simp

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

Goal state before:
pp: case refine_4
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
⊢ IsColimit (c.whisker g).toCocone

Tactic:
· apply IsColimit.ofIsoColimit _ (Bicone.whiskerToCocone c g).symm
    apply (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _).symm _
    exact IsColimit.whiskerEquivalence hc.isColimit (Discrete.equivalence g)

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 : (b : J) → f b ⟶ g b
⊢ map p = map' p

Tactic:
classical
  ext
  simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map_assoc, Limits.IsLimit.map_π,
    ← Bicone.toCone_π_app_mk, ← Bicone.toCocone_ι_app_mk]
  dsimp
  rw [biproduct.ι_π_assoc, biproduct.ι_π]
  split_ifs with h
  · subst h; simp
  · simp

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
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
⊢ (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0

Tactic:
simpa using sub_eq_zero.2 h₂

Goal state after: