mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
⊢ HasLimit F

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
f : G.obj (⊤_ C) ⟶ ⊤_ D
i : IsIso f
⊢ PreservesLimit (Functor.empty C) G

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝² : HasTerminal C
inst✝¹ : HasTerminal D
inst✝ : PreservesLimit (Functor.empty C) G
⊢ IsIso (terminalComparison G)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X✝ : C
inst✝¹ : PreservesColimit (Functor.empty C) G
inst✝ : ReflectsColimit (Functor.empty C) G
X : C
⊢ Function.LeftInverse (isInitialOfObj G X) (isInitialObj G X)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X✝ : C
inst✝¹ : PreservesColimit (Functor.empty C) G
inst✝ : ReflectsColimit (Functor.empty C) G
X : C
⊢ Function.RightInverse (isInitialOfObj G X) (isInitialObj G X)

Tactic:
by

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

Tactic:
by

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
i : IsZero X
⊢ IsZero Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cone K
h : IsLimit c
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (m : s.pt ⟶ ((𝟭 C).mapCone c).pt),
    (∀ (j : J), m ≫ ((𝟭 C).mapCone c).π.app j = s.π.app j) →
      m = h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } }

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : PreservesColimit (Functor.empty C) G
F : Discrete PEmpty.{1} ⥤ D
⊢ HasColimit F

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G

Tactic:
by

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

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✝
X Y : C
f g : X ⟶ Y
X' Y' : C
c : Cofork f g
f' g' : X' ⟶ Y'
c' : Cofork f' g'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
e : c.pt ≅ c'.pt
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
comm₃ : e₁.inv ≫ c.π ≫ e.hom = c'.π
i : parallelPair f g ≅ parallelPair f' g' := parallelPair.ext e₀ e₁ ⋯ ⋯
⊢ π ((Cocone.precompose i.inv).obj c) ≫ e.hom = c'.π

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
f : ⊥_ D ⟶ G.obj (⊥_ C)
i : IsIso f
⊢ PreservesColimit (Functor.empty C) G

Tactic:
by

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
inst✝ : HasEqualizer f g
⊢ (Iso.refl (limit.cone (parallelPair f g)).pt).hom ≫ (Fork.ofι (equalizer.ι f g) ⋯).ι =
    Fork.ι (limit.cone (parallelPair f g))

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝² : HasInitial C
inst✝¹ : HasInitial D
inst✝ : PreservesColimit (Functor.empty C) G
⊢ IsIso (initialComparison G)

Tactic:
by

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
h✝ : f = g
s : Fork f g
m : s.pt ⟶ (idFork h✝).pt
h : m ≫ (idFork h✝).ι = s.ι
⊢ m = s.ι

Tactic:
by

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
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
by

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 : X ⟶ Y
⊢ (isoSourceOfSelf f).inv = lift (𝟙 X) ⋯

Tactic:
by

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
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
Z : C
⊢ f ≫ 0 = 0

Tactic:
by

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✝ f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
c : PullbackCone s.ι h
⊢ c.snd ≫ h ≫ f = c.snd ≫ h ≫ g

Tactic:
by

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✝ f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h
hc : IsLimit c
s' : Fork (h ≫ f) (h ≫ g)
⊢ (s'.ι ≫ h) ≫ f = (s'.ι ≫ h) ≫ g

Tactic:
by

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
inst✝ : HasZeroObject C
X Y Z : C
f : Y ⟶ Z
⊢ 0 ≫ f = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsInitial X
⊢ (zeroIsoIsInitial t).hom = 0

Tactic:
by

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✝ f g : X ⟶ Y
Z : C
h : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h
hc : IsLimit c
⊢ ∀ (s_1 : Fork (h ≫ f) (h ≫ g)), liftPrecomp h hs hc s_1 ≫ (precompFork h s c).ι = s_1.ι

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsInitial X
⊢ (zeroIsoIsInitial t).inv = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsTerminal X
⊢ (zeroIsoIsTerminal t).hom = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsTerminal X
⊢ (zeroIsoIsTerminal t).inv = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ zeroIsoInitial.hom = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ zeroIsoInitial.inv = 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
⊢ f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cocone K
h : IsColimit c
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (j : J),
    ((𝟭 C).mapCocone c).ι.app j ≫ h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } } = s.ι.app j

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
⊢ f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
Z : C
g h : Z ⟶ X
x✝ : g ≫ f = h ≫ f
⊢ g = h

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
Z : C
g h : Y ⟶ Z
x✝ : f ≫ g = f ≫ h
⊢ g = h

Tactic:
by

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
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ Function.LeftInverse ⋯ fun h ↦ { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
by

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
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ Function.RightInverse ⋯ fun h ↦ { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
by

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
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
x✝ : Mono 0
⊢ (0 ≫ 0) ≫ 0 = 𝟙 X ≫ 0

Tactic:
by

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
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
x✝ : Epi 0
⊢ 0 ≫ 0 ≫ 0 = 0 ≫ 𝟙 Y

Tactic:
by

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
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ X ≅ 0

Tactic:
by

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
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : f = 0
⊢ Y ≅ 0

Tactic:
by

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✝ f g : X ⟶ Y
Z : C
h✝ : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h✝
hc : IsLimit c
s' : Fork (h✝ ≫ f) (h✝ ≫ g)
m : s'.pt ⟶ (precompFork h✝ s c).pt
h : m ≫ (precompFork h✝ s c).ι = s'.ι
⊢ ∀ (j : WalkingCospan), m ≫ c.π.app j = liftPrecomp h✝ hs hc s' ≫ c.π.app j

Tactic:
by

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
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : IsIsomorphic X 0
⊢ 0 ≫ 0 = 𝟙 X

Tactic:
by

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
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P : IsIsomorphic X 0
⊢ 0 ≫ 0 = 𝟙 0

Tactic:
by

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
inst✝ : HasCoequalizer f g
⊢ Cofork.π (colimit.cocone (parallelPair f g)) ≫ (Iso.refl (colimit.cocone (parallelPair f g)).pt).hom =
    (Cofork.ofπ (coequalizer.π f g) ⋯).π

Tactic:
by

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
inst✝ : HasZeroMorphisms C
X Y : C
⊢ IsIso 0 → 𝟙 X = 0 ∧ 𝟙 Y = 0

Tactic:
by

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
inst✝ : HasZeroMorphisms C
X Y : C
h : 𝟙 X = 0 ∧ 𝟙 Y = 0
⊢ 0 ≫ 0 = 𝟙 X ∧ 0 ≫ 0 = 𝟙 Y

Tactic:
by

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
inst✝ : HasZeroMorphisms C
X Y : C
⊢ Function.LeftInverse ⋯ ⋯

Tactic:
by

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
inst✝ : HasZeroMorphisms C
X Y : C
⊢ Function.RightInverse ⋯ ⋯

Tactic:
by

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
inst✝ : HasZeroMorphisms C
X : C
⊢ IsIso 0 ≃ 𝟙 X = 0

Tactic:
by

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

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
h✝ : f = g
s : Cofork f g
m : (idCofork h✝).pt ⟶ s.pt
h : (idCofork h✝).π ≫ m = s.π
⊢ m = s.π

Tactic:
by

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
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }
⊢ ∀ (s : Cocone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C))
    (m : ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).pt ⟶ s.pt),
    (∀ (j : J),
        ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).ι.app j ≫ m = s.ι.app j) →
      m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }

Tactic:
intro s m w

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }
s : Cocone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)
m : ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).pt ⟶ s.pt
w : ∀ (j : J), ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).ι.app j ≫ m = s.ι.app j
⊢ m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f : X ⟶ Y
⊢ (isoTargetOfSelf f).hom = desc (𝟙 Y) ⋯

Tactic:
by

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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
⊢ G.map (equalizer.ι f g) ≫ G.map f = G.map (equalizer.ι f g) ≫ G.map g

Tactic:
simp only [← G.map_comp]

Goal state after:
C : Type u
X Y : C
inst✝³ : Category.{v, u} C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
⊢ G.map (equalizer.ι f g ≫ f) = G.map (equalizer.ι f g ≫ g)
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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
⊢ G.map (equalizer.ι f g) ≫ G.map f = G.map (equalizer.ι f g) ≫ G.map g

Tactic:
by

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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map h ≫ G.map f = G.map h ≫ G.map g

Tactic:
by

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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ G.map (equalizer.lift h w) ≫ equalizerComparison f g G = equalizer.lift (G.map h) ⋯

Tactic:
by

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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
⊢ G.map f ≫ G.map (coequalizer.π f g) = G.map g ≫ G.map (coequalizer.π f g)

Tactic:
simp only [← G.map_comp]

Goal state after:
C : Type u
X Y : C
inst✝³ : Category.{v, u} C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
⊢ G.map (f ≫ coequalizer.π f g) = G.map (g ≫ coequalizer.π f g)
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K✝ : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
K : J ⥤ C
c : Cocone K
h : IsColimit c
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (m : ((𝟭 C).mapCocone c).pt ⟶ s.pt),
    (∀ (j : J), ((𝟭 C).mapCocone c).ι.app j ≫ m = s.ι.app j) →
      m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }

Tactic:
by

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✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X : C
hX : IsZero X
⊢ IsZero (F.obj X)

Tactic:
by

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
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
⊢ G.map f ≫ G.map (coequalizer.π f g) = G.map g ≫ G.map (coequalizer.π f g)

Tactic:
by

Goal state after: