awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} 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)
⊢ Eq (α :=
    Functor.obj (𝟭 (CostructuredArrow F d)ᵒᵖ) (op (CostructuredArrow.mk x)) ⟶
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).obj
        (op (CostructuredArrow.mk y)))
    (Functor.map (𝟭 (CostructuredArrow F d)ᵒᵖ) f ≫
      Iso.hom
        ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
          (op (CostructuredArrow.mk y))))
    (Iso.hom
        ((fun (X : (CostructuredArrow F d)ᵒᵖ) ↦ (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op)
          (op (CostructuredArrow.mk x))) ≫
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f)

Tactic:
exact Quiver.Hom.unop_inj (by ext; apply Quiver.Hom.op_inj (by simp))

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
e : E
f : StructuredArrow e G
X Y : StructuredArrow f (pre e F G)
φ : X ⟶ Y
rw :
  (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
⊢ (mk (Hom.right X.hom)).hom ≫ F.map (Hom.right (Hom.right φ)) = (mk (Hom.right Y.hom)).hom

Tactic:
rw [← w φ, comp_right]

Premises used: CategoryTheory.StructuredArrow.comp_right, CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} 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
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
e : E
f : StructuredArrow e G
X Y : StructuredArrow f.right F
φ : X ⟶ Y
⊢ hom
        (right (D := StructuredArrow e G) (S := f) (T := pre e F G)
          (mk (Y := mk (f.hom ≫ G.map X.hom)) (homMk X.hom ⋯))) ≫
      (F ⋙ G).map (Hom.right φ) =
    hom
      (right (D := StructuredArrow e G) (S := f) (T := pre e F G) (mk (Y := mk (f.hom ≫ G.map Y.hom)) (homMk Y.hom ⋯)))

Tactic:
simp only [Functor.comp_obj, mk_right, mk_hom_eq_self,
      Functor.comp_map, Category.assoc, ← w φ, Functor.map_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.StructuredArrow.mk_right, CategoryTheory.StructuredArrow.w, CategoryTheory.Functor.map_comp, CategoryTheory.StructuredArrow.mk_hom_eq_self, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
e : E
f : StructuredArrow e G
X : StructuredArrow f (pre e F G)
⊢ (Functor.obj (𝟭 (StructuredArrow f (pre e F G))) X).right.hom ≫
      (F ⋙ G).map (Iso.hom (Iso.refl (Functor.obj (𝟭 (StructuredArrow f (pre e F G))) X).right.right)) =
    ((preEquivalenceFunctor F f ⋙ preEquivalenceInverse F f).obj X).right.hom

Tactic:
simpa using X.hom.w.symm

Premises used: CategoryTheory.StructuredArrow.hom, Eq.symm, CategoryTheory.StructuredArrow.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
e : E
f : CostructuredArrow G e
X Y : CostructuredArrow (pre F G e) f
φ : X ⟶ Y
rw : F.map φ.left.left ≫ (mk Y.hom.left).hom = (mk (((pre F G e).map φ.left).left ≫ Y.hom.left)).hom
⊢ F.map φ.left.left ≫ (mk Y.hom.left).hom = (mk X.hom.left).hom

Tactic:
rw [← w φ, comp_left]

Premises used: CategoryTheory.CostructuredArrow.w, CategoryTheory.CostructuredArrow.comp_left
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} 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
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
e : E
f : CostructuredArrow G e
X Y : CostructuredArrow F f.left
φ : X ⟶ Y
⊢ Eq (α :=
    (F ⋙ G).obj
        (left.{v₁, v₃, u₁, u₃} (D := E) (S := F ⋙ G) (T := e)
          (left (D := CostructuredArrow G e) (S := pre F G e) (T := f)
            (mk (Y := mk (G.map X.hom ≫ f.hom)) (homMk X.hom ⋯)))) ⟶
      e)
    ((F ⋙ G).map φ.left ≫
      hom
        (left (D := CostructuredArrow G e) (S := pre F G e) (T := f)
          (mk (Y := mk (G.map Y.hom ≫ f.hom)) (homMk Y.hom ⋯))))
    (hom
      (left (D := CostructuredArrow G e) (S := pre F G e) (T := f)
        (mk (Y := mk (G.map X.hom ≫ f.hom)) (homMk X.hom ⋯))))

Tactic:
simp only [Functor.comp_obj, mk_left, Functor.comp_map, mk_hom_eq_self,
      ← w φ, Functor.map_comp, Category.assoc]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.CostructuredArrow.mk_hom_eq_self, CategoryTheory.Category.assoc, CategoryTheory.CostructuredArrow.w, CategoryTheory.CostructuredArrow.mk_left, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
e : E
f : CostructuredArrow G e
X : CostructuredArrow (pre F G e) f
⊢ (F ⋙ G).map (Iso.hom (Iso.refl (Functor.obj (𝟭 (CostructuredArrow (pre F G e) f)) X).left.left)) ≫
      ((preEquivalence.functor F f ⋙ preEquivalence.inverse F f).obj X).left.hom =
    (Functor.obj (𝟭 (CostructuredArrow (pre F G e) f)) X).left.hom

Tactic:
simpa using X.hom.w

Premises used: CategoryTheory.CostructuredArrow.hom, CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : D
S' : D'
T : Functor.{v₁, v₂, u₁, u₂} C D
T' : Functor.{v₃, v₄, u₃, u₄} C' D'
X Y : StructuredArrow (S, S') (T.prod T')
f : X ⟶ Y
⊢ X.hom.1 ≫ T.map (Hom.right f).1 = Y.hom.1

Tactic:
congr_arg _root_.Prod.fst (StructuredArrow.w f)

Premises used: Prod.fst, congr_arg, CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : D
S' : D'
T : Functor.{v₁, v₂, u₁, u₂} C D
T' : Functor.{v₃, v₄, u₃, u₄} C' D'
X Y : StructuredArrow (S, S') (T.prod T')
f : X ⟶ Y
⊢ X.hom.2 ≫ T'.map (Hom.right f).2 = Y.hom.2

Tactic:
congr_arg _root_.Prod.snd (StructuredArrow.w f)

Premises used: congr_arg, CategoryTheory.StructuredArrow.w, Prod.snd
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : D
S' : D'
T : Functor.{v₁, v₂, u₁, u₂} C D
T' : Functor.{v₃, v₄, u₃, u₄} 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 [← η.w]

Premises used: CategoryTheory.StructuredArrow.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : D
S' : D'
T : Functor.{v₁, v₂, u₁, u₂} C D
T' : Functor.{v₃, v₄, u₃, u₄} 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 [← η.w]

Premises used: CategoryTheory.StructuredArrow.Hom.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : D
S' : D'
T : Functor.{v₁, v₂, u₁, u₂} C D
T' : Functor.{v₃, v₄, u₃, u₄} C' D'
X Y : StructuredArrow S T × StructuredArrow S' T'
η : X ⟶ Y
⊢ hom (mk (X.1.hom, X.2.hom)) ≫ (T.prod T').map (Hom.right η.1, Hom.right η.2) = hom (mk (Y.1.hom, Y.2.hom))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : D
S' : D'
T : Functor.{v₁, v₂, u₁, u₂} C D
T' : Functor.{v₃, v₄, u₃, u₄} C' D'
⊢ ∀ {X Y : StructuredArrow (S, S') (T.prod T')} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (𝟭 (StructuredArrow (S, S') (T.prod T'))) X ⟶ (prodFunctor S S' T T' ⋙ prodInverse S S' T T').obj Y)
      (Functor.map (𝟭 (StructuredArrow (S, S') (T.prod T'))) f ≫
        Iso.hom
          ((fun (f : StructuredArrow (S, S') (T.prod T')) ↦
              (Iso.refl (Functor.obj (𝟭 (StructuredArrow (S, S') (T.prod T'))) f) :
                Functor.obj (𝟭 (StructuredArrow (S, S') (T.prod T'))) f ≅
                  Functor.obj (𝟭 (StructuredArrow (S, S') (T.prod T'))) f))
            Y))
      (Iso.hom
          ((fun (f : StructuredArrow (S, S') (T.prod T')) ↦
              (Iso.refl (Functor.obj (𝟭 (StructuredArrow (S, S') (T.prod T'))) f) :
                Functor.obj (𝟭 (StructuredArrow (S, S') (T.prod T'))) f ≅
                  Functor.obj (𝟭 (StructuredArrow (S, S') (T.prod T'))) f))
            X) ≫
        (prodFunctor S S' T T' ⋙ prodInverse S S' T T').map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : D
S' : D'
T : Functor.{v₁, v₂, u₁, u₂} C D
T' : Functor.{v₃, v₄, u₃, u₄} C' D'
X Y : StructuredArrow S T × StructuredArrow S' T'
f : X ⟶ Y
⊢ Eq (α :=
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X).1.right ⟶
      (Functor.obj (𝟭 (StructuredArrow S T × StructuredArrow S' T')) Y).1.right)
    (Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
          Iso.hom
            ((fun (f : StructuredArrow S T × StructuredArrow S' T') ↦
                (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
              Y)).1)
    (Hom.right
      (Iso.hom
            ((fun (f : StructuredArrow S T × StructuredArrow S' T') ↦
                (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
              X) ≫
          Functor.map (𝟭 (StructuredArrow S T × StructuredArrow S' T')) f).1)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : D
S' : D'
T : Functor.{v₁, v₂, u₁, u₂} C D
T' : Functor.{v₃, v₄, u₃, u₄} C' D'
X Y : StructuredArrow S T × StructuredArrow S' T'
f : X ⟶ Y
⊢ Eq (α :=
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X).2.right ⟶
      (Functor.obj (𝟭 (StructuredArrow S T × StructuredArrow S' T')) Y).2.right)
    (Hom.right
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
          Iso.hom
            ((fun (f : StructuredArrow S T × StructuredArrow S' T') ↦
                (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
              Y)).2)
    (Hom.right
      (Iso.hom
            ((fun (f : StructuredArrow S T × StructuredArrow S' T') ↦
                (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
              X) ≫
          Functor.map (𝟭 (StructuredArrow S T × StructuredArrow S' T')) f).2)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : Functor.{v₁, v₂, u₁, u₂} C D
S' : Functor.{v₃, v₄, u₃, u₄} C' D'
T : D
T' : D'
A B : CostructuredArrow (S.prod S') (T, T')
f : A ⟶ B
⊢ S.map f.left.1 ≫ B.hom.1 = A.hom.1

Tactic:
congr_arg _root_.Prod.fst (CostructuredArrow.w f)

Premises used: CategoryTheory.CostructuredArrow.w, Prod.fst, congr_arg
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : Functor.{v₁, v₂, u₁, u₂} C D
S' : Functor.{v₃, v₄, u₃, u₄} C' D'
T : D
T' : D'
A B : CostructuredArrow (S.prod S') (T, T')
f : A ⟶ B
⊢ S'.map f.left.2 ≫ B.hom.2 = A.hom.2

Tactic:
congr_arg _root_.Prod.snd (CostructuredArrow.w f)

Premises used: CategoryTheory.CostructuredArrow.w, congr_arg, Prod.snd
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : Functor.{v₁, v₂, u₁, u₂} C D
S' : Functor.{v₃, v₄, u₃, u₄} 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
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : Functor.{v₁, v₂, u₁, u₂} C D
S' : Functor.{v₃, v₄, u₃, u₄} 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
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : Functor.{v₁, v₂, u₁, u₂} C D
S' : Functor.{v₃, v₄, u₃, u₄} C' D'
T : D
T' : D'
X Y : CostructuredArrow S T × CostructuredArrow S' T'
η : X ⟶ Y
⊢ (S.prod S').map (η.1.left, η.2.left) ≫ hom (mk (Y.1.hom, Y.2.hom)) = hom (mk (X.1.hom, X.2.hom))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : Functor.{v₁, v₂, u₁, u₂} C D
S' : Functor.{v₃, v₄, u₃, u₄} C' D'
T : D
T' : D'
⊢ ∀ {X Y : CostructuredArrow (S.prod S') (T, T')} (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (𝟭 (CostructuredArrow (S.prod S') (T, T'))) X ⟶ (prodFunctor S S' T T' ⋙ prodInverse S S' T T').obj Y)
      (Functor.map (𝟭 (CostructuredArrow (S.prod S') (T, T'))) f ≫
        Iso.hom
          ((fun (f : CostructuredArrow (S.prod S') (T, T')) ↦
              (Iso.refl (Functor.obj (𝟭 (CostructuredArrow (S.prod S') (T, T'))) f) :
                Functor.obj (𝟭 (CostructuredArrow (S.prod S') (T, T'))) f ≅
                  Functor.obj (𝟭 (CostructuredArrow (S.prod S') (T, T'))) f))
            Y))
      (Iso.hom
          ((fun (f : CostructuredArrow (S.prod S') (T, T')) ↦
              (Iso.refl (Functor.obj (𝟭 (CostructuredArrow (S.prod S') (T, T'))) f) :
                Functor.obj (𝟭 (CostructuredArrow (S.prod S') (T, T'))) f ≅
                  Functor.obj (𝟭 (CostructuredArrow (S.prod S') (T, T'))) f))
            X) ≫
        (prodFunctor S S' T T' ⋙ prodInverse S S' T T').map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : Functor.{v₁, v₂, u₁, u₂} C D
S' : Functor.{v₃, v₄, u₃, u₄} C' D'
T : D
T' : D'
X Y : CostructuredArrow S T × CostructuredArrow S' T'
f : X ⟶ Y
⊢ Eq (α :=
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X).1.left ⟶
      (Functor.obj (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) Y).1.left)
    (CommaMorphism.left
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
          Iso.hom
            ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
                (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
              Y)).1)
    (CommaMorphism.left
      (Iso.hom
            ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
                (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
              X) ≫
          Functor.map (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) f).1)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
D' : Type u₄
inst_3 : Category.{v₄, u₄} D'
S : Functor.{v₁, v₂, u₁, u₂} C D
S' : Functor.{v₃, v₄, u₃, u₄} C' D'
T : D
T' : D'
X Y : CostructuredArrow S T × CostructuredArrow S' T'
f : X ⟶ Y
⊢ Eq (α :=
    ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X).2.left ⟶
      (Functor.obj (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) Y).2.left)
    (CommaMorphism.left
      ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
          Iso.hom
            ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
                (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
              Y)).2)
    (CommaMorphism.left
      (Iso.hom
            ((fun (f : CostructuredArrow S T × CostructuredArrow S' T') ↦
                (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f) :
                  (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f ≅
                    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj f))
              X) ≫
          Functor.map (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')) f).2)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} C T
R : Functor.{v₂, v₃, u₂, u₃} D T
C' : Type u₄
inst_3 : Category.{v₄, u₄} C'
D' : Type u₅
inst_4 : Category.{v₅, u₅} D'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} C' T'
R' : Functor.{v₅, v₆, u₅, u₆} D' T'
F₁ : Functor.{v₁, v₄, u₁, u₄} C C'
F₂ : Functor.{v₂, v₅, u₂, u₅} D D'
F : Functor.{v₃, v₆, u₃, u₆} T T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst_6 : IsIso β
X : Comma L' R'
Y : StructuredArrow X (Comma.map α β)
⊢ ((map₂ (𝟙 (L'.obj X.left)) α).obj (mk Y.hom.left)).hom ≫ F.map Y.right.hom =
    ((map₂ X.hom (inv β)).obj (mk Y.hom.right)).hom

Tactic:
simpa only [Functor.const_obj_obj, map₂_obj_left, mk_left, map₂_obj_right, mk_right,
        map₂_obj_hom, mk_hom_eq_self, Category.id_comp, Category.assoc, NatIso.isIso_inv_app,
        Functor.comp_obj, Comma.map_obj_right, Comma.map_obj_left, Comma.map_obj_hom,
        IsIso.hom_inv_id, Category.comp_id] using
        congrFun (congrArg CategoryStruct.comp Y.hom.w) (inv (β.app Y.right.right) :)

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Comma.map_obj_hom, CategoryTheory.Comma.right, CategoryTheory.StructuredArrow.map₂_obj_right, congrArg, CategoryTheory.StructuredArrow.map₂_obj_left, CategoryTheory.Comma.map_obj_right, CategoryTheory.StructuredArrow.hom, CategoryTheory.CommaMorphism.w, CategoryTheory.StructuredArrow.mk_left, CategoryTheory.Category.comp_id, congrFun, CategoryTheory.StructuredArrow.mk_right, CategoryTheory.CategoryStruct.comp, CategoryTheory.StructuredArrow.right, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.inv, CategoryTheory.NatIso.isIso_inv_app, CategoryTheory.StructuredArrow.mk_hom_eq_self, CategoryTheory.Functor.const_obj_obj, CategoryTheory.NatTrans.app, CategoryTheory.StructuredArrow.map₂_obj_hom, CategoryTheory.Category.id_comp, CategoryTheory.Comma.map_obj_left