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 : IsCofilteredOrEmpty.{v₁, u₁} C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
⊢ ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t

Tactic:
obtain ⟨h₁, h₂⟩ := F.op.final_iff_of_isFiltered.mp inferInstance

Premises used: CategoryTheory.Functor.op, inferInstance, Iff.mp, CategoryTheory.Functor.final_iff_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 : IsCofilteredOrEmpty.{v₁, u₁} C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
⊢ (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
    ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'

Tactic:
⟨?_, ?_⟩

Premises used: And.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
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
refine_1 : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
refine_2 : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
⊢ (∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
    ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'

Tactic:
refine ⟨?_, ?_⟩
-- 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
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
d : D
refine_1 : ∀ (c : Cᵒᵖ) (t : op d ⟶ F.op.obj c), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
⊢ ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)

Tactic:
obtain ⟨c, ⟨t⟩⟩ := h₁ (op d)

Premises used: Opposite.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₁} C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
d : D
c : Cᵒᵖ
t : op d ⟶ F.op.obj c
⊢ ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)

Tactic:
⟨c.unop, ⟨t.unop⟩⟩

Premises used: Quiver.Hom.unop, Nonempty.intro, Exists.intro, 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₁} C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
d : D
c : Cᵒᵖ
t : op d ⟶ F.op.obj c
⊢ ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)

Tactic:
exact ⟨c.unop, ⟨t.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₁} C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
d : D
c : C
s s' : F.obj c ⟶ d
refine_2 :
  ∀ (c' : Cᵒᵖ) (t : op c ⟶ c') (ht : Eq (α := op d ⟶ F.op.obj c') (s.op ≫ F.op.map t) (s'.op ≫ F.op.map t)),
    ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
⊢ ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'

Tactic:
obtain ⟨c', t, ht⟩ := h₂ (Quiver.Hom.op s) (Quiver.Hom.op s')

Premises used: Quiver.Hom.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₁} C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
d : D
c : C
s s' : F.obj c ⟶ d
c' : Cᵒᵖ
t : op c ⟶ c'
ht : Eq (α := op d ⟶ F.op.obj c') (s.op ≫ F.op.map t) (s'.op ≫ F.op.map t)
⊢ ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'

Tactic:
⟨c'.unop, t.unop, Quiver.Hom.op_inj ht⟩

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, Exists.intro, 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₁} C
hF : F.Initial
h₁ : ∀ (d : Dᵒᵖ), ∃ (c : Cᵒᵖ), Nonempty.{v₂ + 1} (d ⟶ F.op.obj c)
h₂ : ∀ {d : Dᵒᵖ} {c : Cᵒᵖ} (s s' : d ⟶ F.op.obj c), ∃ (c' : Cᵒᵖ) (t : c ⟶ c'), s ≫ F.op.map t = s' ≫ F.op.map t
d : D
c : C
s s' : F.obj c ⟶ d
c' : Cᵒᵖ
t : op c ⟶ c'
ht : Eq (α := op d ⟶ F.op.obj c') (s.op ≫ F.op.map t) (s'.op ≫ F.op.map t)
⊢ ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'

Tactic:
exact ⟨c'.unop, t.unop, Quiver.Hom.op_inj ht⟩
-- 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
inst_3 : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
⊢ ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t

Tactic:
((final_iff_of_isFiltered F).1 inferInstance).2 s s'

Premises used: inferInstance, And.right, Iff.mp, CategoryTheory.Functor.final_iff_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 : IsCofilteredOrEmpty.{v₁, u₁} C
inst_3 : F.Initial
d : D
c : C
s s' : F.obj c ⟶ d
⊢ ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'

Tactic:
((initial_iff_of_isCofiltered F).1 inferInstance).2 s s'

Premises used: inferInstance, CategoryTheory.Functor.initial_iff_of_isCofiltered, And.right, Iff.mp
-- 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
⊢ F.Final ↔ ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
⟨?_, fun h => final_of_isFiltered_structuredArrow F⟩

Premises used: CategoryTheory.Functor.final_of_isFiltered_structuredArrow, Iff.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
refine : F.Final → ∀ (d : D), IsFiltered (StructuredArrow d F)
⊢ F.Final ↔ ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
refine ⟨?_, fun h => final_of_isFiltered_structuredArrow 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₁} C
rw :
  ((∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) →
    ∀ (d : D), IsFiltered (StructuredArrow d F)
⊢ F.Final → ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
rw [final_iff_of_isFiltered]

Premises used: CategoryTheory.Functor.final_iff_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₁} C
⊢ ((∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) →
    ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
fun h => isFiltered_structuredArrow_of_isFiltered_of_exists F h.1 h.2

Premises used: CategoryTheory.isFiltered_structuredArrow_of_isFiltered_of_exists, And.right, And.left
-- 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
⊢ ((∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)) ∧
      ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) →
    ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
exact fun h => isFiltered_structuredArrow_of_isFiltered_of_exists F h.1 h.2

Premises used: CategoryTheory.isFiltered_structuredArrow_of_isFiltered_of_exists
-- 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
⊢ F.Initial ↔ ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
⟨?_, fun h => initial_of_isCofiltered_costructuredArrow F⟩

Premises used: Iff.intro, CategoryTheory.Functor.initial_of_isCofiltered_costructuredArrow
-- 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
refine : F.Initial → ∀ (d : D), IsCofiltered (CostructuredArrow F d)
⊢ F.Initial ↔ ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
refine ⟨?_, fun h => initial_of_isCofiltered_costructuredArrow 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 : IsCofilteredOrEmpty.{v₁, u₁} C
rw :
  ((∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') →
    ∀ (d : D), IsCofiltered (CostructuredArrow F d)
⊢ F.Initial → ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
rw [initial_iff_of_isCofiltered]

Premises used: CategoryTheory.Functor.initial_iff_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
inst_2 : IsCofilteredOrEmpty.{v₁, u₁} C
⊢ ((∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') →
    ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
fun h => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h.1 h.2

Premises used: CategoryTheory.isCofiltered_costructuredArrow_of_isCofiltered_of_exists, And.right, And.left
-- 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
⊢ ((∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s') →
    ∀ (d : D), IsCofiltered (CostructuredArrow F d)

Tactic:
exact fun h => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h.1 h.2

Premises used: CategoryTheory.isCofiltered_costructuredArrow_of_isCofiltered_of_exists
-- 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
X : C × C
rw : Final (C := Under.{v₁, u₁} X.1) (Under.forget X.1)
⊢ ∀ (Y : C), IsFiltered (StructuredArrow (C := Under.{v₁, u₁} X.1) Y (Under.forget X.1))

Tactic:
rw [← final_iff_isFiltered_structuredArrow (Under.forget X.1)]

Premises used: CategoryTheory.Functor.final_iff_isFiltered_structuredArrow, Prod.fst, CategoryTheory.Under.forget
-- 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
X : C × C
⊢ Final (C := Under.{v₁, u₁} X.1) (Under.forget X.1)

Tactic:
infer_instance
-- 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
X : C × C
⊢ ∀ (Y : C), IsFiltered (StructuredArrow (C := Under.{v₁, u₁} X.1) Y (Under.forget X.1))

Tactic:
haveI : ∀ Y, IsFiltered (StructuredArrow Y (Under.forget X.1)) := by
    rw [← final_iff_isFiltered_structuredArrow (Under.forget X.1)]
    infer_instance
-- 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
X : C × C
this : ∀ (Y : C), IsFiltered (StructuredArrow (C := Under.{v₁, u₁} X.1) Y (Under.forget X.1))
⊢ IsFiltered (StructuredArrow.{v₁, v₁, u₁, u₁} X (Functor.diag C))

Tactic:
apply IsFiltered.of_equivalence (StructuredArrow.ofDiagEquivalence X).symm

Premises used: CategoryTheory.StructuredArrow.ofDiagEquivalence, CategoryTheory.IsFiltered.of_equivalence, CategoryTheory.Equivalence.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 : IsFilteredOrEmpty.{v₁, u₁} C
⊢ Final.{v₁, v₁, u₁, u₁} (diag C)

Tactic:
final_of_isFiltered_structuredArrow _

Premises used: CategoryTheory.Functor.final_of_isFiltered_structuredArrow
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFilteredOrEmpty.{v₁, u₁} C
⊢ IsSiftedOrEmpty.{v₁, u₁} C

Tactic:
Functor.final_diag_of_isFiltered

Premises used: CategoryTheory.Functor.final_diag_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 : IsCofilteredOrEmpty.{v₁, u₁} C
X : C × C
rw : Initial (C := Over.{v₁, u₁} X.1) (Over.forget X.1)
⊢ ∀ (Y : C), IsCofiltered (CostructuredArrow (C := Over.{v₁, u₁} X.1) (Over.forget X.1) Y)

Tactic:
rw [← initial_iff_isCofiltered_costructuredArrow (Over.forget X.1)]

Premises used: CategoryTheory.Over.forget, Prod.fst, CategoryTheory.Functor.initial_iff_isCofiltered_costructuredArrow
-- 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
X : C × C
⊢ Initial (C := Over.{v₁, u₁} X.1) (Over.forget X.1)

Tactic:
infer_instance
-- 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
X : C × C
⊢ ∀ (Y : C), IsCofiltered (CostructuredArrow (C := Over.{v₁, u₁} X.1) (Over.forget X.1) Y)

Tactic:
haveI : ∀ Y, IsCofiltered (CostructuredArrow (Over.forget X.1) Y) := by
    rw [← initial_iff_isCofiltered_costructuredArrow (Over.forget X.1)]
    infer_instance
-- 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
X : C × C
this : ∀ (Y : C), IsCofiltered (CostructuredArrow (C := Over.{v₁, u₁} X.1) (Over.forget X.1) Y)
⊢ IsCofiltered (CostructuredArrow.{v₁, v₁, u₁, u₁} (Functor.diag C) X)

Tactic:
apply IsCofiltered.of_equivalence (CostructuredArrow.ofDiagEquivalence X).symm

Premises used: CategoryTheory.CostructuredArrow.ofDiagEquivalence, CategoryTheory.Equivalence.symm, CategoryTheory.IsCofiltered.of_equivalence
-- 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
⊢ Initial.{v₁, v₁, u₁, u₁} (diag C)

Tactic:
initial_of_isCofiltered_costructuredArrow _

Premises used: CategoryTheory.Functor.initial_of_isCofiltered_costructuredArrow
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
⊢ F.Final

Tactic:
final_of_exists_of_isFiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)

Premises used: CategoryTheory.Functor.final_of_exists_of_isFiltered
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
refine_1 : ∀ (x : Discrete PUnit.{u_1 + 1}), ∃ (c : C), Nonempty.{u_1 + 1} (x ⟶ F.obj c)
refine_2 :
  ∀ {x : Discrete PUnit.{u_1 + 1}} {c : C} (x_1 x_2 : x ⟶ F.obj c),
    ∃ (c' : C) (t : c ⟶ c'), x_1 ≫ F.map t = x_2 ≫ F.map t
⊢ F.Final

Tactic:
refine final_of_exists_of_isFiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)

Premises used: CategoryTheory.Functor.final_of_exists_of_isFiltered
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
h : Nonempty.{u_1 + 1} (x ⟶ F.obj (Classical.choice ⋯))
⊢ ∃ (c : C), Nonempty.{u_1 + 1} (x ⟶ F.obj c)

Tactic:
use Classical.choice IsFiltered.nonempty

Premises used: Classical.choice, CategoryTheory.IsFiltered.nonempty
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
⊢ x.as = (F.obj (Classical.choice ⋯)).as

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
⊢ Nonempty.{u_1 + 1} (x ⟶ F.obj (Classical.choice ⋯))

Tactic:
exact ⟨Discrete.eqToHom (by simp)⟩
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
c : C
x_1 x_2 : x ⟶ F.obj c
h : ∃ (t : c ⟶ c), x_1 ≫ F.map t = x_2 ≫ F.map t
⊢ ∃ (c' : C) (t : c ⟶ c'), x_1 ≫ F.map t = x_2 ≫ F.map t

Tactic:
use c
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
c : C
x_1 x_2 : x ⟶ F.obj c
h : x_1 ≫ F.map (𝟙 c) = x_2 ≫ F.map (𝟙 c)
⊢ ∃ (t : c ⟶ c), x_1 ≫ F.map t = x_2 ≫ F.map t

Tactic:
use 𝟙 c

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsFiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
c : C
x_1 x_2 : x ⟶ F.obj c
⊢ x_1 ≫ F.map (𝟙 c) = x_2 ≫ F.map (𝟙 c)

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
⊢ F.Initial

Tactic:
initial_of_exists_of_isCofiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)

Premises used: CategoryTheory.Functor.initial_of_exists_of_isCofiltered
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
refine_1 : ∀ (x : Discrete PUnit.{u_1 + 1}), ∃ (c : C), Nonempty.{u_1 + 1} (F.obj c ⟶ x)
refine_2 :
  ∀ {x : Discrete PUnit.{u_1 + 1}} {c : C} (x_1 x_2 : F.obj c ⟶ x),
    ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ x_1 = F.map t ≫ x_2
⊢ F.Initial

Tactic:
refine initial_of_exists_of_isCofiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)

Premises used: CategoryTheory.Functor.initial_of_exists_of_isCofiltered
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
h : Nonempty.{u_1 + 1} (F.obj (Classical.choice ⋯) ⟶ x)
⊢ ∃ (c : C), Nonempty.{u_1 + 1} (F.obj c ⟶ x)

Tactic:
use Classical.choice IsCofiltered.nonempty

Premises used: Classical.choice, CategoryTheory.IsCofiltered.nonempty
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
⊢ (F.obj (Classical.choice ⋯)).as = x.as

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
⊢ Nonempty.{u_1 + 1} (F.obj (Classical.choice ⋯) ⟶ x)

Tactic:
exact ⟨Discrete.eqToHom (by simp)⟩
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
c : C
x_1 x_2 : F.obj c ⟶ x
h : ∃ (t : c ⟶ c), F.map t ≫ x_1 = F.map t ≫ x_2
⊢ ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ x_1 = F.map t ≫ x_2

Tactic:
use c
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
c : C
x_1 x_2 : F.obj c ⟶ x
h : F.map (𝟙 c) ≫ x_1 = F.map (𝟙 c) ≫ x_2
⊢ ∃ (t : c ⟶ c), F.map t ≫ x_1 = F.map t ≫ x_2

Tactic:
use 𝟙 c

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Filtered.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsCofiltered.{v₁, u₁} C
F : Functor.{v₁, u_1, u₁, u_1} C (Discrete PUnit.{u_1 + 1})
x : Discrete PUnit.{u_1 + 1}
c : C
x_1 x_2 : F.obj c ⟶ x
⊢ F.map (𝟙 c) ≫ x_1 = F.map (𝟙 c) ≫ x_2

Tactic:
apply Subsingleton.elim

Premises used: Subsingleton.elim
-- 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
⊢ (proj Y T).Final

Tactic:
⟨fun X => ?_⟩

Premises used: CategoryTheory.Functor.Final.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 : IsFilteredOrEmpty.{v₁, u₁} C
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
Y : D
refine : ∀ (X : C), IsConnected (StructuredArrow X (proj Y T))
⊢ (proj Y T).Final

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 : IsFilteredOrEmpty.{v₁, u₁} C
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : T.Final
Y : D
X : C
rw : IsConnected (StructuredArrow Y (Under.forget X ⋙ T))
⊢ IsConnected (StructuredArrow X (proj Y T))

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

Premises used: CategoryTheory.isConnected_iff_of_equivalence, CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence