awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Final
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
hF : F.Final
hG : G.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
rw :
  ∀
    (hF :
      ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
        IsIso (X := colimit ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ G)) (Y := colimit G)
          (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))),
    let s₃ : E ≌ AsSmall E := AsSmall.equiv;
    ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
      IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
        (colimit.pre G_1 ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
      (colimit.pre G_1 ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
rw [final_iff_comp_equivalence F s₂.functor, final_iff_equivalence_comp s₁.inverse,
    final_iff_isIso_colimit_pre] at hF

Premises used: CategoryTheory.Functor.final_iff_comp_equivalence, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.final_iff_isIso_colimit_pre, CategoryTheory.Functor.final_iff_equivalence_comp, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Final
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
hG : G.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ G)) (Y := colimit G)
      (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
      (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
rw [final_iff_comp_equivalence G s₃.functor, final_iff_equivalence_comp s₂.inverse,
    final_iff_isIso_colimit_pre] at hG

Premises used: CategoryTheory.Functor.final_iff_comp_equivalence, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.final_iff_isIso_colimit_pre, CategoryTheory.Functor.final_iff_equivalence_comp, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Final
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
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ G)) (Y := colimit G)
      (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
hG :
  ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
      (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
rw :
  IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (CategoryStruct.comp (Y := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H))
      (colimit.pre ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H) (s₁.inverse ⋙ F ⋙ s₂.functor))
      (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor)))
⊢ IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (colimit.pre H ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
rw [← colimit.pre_pre]

Premises used: CategoryTheory.Limits.colimit.pre_pre
-- Module: Mathlib.CategoryTheory.Limits.Final
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
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ G)) (Y := colimit G)
      (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
hG :
  ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
      (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
⊢ IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (CategoryStruct.comp (Y := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H))
      (colimit.pre ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H) (s₁.inverse ⋙ F ⋙ s₂.functor))
      (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : F.Initial
inst_4 : G.Initial
suffices : (F ⋙ G).op.Final
⊢ (F ⋙ G).Initial

Tactic:
suffices Final (F ⋙ G).op from initial_of_final_op _
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : F.Initial
inst_4 : G.Initial
⊢ (F ⋙ G).op.Final

Tactic:
final_comp F.op G.op

Premises used: CategoryTheory.Functor.op, Quiver.Hom.op, CategoryTheory.Functor.comp, Quiver.Hom.unop, CategoryTheory.Functor.final_comp
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : F.Initial
inst_4 : G.Initial
⊢ (F ⋙ G).op.Final

Tactic:
exact final_comp F.op G.op

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.final_comp
-- Module: Mathlib.CategoryTheory.Limits.Final
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
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
rw :
  ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
      (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
⊢ G.Final

Tactic:
rw [final_iff_comp_equivalence G s₃.functor, final_iff_equivalence_comp s₂.inverse,
    final_iff_isIso_colimit_pre]

Premises used: CategoryTheory.Functor.final_iff_comp_equivalence, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.final_iff_isIso_colimit_pre, CategoryTheory.Functor.final_iff_equivalence_comp, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Final
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
hF : F.Final
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
rw :
  ∀
    (hF :
      ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
        IsIso (X := colimit ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ G)) (Y := colimit G)
          (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))),
    let s₃ : E ≌ AsSmall E := AsSmall.equiv;
    ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
      IsIso (X := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
        (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
      (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
rw [final_iff_comp_equivalence F s₂.functor, final_iff_equivalence_comp s₁.inverse,
    final_iff_isIso_colimit_pre] at hF

Premises used: CategoryTheory.Functor.final_iff_comp_equivalence, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.final_iff_isIso_colimit_pre, CategoryTheory.Functor.final_iff_equivalence_comp, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Final
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
hFG : (F ⋙ G).Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ G)) (Y := colimit G)
      (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
⊢ ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
      (colimit.pre G_1 ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
rw [final_iff_comp_equivalence (F ⋙ G) s₃.functor, final_iff_equivalence_comp s₁.inverse,
    final_natIso_iff _i, final_iff_isIso_colimit_pre] at hFG

Premises used: CategoryTheory.Functor.final_iff_comp_equivalence, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.final_iff_isIso_colimit_pre, CategoryTheory.Functor.final_natIso_iff, CategoryTheory.Functor.final_iff_equivalence_comp, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Final
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
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ G)) (Y := colimit G)
      (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
hFG :
  ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
      (colimit.pre G_1 ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
⊢ IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (colimit.pre H ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
replace hFG := hFG H
-- Module: Mathlib.CategoryTheory.Limits.Final
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
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ G)) (Y := colimit G)
      (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
hFG :
  IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (colimit.pre H ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))
⊢ IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (CategoryStruct.comp (Y := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H))
      (colimit.pre ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H) (s₁.inverse ⋙ F ⋙ s₂.functor))
      (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor)))

Tactic:
rw [← colimit.pre_pre] at hFG

Premises used: CategoryTheory.Limits.colimit.pre_pre
-- Module: Mathlib.CategoryTheory.Limits.Final
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
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ G)) (Y := colimit G)
      (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
hFG :
  IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (CategoryStruct.comp (Y := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H))
      (colimit.pre ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H) (s₁.inverse ⋙ F ⋙ s₂.functor))
      (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor)))
⊢ IsIso (X := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
IsIso.of_isIso_comp_left (colimit.pre _ (s₁.inverse ⋙ F ⋙ s₂.functor)) _

Premises used: CategoryTheory.IsIso.of_isIso_comp_left, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.functor, CategoryTheory.Limits.colimit.pre, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Final
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
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
hF :
  ∀ (G : AsSmall D ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ G)) (Y := colimit G)
      (colimit.pre G (s₁.inverse ⋙ F ⋙ s₂.functor))
s₃ : E ≌ AsSmall E := AsSmall.equiv
_i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
H : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)
hFG :
  IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (CategoryStruct.comp (Y := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H))
      (colimit.pre ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H) (s₁.inverse ⋙ F ⋙ s₂.functor))
      (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor)))
⊢ IsIso (X := colimit ((s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))

Tactic:
exact IsIso.of_isIso_comp_left (colimit.pre _ (s₁.inverse ⋙ F ⋙ s₂.functor)) _

Premises used: CategoryTheory.IsIso.of_isIso_comp_left, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.functor, CategoryTheory.Limits.colimit.pre, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : F.Initial
inst_4 : (F ⋙ G).Initial
suffices : G.op.Final
⊢ G.Initial

Tactic:
suffices Final G.op from initial_of_final_op _
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : F.Initial
inst_4 : (F ⋙ G).Initial
⊢ (F.op ⋙ G.op).Final

Tactic:
have : Final (F.op ⋙ G.op) := show Final (F ⋙ G).op from inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : F.Initial
inst_4 : (F ⋙ G).Initial
this : (F.op ⋙ G.op).Final
⊢ G.op.Final

Tactic:
final_of_final_comp F.op G.op

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.final_of_final_comp
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : F.Initial
inst_4 : (F ⋙ G).Initial
this : (F.op ⋙ G.op).Final
⊢ G.op.Final

Tactic:
exact final_of_final_comp F.op G.op

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.final_of_final_comp
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : G.Full
inst_4 : G.Faithful
inst_5 : (F ⋙ G).Final
⊢ G.Final

Tactic:
have := final_of_comp_full_faithful F G
  final_of_final_comp F G

Premises used: CategoryTheory.Functor.final_of_final_comp, CategoryTheory.Functor.final_of_comp_full_faithful
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : G.Full
inst_4 : G.Faithful
inst_5 : (F ⋙ G).Initial
⊢ G.Initial

Tactic:
have := initial_of_comp_full_faithful F G
  initial_of_initial_comp F G

Premises used: CategoryTheory.Functor.initial_of_initial_comp, CategoryTheory.Functor.initial_of_comp_full_faithful
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : G.Final
inst_4 : G.Full
inst_5 : G.Faithful
⊢ F.Final ↔ (F ⋙ G).Final

Tactic:
⟨fun _ => final_comp _ _, fun _ => final_of_comp_full_faithful F G⟩

Premises used: CategoryTheory.Functor.final_comp, Iff.intro, CategoryTheory.Functor.final_of_comp_full_faithful
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : G.Initial
inst_4 : G.Full
inst_5 : G.Faithful
⊢ F.Initial ↔ (F ⋙ G).Initial

Tactic:
⟨fun _ => initial_comp _ _, fun _ => initial_of_comp_full_faithful F G⟩

Premises used: CategoryTheory.Functor.initial_comp, Iff.intro, CategoryTheory.Functor.initial_of_comp_full_faithful
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : F.Final
⊢ G.Final ↔ (F ⋙ G).Final

Tactic:
⟨fun _ => final_comp _ _, fun _ => final_of_final_comp F G⟩

Premises used: CategoryTheory.Functor.final_of_final_comp, CategoryTheory.Functor.final_comp, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : F.Initial
⊢ G.Initial ↔ (F ⋙ G).Initial

Tactic:
⟨fun _ => initial_comp _ _, fun _ => initial_of_initial_comp F G⟩

Premises used: CategoryTheory.Functor.initial_comp, Iff.intro, CategoryTheory.Functor.initial_of_initial_comp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
c : C
hc : IsTerminal.{v₁, u₁} c
c' : C
this_1 : Inhabited (StructuredArrow.{u_1, v₁, u_1, u₁} c' (fromPUnit c)) :=
  { default := StructuredArrow.mk (Y := default) (hc.from c') }
this : Subsingleton (StructuredArrow.{u_1, v₁, u_1, u₁} c' (fromPUnit c)) := ⋯
⊢ IsConnected (StructuredArrow.{u_1, v₁, u_1, u₁} c' (fromPUnit c))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
c : C
hc : IsInitial.{v₁, u₁} c
c' : C
this_1 : Inhabited (CostructuredArrow.{u_1, v₁, u_1, u₁} (fromPUnit c) c') :=
  { default := CostructuredArrow.mk (Y := default) (hc.to c') }
this : Subsingleton (CostructuredArrow.{u_1, v₁, u_1, u₁} (fromPUnit c) c') := ⋯
⊢ IsConnected (CostructuredArrow.{u_1, v₁, u_1, u₁} (fromPUnit c) c')

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C Dᵒᵖ
inst_2 : F.Initial
⊢ F.leftOp.Final

Tactic:
inferInstanceAs (F.op ⋙ (opOpEquivalence D).functor).Final

Premises used: _private.0.CategoryTheory.Functor.instFinalOppositeLeftOpOfInitial._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C Dᵒᵖ
inst_2 : F.Final
⊢ F.leftOp.Initial

Tactic:
inferInstanceAs (F.op ⋙ (opOpEquivalence D).functor).Initial

Premises used: _private.0.CategoryTheory.Functor.instInitialOppositeLeftOpOfFinal._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} Cᵒᵖ D
inst_2 : F.Initial
⊢ F.rightOp.Final

Tactic:
inferInstanceAs ((opOpEquivalence C).inverse ⋙ F.op).Final

Premises used: _private.0.CategoryTheory.Functor.instFinalOppositeRightOpOfInitial._proof_1