awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
x : Arrow.{w, u} (ShrinkHoms.{u} C)
⊢ Functor.obj (Functor.mapArrow (Equivalence.functor (ShrinkHoms.equivalence C)))
      (Functor.obj (Functor.mapArrow (Equivalence.inverse (ShrinkHoms.equivalence C))) x) =
    x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
x : Arrow.{v, u} C
⊢ Functor.obj (C := Arrow.{w, u} (ShrinkHoms.{u} C)) (Functor.mapArrow (Equivalence.inverse (ShrinkHoms.equivalence C)))
      (Functor.obj (Functor.mapArrow (Equivalence.functor (ShrinkHoms.equivalence C))) x) =
    x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
x : Arrow.{v, w} (Shrink.{w, u} C)
simp :
  Eq (α :=
    Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
      (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
        (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.left))
      (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
        (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.right)))
    (CategoryStruct.comp (Y := x.left) (NatTrans.app (Equivalence.counit (Shrink.equivalence C)) x.left)
        (x.hom ≫ NatTrans.app (Equivalence.counitInv (Shrink.equivalence C)) x.right) :
      Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
        (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
          (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.left))
        (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
          (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.right)))
    (eqToHom ⋯ ≫ x.hom ≫ eqToHom ⋯ :
      Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
        (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
          (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.left))
        (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
          (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.right)))
⊢ Eq (α :=
    Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
      (left
        (Functor.obj (Functor.mapArrow (Equivalence.functor (Shrink.equivalence C)))
          (Functor.obj (Functor.mapArrow (Equivalence.inverse (Shrink.equivalence C))) x)))
      (right
        (Functor.obj (Functor.mapArrow (Equivalence.functor (Shrink.equivalence C)))
          (Functor.obj (Functor.mapArrow (Equivalence.inverse (Shrink.equivalence C))) x))))
    (hom
      (Functor.obj (Functor.mapArrow (Equivalence.functor (Shrink.equivalence C)))
        (Functor.obj (Functor.mapArrow (Equivalence.inverse (Shrink.equivalence C))) x)))
    (eqToHom ⋯ ≫ x.hom ≫ eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
x : Arrow.{v, w} (Shrink.{w, u} C)
⊢ Eq (α :=
    Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
      (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
        (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.left))
      (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
        (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.right)))
    (CategoryStruct.comp (Y := x.left) (NatTrans.app (Equivalence.counit (Shrink.equivalence C)) x.left)
        (x.hom ≫ NatTrans.app (Equivalence.counitInv (Shrink.equivalence C)) x.right) :
      Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
        (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
          (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.left))
        (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
          (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.right)))
    (eqToHom ⋯ ≫ x.hom ≫ eqToHom ⋯ :
      Quiver.Hom.{v, w} (V := Shrink.{w, u} C)
        (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
          (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.left))
        (Functor.obj.{v, v, u, w} (Equivalence.functor (Shrink.equivalence C))
          (Functor.obj.{v, v, w, u} (Equivalence.inverse (Shrink.equivalence C)) x.right)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
x : Arrow.{v, u} C
⊢ (Functor.obj (C := Arrow.{v, w} (Shrink.{w, u} C)) (Functor.mapArrow (Equivalence.inverse (Shrink.equivalence C)))
        (Functor.obj (Functor.mapArrow (Equivalence.functor (Shrink.equivalence C))) x)).left =
    x.left

Tactic:
simp [Shrink.equivalence]

Premises used: CategoryTheory.Shrink.equivalence
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
x : Arrow.{v, u} C
⊢ (Functor.obj (C := Arrow.{v, w} (Shrink.{w, u} C)) (Functor.mapArrow (Equivalence.inverse (Shrink.equivalence C)))
        (Functor.obj (Functor.mapArrow (Equivalence.functor (Shrink.equivalence C))) x)).right =
    x.right

Tactic:
simp [Shrink.equivalence]

Premises used: CategoryTheory.Shrink.equivalence
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w, u} C
x : Arrow.{v, u} C
⊢ (Functor.obj (C := Arrow.{v, w} (Shrink.{w, u} C)) (Functor.mapArrow (Equivalence.inverse (Shrink.equivalence C)))
        (Functor.obj (Functor.mapArrow (Equivalence.functor (Shrink.equivalence C))) x)).hom =
    eqToHom ⋯ ≫ x.hom ≫ eqToHom ⋯

Tactic:
simp [Shrink.equivalence]

Premises used: CategoryTheory.Shrink.equivalence
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
κ : Cardinal.{w}
⊢ HasCardinalLT (Arrow.{w', u} (ShrinkHoms.{u} C)) κ ↔ HasCardinalLT (Arrow.{v, u} C) κ

Tactic:
hasCardinalLT_iff_of_equiv (Arrow.shrinkHomsEquiv C) κ

Premises used: hasCardinalLT_iff_of_equiv, CategoryTheory.Arrow.shrinkHomsEquiv
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Small.{w', u} C
κ : Cardinal.{w}
⊢ HasCardinalLT (Arrow.{v, w'} (Shrink.{w', u} C)) κ ↔ HasCardinalLT (Arrow.{v, u} C) κ

Tactic:
hasCardinalLT_iff_of_equiv (Arrow.shrinkEquiv C) κ

Premises used: hasCardinalLT_iff_of_equiv, CategoryTheory.Arrow.shrinkEquiv
-- Module: Mathlib.CategoryTheory.Comma.CardinalArrow
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
h : HasCardinalLT (Arrow.{v, u} C) κ
⊢ HasCardinalLT C κ

Tactic:
h.of_injective (fun X ↦ Arrow.mk (𝟙 X)) (fun _ _ h ↦ congr_arg Comma.left h)

Premises used: HasCardinalLT.of_injective, CategoryTheory.Comma.left, CategoryTheory.CategoryStruct.id, congr_arg, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type v₁
inst : Category.{v₁, v₁} A
B : Type v₁
inst_1 : Category.{v₁, v₁} B
T : Type v₁
inst_2 : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
rw : ∀ (G : A ⥤ Type v₁), IsIso (X := colimit (fst L R ⋙ G)) (Y := colimit G) (colimit.pre G (fst L R))
⊢ (fst L R).Final

Tactic:
rw [Functor.final_iff_isIso_colimit_pre]

Premises used: CategoryTheory.Functor.final_iff_isIso_colimit_pre
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type v₁
inst : Category.{v₁, v₁} A
B : Type v₁
inst_1 : Category.{v₁, v₁} B
T : Type v₁
inst_2 : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  Iso.trans (Y := colimit (grothendieckProj L ⋙ G))
    (L.colimitIsoColimitGrothendieck G : colimit G ≅ colimit (grothendieckProj L ⋙ G))
    (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.symm (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)) :
          colimit (grothendieckProj L ⋙ G) ≅ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G) :
              colimit ((grothendieckPrecompFunctorEquivalence L R).functor ⋙ fst L R ⋙ G) ≅ colimit (fst L R ⋙ G)) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G)) :
      colimit (grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G))
⊢ IsIso i.inv

Tactic:
i.isIso_inv

Premises used: CategoryTheory.Iso.isIso_inv
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type v₁
inst : Category.{v₁, v₁} A
B : Type v₁
inst_1 : Category.{v₁, v₁} B
T : Type v₁
inst_2 : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  Iso.trans (Y := colimit (grothendieckProj L ⋙ G))
    (L.colimitIsoColimitGrothendieck G : colimit G ≅ colimit (grothendieckProj L ⋙ G))
    (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.symm (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)) :
          colimit (grothendieckProj L ⋙ G) ≅ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G) :
              colimit ((grothendieckPrecompFunctorEquivalence L R).functor ⋙ fst L R ⋙ G) ≅ colimit (fst L R ⋙ G)) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G)) :
      colimit (grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G))
h : colimit.pre G (fst L R) = i.inv
⊢ IsIso (X := colimit (fst L R ⋙ G)) (Y := colimit G) (colimit.pre G (fst L R))

Tactic:
convert! i.isIso_inv

Premises used: CategoryTheory.Iso.isIso_inv
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type v₁
inst : Category.{v₁, v₁} A
B : Type v₁
inst_1 : Category.{v₁, v₁} B
T : Type v₁
inst_2 : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  Iso.trans (Y := colimit (grothendieckProj L ⋙ G))
    (L.colimitIsoColimitGrothendieck G : colimit G ≅ colimit (grothendieckProj L ⋙ G))
    (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.symm (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)) :
          colimit (grothendieckProj L ⋙ G) ≅ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G) :
              colimit ((grothendieckPrecompFunctorEquivalence L R).functor ⋙ fst L R ⋙ G) ≅ colimit (fst L R ⋙ G)) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G)) :
      colimit (grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G))
h :
  ∀ (j : Comma L R),
    CategoryStruct.comp (Y := colimit (fst L R ⋙ G)) (colimit.ι (fst L R ⋙ G) j) (colimit.pre G (fst L R)) =
      colimit.ι (fst L R ⋙ G) j ≫ i.inv
⊢ colimit.pre G (fst L R) = i.inv

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type v₁
inst : Category.{v₁, v₁} A
B : Type v₁
inst_1 : Category.{v₁, v₁} B
T : Type v₁
inst_2 : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  Iso.trans (Y := colimit (grothendieckProj L ⋙ G))
    (L.colimitIsoColimitGrothendieck G : colimit G ≅ colimit (grothendieckProj L ⋙ G))
    (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.symm (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)) :
          colimit (grothendieckProj L ⋙ G) ≅ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G) :
              colimit ((grothendieckPrecompFunctorEquivalence L R).functor ⋙ fst L R ⋙ G) ≅ colimit (fst L R ⋙ G)) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G)) :
      colimit (grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G))
a : A
b : B
f : L.obj a ⟶ R.obj b
⊢ Eq (α :=
    (fst L R ⋙ G).obj
        ((grothendieckPrecompFunctorToComma L R).obj
          { base := b, fiber := CostructuredArrow.mk f : Grothendieck (R ⋙ functor L) }) ⟶
      colimit G)
    (colimit.ι G a)
    (CategoryStruct.comp (Y := colimit (fst L R ⋙ G))
      (colimit.ι (fst L R ⋙ G)
        ((grothendieckPrecompFunctorToComma L R).obj { base := b, fiber := CostructuredArrow.mk f }))
      (CategoryStruct.comp (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.inv (Final.colimitIso (grothendieckPrecompFunctorToComma L R) (fst L R ⋙ G)) :
          colimit (fst L R ⋙ G) ⟶ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (CategoryStruct.comp (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (Iso.inv (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (CategoryStruct.comp (Y := colimit (grothendieckProj L ⋙ G))
                (Iso.hom (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)) :
                  colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶ colimit (grothendieckProj L ⋙ G))
                (Iso.inv (L.colimitIsoColimitGrothendieck G) : colimit (grothendieckProj L ⋙ G) ⟶ colimit G) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶ colimit G) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶ colimit G)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.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
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
fC : Comma L R ⥤ Comma L' R' :=
  map (F₁ := sA.functor) (F₂ := sB.functor) (F := sT.functor) (isoWhiskerRight sA.unitIso (L ⋙ sT.functor)).hom
    (isoWhiskerRight sB.unitIso (R ⋙ sT.functor)).hom
⊢ (fst L' R').Final

Tactic:
have : Final (fst L' R') := final_fst_small _ _
-- Module: Mathlib.CategoryTheory.Comma.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
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
fC : Comma L R ⥤ Comma L' R' :=
  map (F₁ := sA.functor) (F₂ := sB.functor) (F := sT.functor) (isoWhiskerRight sA.unitIso (L ⋙ sT.functor)).hom
    (isoWhiskerRight sB.unitIso (R ⋙ sT.functor)).hom
this : (fst L' R').Final
apply : fC ⋙ fst L' R' ⋙ sA.inverse ≅ fst L R
⊢ (fst L R).Final

Tactic:
apply final_of_natIso (F := (fC ⋙ fst L' R' ⋙ sA.inverse))

Premises used: CategoryTheory.Functor.final_of_natIso
-- Module: Mathlib.CategoryTheory.Comma.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
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
fC : Comma L R ⥤ Comma L' R' :=
  map (F₁ := sA.functor) (F₂ := sB.functor) (F := sT.functor) (isoWhiskerRight sA.unitIso (L ⋙ sT.functor)).hom
    (isoWhiskerRight sB.unitIso (R ⋙ sT.functor)).hom
this : (fst L' R').Final
⊢ fC ⋙ fst L' R' ⋙ sA.inverse ≅ fst L R

Tactic:
exact (Functor.associator _ _ _).symm.trans (Iso.compInverseIso (mapFst _ _))

Premises used: CategoryTheory.Comma.mapFst, CategoryTheory.Functor.associator, CategoryTheory.Iso.compInverseIso, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Comma.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 : L.Initial
⊢ ((opFunctor L R).leftOp ⋙ fst R.op L.op).Final

Tactic:
have : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Final :=
    final_equivalence_comp (opEquiv L R).functor.leftOp (fst R.op L.op)
-- Module: Mathlib.CategoryTheory.Comma.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 : L.Initial
this : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Final
⊢ (snd L R).op.Final

Tactic:
have : (snd L R).op.Final := final_of_natIso (opFunctorCompFst _ _)
-- Module: Mathlib.CategoryTheory.Comma.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 : L.Initial
this_1 : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Final
this : (snd L R).op.Final
⊢ (snd L R).Initial

Tactic:
apply initial_of_final_op

Premises used: CategoryTheory.Functor.initial_of_final_op
-- Module: Mathlib.CategoryTheory.Comma.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 : IsConnected.{v₁, u₁} A
inst_4 : R.Final
rwa rwa₁ rwa₂ rwa₃ : IsConnected.{v₁, u₁} A
⊢ IsConnected (Comma L R)

Tactic:
rwa [isConnected_iff_of_final (fst L R)]

Premises used: CategoryTheory.Functor.isConnected_iff_of_final, CategoryTheory.Comma.fst
-- Module: Mathlib.CategoryTheory.Comma.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 : IsConnected.{v₂, u₂} B
inst_4 : L.Initial
rwa rwa₁ rwa₂ rwa₃ : IsConnected.{v₂, u₂} B
⊢ IsConnected (Comma L R)

Tactic:
rwa [isConnected_iff_of_initial (snd L R)]

Premises used: CategoryTheory.Comma.snd, CategoryTheory.Functor.isConnected_iff_of_initial
-- Module: Mathlib.CategoryTheory.Comma.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
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F : Functor.{v₁, v₄, u₁, u₄} A A'
G : Functor.{v₂, v₅, u₂, u₅} B B'
H : Functor.{v₃, v₆, u₃, u₆} T T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst_6 : IsFiltered.{v₂, u₂} B
inst_7 : R.Final
inst_8 : R'.Final
inst_9 : F.Final
inst_10 : G.Final
x : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
⊢ (R ⋙ H).Final

Tactic:
haveI := final_of_natIso iR
-- Module: Mathlib.CategoryTheory.Comma.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
A' : Type u₄
inst_3 : Category.{v₄, u₄} A'
B' : Type u₅
inst_4 : Category.{v₅, u₅} B'
T' : Type u₆
inst_5 : Category.{v₆, u₆} T'
L' : Functor.{v₄, v₆, u₄, u₆} A' T'
R' : Functor.{v₅, v₆, u₅, u₆} B' T'
F : Functor.{v₁, v₄, u₁, u₄} A A'
G : Functor.{v₂, v₅, u₂, u₅} B B'
H : Functor.{v₃, v₆, u₃, u₆} T T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst_6 : IsFiltered.{v₂, u₂} B
inst_7 : R.Final
inst_8 : R'.Final
inst_9 : F.Final
inst_10 : G.Final
x : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
rw :
  IsConnected
    (Comma (StructuredArrow.map₂ (𝟙 (L'.obj { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.left)) iL.hom)
      (StructuredArrow.map₂ { left := i₂, right := j₂, hom := u₂ : Comma L' R' }.hom (inv iR.inv)))
⊢ IsConnected (StructuredArrow { left := i₂, right := j₂, hom := u₂ : Comma L' R' } (map iL.hom iR.inv))

Tactic:
rw [isConnected_iff_of_equivalence (StructuredArrow.commaMapEquivalence iL.hom iR.inv _)]

Premises used: CategoryTheory.isConnected_iff_of_equivalence, CategoryTheory.StructuredArrow.commaMapEquivalence, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv