awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsFilteredOrEmpty.{v₁, u₁} C
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
Y : D
X : C
⊢ IsConnected (StructuredArrow Y (Under.forget X ⋙ T))

Tactic:
(final_comp (Under.forget X) T).out _

Premises used: CategoryTheory.Functor.Final.out
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsFilteredOrEmpty.{v₁, u₁} C
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
Y : D
X : C
⊢ IsConnected (StructuredArrow Y (Under.forget X ⋙ T))

Tactic:
exact (final_comp (Under.forget X) T).out _

Premises used: CategoryTheory.Functor.Final.out
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsCofilteredOrEmpty.{v₁, u₁} C
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
Y : D
⊢ (proj T Y).Initial

Tactic:
⟨fun X => ?_⟩

Premises used: CategoryTheory.Functor.Initial.mk
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsCofilteredOrEmpty.{v₁, u₁} C
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
Y : D
refine : ∀ (X : C), IsConnected (CostructuredArrow (proj T Y) X)
⊢ (proj T Y).Initial

Tactic:
refine ⟨fun X => ?_⟩
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsCofilteredOrEmpty.{v₁, u₁} C
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
Y : D
X : C
rw : IsConnected (CostructuredArrow (Over.forget X ⋙ T) Y)
⊢ IsConnected (CostructuredArrow (proj T Y) X)

Tactic:
rw [isConnected_iff_of_equivalence (ofCostructuredArrowProjEquivalence T Y X)]

Premises used: CategoryTheory.isConnected_iff_of_equivalence, CategoryTheory.CostructuredArrow.ofCostructuredArrowProjEquivalence
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsCofilteredOrEmpty.{v₁, u₁} C
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
Y : D
X : C
⊢ IsConnected (CostructuredArrow (Over.forget X ⋙ T) Y)

Tactic:
(initial_comp (Over.forget X) T).out _

Premises used: CategoryTheory.Functor.Initial.out
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsCofilteredOrEmpty.{v₁, u₁} C
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Initial
Y : D
X : C
⊢ IsConnected (CostructuredArrow (Over.forget X ⋙ T) Y)

Tactic:
exact (initial_comp (Over.forget X) T).out _

Premises used: CategoryTheory.Functor.Initial.out
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsFiltered.{v₁, u₁} C
E : Type u₃
inst_3 : Category.{v₃, u₃} E
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : T.Final
S : Functor.{v₂, v₃, u₂, u₃} D E
inst_5 : S.Final
T' : Functor.{v₁, v₃, u₁, u₃} C E
d : D
e : E
u : e ⟶ S.obj d
α : T ⋙ S ⟶ T'
inst_6 : IsIso α
⊢ IsFiltered (StructuredArrow e (T ⋙ S))

Tactic:
haveI : IsFiltered (StructuredArrow e (T ⋙ S)) :=
    (T ⋙ S).final_iff_isFiltered_structuredArrow.mp inferInstance e
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsFiltered.{v₁, u₁} C
E : Type u₃
inst_3 : Category.{v₃, u₃} E
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : T.Final
S : Functor.{v₂, v₃, u₂, u₃} D E
inst_5 : S.Final
T' : Functor.{v₁, v₃, u₁, u₃} C E
d : D
e : E
u : e ⟶ S.obj d
α : T ⋙ S ⟶ T'
inst_6 : IsIso α
this : IsFiltered (StructuredArrow e (T ⋙ S))
⊢ Final (C := StructuredArrow d T) (D := StructuredArrow e T') (map₂ (F := 𝟭 C) u α)

Tactic:
apply final_of_natIso (map₂IsoPreEquivalenceInverseCompProj d e u α).symm

Premises used: CategoryTheory.StructuredArrow.map₂IsoPreEquivalenceInverseCompProj, CategoryTheory.Functor.final_of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsFiltered.{v₁, u₁} C
S S' : D
f : S ⟶ S'
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
⊢ IsIso (𝟙 T)

Tactic:
haveI := NatIso.isIso_of_isIso_app (𝟙 T)
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsFiltered.{v₁, u₁} C
S S' : D
f : S ⟶ S'
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
this : IsIso (𝟙 T)
⊢ Final (C := StructuredArrow S' T) (D := StructuredArrow S T) (map₂ (F := 𝟭 C) (G := 𝟭 D) f (𝟙 T))

Tactic:
apply StructuredArrow.final_map₂_id (S := 𝟭 D) (T := T) (T' := T) f (𝟙 T)

Premises used: CategoryTheory.StructuredArrow.final_map₂_id, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsFiltered.{v₁, u₁} C
S S' : D
f : S ⟶ S'
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
this : IsIso (𝟙 T)
⊢ Final (C := StructuredArrow S' T) (D := StructuredArrow S T) (map₂ (F := 𝟭 C) (G := 𝟭 D) f (𝟙 T))

Tactic:
have : (map₂ (F := 𝟭 C) (G := 𝟭 D) f (𝟙 T)).Final := by
    apply StructuredArrow.final_map₂_id (S := 𝟭 D) (T := T) (T' := T) f (𝟙 T)
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsFiltered.{v₁, u₁} C
S S' : D
f : S ⟶ S'
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
this_1 : IsIso (𝟙 T)
this : Final (C := StructuredArrow S' T) (D := StructuredArrow S T) (map₂ (F := 𝟭 C) (G := 𝟭 D) f (𝟙 T))
⊢ Final (C := StructuredArrow S' T) (map f)

Tactic:
apply final_of_natIso (mapIsoMap₂ f).symm

Premises used: CategoryTheory.Functor.final_of_natIso, CategoryTheory.StructuredArrow.mapIsoMap₂, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsFiltered.{v₁, u₁} C
E : Type u₃
inst_3 : Category.{v₃, u₃} E
X : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : T.Final
S : Functor.{v₂, v₃, u₂, u₃} D E
inst_5 : S.Final
⊢ (post X T S).Final

Tactic:
apply final_of_natIso (postIsoMap₂ X T S).symm

Premises used: CategoryTheory.Functor.final_of_natIso, CategoryTheory.Iso.symm, CategoryTheory.StructuredArrow.postIsoMap₂
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsCofiltered.{v₁, u₁} C
E : Type u₃
inst_3 : Category.{v₃, u₃} E
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : T.Initial
S : Functor.{v₂, v₃, u₂, u₃} D E
inst_5 : S.Initial
d : D
e : E
u : S.obj d ⟶ e
⊢ IsCofiltered (CostructuredArrow (T ⋙ S) e)

Tactic:
have := (T ⋙ S).initial_iff_isCofiltered_costructuredArrow.mp inferInstance e
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsCofiltered.{v₁, u₁} C
E : Type u₃
inst_3 : Category.{v₃, u₃} E
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : T.Initial
S : Functor.{v₂, v₃, u₂, u₃} D E
inst_5 : S.Initial
d : D
e : E
u : S.obj d ⟶ e
this : IsCofiltered (CostructuredArrow (T ⋙ S) e)
⊢ Initial (C := CostructuredArrow T d) (D := CostructuredArrow (T ⋙ S) e) (map₂ (F := 𝟭 C) (𝟙 (T ⋙ S)) u)

Tactic:
apply initial_of_natIso (map₂IsoPreEquivalenceInverseCompProj T S d e u).symm

Premises used: CategoryTheory.CostructuredArrow.map₂IsoPreEquivalenceInverseCompProj, CategoryTheory.Iso.symm, CategoryTheory.Functor.initial_of_natIso
-- Module: Mathlib.CategoryTheory.Filtered.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 : IsCofiltered.{v₁, u₁} C
E : Type u₃
inst_3 : Category.{v₃, u₃} E
X : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : T.Initial
S : Functor.{v₂, v₃, u₂, u₃} D E
inst_5 : S.Initial
⊢ (post T S X).Initial

Tactic:
apply initial_of_natIso (postIsoMap₂ X T S).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.CostructuredArrow.postIsoMap₂, CategoryTheory.Functor.initial_of_natIso
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
h₁ : ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (d ⟶ obj (Pi.eval I s) c)
h₂ :
  ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : d ⟶ obj (Pi.eval I s) c),
    ∃ (c' : (i : α) → I i) (t : c ⟶ c'), s_1 ≫ map (Pi.eval I s) t = s' ≫ map (Pi.eval I s) t
⊢ Final (Pi.eval I s)

Tactic:
apply Functor.final_of_exists_of_isFiltered

Premises used: CategoryTheory.Functor.final_of_exists_of_isFiltered
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
i : I s
⊢ i ⟶ obj (Pi.eval I s) (Function.update (β := I) (fun (t : α) ↦ Nonempty.some ⋯) s i)

Tactic:
simpa using 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
⊢ ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (d ⟶ obj (Pi.eval I s) c)

Tactic:
exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : d ⟶ obj (Pi.eval I s) c
c't : (s : α) → (c' : I s) × (c s ⟶ c') :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g))
⊢ ∃ (c' : (i : α) → I i) (t : c ⟶ c'), f ≫ map (Pi.eval I s) t = g ≫ map (Pi.eval I s) t

Tactic:
⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩

Premises used: Sigma.fst, Exists.intro, Sigma.snd
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : d ⟶ obj (Pi.eval I s) c
c't : (s : α) → (c' : I s) × (c s ⟶ c') :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g))
h₂ :
  Eq (α := d ⟶ obj (Pi.eval I s) fun (t : α) ↦ (c't t).fst (β := fun (c' : I t) ↦ c t ⟶ c'))
    (f ≫ map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c t ⟶ c'))
    (g ≫ map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c t ⟶ c'))
⊢ ∃ (c' : (i : α) → I i) (t : c ⟶ c'), f ≫ map (Pi.eval I s) t = g ≫ map (Pi.eval I s) t

Tactic:
refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : d ⟶ obj (Pi.eval I s) c
c't : (s : α) → (c' : I s) × (c s ⟶ c') :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g))
h₂ :
  Eq (α :=
    d ⟶
      Sigma.fst (β := fun (c' : I s) ↦ c s ⟶ c')
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)) s))
    (f ≫
      Sigma.snd (β := fun (c' : I s) ↦ c s ⟶ c')
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)) s))
    (g ≫
      Sigma.snd (β := fun (c' : I s) ↦ c s ⟶ c')
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)) s))
⊢ Eq (α := d ⟶ obj (Pi.eval I s) fun (t : α) ↦ (c't t).fst (β := fun (c' : I t) ↦ c t ⟶ c'))
    (f ≫ map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c t ⟶ c'))
    (g ≫ map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c t ⟶ c'))

Tactic:
dsimp only [Pi.eval_obj, Pi.eval_map, c't]

Premises used: CategoryTheory.Pi.eval_obj, CategoryTheory.Pi.eval_map
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : d ⟶ obj (Pi.eval I s) c
c't : (s : α) → (c' : I s) × (c s ⟶ c') :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g))
h₂ :
  f ≫ (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)).snd (β := fun (c' : I s) ↦ c s ⟶ c') =
    g ≫ (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)).snd (β := fun (c' : I s) ↦ c s ⟶ c')
⊢ Eq (α :=
    d ⟶
      Sigma.fst (β := fun (c' : I s) ↦ c s ⟶ c')
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)) s))
    (f ≫
      Sigma.snd (β := fun (c' : I s) ↦ c s ⟶ c')
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)) s))
    (g ≫
      Sigma.snd (β := fun (c' : I s) ↦ c s ⟶ c')
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)) s))

Tactic:
rw [Function.update_self]

Premises used: Function.update_self
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : d ⟶ obj (Pi.eval I s) c
c't : (s : α) → (c' : I s) × (c s ⟶ c') :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c s ⟶ c'))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c t ⟶ c') (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g))
⊢ f ≫ (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)).snd (β := fun (c' : I s) ↦ c s ⟶ c') =
    g ≫ (Sigma.mk (β := fun (c' : I s) ↦ c s ⟶ c') (coeq f g) (coeqHom f g)).snd (β := fun (c' : I s) ↦ c s ⟶ c')

Tactic:
simpa using coeq_condition _ _

Premises used: CategoryTheory.IsFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsFiltered.{v₂, u₂} (I s)
s : α
h₁ : ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (d ⟶ obj (Pi.eval I s) c)
h₂ h₃ :
  ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : d ⟶ obj (Pi.eval I s) c),
    ∃ (c' : (i : α) → I i) (t : c ⟶ c'), s_1 ≫ map (Pi.eval I s) t = s' ≫ map (Pi.eval I s) t
⊢ Final (Pi.eval I s)

Tactic:
classical
  apply Functor.final_of_exists_of_isFiltered
  · exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
  · intro d c f g
    let c't : (∀ s, (c' : I s) × (c s ⟶ c')) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨coeq f g, coeqHom f g⟩
    refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
    dsimp only [Pi.eval_obj, Pi.eval_map, c't]
    rw [Function.update_self]
    simpa using coeq_condition _ _

Premises used: CategoryTheory.Functor.final_of_exists_of_isFiltered, CategoryTheory.IsFiltered.coeq_condition, CategoryTheory.Pi.eval_obj, Function.update_self, CategoryTheory.Pi.eval_map
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
h₁ : ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (obj (Pi.eval I s) c ⟶ d)
h₂ :
  ∀ {d : I s} {c : (i : α) → I i} (s_1 s' : obj (Pi.eval I s) c ⟶ d),
    ∃ (c' : (i : α) → I i) (t : c' ⟶ c), map (Pi.eval I s) t ≫ s_1 = map (Pi.eval I s) t ≫ s'
⊢ Initial (Pi.eval I s)

Tactic:
apply Functor.initial_of_exists_of_isCofiltered

Premises used: CategoryTheory.Functor.initial_of_exists_of_isCofiltered
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
i : I s
⊢ obj (Pi.eval I s) (Function.update (β := I) (fun (t : α) ↦ Nonempty.some ⋯) s i) ⟶ i

Tactic:
simpa using 𝟙 _

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
⊢ ∀ (d : I s), ∃ (c : (i : α) → I i), Nonempty.{v₂ + 1} (obj (Pi.eval I s) c ⟶ d)

Tactic:
exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : obj (Pi.eval I s) c ⟶ d
c't : (s : α) → (c' : I s) × (c' ⟶ c s) :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g))
⊢ ∃ (c' : (i : α) → I i) (t : c' ⟶ c), map (Pi.eval I s) t ≫ f = map (Pi.eval I s) t ≫ g

Tactic:
⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩

Premises used: Sigma.fst, Exists.intro, Sigma.snd
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : obj (Pi.eval I s) c ⟶ d
c't : (s : α) → (c' : I s) × (c' ⟶ c s) :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g))
h₂ :
  Eq (α := (obj (Pi.eval I s) fun (t : α) ↦ (c't t).fst (β := fun (c' : I t) ↦ c' ⟶ c t)) ⟶ d)
    ((map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c' ⟶ c t)) ≫ f)
    ((map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c' ⟶ c t)) ≫ g)
⊢ ∃ (c' : (i : α) → I i) (t : c' ⟶ c), map (Pi.eval I s) t ≫ f = map (Pi.eval I s) t ≫ g

Tactic:
refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
-- Module: Mathlib.CategoryTheory.Filtered.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
α : Type u₁
I : α → Type u₂
inst_2 : (s : α) → Category.{v₂, u₂} (I s)
inst_3 : ∀ (s : α), IsCofiltered.{v₂, u₂} (I s)
s : α
d : I s
c : (i : α) → I i
f g : obj (Pi.eval I s) c ⟶ d
c't : (s : α) → (c' : I s) × (c' ⟶ c s) :=
  Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
    (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
    (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g))
h₂ :
  Eq.{v₂ + 1} (α :=
    Sigma.fst (β := fun (c' : I s) ↦ c' ⟶ c s)
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g) : (c' : I s) × (c' ⟶ c s)) s) ⟶
      d)
    (Sigma.snd (β := fun (c' : I s) ↦ c' ⟶ c s)
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g) : (c' : I s) × (c' ⟶ c s)) s) ≫
      f)
    (Sigma.snd (β := fun (c' : I s) ↦ c' ⟶ c s)
        (Function.update (β := fun (s : α) ↦ (c' : I s) × (c' ⟶ c s))
          (fun (t : α) ↦ Sigma.mk (β := fun (c' : I t) ↦ c' ⟶ c t) (c t) (𝟙 (c t))) s
          (Sigma.mk (β := fun (c' : I s) ↦ c' ⟶ c s) (eq f g) (eqHom f g) : (c' : I s) × (c' ⟶ c s)) s) ≫
      g)
⊢ Eq (α := (obj (Pi.eval I s) fun (t : α) ↦ (c't t).fst (β := fun (c' : I t) ↦ c' ⟶ c t)) ⟶ d)
    ((map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c' ⟶ c t)) ≫ f)
    ((map (Pi.eval I s) fun (t : α) ↦ (c't t).snd (β := fun (c' : I t) ↦ c' ⟶ c t)) ≫ g)

Tactic:
dsimp only [Pi.eval_obj, Pi.eval_map, c't]

Premises used: CategoryTheory.Pi.eval_obj, CategoryTheory.Pi.eval_map