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 ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst✝ : Mono f
s : PullbackCone f f
⊢ s.fst ≫ 𝟙 X = s.snd

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst✝ : Mono f
s : PullbackCone f f
m : s.pt ⟶ X
m₁ : m ≫ 𝟙 X = s.fst
x✝ : m ≫ 𝟙 X = s.snd
⊢ m = s.fst

Tactic:
by

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

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Under (op X)
f : Z ⟶ Y
⊢ (Hom.right f).unop ≫ (unop (op (Over.mk Z.hom.unop))).hom = (unop (op (Over.mk Y.hom.unop))).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
g h : Z ⟶ X
eq : g ≫ f = h ≫ f
⊢ g = h

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : (Over X)ᵒᵖ
f : Z ⟶ Y
⊢ (mk (unop Z).hom.op).hom ≫ (Over.Hom.left f.unop).op = (mk (unop Y).hom.op).hom

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
hf : W₁.MapFactorizationData W₂ f
⊢ (hf.p.op ≫ hf.i.op).unop = f.op.unop

Tactic:
by

Goal state after:
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
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
W₁ W₂ : MorphismProperty Cᵒᵖ
X Y : Cᵒᵖ
f : X ⟶ Y
φ : W₁.MapFactorizationData W₂ f
⊢ φ.p.unop ≫ φ.i.unop = f.unop

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
⊢ W₁.comp W₂ = ⊤ ↔ W₁.HasFactorization W₂

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
f : Arrow C
⊢ data.i.app f ≫ data.p.app f = f.hom

Tactic:
by

Goal state after:
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.map (𝟙 j)) (f.right.map (𝟙 j)) ⋯) = 𝟙 (data.factorizationData (f.hom.app j)).Z

Tactic:
by

Goal state after:
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)
X✝ Y✝ Z✝ : J
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ data.mapZ (Arrow.homMk (f.left.map (x✝¹ ≫ x✝)) (f.right.map (x✝¹ ≫ x✝)) ⋯) =
    data.mapZ (Arrow.homMk (f.left.map x✝¹) (f.right.map x✝¹) ⋯) ≫
      data.mapZ (Arrow.homMk (f.left.map x✝) (f.right.map x✝) ⋯)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝ : Mono i
s✝ : PullbackCone f g
H : IsLimit s✝
s : PullbackCone (f ≫ i) (g ≫ i)
⊢ (s.fst ≫ f) ≫ i = (s.snd ≫ g) ≫ i

Tactic:
by

Goal state after:
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✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ { obj := fun j ↦ (data.factorizationData (X✝.hom.app j)).Z,
            map := fun {X Y} φ ↦ data.mapZ (Arrow.homMk (X✝.left.map φ) (X✝.right.map φ) ⋯), map_id := ⋯,
            map_comp := ⋯ }.map
        x✝ ≫
      data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯) ≫
      { obj := fun j ↦ (data.factorizationData (Y✝.hom.app j)).Z,
            map := fun {X Y} φ ↦ data.mapZ (Arrow.homMk (Y✝.left.map φ) (Y✝.right.map φ) ⋯), map_id := ⋯,
            map_comp := ⋯ }.map
        x✝

Tactic:
by

Goal state after:
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)
⊢ { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left (𝟙 f)).app j) ((Arrow.Hom.right (𝟙 f)).app j) ⋯),
      naturality := ⋯ } =
    𝟙
      { obj := fun j ↦ (data.factorizationData (f.hom.app j)).Z,
        map := fun {X Y} φ ↦ data.mapZ (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯), map_id := ⋯, map_comp := ⋯ }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝ : Mono i
s : PullbackCone f g
H : IsLimit s
⊢ IsLimit (mk s.fst s.snd ⋯)

Tactic:
by

Goal state after:
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✝
⊢ { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left (f ≫ g)).app j) ((Arrow.Hom.right (f ≫ g)).app j) ⋯),
      naturality := ⋯ } =
    { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯),
        naturality := ⋯ } ≫
      { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯),
        naturality := ⋯ }

Tactic:
by

Goal state after:
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
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ F.map (F.preimage (h.i ≫ (F.objObjPreimageIso h.Z).inv) ≫ F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p)) = F.map f

Tactic:
by

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✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasBinaryProduct X Y
W : C
i₁ i₂ : W ⟶ pullback f g
h : i₁ ≫ prod.lift (pullback.fst f g) (pullback.snd f g) = i₂ ≫ prod.lift (pullback.fst f g) (pullback.snd f g)
⊢ i₁ = i₂

Tactic:
by

