mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ data.mapZ (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) ⋯) = data.mapZ (𝟙 (Arrow.mk (f.hom.app j)))

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ data.mapZ (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) ⋯) = data.mapZ (𝟙 (Arrow.mk (f.hom.app j)))
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ Z✝ : Arrow (J ⥤ C)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
j : J
⊢ data.mapZ
      (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
        ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) ⋯) =
    data.mapZ
      (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯)

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ Z✝ : Arrow (J ⥤ C)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
j : J
⊢ data.mapZ
      (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
        ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) ⋯) =
    data.mapZ
      (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯)
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 = pullback.snd f g ≫ g

Tactic:
]

Goal state after:
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 = pullback.snd f g ≫ g
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 ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst✝ : Epi f
s : PushoutCocone f f
⊢ f ≫ s.inr = f ≫ s.inr

Tactic:
]

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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
⊢ (h ≫ x) ≫ s.inl = f ≫ s.inl

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
⊢ (h ≫ x) ≫ s.inl = f ≫ s.inl
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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
⊢ (h ≫ y) ≫ s.inr = g ≫ s.inr

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
⊢ (h ≫ y) ≫ s.inr = g ≫ s.inr
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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
⊢ h ≫ y ≫ s.inr = g ≫ s.inr

Tactic:
by
      rw [← Category.assoc]; apply congrArg (· ≫ inr s) hhy

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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
reassoc₁ : h ≫ x ≫ s.inl = f ≫ s.inl
reassoc₂ : h ≫ y ≫ s.inr = g ≫ s.inr
⊢ g ≫ s.inr = g ≫ s.inr

Tactic:
]

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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
⊢ h ≫ y ≫ t.inr = h ≫ y ≫ t.inr

Tactic:
]

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

Goal state before:
pp: case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op

Tactic:
]

Goal state after:
case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op
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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s : PushoutCocone f g
H : IsColimit s
⊢ h ≫ g ≫ s.inr = h ≫ g ≫ s.inr

Tactic:
]

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 : D
S : C ⥤ D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
⊢ h.lift (mk (S.map η' ≫ f.hom)) = h.lift (mk (S.map η' ≫ f.hom))

Tactic:
]

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 ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s : PushoutCocone f g
H : IsColimit s
⊢ IsColimit (mk s.inl s.inr ⋯)

Tactic:
apply PushoutCocone.isColimitAux'
  intro s
  rcases PushoutCocone.IsColimit.desc' H s.inl s.inr
      ((cancel_epi h).mp (by simpa using s.condition)) with
    ⟨l, h₁, h₂⟩
  refine ⟨l, h₁, h₂, ?_⟩
  intro m hm₁ hm₂
  exact (PushoutCocone.IsColimit.hom_ext H (hm₁.trans h₁.symm) (hm₂.trans h₂.symm) :)

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 ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝¹ : Epi h
inst✝ : HasPushout f g
⊢ f ≫ pushout.inl f g = g ≫ pushout.inr f g

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝¹ : Epi h
inst✝ : HasPushout f g
⊢ f ≫ pushout.inl f g = g ≫ pushout.inr f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: case e_e
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ f = e✝ ≫ Fm

Tactic:
hm,

Goal state after:
case e_e
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ f = e✝ ≫ Fm'
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: case e_e
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ f = f

Tactic:
]

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 : MonoFactorisation f
m : F.I ⟶ Y
e : X ⟶ F.I
hm : m = F.m
he : e = F.e
⊢ Mono F.m

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : MonoFactorisation f
m : F.I ⟶ Y
e : X ⟶ F.I
hm : m = F.m
he : e = F.e
⊢ Mono F.m
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✝ : Mono f
⊢ image.ι f = image.ι f

Tactic:
]

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
e : E
f : StructuredArrow e G
X✝ Y✝ : StructuredArrow f (pre e F G)
φ : X✝ ⟶ Y✝
⊢ (mk (Hom.right X✝.hom)).hom ≫ F.map (Hom.right (Hom.right φ)) =
    (mk (Hom.right X✝.hom ≫ Hom.right ((pre e F G).map (Hom.right φ)))).hom

Tactic:
]

Goal state after:
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
e : E
f : StructuredArrow e G
X✝ Y✝ : StructuredArrow f (pre e F G)
φ : X✝ ⟶ Y✝
⊢ (mk (Hom.right X✝.hom)).hom ≫ F.map (Hom.right (Hom.right φ)) =
    (mk (Hom.right X✝.hom ≫ Hom.right ((pre e F G).map (Hom.right φ)))).hom
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'
t₀ : v ≫ q ≫ ι f = ι f
⊢ v ≫ q ≫ ι f = v ≫ q ≫ ι f

Tactic:
]

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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
e : E
f : CostructuredArrow G e
X✝ Y✝ : CostructuredArrow (pre F G e) f
φ : X✝ ⟶ Y✝
⊢ F.map φ.left.left ≫ (mk Y✝.hom.left).hom = (mk (((pre F G e).map φ.left).left ≫ Y✝.hom.left)).hom

Tactic:
]

Goal state after:
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
e : E
f : CostructuredArrow G e
X✝ Y✝ : CostructuredArrow (pre F G e) f
φ : X✝ ⟶ Y✝
⊢ F.map φ.left.left ≫ (mk Y✝.hom.left).hom = (mk (((pre F G e).map φ.left).left ≫ Y✝.hom.left)).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ e.inv ≫ f = e.inv ≫ default

Tactic:
]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ e.inv ≫ f = e.inv ≫ default
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f ≫ e.hom = default ≫ e.hom

Tactic:
]

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : Z ⟶ X
⊢ f ≫ e.hom = default ≫ e.hom
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'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ g = g

Tactic:
]

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 : Fork f g
⊢ s.π.app zero ≫ f = s.π.app zero ≫ f

Tactic:
]

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'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ v ≫ q ≫ g = v ≫ q ≫ g

Tactic:
]

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 : Fork f g
⊢ s.π.app zero ≫ g = s.π.app zero ≫ g

Tactic:
]

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
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
X✝ Y✝ : CostructuredArrow (snd L R) b
f : X✝ ⟶ Y✝
⊢ X✝.left.hom ≫ R.map X✝.hom = X✝.left.hom ≫ R.map X✝.hom

Tactic:
]

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 : Cofork f g
⊢ f ≫ s.ι.app one = f ≫ s.ι.app one

Tactic:
]

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'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ v ≫ equalizer.ι g h ≫ h = v ≫ q ≫ h

Tactic:
]

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 : Cofork f g
⊢ g ≫ s.ι.app one = g ≫ s.ι.app one

Tactic:
]

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'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ 𝟙 (image f) ≫ h = 𝟙 (image f) ≫ h

Tactic:
]

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'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ h = h

Tactic:
]

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
E : Epi (factorThruImage f ≫ image.ι f)
⊢ Epi (image.ι f)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi (factorThruImage f ≫ image.ι f)
⊢ Epi (image.ι f)
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
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi (factorThruImage f ≫ image.ι f)

Tactic:
]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi (factorThruImage f ≫ image.ι f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ ι f' = f'

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ ι f' = f'
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
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) = ι (f ≫ g ≫ h)

Tactic:
]

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✝¹ : IsIso f
inst✝ : HasImage g
F' : MonoFactorisation (f ≫ g)
this : (MonoFactorisation.ofIsoComp f F').m = F'.m
⊢ image.ι g = image.ι g

Tactic:
]

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
t : Fork f g
⊢ t.π.app one = t.π.app one

Tactic:
]

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
t : Cofork f g
⊢ t.ι.app zero = t.ι.app zero

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
M : SemimoduleCat R
inst✝ : Subsingleton ↑M
X : SemimoduleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = (Hom.hom default) 0

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : Semiring R
M : SemimoduleCat R
inst✝ : Subsingleton ↑M
X : SemimoduleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = (Hom.hom default) 0
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
F' : MonoFactorisation (f ≫ g)
⊢ ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) ≫ g = ((Image.monoFactorisation f).compMono g).m

Tactic:
]

Goal state after:
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
F' : MonoFactorisation (f ≫ g)
⊢ ((image.lift F'.ofCompIso ≫ F'.m) ≫ inv g) ≫ g = ((Image.monoFactorisation f).compMono g).m
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 : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
this : k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
⊢ l ≫ s.ι ≫ f = l ≫ s.ι ≫ f

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : SemimoduleCat R
h : IsZero M
x : ↑M
⊢ (Hom.hom (𝟙 M)) x = 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : Semiring R
M : SemimoduleCat R
h : IsZero M
x : ↑M
⊢ (Hom.hom (𝟙 M)) x = 0
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Semiring S
inst✝ : Algebra S₀ S
M N : SemimoduleCat S
x✝² : S₀
x✝¹ : S
x✝ : ↑M
⊢ (algebraMap S₀ S) x✝² • x✝¹ • x✝ = x✝² • x✝¹ • x✝

Tactic:
]

Goal state after:
R : Type u
inst✝³ : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Semiring S
inst✝ : Algebra S₀ S
M N : SemimoduleCat S
x✝² : S₀
x✝¹ : S
x✝ : ↑M
⊢ (algebraMap S₀ S) x✝² • x✝¹ • x✝ = x✝² • x✝¹ • x✝
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Semiring S
inst✝ : Algebra S₀ S
M N : SemimoduleCat S
s : S
s₀ : S₀
n : ↑M
⊢ (algebraMap S₀ S) s₀ • s • n = (algebraMap S₀ S) s₀ • s • n

Tactic:
]

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
F' : MonoFactorisation (f ≫ g)
this : (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = image.lift F'.ofCompIso ≫ F'.ofCompIso.m
⊢ image.ι f = image.ι f

Tactic:
]

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
that : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero ≫ Zero.zero = Zero.zero ≫ Zero.zero

Tactic:
]

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.ι f.hom = image.ι f.hom

Tactic:
]

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
h : f = 0
⊢ f = 0

Tactic:
]

Goal state after:
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
h : f = 0
⊢ f = 0
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
h : g = 0
⊢ g = 0

Tactic:
]

Goal state after:
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
h : g = 0
⊢ g = 0
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
⊢ image.ι f.hom ≫ Arrow.Hom.right sq1 ≫ Arrow.Hom.right sq2 = image.ι f.hom ≫ Arrow.Hom.right sq1 ≫ Arrow.Hom.right sq2

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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
⊢ image.ι f.hom ≫ Arrow.Hom.right sq = image.ι f.hom ≫ Arrow.Hom.right sq

Tactic:
]

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

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default