awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 Z : StructuredArrow X (Comma.map α β)
f : Y ⟶ Z
⊢ Eq (α :=
    (map₂ (𝟙 (L'.obj X.left)) α).obj
        (Comma.left (T := StructuredArrow (L'.obj X.left) F) (L := map₂ (𝟙 (L'.obj X.left)) α) (R := map₂ X.hom (inv β))
          { left := mk Y.hom.left, right := mk Y.hom.right, hom := homMk Y.right.hom ⋯ :
            Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β)) }) ⟶
      (map₂ X.hom (inv β)).obj
        (Comma.right (T := StructuredArrow (L'.obj X.left) F) (L := map₂ (𝟙 (L'.obj X.left)) α) (R :=
          map₂ X.hom (inv β)) { left := mk Z.hom.left, right := mk Z.hom.right, hom := homMk Z.right.hom ⋯ }))
    ((map₂ (𝟙 (L'.obj X.left)) α).map (homMk (Hom.right f).left ⋯) ≫
      Comma.hom
        { left := mk Z.hom.left, right := mk Z.hom.right, hom := homMk Z.right.hom ⋯ :
          Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β)) })
    (Comma.hom
        { left := mk Y.hom.left, right := mk Y.hom.right, hom := homMk Y.right.hom ⋯ :
          Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β)) } ≫
      (map₂ X.hom (inv β)).map (homMk (Hom.right f).right ⋯))

Tactic:
simp only [map₂_obj_right, mk_right, hom_eq_iff, comp_right,
      map₂_map_right, homMk_right, CommaMorphism.w]

Premises used: CategoryTheory.StructuredArrow.map₂_obj_right, CategoryTheory.StructuredArrow.map₂_map_right, CategoryTheory.CommaMorphism.w, CategoryTheory.StructuredArrow.hom_eq_iff, CategoryTheory.StructuredArrow.homMk_right, CategoryTheory.StructuredArrow.comp_right, CategoryTheory.StructuredArrow.mk_right
-- 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 : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
⊢ X.left ⟶
    ((Comma.map α β).obj { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom : Comma L R }).left

Tactic:
exact Y.left.hom

Premises used: CategoryTheory.Comma.left, CategoryTheory.StructuredArrow.hom
-- 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 : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
⊢ X.right ⟶
    ((Comma.map α β).obj { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom : Comma L R }).right

Tactic:
exact Y.right.hom

Premises used: CategoryTheory.Comma.right, CategoryTheory.StructuredArrow.hom
-- 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 : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
⊢ L'.map Y.left.hom ≫
      ((Comma.map α β).obj { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom : Comma L R }).hom =
    X.hom ≫ R'.map Y.right.hom

Tactic:
simpa using congrFun (congrArg CategoryStruct.comp (StructuredArrow.w Y.hom))
        (β.app Y.right.right)

Premises used: CategoryTheory.Comma.right, congrArg, CategoryTheory.Comma.hom, congrFun, CategoryTheory.StructuredArrow.w, CategoryTheory.CategoryStruct.comp, CategoryTheory.StructuredArrow.right, CategoryTheory.NatTrans.app
-- 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 Z : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
f : Y ⟶ Z
⊢ Quiver.Hom.{v₁, u₁} (V := C)
    (Comma.left.{v₁, v₂, v₃, u₁, u₂, u₃} (B := D) (T := T) (L := L) (R := R)
      (right (D := Comma L' R') (S := X) (T := Comma.map α β)
        (mk (Y := { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom })
          { left := Y.left.hom, right := Y.right.hom, w := ⋯ })))
    (Comma.left.{v₁, v₂, v₃, u₁, u₂, u₃} (B := D) (T := T) (L := L) (R := R)
      (right (D := Comma L' R') (S := X) (T := Comma.map α β)
        (mk (Y := { left := Z.left.right, right := Z.right.right, hom := Hom.right Z.hom })
          { left := Z.left.hom, right := Z.right.hom, w := ⋯ })))

Tactic:
exact f.left.right

Premises used: CategoryTheory.CommaMorphism.left, CategoryTheory.StructuredArrow.Hom.right
-- 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 Z : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
f : Y ⟶ Z
⊢ Quiver.Hom.{v₂, u₂} (V := D)
    (Comma.right.{v₁, v₂, v₃, u₁, u₂, u₃} (A := C) (T := T) (L := L) (R := R)
      (right (D := Comma L' R') (S := X) (T := Comma.map α β)
        (mk (Y := { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom })
          { left := Y.left.hom, right := Y.right.hom, w := ⋯ })))
    (Comma.right.{v₁, v₂, v₃, u₁, u₂, u₃} (A := C) (T := T) (L := L) (R := R)
      (right (D := Comma L' R') (S := X) (T := Comma.map α β)
        (mk (Y := { left := Z.left.right, right := Z.right.right, hom := Hom.right Z.hom })
          { left := Z.left.hom, right := Z.right.hom, w := ⋯ })))

Tactic:
exact f.right.right

Premises used: CategoryTheory.CommaMorphism.right, CategoryTheory.StructuredArrow.Hom.right
-- 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 Z : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
f : Y ⟶ Z
⊢ L.map (Hom.right f.left) ≫
      Comma.hom
        (right (D := Comma L' R') (S := X) (T := Comma.map α β)
          (mk (Y := { left := Z.left.right, right := Z.right.right, hom := Hom.right Z.hom })
            { left := Z.left.hom, right := Z.right.hom, w := ⋯ })) =
    Comma.hom
        (right (D := Comma L' R') (S := X) (T := Comma.map α β)
          (mk (Y := { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom : Comma L R })
            { left := Y.left.hom, right := Y.right.hom, w := ⋯ :
              CommaMorphism X
                ((Comma.map α β).obj
                  { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom : Comma L R }) })) ≫
      R.map (Hom.right f.right)

Tactic:
congrArg CommaMorphism.right f.w

Premises used: congrArg, CategoryTheory.CommaMorphism.w, CategoryTheory.CommaMorphism.right, CategoryTheory.StructuredArrow
-- 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 Z : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
f : Y ⟶ Z
⊢ L.map (Hom.right f.left) ≫
      Comma.hom
        (right (D := Comma L' R') (S := X) (T := Comma.map α β)
          (mk (Y := { left := Z.left.right, right := Z.right.right, hom := Hom.right Z.hom })
            { left := Z.left.hom, right := Z.right.hom, w := ⋯ })) =
    Comma.hom
        (right (D := Comma L' R') (S := X) (T := Comma.map α β)
          (mk (Y := { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom : Comma L R })
            { left := Y.left.hom, right := Y.right.hom, w := ⋯ :
              CommaMorphism X
                ((Comma.map α β).obj
                  { left := Y.left.right, right := Y.right.right, hom := Hom.right Y.hom : Comma L R }) })) ≫
      R.map (Hom.right f.right)

Tactic:
exact congrArg CommaMorphism.right f.w

Premises used: congrArg, CategoryTheory.CommaMorphism.w, CategoryTheory.CommaMorphism.right
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
inst_4 : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
rw : ∀ (G : T ⥤ Type u₁), IsIso (X := colimit (L ⋙ G)) (Y := colimit G) (colimit.pre G L)
⊢ L.Final

Tactic:
rw [final_iff_isIso_colimit_pre]

Premises used: CategoryTheory.Functor.final_iff_isIso_colimit_pre
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
inst_4 : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
G : T ⥤ Type u₁
⊢ ∀ (b : B), ((R.whiskerLeft (preFunctor L (𝟭 T))).app b).toFunctor.Final

Tactic:
have : ∀ (b : B), Final ((whiskerLeft R (preFunctor L (𝟭 T))).app b).toFunctor := fun b =>
    inferInstanceAs (Final (CostructuredArrow.toOver L (R.obj b)))
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
dsimp :
  Final (C := CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
    (pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
⊢ Final (C := CostructuredArrow L' (R'.obj b)) (CostructuredArrow.toOver L' (R'.obj b))

Tactic:
dsimp only [L', R', CostructuredArrow.toOver] at hB ⊢