Goal state after:
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
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ W₁.inverseImage F (F.preimage (h.i ≫ (F.objObjPreimageIso h.Z).inv))

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ W₂.inverseImage F (F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
⊢ IsIso (pullback.snd i (f ≫ i))

Tactic:
have := limit.isoLimitCone_hom_π ⟨_, pullbackIsPullbackOfCompMono (𝟙 _) f i⟩ WalkingCospan.right

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
this :
  (limit.isoLimitCone
          { cone := mk (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
            isLimit := pullbackIsPullbackOfCompMono (𝟙 Z) f i }).hom ≫
      { cone := mk (pullback.fst (𝟙 Z) f) (pullback.snd (𝟙 Z) f) ⋯,
                isLimit := pullbackIsPullbackOfCompMono (𝟙 Z) f i }.cone.π.app
        WalkingCospan.right =
    limit.π (cospan (𝟙 Z ≫ i) (f ≫ i)) WalkingCospan.right
⊢ IsIso (pullback.snd i (f ≫ i))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
⊢ IsIso (pullback.snd i (f ≫ i))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
i : Z ⟶ W
inst✝ : Mono i
⊢ IsIso (pullback.fst (f ≫ i) i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (pullbackSymmetry f f).hom = 𝟙 (pullback f f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsLimit.lift ht (𝟙 X) (𝟙 X) ⋯ ≫ t.fst = 𝟙 X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsIso t.fst

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
inst✝ : Epi f
W : C
h k : t.pt ⟶ W
i : t.inr ≫ h = t.inr ≫ k
⊢ t.inl ≫ h = t.inl ≫ k

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
ht : IsColimit t
inst✝ : Epi g
W : C
h k : t.pt ⟶ W
i : t.inl ≫ h = t.inl ≫ k
⊢ t.inr ≫ h = t.inr ≫ k

Tactic:
by

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
inst✝ : Epi f
s : PushoutCocone f f
⊢ 𝟙 Y ≫ s.inl = s.inr

Tactic:
by

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
inst✝ : Epi f
s : PushoutCocone f f
m : Y ⟶ s.pt
m₁ : 𝟙 Y ≫ m = s.inl
x✝ : 𝟙 Y ≫ m = s.inr
⊢ m = s.inl

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
g h : Y ⟶ Z
eq : f ≫ g = f ≫ h
⊢ g = h

Tactic:
by

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

Goal state before:
pp: j : WalkingParallelPair
⊢ (𝟭 WalkingParallelPair).obj j = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j

Tactic:
by

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

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

Goal state before:
pp: ⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    (𝟭 WalkingParallelPair).map f ≫ (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map f

Tactic:
by

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
⊢ h ≫ y ≫ s.inr = g ≫ s.inr

Tactic:
by

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

Goal state before:
pp: j : WalkingParallelPairᵒᵖ
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j = (𝟭 WalkingParallelPairᵒᵖ).obj j

Tactic:
by

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
⊢ h ≫ x ≫ s.inl = h ≫ y ≫ s.inr

Tactic:
by

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
⊢ f ≫ t.inl = g ≫ t.inr

Tactic:
by

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
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : (mk s.inl s.inr ⋯).inl ≫ m✝ = t.inl
hr' : (mk s.inl s.inr ⋯).inr ≫ m✝ = t.inr
⊢ m✝ = hs.desc (mk t.inl t.inr ⋯)

Tactic:
by

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

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

Tactic:
by

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✝
s : PushoutCocone (h ≫ f) (h ≫ g)
⊢ h ≫ f ≫ s.inl = h ≫ g ≫ s.inr

Tactic:
by

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

Goal state before:
pp: j : WalkingParallelPair
⊢ walkingParallelPairOp.map ((NatIso.ofComponents (fun j ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app j) ≫
      (NatIso.ofComponents (fun j ↦ eqToIso ⋯) ⋯).hom.app (walkingParallelPairOp.obj j) =
    𝟙 (walkingParallelPairOp.obj j)

Tactic:
by

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
⊢ η = η'

Tactic:
by

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
g : CostructuredArrow S T
f : g.left ⟶ f✝.left
w : (fun η ↦ S.map η ≫ f✝.hom = g.hom) f
⊢ S.map f ≫ f✝.hom = S.map (h.lift g) ≫ f✝.hom

Tactic:
by

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
F : C ⥤ D
d : D
X✝ Y✝ : (StructuredArrow d F)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ F.op.map (Hom.right f.unop).op ≫ (CostructuredArrow.mk (unop Y✝).hom.op).hom =
    (CostructuredArrow.mk (unop X✝).hom.op).hom

Tactic:
by

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

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
F : C ⥤ D
d : D
X✝ Y✝ : (StructuredArrow (op d) F.op)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (F.map (Hom.right f.unop).unop ≫ (CostructuredArrow.mk (unop Y✝).hom.unop).hom).op =
    (CostructuredArrow.mk (unop X✝).hom.unop).hom.op

Tactic:
by

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
F : C ⥤ D
d : D
X✝ Y✝ : (CostructuredArrow F d)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (StructuredArrow.mk (unop X✝).hom.op).hom ≫ F.op.map f.unop.left.op = (StructuredArrow.mk (unop Y✝).hom.op).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
⊢ ∀ {X_1 Y_1 Z : WalkingParallelPair} (f_1 : X_1 ⟶ Y_1) (g_1 : Y_1 ⟶ Z),
    parallelPairHom f g (f_1 ≫ g_1) = parallelPairHom f g f_1 ≫ parallelPairHom f g g_1

Tactic:
by

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
F : C ⥤ D
d : D
X✝ Y✝ : (CostructuredArrow F.op (op d))ᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((StructuredArrow.mk (unop X✝).hom.unop).hom ≫ F.map f.unop.left.unop).op =
    (StructuredArrow.mk (unop Y✝).hom.unop).hom.op

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
by

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✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasBinaryCoproduct Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h : coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁ = coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂
⊢ i₁ = i₂

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

Tactic:
by

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

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

Tactic:
by

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
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).op =
    (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).op

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 : WalkingParallelPair ⥤ C
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map f

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
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 :
  { I := I✝, m := Fm, m_mono := m_mono✝¹, e := e✝¹, fac := Ffac }.m =
    eqToHom ⋯ ≫ { I := I✝, m := Fm', m_mono := m_mono✝, e := e✝, fac := Ffac' }.m
⊢ Fm = Fm'

Tactic:
by

Goal state after: