awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.rightOp.Initial

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

Premises used: _private.0.CategoryTheory.Functor.instInitialOppositeRightOpOfFinal._proof_1
-- Module: Mathlib.CategoryTheory.Limits.Final
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
rsuffices₁ : Nonempty (P (StructuredArrow.mk (Y := Final.lift F Y) (g ≫ Final.homToLift F Y)))
⊢ ∃ (Z : D) (h : Y ⟶ Z), f ≫ h = g ≫ h

Tactic:
rsuffices ⟨Z, q₁, q₂, h⟩ : Nonempty (P (StructuredArrow.mk (g ≫ Final.homToLift F Y)))

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.StructuredArrow.mk, Nonempty, CategoryTheory.Functor.Final.homToLift
-- Module: Mathlib.CategoryTheory.Limits.Final
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

Tactic:
⟨F.obj (IsFiltered.coeq q₁ q₂),
        Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂), ?_⟩

Premises used: CategoryTheory.IsFiltered.coeqHom, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsFiltered.coeq, CategoryTheory.Functor.obj, CategoryTheory.Functor.Final.homToLift
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
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₂))
⊢ ∃ (Z : D) (h : Y ⟶ Z), f ≫ h = g ≫ h

Tactic:
refine ⟨F.obj (IsFiltered.coeq q₁ q₂),
        Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂), ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
rw : f ≫ Final.homToLift F Y ≫ F.map (q₂ ≫ IsFiltered.coeqHom q₁ q₂)
| f ≫ Final.homToLift F Y ≫ F.map (q₁ ≫ IsFiltered.coeqHom q₁ q₂)

Tactic:
rw [IsFiltered.coeq_condition]

Premises used: CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
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₂))
⊢ 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]

Premises used: CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂))

Tactic:
simp only [F.map_comp, ← reassoc_of% h, StructuredArrow.mk_hom_eq_self, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.StructuredArrow.mk_hom_eq_self
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
⊢ (StructuredArrow.mk (Y := Final.lift F Y) (f ≫ Final.homToLift F Y)).hom ≫
      F.map (𝟙 (StructuredArrow.mk (Y := Final.lift F Y) (f ≫ Final.homToLift F Y)).right) =
    f ≫ Final.homToLift F Y ≫ F.map (𝟙 (Final.lift F Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
⊢ 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⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
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)))

Tactic:
isPreconnected_induction P ?_ ?_ h₀ _

Premises used: CategoryTheory.isPreconnected_induction
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
refine_2 : ∀ {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)))

Tactic:
refine isPreconnected_induction P ?_ ?_ h₀ _

Premises used: CategoryTheory.isPreconnected_induction
-- Module: Mathlib.CategoryTheory.Limits.Final
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))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : U.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : U.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
refine_1 : ∀ (W : C) (q₃ : Z ⟶ W) (q₄ : V.right ⟶ W) (hq' : q₁ ≫ q₃ = StructuredArrow.Hom.right h ≫ q₄), P V
⊢ P V

Tactic:
obtain ⟨W, q₃, q₄, hq'⟩ := IsFiltered.span q₁ h.right

Premises used: CategoryTheory.IsFiltered.span, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.Limits.Final
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))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : U.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : U.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
W : C
q₃ : Z ⟶ W
q₄ : V.right ⟶ W
hq' : q₁ ≫ q₃ = StructuredArrow.Hom.right h ≫ q₄
⊢ P V

Tactic:
⟨W, q₄, q₂ ≫ q₃, ?_⟩

Premises used: Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Limits.Final
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))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : U.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : U.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
W : C
q₃ : Z ⟶ W
q₄ : V.right ⟶ W
hq' : q₁ ≫ q₃ = StructuredArrow.Hom.right h ≫ q₄
refine_1 : V.hom ≫ F.map q₄ = f ≫ Final.homToLift F Y ≫ F.map (q₂ ≫ q₃)
⊢ P V

Tactic:
refine ⟨W, q₄, q₂ ≫ q₃, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
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))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : U.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : U.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
W : C
q₃ : Z ⟶ W
q₄ : V.right ⟶ W
hq' : q₁ ≫ q₃ = StructuredArrow.Hom.right h ≫ q₄
refine_1 : V.hom ≫ F.map q₄ = f ≫ Final.homToLift F Y ≫ F.map q₂ ≫ F.map q₃
refine_1₁ : V.hom ≫ F.map q₄ = U.hom ≫ F.map q₁ ≫ F.map q₃
refine_1₂ : V.hom ≫ F.map q₄ = U.hom ≫ F.map (q₁ ≫ q₃)
refine_1₃ : V.hom ≫ F.map q₄ = U.hom ≫ F.map (StructuredArrow.Hom.right h ≫ q₄)
refine_1₄ : V.hom ≫ F.map q₄ = U.hom ≫ F.map (StructuredArrow.Hom.right h) ≫ F.map q₄
refine_1₅ refine_1₆ : V.hom ≫ F.map q₄ = V.hom ≫ F.map q₄
⊢ V.hom ≫ F.map q₄ = f ≫ Final.homToLift F Y ≫ F.map (q₂ ≫ q₃)

Tactic:
rw [F.map_comp, ← reassoc_of% hq, ← F.map_comp, hq', F.map_comp, StructuredArrow.w_assoc]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.StructuredArrow.w_assoc
-- Module: Mathlib.CategoryTheory.Limits.Final
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))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : V.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : V.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ U.hom ≫ F.map (StructuredArrow.Hom.right h ≫ q₁) = f ≫ Final.homToLift F Y ≫ F.map q₂

Tactic:
simp only [F.map_comp, StructuredArrow.w_assoc, hq]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.StructuredArrow.w_assoc
-- Module: Mathlib.CategoryTheory.Limits.Final
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))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : V.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : V.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
⊢ P U

Tactic:
exact ⟨Z, h.right ≫ q₁, q₂, by simp only [F.map_comp, StructuredArrow.w_assoc, hq]⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
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 : IsFiltered.{v₁, u₁} C
⊢ IsFiltered.{v₂, u₂} D

Tactic:
{ IsFilteredOrEmpty.of_final F with
  nonempty := Nonempty.map F.obj IsFiltered.nonempty }

Premises used: CategoryTheory.IsFilteredOrEmpty.of_final, CategoryTheory.IsFiltered.mk
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : IsCofilteredOrEmpty.{v₁, u₁} C
⊢ IsCofilteredOrEmpty.{v₂, u₂} D

Tactic:
have : IsFilteredOrEmpty Dᵒᵖ := IsFilteredOrEmpty.of_final F.op
  isCofilteredOrEmpty_of_isFilteredOrEmpty_op _

Premises used: CategoryTheory.Functor.op, CategoryTheory.isCofilteredOrEmpty_of_isFilteredOrEmpty_op, CategoryTheory.IsFilteredOrEmpty.of_final
-- Module: Mathlib.CategoryTheory.Limits.Final
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
inst_3 : IsCofiltered.{v₁, u₁} C
⊢ IsCofiltered.{v₂, u₂} D

Tactic:
have : IsFiltered Dᵒᵖ := IsFiltered.of_final F.op
  isCofiltered_of_isFiltered_op _

Premises used: CategoryTheory.Functor.op, CategoryTheory.IsFiltered.of_final, CategoryTheory.isCofiltered_of_isFiltered_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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
S : Functor.{v₂, v₃, u₂, u₃} D E
X : E
⊢ (pre X T S).Final

Tactic:
⟨fun f => ?_⟩

Premises used: CategoryTheory.Functor.Final.mk
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
S : Functor.{v₂, v₃, u₂, u₃} D E
X : E
refine : ∀ (f : StructuredArrow X S), IsConnected (StructuredArrow f (pre X T S))
⊢ (pre X T S).Final

Tactic:
refine ⟨fun f => ?_⟩
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
S : Functor.{v₂, v₃, u₂, u₃} D E
X : E
f : StructuredArrow X S
rw : IsConnected (StructuredArrow f.right T)
⊢ IsConnected (StructuredArrow f (pre X T S))

Tactic:
rw [isConnected_iff_of_equivalence (StructuredArrow.preEquivalence T f)]

Premises used: CategoryTheory.isConnected_iff_of_equivalence, CategoryTheory.StructuredArrow.preEquivalence
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
S : Functor.{v₂, v₃, u₂, u₃} D E
X : E
f : StructuredArrow X S
⊢ IsConnected (StructuredArrow f.right T)

Tactic:
Final.out f.right

Premises used: CategoryTheory.Functor.Final.out, CategoryTheory.StructuredArrow.right
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
S : Functor.{v₂, v₃, u₂, u₃} D E
X : E
f : StructuredArrow X S
⊢ IsConnected (StructuredArrow f.right T)

Tactic:
exact Final.out f.right

Premises used: CategoryTheory.Functor.Final.out, CategoryTheory.StructuredArrow.right
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
S : Functor.{v₂, v₃, u₂, u₃} D E
X : E
⊢ (pre T S X).Initial

Tactic:
⟨fun f => ?_⟩

Premises used: CategoryTheory.Functor.Initial.mk
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
S : Functor.{v₂, v₃, u₂, u₃} D E
X : E
refine : ∀ (f : CostructuredArrow S X), IsConnected (CostructuredArrow (pre T S X) f)
⊢ (pre T S X).Initial

Tactic:
refine ⟨fun f => ?_⟩
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
S : Functor.{v₂, v₃, u₂, u₃} D E
X : E
f : CostructuredArrow S X
rw : IsConnected (CostructuredArrow T f.left)
⊢ IsConnected (CostructuredArrow (pre T S X) f)

Tactic:
rw [isConnected_iff_of_equivalence (CostructuredArrow.preEquivalence T f)]

Premises used: CategoryTheory.isConnected_iff_of_equivalence, CategoryTheory.CostructuredArrow.preEquivalence
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
S : Functor.{v₂, v₃, u₂, u₃} D E
X : E
f : CostructuredArrow S X
⊢ IsConnected (CostructuredArrow T f.left)

Tactic:
Initial.out f.left

Premises used: CategoryTheory.Functor.Initial.out, CategoryTheory.CostructuredArrow.left
-- 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
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
S : Functor.{v₂, v₃, u₂, u₃} D E
X : E
f : CostructuredArrow S X
⊢ IsConnected (CostructuredArrow T f.left)

Tactic:
exact Initial.out f.left

Premises used: CategoryTheory.Functor.Initial.out, CategoryTheory.CostructuredArrow.left
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
out : ∀ (d : Grothendieck F), IsConnected (StructuredArrow d (pre F G))
⊢ (pre F G).Final

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
out :
  ∀ (u : Discrete PUnit.{1}) (c : C) (g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c),
    IsConnected (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G))
⊢ IsConnected (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G))

Tactic:
let ⟨u, c, g⟩ : Nonempty (StructuredArrow d G) := inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
⊢ (obj (fromPUnit { base := d, fiber := f : Grothendieck F }) u).base ⟶
    ((pre F G).obj { base := c, fiber := (F.map g).toFunctor.obj f : Grothendieck (G ⋙ F) }).base

Tactic:
exact g
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
⊢ (F.map g).toFunctor.obj (obj (fromPUnit { base := d, fiber := f : Grothendieck F }) u).fiber ⟶
    ((pre F G).obj { base := c, fiber := (F.map g).toFunctor.obj f }).fiber

Tactic:
exact 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : D ⥤ Cat
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : G.Final
d : D
f : (↑(F.obj d) : Type u_2)
u : Discrete PUnit.{1}
c : C
g : obj.{0, v₂, 0, u₂} (fromPUnit d) u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)) := ⋯
out : ∀ (j₁ j₂ : StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G)), Zigzag j₁ j₂
⊢ IsConnected (StructuredArrow { base := d, fiber := f : Grothendieck F } (pre F G))

Tactic:
apply zigzag_isConnected

Premises used: CategoryTheory.zigzag_isConnected