Premises used: CategoryTheory.CostructuredArrow.toOver
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (pre L (𝟭 T) (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x :=
  map₂ (F := sA.inverse) ((sA.inverse ⋙ L).whiskerLeft sT.unit) (𝟙 (sT.inverse.obj x)) ⋙
    pre L (𝟭 T) (R.obj (sB.inverse.obj b)) ⋙
      map₂ (F := sT.functor) (𝟙 (sT.functor ⋙ 𝟭 (AsSmall T))) (𝟙 (sT.functor.obj (R.obj (sB.inverse.obj b))))
apply : F'' ≅ pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)
⊢ Final (C := CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
    (pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))

Tactic:
apply final_of_natIso (F := F'')

Premises used: CategoryTheory.Functor.final_of_natIso
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (pre L (𝟭 T) (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x :=
  map₂ (F := sA.inverse) ((sA.inverse ⋙ L).whiskerLeft sT.unit) (𝟙 (sT.inverse.obj x)) ⋙
    pre L (𝟭 T) (R.obj (sB.inverse.obj b)) ⋙
      map₂ (F := sT.functor) (𝟙 (sT.functor ⋙ 𝟭 (AsSmall T))) (𝟙 (sT.functor.obj (R.obj (sB.inverse.obj b))))
⊢ ∀ (X : AsSmall T), sT.counitInv.app X = 𝟙 (obj (𝟭 (AsSmall T)) X)

Tactic:
have hsT (X) : sT.counitInv.app X = 𝟙 _ := rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (pre L (𝟭 T) (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x :=
  map₂ (F := sA.inverse) ((sA.inverse ⋙ L).whiskerLeft sT.unit) (𝟙 (sT.inverse.obj x)) ⋙
    pre L (𝟭 T) (R.obj (sB.inverse.obj b)) ⋙
      map₂ (F := sT.functor) (𝟙 (sT.functor ⋙ 𝟭 (AsSmall T))) (𝟙 (sT.functor.obj (R.obj (sB.inverse.obj b))))
hsT : ∀ (X : AsSmall T), sT.counitInv.app X = 𝟙 (obj (𝟭 (AsSmall T)) X)
X : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x
⊢ map (𝟭 (AsSmall T)) (Iso.hom (Iso.refl (F''.obj X).left)) ≫
      (obj (pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)) X).hom =
    (F''.obj X).hom

Tactic:
simp [F'', hsT]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (pre L (𝟭 T) (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x :=
  map₂ (F := sA.inverse) ((sA.inverse ⋙ L).whiskerLeft sT.unit) (𝟙 (sT.inverse.obj x)) ⋙
    pre L (𝟭 T) (R.obj (sB.inverse.obj b)) ⋙
      map₂ (F := sT.functor) (𝟙 (sT.functor ⋙ 𝟭 (AsSmall T))) (𝟙 (sT.functor.obj (R.obj (sB.inverse.obj b))))
hsT : ∀ (X : AsSmall T), sT.counitInv.app X = 𝟙 (obj (𝟭 (AsSmall T)) X)
⊢ F'' ≅ pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)

Tactic:
exact NatIso.ofComponents (fun X => CostructuredArrow.isoMk (Iso.refl _) (by simp [F'', hsT]))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.CostructuredArrow.isoMk, CategoryTheory.CostructuredArrow.left, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
⊢ ∀ (b : AsSmall B), Final (C := CostructuredArrow L' (R'.obj b)) (CostructuredArrow.toOver L' (R'.obj b))

Tactic:
have (b : _) : (CostructuredArrow.toOver L' (R'.obj b)).Final := by
    dsimp only [L', R', CostructuredArrow.toOver] at hB ⊢
    let x := (sB.inverse ⋙ R ⋙ sT.functor).obj b
    let F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 _) x :=
      map₂ (F := sA.inverse) (G := sT.inverse) (whiskerLeft (sA.inverse ⋙ L) sT.unit) (𝟙 _) ⋙
      pre L (𝟭 T) (R.obj _) ⋙ map₂ (F := sT.functor) (G := sT.functor) (𝟙 _) (𝟙 _)
    apply final_of_natIso (F := F'')
    have hsT (X) : sT.counitInv.app X = 𝟙 _ := rfl
    exact NatIso.ofComponents (fun X => CostructuredArrow.isoMk (Iso.refl _) (by simp [F'', hsT]))
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
this : ∀ (b : AsSmall B), Final (C := CostructuredArrow L' (R'.obj b)) (CostructuredArrow.toOver L' (R'.obj b))
⊢ L'.Final

Tactic:
have := final_of_final_costructuredArrowToOver_small L' R'
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
this_1 : ∀ (b : AsSmall B), Final (C := CostructuredArrow L' (R'.obj b)) (CostructuredArrow.toOver L' (R'.obj b))
this : L'.Final
apply : sA.functor ⋙ L' ⋙ sT.inverse ≅ L
⊢ L.Final

Tactic:
apply final_of_natIso (F := (sA.functor ⋙ L' ⋙ sT.inverse))

Premises used: CategoryTheory.Functor.final_of_natIso
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
this_1 : ∀ (b : AsSmall B), Final (C := CostructuredArrow L' (R'.obj b)) (CostructuredArrow.toOver L' (R'.obj b))
this : L'.Final
⊢ sA.functor ⋙ L' ⋙ sT.inverse ≅ L

Tactic:
exact (sA.functor.associator (sA.inverse ⋙ L ⋙ sT.functor) sT.inverse).symm ≪≫
    ((sA.functor.associator sA.inverse (L ⋙ sT.functor)).symm ≪≫
      isoWhiskerRight sA.unitIso.symm _ ≪≫ (L ⋙ sT.functor).leftUnitor).compInverseIso

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, CategoryTheory.Equivalence.functor, CategoryTheory.Iso.compInverseIso, CategoryTheory.Functor.leftUnitor, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.isoWhiskerRight, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
d : Dᵒᵖ
h :
  Cat.Hom.toFunctor (Functor.toCatHom (map (Quiver.Hom.unop (𝟙 d)))) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T)))
⊢ Functor.toCatHom (map (Quiver.Hom.unop (𝟙 d))) = 𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
d : Dᵒᵖ
x : (↑(Cat.of (StructuredArrow (Opposite.unop d) T)) : Type (max u₁ v₂))
left : Discrete PUnit.{1}
right : C
hom : Functor.obj.{0, v₂, 0, u₂} (Functor.fromPUnit (Opposite.unop d)) left ⟶ T.obj right
⊢ Functor.obj (Cat.Hom.toFunctor (Functor.toCatHom (map (Quiver.Hom.unop (𝟙 d)))))
      { left := left, right := right, hom := hom : Comma (Functor.fromPUnit (Opposite.unop d)) T } =
    (Cat.Hom.toFunctor (𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T)))).obj
      { left := left, right := right, hom := hom : Comma (Functor.fromPUnit (Opposite.unop d)) T }

Tactic:
simp