mathlib-initiative/mathlib-tactics huggingface dataset:
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.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F' : MonoFactorisation f
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝ : Mono Fm
e✝ : X ⟶ I✝
Ffac : e✝ ≫ Fm = f
hI : { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac }.I = F'.I
hm : { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac }.m = eqToHom hI ≫ F'.m
⊢ { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac } = F'

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F' : MonoFactorisation f
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝ : Mono Fm
e✝ : X ⟶ I✝
Ffac : e✝ ≫ Fm = f
hI : { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac }.I = F'.I
hm : { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac }.m = eqToHom hI ≫ F'.m
⊢ { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac } = F'
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
F : C ⥤ D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ StructuredArrow.Hom.right
      ((𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫
          (StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk y))).right) ⋯).op.hom).unop =
    StructuredArrow.Hom.right
      ((StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk x))).right) ⋯).op.hom ≫
          (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f).unop

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ StructuredArrow.Hom.right
      ((𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫
          (StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk y))).right) ⋯).op.hom).unop =
    StructuredArrow.Hom.right
      ((StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk x))).right) ⋯).op.hom ≫
          (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f).unop
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
⊢ h ≫ f ≫ pushout.inl f g = h ≫ 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
⊢ h ≫ f ≫ pushout.inl f g = h ≫ g ≫ pushout.inr f 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
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.Equalizers

Goal state before:
pp: case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.obj zero ⟶ G.obj zero

pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.obj one ⟶ G.obj one

Tactic:
;

Goal state after:
case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.obj zero ⟶ G.obj zero

case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.obj one ⟶ G.obj one
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.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.map left ≫ WalkingParallelPair.casesOn one p q = WalkingParallelPair.casesOn zero p q ≫ G.map left

pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.map right ≫ WalkingParallelPair.casesOn one p q = WalkingParallelPair.casesOn zero p q ≫ G.map right

pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ WalkingParallelPair.casesOn X✝ p q =
    WalkingParallelPair.casesOn X✝ p q ≫ G.map (WalkingParallelPairHom.id X✝)

Tactic:
;

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.map left ≫ WalkingParallelPair.casesOn one p q = WalkingParallelPair.casesOn zero p q ≫ G.map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ F.map right ≫ WalkingParallelPair.casesOn one p q = WalkingParallelPair.casesOn zero p q ≫ G.map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ WalkingParallelPair.casesOn X✝ p q =
    WalkingParallelPair.casesOn X✝ p q ≫ G.map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.obj zero ≅ G.obj zero

pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.obj one ≅ G.obj one

Tactic:
;

Goal state after:
case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.obj zero ≅ G.obj zero

case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.obj one ≅ G.obj one
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
F : C ⥤ D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
⊢ ((𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫
          (CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk y))).left) ⋯).op.hom).unop.left =
    ((CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk x))).left) ⋯).op.hom ≫
          (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map
            f).unop.left

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
⊢ ((𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫
          (CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk y))).left) ⋯).op.hom).unop.left =
    ((CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk x))).left) ⋯).op.hom ≫
          (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map
            f).unop.left
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.map left ≫ (WalkingParallelPair.casesOn one p q).hom = (WalkingParallelPair.casesOn zero p q).hom ≫ G.map left

pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.map right ≫ (WalkingParallelPair.casesOn one p q).hom = (WalkingParallelPair.casesOn zero p q).hom ≫ G.map right

pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (WalkingParallelPair.casesOn X✝ p q).hom =
    (WalkingParallelPair.casesOn X✝ p q).hom ≫ G.map (WalkingParallelPairHom.id X✝)

Tactic:
;

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.map left ≫ (WalkingParallelPair.casesOn one p q).hom = (WalkingParallelPair.casesOn zero p q).hom ≫ G.map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ F.map right ≫ (WalkingParallelPair.casesOn one p q).hom = (WalkingParallelPair.casesOn zero p q).hom ≫ G.map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (WalkingParallelPair.casesOn X✝ p q).hom =
    (WalkingParallelPair.casesOn X✝ p q).hom ≫ G.map (WalkingParallelPairHom.id X✝)
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
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ (prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
      (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom =
    (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
      (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ (prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
      (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom =
    (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
      (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).1 =
    Hom.right
      ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝).1

pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).2 =
    Hom.right
      ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝).2

Tactic:
;

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).1 =
    Hom.right
      ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝).1

case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).2 =
    Hom.right
      ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝).2
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
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ (prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
      (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom =
    (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
      (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ (prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
      (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom =
    (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
      (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).1.left =
    ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝).1.left

pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).2.left =
    ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝).2.left

Tactic:
;

Goal state after:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).1.left =
    ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝).1.left

case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
          (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom).2.left =
    ((Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
          (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝).2.left
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.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: case mk
R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
g : M.Hom N
hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝ }.hom = g.hom
⊢ { hom' := hom'✝ } = g

Tactic:
;

Goal state after:
case mk
R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
g : M.Hom N
hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝ }.hom = g.hom
⊢ { hom' := hom'✝ } = g
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: case mk.mk
R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
hom'✝¹ hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝¹ }.hom = { hom' := hom'✝ }.hom
⊢ { hom' := hom'✝¹ } = { hom' := hom'✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
hom'✝¹ hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝¹ }.hom = { hom' := hom'✝ }.hom
⊢ { hom' := hom'✝¹ } = { hom' := hom'✝ }
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.ι
⊢ (k ≫ s.ι) ≫ f = (l ≫ s.ι) ≫ f

Tactic:
;

Goal state after:
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.ι
⊢ (k ≫ s.ι) ≫ f = (l ≫ s.ι) ≫ f
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₁)
⊢ (Hom.hom (↟↑e ≫ ↟↑e.symm)) x✝ = (Hom.hom (𝟙 (of R X₁))) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₁)
⊢ (Hom.hom (↟↑e ≫ ↟↑e.symm)) x✝ = (Hom.hom (𝟙 (of R X₁))) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₂)
⊢ (Hom.hom (↟↑e.symm ≫ ↟↑e)) x✝ = (Hom.hom (𝟙 (of R X₂))) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
X₁ X₂ : Type v
g₁ : AddCommMonoid X₁
g₂ : AddCommMonoid X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
x✝ : ↑(of R X₂)
⊢ (Hom.hom (↟↑e.symm ≫ ↟↑e)) x✝ = (Hom.hom (𝟙 (of R 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
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.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
⊢ ∀ (a b : PreservesLimit K F), a = b

Tactic:
;

Goal state after:
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
⊢ ∀ (a b : PreservesLimit K F), a = b