mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (X Y : Discrete PEmpty.{?u.10 + 1}) → Zero (X ⟶ Y)

Tactic:
by

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
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ (compIso f g).inv ≫ ι f = ι (f ≫ g) ≫ inv 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
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    ((Functor.const WalkingParallelPair).obj t.pt).map f ≫ t.π.app Y ≫ eqToHom ⋯ = (t.π.app X ≫ eqToHom ⋯) ≫ F.map f

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
X Y : Discrete PUnit.{?u.10 + 1}
⊢ Zero (X ⟶ Y)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : HasImage f.hom
⊢ 𝟙 (image f.hom) ≫ image.ι f.hom = image.ι f.hom ≫ Arrow.Hom.right (𝟙 f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
⊢ zero = zero

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 : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
X : WalkingParallelPair
⊢ F.obj X = (parallelPair (F.map left) (F.map right)).obj X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
m : ImageMap sq
⊢ (factorThruImage f.hom ≫ m.map) ≫ image.ι g.hom = (Arrow.Hom.left sq ≫ factorThruImage g.hom) ≫ image.ι g.hom

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✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesLimit K F)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
F : MonoFactorisation f.hom
F' : MonoFactorisation g.hom
hF' : IsImage F'
map : F.I ⟶ F'.I
map_ι : map ≫ F'.m = F.m ≫ Arrow.Hom.right sq
⊢ (image.lift F ≫ map ≫ hF'.lift (Image.monoFactorisation g.hom)) ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq

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✝ K : J ⥤ C
F : C ⥤ D
⊢ Subsingleton (PreservesColimit K F)

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
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (PreservesLimitsOfShape J 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 g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    F.map f ≫ eqToHom ⋯ ≫ t.ι.app Y = (eqToHom ⋯ ≫ t.ι.app X) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map 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 g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
⊢ I = J

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
inst✝ : Category.{w', w} J
F : C ⥤ D
⊢ Subsingleton (PreservesColimitsOfShape J 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 g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
j : WalkingParallelPair
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
⊢ Zero.zero ≫ Zero.zero = Zero.zero

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 : WalkingParallelPair ⥤ C
t : Cone F
X : WalkingParallelPair
⊢ F.obj X = (parallelPair (F.map left) (F.map right)).obj X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero ≫ Zero.zero = Zero.zero

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
F : C ⥤ D
⊢ Subsingleton (PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
⊢ I = J

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
F : C ⥤ D
⊢ Subsingleton (PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq

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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Mono g
h : f ≫ g = 0
⊢ f = 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
F : WalkingParallelPair ⥤ C
t : Cone F
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    ((Functor.const WalkingParallelPair).obj t.pt).map f ≫ t.π.app Y ≫ eqToHom ⋯ =
      (t.π.app X ≫ eqToHom ⋯) ≫ (parallelPair (F.map left) (F.map right)).map 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 g : X✝ ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cocone F
X : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj X = F.obj 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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi f
h : f ≫ g = 0
⊢ g = 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✝¹ : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi f
⊢ g = 0 → f ≫ g = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
f g h : Arrow C
inst✝⁴ : HasImage f.hom
inst✝³ : HasImage g.hom
inst✝² : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst✝¹ : HasImageMap sq1
inst✝ : HasImageMap sq2
⊢ ((imageMap sq1).map ≫ (imageMap sq2).map) ≫ image.ι h.hom = image.ι f.hom ≫ Arrow.Hom.right (sq1 ≫ sq2)

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✝ : HasImage f
w : image.ι f = 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
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
H : C ⥤ D
⊢ η ≫ 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
F : WalkingParallelPair ⥤ C
t : Cocone F
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    (parallelPair (F.map left) (F.map right)).map f ≫ eqToHom ⋯ ≫ t.ι.app Y =
      (eqToHom ⋯ ≫ t.ι.app X) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map 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 g : X ⟶ Y
F : WalkingParallelPair ⥤ C
t : Cone F
j : WalkingParallelPair
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj 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✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
⊢ 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
F : WalkingParallelPair ⥤ C
t : Cocone F
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
⊢ map ≫ image.ι g.hom = map' ≫ image.ι g.hom

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
s t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ ∀ (j : WalkingParallelPair), k ≫ t.π.app j = 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✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default

Tactic:
simp only

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq
⊢ map = map'

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 : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ f = default

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
F G : ImageMap sq
⊢ F.map = G.map

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
s t : Fork f g
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
⊢ i.inv ≫ s.ι = t.ι

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : HasImageMap sq
⊢ factorThruImage f.hom ≫ map sq = Arrow.Hom.left sq ≫ factorThruImage g.hom

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
P : C
ι ι' : P ⟶ X
w : ι ≫ f = ι ≫ g
w' : ι' ≫ f = ι' ≫ g
h : ι = ι'
⊢ (Iso.refl (Fork.ofι ι w).pt).hom ≫ (Fork.ofι ι' w').ι = (Fork.ofι ι w).ι

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : HasImageMap sq
⊢ map sq ≫ ι g.hom = ι f.hom ≫ Arrow.Hom.right sq

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)) (j : J),
    h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } } ≫ ((𝟭 C).mapCone c).π.app j = s.π.app j

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
f' g' : X' ⟶ Y'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
⊢ (parallelPair f g).map left ≫ e₁.hom = e₀.hom ≫ (parallelPair f' g').map left

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 : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ 0 = default

Tactic:
simp only

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 : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ f = default

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
f' g' : X' ⟶ Y'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
⊢ (parallelPair f g).map right ≫ e₁.hom = e₀.hom ≫ (parallelPair f' g').map right

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

Tactic:
by

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✝ : StrongEpi f
⊢ f ≫ 𝟙 Y = 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✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ 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
h : f = 0
⊢ IsZero Y

Tactic:
by

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 : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi F'.e

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
s t : Cofork f g
k : s.pt ⟶ t.pt
w : s.π ≫ k = t.π
⊢ ∀ (j : WalkingParallelPair), s.ι.app j ≫ k = t.ι.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ factorThruImage f ≫
      image.lift
          { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
            e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ } ≫
        pullback.fst h y =
    x

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ (image.lift
          { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
            e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ } ≫
        pullback.fst h y) ≫
      h =
    y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ (isoStrongEpiMono e m comm).hom ≫ ι f = m

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
s t : Fork f✝ g
f : s ⟶ t
⊢ f.hom ≫ t.ι = s.ι

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✝ : IsSplitMono f
⊢ IsZero X ↔ f = 0

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) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }
⊢ ∀ (s : Cone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C))
    (m : s.pt ⟶ ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).pt),
    (∀ (j : J),
        m ≫ ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).π.app j = s.π.app j) →
      m = h.lift { 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) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }
s : Cone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)
m : s.pt ⟶ ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).pt
w : ∀ (j : J), m ≫ ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).π.app j = s.π.app j
⊢ m = h.lift { 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✝ g : X ⟶ Y
s t : Cofork f✝ g
f : s ⟶ t
⊢ s.π ≫ f.hom = t.π

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this✝ : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
this : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)
⊢ (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) ≫ F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y = f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation 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 g : X ⟶ Y
s t : Cofork f g
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π ≫ i.inv = 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
P : C
π π' : Y ⟶ P
w : f ≫ π = g ≫ π
w' : f ≫ π' = g ≫ π'
h : π = π'
⊢ (Cofork.ofπ π w).π ≫ (Iso.refl (Cofork.ofπ π w).pt).hom = (Cofork.ofπ π' w').π

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✝ : IsSplitEpi f
⊢ IsZero Y ↔ 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✝¹ : PreservesLimit (Functor.empty C) G
inst✝ : ReflectsLimit (Functor.empty C) G
X : C
⊢ Function.LeftInverse (isTerminalOfObj G X) (isTerminalObj 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✝¹ : PreservesLimit (Functor.empty C) G
inst✝ : ReflectsLimit (Functor.empty C) G
X : C
⊢ Function.RightInverse (isTerminalOfObj G X) (isTerminalObj G X)

Tactic:
by

Goal state after: