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
inst_2 : IsCofiltered.{v₁, u₁} C
X : D
hX : IsInitial.{v₂, u₂} X
⊢ Initial.{v₁, v₂, u₁, u₂} (obj (const C) X)

Tactic:
Functor.initial_of_exists_of_isCofiltered _ (fun _ => ⟨IsCofiltered.nonempty.some, ⟨hX.to _⟩⟩)
    (fun {_ c} _ _ => ⟨c, 𝟙 _, hX.hom_ext _ _⟩)

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Functor.initial_of_exists_of_isCofiltered, CategoryTheory.CategoryStruct.id, Nonempty.some, Nonempty.intro, CategoryTheory.Functor.map, CategoryTheory.Limits.IsInitial.to, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsCofiltered.nonempty, CategoryTheory.Functor.const, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : IsCofiltered.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
⊢ Initial.{v₁, v₂, u₁, u₂} (obj (const C) (initial.{v₂, u₂} D))

Tactic:
Functor.initial_const_of_isInitial initialIsInitial

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Functor.initial_const_of_isInitial
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
c c' : C
obtain :
  ∀ (c₀ : C) (f : IsFiltered.max.{v₂, u₂} (F.obj c) (F.obj c') ⟶ F.obj c₀), ∃ (Z : C) (x : c ⟶ Z) (x : c' ⟶ Z), True
⊢ ∃ (Z : C) (x : c ⟶ Z) (x : c' ⟶ Z), True

Tactic:
obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.max (F.obj c) (F.obj c'))

Premises used: CategoryTheory.IsFiltered.max, CategoryTheory.Functor.obj
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
c c' c₀ : C
f : IsFiltered.max.{v₂, u₂} (F.obj c) (F.obj c') ⟶ F.obj c₀
⊢ ∃ (Z : C) (x : c ⟶ Z) (x : c' ⟶ Z), True

Tactic:
⟨c₀, F.preimage (IsFiltered.leftToMax _ _ ≫ f),
      F.preimage (IsFiltered.rightToMax _ _ ≫ f), trivial⟩

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.IsFiltered.rightToMax, trivial, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsFiltered.leftToMax
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
c c' c₀ : C
f : IsFiltered.max.{v₂, u₂} (F.obj c) (F.obj c') ⟶ F.obj c₀
⊢ ∃ (Z : C) (x : c ⟶ Z) (x : c' ⟶ Z), True

Tactic:
exact ⟨c₀, F.preimage (IsFiltered.leftToMax _ _ ≫ f),
      F.preimage (IsFiltered.rightToMax _ _ ≫ f), trivial⟩
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
c c' : C
f g : c ⟶ c'
obtain : ∀ (c₀ : C) (f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀), ∃ (Z : C) (h : c' ⟶ Z), f ≫ h = g ≫ h
⊢ ∃ (Z : C) (h : c' ⟶ Z), f ≫ h = g ≫ h

Tactic:
obtain ⟨c₀, ⟨f₀⟩⟩ := h (IsFiltered.coeq (F.map f) (F.map g))

Premises used: CategoryTheory.Functor.map, CategoryTheory.IsFiltered.coeq
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
⊢ ∃ (Z : C) (h : c' ⟶ Z), f ≫ h = g ≫ h

Tactic:
⟨_, F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀), F.map_injective ?_⟩

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.IsFiltered.coeqHom, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_injective
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
refine :
  F.map (f ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀)) =
    F.map (g ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀))
⊢ ∃ (Z : C) (h : c' ⟶ Z), f ≫ h = g ≫ h

Tactic:
refine ⟨_, F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀), F.map_injective ?_⟩
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
c c' : C
f g : c ⟶ c'
c₀ : C
f₀ : IsFiltered.coeq (F.map f) (F.map g) ⟶ F.obj c₀
⊢ F.map (f ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀)) =
    F.map (g ≫ F.preimage (IsFiltered.coeqHom (F.map f) (F.map g) ≫ f₀))

Tactic:
simp [reassoc_of% (IsFiltered.coeq_condition (F.map f) (F.map g))]

Premises used: CategoryTheory.Functor.map, 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
inst_2 : IsCofilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
suffices : IsFilteredOrEmpty.{v₁, u₁} Cᵒᵖ
⊢ IsCofilteredOrEmpty.{v₁, u₁} C

Tactic:
suffices IsFilteredOrEmpty Cᵒᵖ from isCofilteredOrEmpty_of_isFilteredOrEmpty_op _
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
⊢ IsFilteredOrEmpty.{v₁, u₁} Cᵒᵖ

Tactic:
IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)

Premises used: CategoryTheory.Functor.op, CategoryTheory.IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
refine : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
⊢ IsFilteredOrEmpty.{v₁, u₁} Cᵒᵖ

Tactic:
refine IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)

Premises used: CategoryTheory.Functor.op, CategoryTheory.IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
d : Dᵒᵖ
obtain : ∀ (c : C) (f : F.obj c ⟶ unop d), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
⊢ ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)

Tactic:
obtain ⟨c, ⟨f⟩⟩ := h d.unop

Premises used: Opposite.unop
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
d : Dᵒᵖ
c : C
f : F.obj c ⟶ unop d
⊢ ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)

Tactic:
⟨op c, ⟨f.op⟩⟩

Premises used: Quiver.Hom.op, Nonempty.intro, Opposite.op, Exists.intro
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
d : Dᵒᵖ
c : C
f : F.obj c ⟶ unop d
⊢ ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)

Tactic:
exact ⟨op c, ⟨f.op⟩⟩
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
⊢ Nonempty D

Tactic:
have : Nonempty D := IsFiltered.nonempty
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : Nonempty D
obtain : ∀ (c : C), Nonempty C
⊢ Nonempty C

Tactic:
obtain ⟨c, -⟩ := h (Classical.arbitrary D)

Premises used: Classical.arbitrary
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : Nonempty D
c : C
⊢ Nonempty C

Tactic:
⟨c⟩

Premises used: Nonempty.intro
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : Nonempty D
c : C
⊢ Nonempty C

Tactic:
exact ⟨c⟩
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
⊢ Nonempty D

Tactic:
have : Nonempty D := IsCofiltered.nonempty
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
this : Nonempty D
obtain : ∀ (c : C), Nonempty C
⊢ Nonempty C

Tactic:
obtain ⟨c, -⟩ := h (Classical.arbitrary D)

Premises used: Classical.arbitrary
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
this : Nonempty D
c : C
⊢ Nonempty C

Tactic:
⟨c⟩

Premises used: Nonempty.intro
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
this : Nonempty D
c : C
⊢ Nonempty C

Tactic:
exact ⟨c⟩
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
⊢ IsFilteredOrEmpty.{v₁, u₁} C

Tactic:
have := IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F h
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : IsFilteredOrEmpty.{v₁, u₁} C
⊢ F.Final

Tactic:
Functor.final_of_exists_of_isFiltered F h (fun {d c} s s' => ?_)

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
inst_2 : IsFilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : IsFilteredOrEmpty.{v₁, u₁} C
refine : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
⊢ F.Final

Tactic:
refine Functor.final_of_exists_of_isFiltered F h (fun {d c} s s' => ?_)

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
inst_2 : IsFilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : IsFilteredOrEmpty.{v₁, u₁} C
d : D
c : C
s s' : d ⟶ F.obj c
obtain : ∀ (c₀ : C) (f : IsFiltered.coeq s s' ⟶ F.obj c₀), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.coeq s s')

Premises used: CategoryTheory.IsFiltered.coeq
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : IsFilteredOrEmpty.{v₁, u₁} C
d : D
c : C
s s' : d ⟶ F.obj c
c₀ : C
f : IsFiltered.coeq s s' ⟶ F.obj c₀
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
⟨c₀, F.preimage (IsFiltered.coeqHom s s' ≫ f), ?_⟩

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.IsFiltered.coeqHom, Exists.intro, CategoryTheory.CategoryStruct.comp
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : IsFilteredOrEmpty.{v₁, u₁} C
d : D
c : C
s s' : d ⟶ F.obj c
c₀ : C
f : IsFiltered.coeq s s' ⟶ F.obj c₀
refine : s ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f)) = s' ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f))
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
refine ⟨c₀, F.preimage (IsFiltered.coeqHom s s' ≫ f), ?_⟩
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
this : IsFilteredOrEmpty.{v₁, u₁} C
d : D
c : C
s s' : d ⟶ F.obj c
c₀ : C
f : IsFiltered.coeq s s' ⟶ F.obj c₀
⊢ s ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f)) = s' ≫ F.map (F.preimage (IsFiltered.coeqHom s s' ≫ f))

Tactic:
simp [reassoc_of% (IsFiltered.coeq_condition s s')]

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
inst_2 : IsCofilteredOrEmpty.{v₂, u₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
suffices : F.op.Final
⊢ F.Initial

Tactic:
suffices Final F.op from initial_of_final_op _
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
⊢ F.op.Final

Tactic:
Functor.final_of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful
-- 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₂} D
inst_3 : F.Full
inst_4 : F.Faithful
h : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
refine : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
⊢ F.op.Final

Tactic:
refine Functor.final_of_exists_of_isFiltered_of_fullyFaithful F.op (fun d => ?_)

Premises used: CategoryTheory.Functor.op, CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful
-- 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
c : C
⊢ IsFiltered (Under.{v₁, u₁} c)

Tactic:
isFiltered_structuredArrow_of_isFiltered_of_exists _
    (fun c' => ⟨c', ⟨𝟙 _⟩⟩)
    (fun s s' => IsFilteredOrEmpty.cocone_maps s s') c

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.isFiltered_structuredArrow_of_isFiltered_of_exists, CategoryTheory.Under, Nonempty.intro, CategoryTheory.Under.Hom, Exists.intro
-- 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
c : C
⊢ IsCofiltered (Over.{v₁, u₁} c)

Tactic:
isCofiltered_costructuredArrow_of_isCofiltered_of_exists _
    (fun c' => ⟨c', ⟨𝟙 _⟩⟩)
    (fun s s' => IsCofilteredOrEmpty.cone_maps s s') c

Premises used: CategoryTheory.Over, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.isCofiltered_costructuredArrow_of_isCofiltered_of_exists, Nonempty.intro, Exists.intro
-- 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
c x_1 : C
x : Under.{v₁, u₁} c
s s' : x_1 ⟶ obj (forget c) x
h :
  ∃ (t : x ⟶ mk (Y := IsFiltered.coeq s s') (x.hom ≫ IsFiltered.coeqHom s s')),
    s ≫ Functor.map (forget c) t = s' ≫ Functor.map (forget c) t
⊢ ∃ (c' : Under.{v₁, u₁} c) (t : x ⟶ c'), s ≫ Functor.map (forget c) t = s' ≫ Functor.map (forget c) t

Tactic:
use mk (x.hom ≫ IsFiltered.coeqHom s s')

Premises used: CategoryTheory.IsFiltered.coeqHom, CategoryTheory.Under.mk, CategoryTheory.Under.hom, CategoryTheory.CategoryStruct.comp
-- 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
c x_1 : C
x : Under.{v₁, u₁} c
s s' : x_1 ⟶ obj (forget c) x
⊢ x.hom ≫ IsFiltered.coeqHom s s' = (mk (Y := IsFiltered.coeq s s') (x.hom ≫ IsFiltered.coeqHom s s')).hom

Tactic:
simp
-- 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
c x_1 : C
x : Under.{v₁, u₁} c
s s' : x_1 ⟶ obj (forget c) x
h :
  Eq (α := x_1 ⟶ obj (forget c) (mk (Y := IsFiltered.coeq s s') (x.hom ≫ IsFiltered.coeqHom s s')))
    (s ≫ Functor.map (forget c) (homMk (IsFiltered.coeqHom s s') ⋯))
    (s' ≫ Functor.map (forget c) (homMk (IsFiltered.coeqHom s s') ⋯))
⊢ ∃ (t : x ⟶ mk (Y := IsFiltered.coeq s s') (x.hom ≫ IsFiltered.coeqHom s s')),
    s ≫ Functor.map (forget c) t = s' ≫ Functor.map (forget c) t

Tactic:
use homMk (IsFiltered.coeqHom s s') (by simp)

Premises used: CategoryTheory.Under.homMk
-- 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
c x_1 : C
x : Under.{v₁, u₁} c
s s' : x_1 ⟶ obj (forget c) x
h : Eq (α := x_1 ⟶ IsFiltered.coeq s s') (s ≫ IsFiltered.coeqHom s s') (s' ≫ IsFiltered.coeqHom s s')
⊢ Eq (α := x_1 ⟶ obj (forget c) (mk (Y := IsFiltered.coeq s s') (x.hom ≫ IsFiltered.coeqHom s s')))
    (s ≫ Functor.map (forget c) (homMk (IsFiltered.coeqHom s s') ⋯))
    (s' ≫ Functor.map (forget c) (homMk (IsFiltered.coeqHom s s') ⋯))

Tactic:
simp only [forget_obj, mk_right, forget_map, homMk_right]

Premises used: CategoryTheory.Under.homMk_right, CategoryTheory.Under.forget_map, CategoryTheory.Under.mk_right, CategoryTheory.Under.forget_obj
-- 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
c x_1 : C
x : Under.{v₁, u₁} c
s s' : x_1 ⟶ obj (forget c) x
h h₁ : Eq (α := x_1 ⟶ IsFiltered.coeq s s') (s' ≫ IsFiltered.coeqHom s s') (s' ≫ IsFiltered.coeqHom s s')
⊢ Eq (α := x_1 ⟶ IsFiltered.coeq s s') (s ≫ IsFiltered.coeqHom s s') (s' ≫ IsFiltered.coeqHom s s')

Tactic:
rw [IsFiltered.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
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
c x_1 : C
x : Over.{v₁, u₁} c
s s' : obj (forget c) x ⟶ x_1
h :
  ∃ (t : mk (Y := IsCofiltered.eq s s') (IsCofiltered.eqHom s s' ≫ x.hom) ⟶ x),
    Functor.map (forget c) t ≫ s = Functor.map (forget c) t ≫ s'
⊢ ∃ (c' : Over.{v₁, u₁} c) (t : c' ⟶ x), Functor.map (forget c) t ≫ s = Functor.map (forget c) t ≫ s'

Tactic:
use mk (IsCofiltered.eqHom s s' ≫ x.hom)

Premises used: CategoryTheory.Over.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsCofiltered.eqHom, CategoryTheory.Over.hom
-- 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
c x_1 : C
x : Over.{v₁, u₁} c
s s' : obj (forget c) x ⟶ x_1
⊢ IsCofiltered.eqHom s s' ≫ x.hom = (mk (Y := IsCofiltered.eq s s') (IsCofiltered.eqHom s s' ≫ x.hom)).hom

Tactic:
simp
-- 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
c x_1 : C
x : Over.{v₁, u₁} c
s s' : obj (forget c) x ⟶ x_1
h :
  Eq (α := obj (forget c) (mk (Y := IsCofiltered.eq s s') (IsCofiltered.eqHom s s' ≫ x.hom)) ⟶ x_1)
    (Functor.map (forget c) (homMk (IsCofiltered.eqHom s s') ⋯) ≫ s)
    (Functor.map (forget c) (homMk (IsCofiltered.eqHom s s') ⋯) ≫ s')
⊢ ∃ (t : mk (Y := IsCofiltered.eq s s') (IsCofiltered.eqHom s s' ≫ x.hom) ⟶ x),
    Functor.map (forget c) t ≫ s = Functor.map (forget c) t ≫ s'

Tactic:
use homMk (IsCofiltered.eqHom s s') (by simp)

Premises used: CategoryTheory.Over.homMk