awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
⊢ Nonempty (IsLimit (H.mapCone c))
have refine : IsLimit (Cone.whisker F (H.mapCone c))
Tactic: refine ⟨isLimitWhiskerEquiv F _ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
⊢ Nonempty (IsLimit c)
have refine : IsLimit (H.mapCone (Cone.whisker F c))
Tactic: refine ⟨isLimitWhiskerEquiv F _ (isLimitOfReflects H ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : CreatesLimit (F ⋙ G) H
c : Cone (G ⋙ H)
hc : IsLimit c
⊢ LiftableCone G H c
have refine : H.mapCone
    (obj (C := Cone (F ⋙ G)) extendCone
      (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
        (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc))) ≅
  c
Tactic: refine ⟨(extendCone (F := F)).obj (liftLimit ((isLimitWhiskerEquiv F _).symm hc)), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : CreatesLimit (F ⋙ G) H
c : Cone (G ⋙ H)
hc : IsLimit c
i : H.mapCone
    (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
      (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)) ≅
  Cone.whisker F c :=
  liftedLimitMapsToOriginal (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)
⊢ H.mapCone
      (obj (C := Cone (F ⋙ G)) extendCone
        (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
          (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc))) ≅
    c
have refine : H.mapCone
    (obj (C := Cone (F ⋙ G)) extendCone
      (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
        (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc))) ≅
  obj (C := Cone (F ⋙ G ⋙ H)) extendCone
    (H.mapCone
      (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
        (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)))
Tactic: refine ?_ ≪≫ ((extendCone (F := F)).mapIso i) ≪≫ ((conesEquiv F (G ⋙ H)).counitIso.app _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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))
⊢ (F ⋙ G).Final
have rw : ∀ (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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))
⊢ ∀ (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))
have 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))
Tactic: rw [final_iff_comp_equivalence F s₂.functor, final_iff_equivalence_comp s₁.inverse,
    final_iff_isIso_colimit_pre] at hF
Cleared hypotheses: hF, s₃, i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
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 ⋙ 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))
have 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))
Tactic: rw [final_iff_comp_equivalence G s₃.functor, final_iff_equivalence_comp s₂.inverse,
    final_iff_isIso_colimit_pre] at hG
Cleared hypotheses: hG, i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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)
    (colimit.pre H ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))
have 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)))
Tactic: rw [← colimit.pre_pre]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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).Initial
have suffices : (F ⋙ G).op.Final
Tactic: suffices Final (F ⋙ G).op from initial_of_final_op _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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))
⊢ G.Final
have 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))
Tactic: rw [final_iff_comp_equivalence G s₃.functor, final_iff_equivalence_comp s₂.inverse,
    final_iff_isIso_colimit_pre]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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))
⊢ ∀ (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))
have 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))
Tactic: rw [final_iff_comp_equivalence F s₂.functor, final_iff_equivalence_comp s₁.inverse,
    final_iff_isIso_colimit_pre] at hF
Cleared hypotheses: hF, s₃, _i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
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 ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
      (colimit.pre G_1 (s₂.inverse ⋙ G ⋙ s₃.functor))
have 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))
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
Cleared hypotheses: hFG, _i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
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 ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))
have 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))
Tactic: replace hFG := hFG H
Cleared hypotheses: hFG
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
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 ⋙ G ⋙ s₃.functor) ⋙ H)) (Y := colimit H)
    (colimit.pre H (s₂.inverse ⋙ G ⋙ s₃.functor))
have 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)))
Tactic: rw [← colimit.pre_pre] at hFG
Cleared hypotheses: hFG
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
⊢ G.Initial
have suffices : G.op.Final
Tactic: suffices Final G.op from initial_of_final_op _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
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
⊢ G.op.Final
have this : (F.op ⋙ G.op).Final
Tactic: have : Final (F.op ⋙ G.op) := show Final (F ⋙ G).op from inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Final
inst_3 : IsFilteredOrEmpty.{v₁, u₁} C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop :=
  fun (h : StructuredArrow X F) ↦
    ∃ (Z : C) (q₁ : h.right ⟶ Z) (q₂ : Final.lift F Y ⟶ Z), h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ ∃ (Z : D) (h : Y ⟶ Z), f ≫ h = g ≫ h
have rsuffices : ∀ (Z : C) (q₁ : (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)).right ⟶ Z)
  (q₂ : Final.lift F Y ⟶ Z)
  (h :
    (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ =
      f ≫ Final.homToLift F Y ≫ F.map q₂),
  ∃ (Z : D) (h : Y ⟶ Z), f ≫ h = g ≫ h
Tactic: rsuffices ⟨Z, q₁, q₂, h⟩ : Nonempty (P (StructuredArrow.mk (g ≫ Final.homToLift F Y)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Final
inst_3 : IsFilteredOrEmpty.{v₁, u₁} C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop :=
  fun (h : StructuredArrow X F) ↦
    ∃ (Z : C) (q₁ : h.right ⟶ Z) (q₂ : Final.lift F Y ⟶ Z), h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
rsuffices :
  ∀ (Z : C) (q₁ : (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)).right ⟶ Z)
    (q₂ : Final.lift F Y ⟶ Z)
    (h :
      (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ =
        f ≫ Final.homToLift F Y ≫ F.map q₂),
    ∃ (Z : D) (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ ∃ (Z : D) (h : Y ⟶ Z), f ≫ h = g ≫ h
have rsuffices₁ : Nonempty (P (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)))
Tactic: rsuffices ⟨Z, q₁, q₂, h⟩ : Nonempty (P (StructuredArrow.mk (g ≫ Final.homToLift F Y)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Final
inst_3 : IsFilteredOrEmpty.{v₁, u₁} C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop :=
  fun (h : StructuredArrow X F) ↦
    ∃ (Z : C) (q₁ : h.right ⟶ Z) (q₂ : Final.lift F Y ⟶ Z), h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
Z : C
q₁ : (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)).right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
h :
  (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ =
    f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ ∃ (Z : D) (h : Y ⟶ Z), f ≫ h = g ≫ h
have refine : Eq (α := X ⟶ F.obj (IsFiltered.coeq q₁ q₂)) (f ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂))
  (g ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂))
Tactic: refine ⟨F.obj (IsFiltered.coeq q₁ q₂),
        Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Final
inst_3 : IsFilteredOrEmpty.{v₁, u₁} C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop :=
  fun (h : StructuredArrow X F) ↦
    ∃ (Z : C) (q₁ : h.right ⟶ Z) (q₂ : Final.lift F Y ⟶ Z), h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
Z : C
q₁ : (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)).right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
h :
  (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ =
    f ≫ Final.homToLift F Y ≫ F.map q₂
| f ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂)
have rw : f ≫ Final.homToLift F Y ≫ F.map (q₂ ≫ IsFiltered.coeqHom q₁ q₂)
Tactic: rw [IsFiltered.coeq_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Final
inst_3 : IsFilteredOrEmpty.{v₁, u₁} C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop :=
  fun (h : StructuredArrow X F) ↦
    ∃ (Z : C) (q₁ : h.right ⟶ Z) (q₂ : Final.lift F Y ⟶ Z), h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
Z : C
q₁ : (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)).right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
h :
  (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)).hom ≫ F.map q₁ =
    f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ Eq (α := X ⟶ F.obj (IsFiltered.coeq q₁ q₂)) (f ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂))
    (g ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂))
have conv_lhs : Eq (α := X ⟶ F.obj (IsFiltered.coeq q₁ q₂)) (f ≫ Final.homToLift F Y ≫ F.map (q₂ ≫ IsFiltered.coeqHom q₁ q₂))
  (g ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂))
Tactic: conv_lhs => rw [IsFiltered.coeq_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
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
inst_2 : F.Final
inst_3 : IsFilteredOrEmpty.{v₁, u₁} C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop :=
  fun (h : StructuredArrow X F) ↦
    ∃ (Z : C) (q₁ : h.right ⟶ Z) (q₂ : Final.lift F Y ⟶ Z), h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ Nonempty (P (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)))
have h₀ : P (StructuredArrow.mk (Y := Final.lift F Y) (f ≫ Final.homToLift F Y))
Tactic: have h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y)) := ⟨_, 𝟙 _, 𝟙 _, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Final
inst_3 : IsFilteredOrEmpty.{v₁, u₁} C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop :=
  fun (h : StructuredArrow X F) ↦
    ∃ (Z : C) (q₁ : h.right ⟶ Z) (q₂ : Final.lift F Y ⟶ Z), h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (Y := Final.lift F Y) (f ≫ Final.homToLift F Y))
⊢ Nonempty (P (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)))
have refine_1 : ∀ {j₁ j₂ : StructuredArrow X F} (x : j₁ ⟶ j₂), P j₁ → P j₂
Tactic: refine isPreconnected_induction P ?_ ?_ h₀ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_2 : F.Final
inst_3 : IsFilteredOrEmpty.{v₁, u₁} C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop :=
  fun (h : StructuredArrow X F) ↦
    ∃ (Z : C) (q₁ : h.right ⟶ Z) (q₂ : Final.lift F Y ⟶ Z), h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (Y := Final.lift F Y) (f ≫ Final.homToLift F Y))
refine_1 : ∀ {j₁ j₂ : StructuredArrow X F} (x : j₁ ⟶ j₂), P j₁ → P j₂
⊢ Nonempty (P (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)))
have refine_2 : ∀ {j₁ j₂ : StructuredArrow X F} (x : j₁ ⟶ j₂), P j₂ → P j₁
Tactic: refine isPreconnected_induction P ?_ ?_ h₀ _