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

Goal state before:
pp: case e_u
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
⊢ f.left.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).left

Tactic:
simp

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

Goal state before:
pp: case e_v
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
⊢ f.right.map (𝟙 j) = 𝟙 (Arrow.mk (f.hom.app j)).right

Tactic:
simp

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

Goal state before:
pp: case e_u
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✝
⊢ f.left.map (x✝¹ ≫ x✝) =
    (Arrow.homMk (f.left.map x✝¹) (f.right.map x✝¹) ⋯).left ≫ (Arrow.homMk (f.left.map x✝) (f.right.map x✝) ⋯).left

Tactic:
simp

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

Goal state before:
pp: case e_v
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✝
⊢ f.right.map (x✝¹ ≫ x✝) =
    (Arrow.homMk (f.left.map x✝¹) (f.right.map x✝¹) ⋯).right ≫ (Arrow.homMk (f.left.map x✝) (f.right.map x✝) ⋯).right

Tactic:
simp

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

Goal state before:
pp: case h₁
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✝¹
⊢ Arrow.Hom.left
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    Arrow.Hom.left
      (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
        Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)

Tactic:
simp

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

Goal state before:
pp: case h₂
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✝¹
⊢ Arrow.Hom.right
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    Arrow.Hom.right
      (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
        Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)

Tactic:
simp

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

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
    refine (W₁.arrow_mk_iso_iff ?_).1 h.hi
    refine Arrow.isoMk (Iso.refl _) (F.objObjPreimageIso h.Z).symm ?_
    simp [F.map_preimage]

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
  simpa only [Category.id_comp] using hasPullback_of_comp_mono (𝟙 Z) f i

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

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

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

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

Tactic:
simp

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

Goal state before:
pp: case left
⊢ (𝟭 WalkingParallelPair).map left ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map left

Tactic:
simp

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

Goal state before:
pp: case right
⊢ (𝟭 WalkingParallelPair).map right ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map right

Tactic:
simp

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

Goal state before:
pp: case id
X✝ : WalkingParallelPair
⊢ (𝟭 WalkingParallelPair).map (WalkingParallelPairHom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).map (WalkingParallelPairHom.id X✝)

Tactic:
simp

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

Goal state before:
pp: case h₁
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
⊢ s.inr ≫ m✝ = s.inr ≫ hs.desc (mk t.inl t.inr ⋯)

Tactic:
· simp only [PushoutCocone.mk_inl, PushoutCocone.mk_inr] at hr hr' ⊢
          simp only [hr']
          symm
          exact hs.fac _ WalkingSpan.right

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

Goal state before:
pp: case left.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (left ≫ WalkingParallelPairHom.id one) =
    parallelPairHom f g left ≫ parallelPairHom f g (WalkingParallelPairHom.id one)

Tactic:
simp

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

Goal state before:
pp: case right.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (right ≫ WalkingParallelPairHom.id one) =
    parallelPairHom f g right ≫ parallelPairHom f g (WalkingParallelPairHom.id one)

Tactic:
simp

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

Goal state before:
pp: case id.left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (WalkingParallelPairHom.id zero ≫ left) =
    parallelPairHom f g (WalkingParallelPairHom.id zero) ≫ parallelPairHom f g left

Tactic:
simp

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

Goal state before:
pp: case id.right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (WalkingParallelPairHom.id zero ≫ right) =
    parallelPairHom f g (WalkingParallelPairHom.id zero) ≫ parallelPairHom f g right

Tactic:
simp

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

Goal state before:
pp: case id.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
X✝ : WalkingParallelPair
⊢ parallelPairHom f g (WalkingParallelPairHom.id X✝ ≫ WalkingParallelPairHom.id X✝) =
    parallelPairHom f g (WalkingParallelPairHom.id X✝) ≫ parallelPairHom f g (WalkingParallelPairHom.id X✝)

Tactic:
simp

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

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

Goal state before:
pp: case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.map left ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map left

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
⊢ F.map right ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map right

Tactic:
simp

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

Goal state before:
pp: case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
X✝ : WalkingParallelPair
⊢ F.map (WalkingParallelPairHom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (parallelPair (F.map left) (F.map right)).map (WalkingParallelPairHom.id X✝)

Tactic:
simp

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
hF : IsImage F
F' : MonoFactorisation f
⊢ (F.e ≫ hF.lift F') ≫ F'.m = F'.e ≫ F'.m

Tactic:
simp

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 F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.lift F' ≫ hF'.lift F) ≫ F.m = 𝟙 F.I ≫ F.m

Tactic:
simp

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 F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF'.lift F ≫ hF.lift F') ≫ F'.m = 𝟙 F'.I ≫ F'.m

Tactic:
simp

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 F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.isoExt hF').hom ≫ F'.m = F.m

Tactic:
simp

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 F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (hF.isoExt hF').inv ≫ F.m = F'.m

Tactic:
simp

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 F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ F.e ≫ (hF.isoExt hF').hom = F'.e

Tactic:
simp

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 F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ F'.e ≫ (hF.isoExt hF').inv = F.e

Tactic:
simp

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✝ : Mono f
⊢ (imageMonoIsoSource f).inv ≫ image.ι f = f

Tactic:
simp [imageMonoIsoSource]

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✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ f ≫ 𝟙 Y = f ≫ 𝟙 Y

Tactic:
simp

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✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ = 𝟙 Y

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
t : PushoutCocone f f
ht : IsColimit t
⊢ t.inl ≫ IsColimit.desc ht (𝟙 Y) (𝟙 Y) ⋯ ≫ t.inl = t.inl ≫ 𝟙 t.pt

Tactic:
simp

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

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 : StructuredArrow f (pre e F G)
⊢ ((𝟭 (StructuredArrow f (pre e F G))).obj X).right.hom ≫
      (F ⋙ G).map (Iso.refl ((𝟭 (StructuredArrow f (pre e F G))).obj X).right.right).hom =
    ((preEquivalenceFunctor F f ⋙ preEquivalenceInverse F f).obj X).right.hom

Tactic:
simp

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

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 : CostructuredArrow (pre F G e) f
⊢ (F ⋙ G).map (Iso.refl ((𝟭 (CostructuredArrow (pre F G e) f)).obj X).left.left).hom ≫
      ((preEquivalence.functor F f ⋙ preEquivalence.inverse F f).obj X).left.hom =
    ((𝟭 (CostructuredArrow (pre F G e) f)).obj X).left.hom

Tactic:
simp

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
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, S') (T.prod T')
η : X✝ ⟶ Y✝
⊢ (mk X✝.hom.1, mk X✝.hom.2).1.hom ≫ T.map (Hom.right η).1 = (mk Y✝.hom.1, mk Y✝.hom.2).1.hom

Tactic:
simp

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
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, S') (T.prod T')
η : X✝ ⟶ Y✝
⊢ (mk X✝.hom.1, mk X✝.hom.2).2.hom ≫ T'.map (Hom.right η).2 = (mk Y✝.hom.1, mk Y✝.hom.2).2.hom

Tactic:
simp

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
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'
η : X✝ ⟶ Y✝
⊢ (mk (X✝.1.hom, X✝.2.hom)).hom ≫ (T.prod T').map (Hom.right η.1, Hom.right η.2) = (mk (Y✝.1.hom, Y✝.2.hom)).hom

Tactic:
simp

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
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, S') (T.prod T')} (f : X ⟶ Y),
    (𝟭 (StructuredArrow (S, S') (T.prod T'))).map f ≫ (Iso.refl ((𝟭 (StructuredArrow (S, S') (T.prod T'))).obj Y)).hom =
      (Iso.refl ((𝟭 (StructuredArrow (S, S') (T.prod T'))).obj X)).hom ≫
        (prodFunctor S S' T T' ⋙ prodInverse S S' T T').map f

Tactic:
simp

Goal state after:
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

Tactic:
simp

Goal state after:
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).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:
simp

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
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.prod S') (T, T')
η : X✝ ⟶ Y✝
⊢ S.map η.left.1 ≫ (mk Y✝.hom.1, mk Y✝.hom.2).1.hom = (mk X✝.hom.1, mk X✝.hom.2).1.hom

Tactic:
simp

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
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.prod S') (T, T')
η : X✝ ⟶ Y✝
⊢ S'.map η.left.2 ≫ (mk Y✝.hom.1, mk Y✝.hom.2).2.hom = (mk X✝.hom.1, mk X✝.hom.2).2.hom

Tactic:
simp

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
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'
η : X✝ ⟶ Y✝
⊢ (S.prod S').map (η.1.left, η.2.left) ≫ (mk (Y✝.1.hom, Y✝.2.hom)).hom = (mk (X✝.1.hom, X✝.2.hom)).hom

Tactic:
simp

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
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.prod S') (T, T')} (f : X ⟶ Y),
    (𝟭 (CostructuredArrow (S.prod S') (T, T'))).map f ≫
        (Iso.refl ((𝟭 (CostructuredArrow (S.prod S') (T, T'))).obj Y)).hom =
      (Iso.refl ((𝟭 (CostructuredArrow (S.prod S') (T, T'))).obj X)).hom ≫
        (prodFunctor S S' T T' ⋙ prodInverse S S' T T').map f

Tactic:
simp

Goal state after:
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

Tactic:
simp

Goal state after:
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).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:
simp

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 L (R.obj b)
f : X✝ ⟶ Y✝
⊢ L.map f.left ≫
      (CostructuredArrow.left
          { left := { left := Y✝.left, right := b, hom := Y✝.hom }, right := { as := PUnit.unit }, hom := 𝟙 b }).hom =
    (CostructuredArrow.left
          { left := { left := X✝.left, right := b, hom := X✝.hom }, right := { as := PUnit.unit }, hom := 𝟙 b }).hom ≫
      R.map (𝟙 b)

Tactic:
simp

Goal state after: