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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
G : C ⥤ Type u_2
e : (j : C) → F.obj j ≃ G.obj j
naturality :
  ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)
j j' : C
f : j ⟶ j'
x : (fun X ↦ X) (G.obj j)
⊢ (⇑(e j').symm ∘ ⇑(ConcreteCategory.hom (G.map f))) x = (⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm) x

Tactic:
obtain ⟨y, rfl⟩ := (e j).surjective x

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
G : C ⥤ Type u_2
e : (j : C) → F.obj j ≃ G.obj j
naturality :
  ∀ {j j' : C} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (F.map f)) = ⇑(ConcreteCategory.hom (G.map f)) ∘ ⇑(e j)
j j' : C
f : j ⟶ j'
y : F.obj j
⊢ (⇑(e j').symm ∘ ⇑(ConcreteCategory.hom (G.map f))) ((e j) y) =
    (⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j).symm) ((e j) y)
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
e : F ≅ G
⊢ P.map F ≤ P.map G

Tactic:
X

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 G : C ⥤ D
e : F ≅ G
X : D
⊢ ∀ ⦃Y : D⦄ (f : X ⟶ Y), P.map F f → P.map G f
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ : X →* Y
⊢ ∀ ⦃a₂ : X →* Y⦄, (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂ → a₁✝ = a₂

Tactic:
_

Goal state after:
X Y : Type u
inst✝¹ : Group X
inst✝ : Group Y
a₁✝ a₂✝ : X →* Y
⊢ (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂✝ → a₁✝ = a₂✝
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ : X →* Y
⊢ ∀ ⦃a₂ : X →* Y⦄, (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂ → a₁✝ = a₂

Tactic:
_

Goal state after:
X Y : Type u
inst✝¹ : CommGroup X
inst✝ : CommGroup Y
a₁✝ a₂✝ : X →* Y
⊢ (fun f ↦ ofHom f) a₁✝ = (fun f ↦ ofHom f) a₂✝ → a₁✝ = a₂✝
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g = h.liftConeMorphism s

Tactic:
apply ConeMorphism.ext

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
s t : Cone F
h : IsLimit t
f f' g : s ⟶ t
⊢ g.hom = (h.liftConeMorphism s).hom
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 : CoreHomEquiv F G
⊢ (mkOfHomEquiv adj).homEquiv = adj.homEquiv

Tactic:
ext X Y g
  simp [mkOfHomEquiv, ← adj.homEquiv_naturality_right (𝟙 _) g]

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
A B : Cone K
f : A ⟶ B
⊢ ∀ [IsIso ((functoriality K F).map f)], IsIso f

Tactic:
_

Goal state after:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁵ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝⁴ : Category.{v₃, u₃} C
D : Type u₄
inst✝³ : Category.{v₄, u₄} D
E : Type u₅
inst✝² : Category.{v₅, u₅} E
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : F.ReflectsIsomorphisms
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
⊢ IsIso f
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
⊢ x ⟶ y

Tactic:
have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert! h.unitInv.app y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
hx : x ⟶ h.inverse.obj { as := PUnit.unit }
hy : h.inverse.obj { as := PUnit.unit } ⟶ y
⊢ x ⟶ y
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
s : Cocone F
m : (coconeOfDiagramTerminal tX F).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfDiagramTerminal tX F).ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app X

Tactic:
by simp [← w X]

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
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E

Tactic:
have : HasLimit (E ⋙ F ⋙ G) := h

Goal state after:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
X✝ : WidePullbackShape J
⊢ Option.casesOn X✝ B objs ⟶ Option.casesOn X✝ B objs

Tactic:
apply 𝟙 _

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

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ : WidePushoutShape J
⊢ Option.casesOn X✝ B objs ⟶ Option.casesOn X✝ B objs

Tactic:
apply 𝟙 _

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

Goal state before:
pp: case none
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
⊢ g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app none =
    (WidePullbackShape.mkCone f fs w).π.app none

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 h2

Goal state after:
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✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
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
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none

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 h2

Goal state after:
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✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
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
⊢ (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app none ≫ g =
    (WidePushoutShape.mkCocone f fs w).ι.app none

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 h2

Goal state after:
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✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
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
⊢ colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g2

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 h2

Goal state after:
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
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
l : WalkingPair
⊢ c.π.app { as := l } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := l }

Tactic:
by cases l; repeat simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
l : WalkingPair
⊢ c.ι.app { as := l } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := l }

Tactic:
by cases l; repeat simp

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

Goal state before:
pp: β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ (reindex ε f).hom ≫ π f (ε b) = π (f ∘ ⇑ε) b

Tactic:
dsimp [Pi.reindex]
  simp only [HasLimit.isoOfEquivalence_hom_π, Discrete.equivalence_inverse, Discrete.functor_obj,
    Function.comp_apply, Functor.id_obj, Discrete.equivalence_functor, Functor.comp_obj,
    Discrete.natIso_inv_app, Iso.refl_inv, Category.id_comp]
  exact limit.w (Discrete.functor (f ∘ ε)) (Discrete.eqToHom' (ε.symm_apply_apply b))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ IsColimit (mk (f ≫ c.inl) c.inr)

Tactic:
fapply BinaryCofan.isColimitMk
  · exact fun s => BinaryCofan.IsColimit.desc h (inv f ≫ s.inl) s.inr
  · simp
  · simp
  · intro s m e₁ e₂
    apply BinaryCofan.IsColimit.hom_ext h
    · rw [← cancel_epi f]
      simpa using e₁
    · simpa

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
W : C
k l : W ⟶ t.pt
h₀ : k ≫ t.fst = l ≫ t.fst
h₁ : k ≫ t.snd = l ≫ t.snd
⊢ k ≫ t.π.app none = l ≫ t.π.app none

Tactic:
rw [← t.w inl, reassoc_of% h₀]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ Nonempty (W₁.MapFactorizationData W₂ f)

Tactic:
have : W₁.comp W₂ f := by simp only [h, top_apply]

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : W₁.comp W₂ f
⊢ Nonempty (W₁.MapFactorizationData W₂ f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ (mk s.fst s.snd ⋯).fst = t.fst
hr' : m✝ ≫ (mk s.fst s.snd ⋯).snd = t.snd
⊢ m✝ = hs.lift (mk t.fst t.snd ⋯)

Tactic:
apply PullbackCone.IsLimit.hom_ext hs <;>
              simp only [PullbackCone.mk_fst, PullbackCone.mk_snd] at hr hr' ⊢ <;>
            simp only [hr, hr'] <;>
          symm
        exacts [hs.fac _ WalkingCospan.left, hs.fac _ WalkingCospan.right]

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

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

Tactic:
simpa using congr($(hαα').app X)

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

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

Tactic:
simp only [← Category.assoc]; rw [cancel_mono]; apply pullback.condition

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
f : X ⟶ Y
⊢ HasPushout (h ≫ f) h

Tactic:
simpa only [Category.comp_id] using hasPushout_of_epi_comp f (𝟙 X) h

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

Goal state before:
pp: case unique_to.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
⊢ F ⟶ G

Tactic:
refine
      { app := fun X => (hF _).to_ _
        naturality := ?_ }

Goal state after:
case unique_to.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
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ ⋯.to_ (G.obj Y) = ⋯.to_ (G.obj X) ≫ G.map f
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: 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)
⊢ IsZero F

Tactic:
by
  constructor <;> intro G <;> refine ⟨⟨⟨?_⟩, ?_⟩⟩
  · refine
      { app := fun X => (hF _).to_ _
        naturality := ?_ }
    intros
    exact (hF _).eq_of_src _ _
  · intro f
    ext
    apply (hF _).eq_of_src _ _
  · refine
      { app := fun X => (hF _).from_ _
        naturality := ?_ }
    intros
    exact (hF _).eq_of_tgt _ _
  · intro f
    ext
    apply (hF _).eq_of_tgt _ _

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

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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : c.IsBilimit
⊢ IsLimit
    ((Cone.postcompose (Discrete.functorComp f ⇑g).inv).obj
      (Cone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCone))
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: 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 : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
j : J
⊢ j ∈ Finset.univ → m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j

Tactic:
_

Goal state after:
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 : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
j : J
a✝ : j ∈ Finset.univ
⊢ m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: 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)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
j : J
⊢ j ∈ Finset.univ → (b.π j ≫ b.ι j) ≫ m = b.π j ≫ s.ι.app { as := j }

Tactic:
_

Goal state after:
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)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
j : J
a✝ : j ∈ Finset.univ
⊢ (b.π j ≫ b.ι j) ≫ m = b.π j ≫ s.ι.app { as := j }
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 W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Epi (map f g)

Tactic:
by
  rw [show prod.map f g = (biprod.isoProd _ _).inv ≫ biprod.map f g ≫
    (biprod.isoProd _ _).hom by simp]
  infer_instance

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
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
this : Epi (Cofork.π c) := epi_of_isColimit_cofork i
⊢ 𝟙 Y ≫ retraction f - retraction f = 0

Tactic:
apply sub_eq_zero_of_eq

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
this : Epi (Cofork.π c) := ⋯
⊢ 𝟙 Y ≫ retraction f = retraction f
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
⊢ HAdd.hAdd = HAdd.hAdd

Tactic:
funext f g

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
⊢ f + g = f + g
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
i : μ × μ
⊢ i ∈ ↑(antidiagonal n) →
    ∀ ⦃y : μ × μ⦄,
      y ∈ ↑(antidiagonal n) → i ≠ y → (Disjoint on fun ab ↦ map { toFun := Fin.cons ab.1, inj' := ⋯ } ↑(aux d ab.2)) i y

Tactic:
_

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
i : μ × μ
a✝ : i ∈ ↑(antidiagonal n)
⊢ ∀ ⦃y : μ × μ⦄,
    y ∈ ↑(antidiagonal n) → i ≠ y → (Disjoint on fun ab ↦ map { toFun := Fin.cons ab.1, inj' := ⋯ } ↑(aux d ab.2)) i y
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
i : μ × μ
a✝ : i ∈ ↑(antidiagonal n)
j : μ × μ
⊢ j ∈ ↑(antidiagonal n) → i ≠ j → (Disjoint on fun ab ↦ map { toFun := Fin.cons ab.1, inj' := ⋯ } ↑(aux d ab.2)) i j

Tactic:
_

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
d✝ : ℕ
n : μ
d : ℕ
i : μ × μ
a✝¹ : i ∈ ↑(antidiagonal n)
j : μ × μ
a✝ : j ∈ ↑(antidiagonal n)
⊢ i ≠ j → (Disjoint on fun ab ↦ map { toFun := Fin.cons ab.1, inj' := ⋯ } ↑(aux d ab.2)) i j