awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Filtered.CostructuredArrow
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : IsFiltered.{v₂, u₂} B
inst_4 : R.Final
inst_5 : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
sC : (b : B) →
  CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj { down := b }) ≌
    CostructuredArrow L (R.obj b) :=
  fun (b : B) ↦
    Equivalence.trans
      (asEquivalence
        (CostructuredArrow.pre sA.inverse (L ⋙ sT.functor)
          ((sB.inverse ⋙ R ⋙ sT.functor).obj
            { down := b : ULift.{max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃, u₂} B })))
      (Equivalence.symm (asEquivalence (CostructuredArrow.post L sT.functor (R.obj (sB.inverse.obj { down := b })))))
this_1 :
  ∀ (b : AsSmall B), IsFiltered (CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
this : IsFiltered (AsSmall A)
⊢ IsFiltered.{v₁, u₁} A

Tactic:
exact IsFiltered.of_equivalence sA.symm

Premises used: 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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
obtain : ∀ (c : C) (f : d ⟶ F.obj c), Nonempty (StructuredArrow d F)
⊢ Nonempty (StructuredArrow d F)

Tactic:
obtain ⟨c, ⟨f⟩⟩ := h₁ d
-- 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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
c : C
f : d ⟶ F.obj c
⊢ Nonempty (StructuredArrow d F)

Tactic:
⟨.mk f⟩

Premises used: Nonempty.intro, CategoryTheory.StructuredArrow.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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
c : C
f : d ⟶ F.obj c
⊢ Nonempty (StructuredArrow d F)

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

Tactic:
have : Nonempty (StructuredArrow d F) := by
    obtain ⟨c, ⟨f⟩⟩ := h₁ d
    exact ⟨.mk 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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
suffices : IsFilteredOrEmpty (StructuredArrow d F)
⊢ IsFiltered (StructuredArrow d F)

Tactic:
suffices IsFilteredOrEmpty (StructuredArrow d F) from IsFiltered.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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
⊢ IsFilteredOrEmpty (StructuredArrow d F)

Tactic:
⟨fun f g => ?_, fun f g η μ => ?_⟩

Premises used: CategoryTheory.IsFilteredOrEmpty.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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
refine_1 : ∀ (f g : StructuredArrow d F), ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True
refine_2 : ∀ (f g : StructuredArrow d F) (η μ : f ⟶ g), ∃ (Z : StructuredArrow d F) (h : g ⟶ Z), η ≫ h = μ ≫ h
⊢ IsFilteredOrEmpty (StructuredArrow d F)

Tactic:
refine ⟨fun f g => ?_, fun f g η μ => ?_⟩
-- 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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
refine_1 :
  ∀ (c : C) (t : IsFiltered.max.{v₁, u₁} f.right g.right ⟶ c)
    (ht :
      (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
        (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t),
    ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True
⊢ ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True

Tactic:
obtain ⟨c, ⟨t, ht⟩⟩ := h₂ (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right))
        (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right))

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.StructuredArrow.hom, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.StructuredArrow.right, 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₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max.{v₁, u₁} f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True

Tactic:
⟨.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t)), ?_, ?_, trivial⟩

Premises used: trivial, CategoryTheory.StructuredArrow.hom, CategoryTheory.Functor.map, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.StructuredArrow.mk, CategoryTheory.StructuredArrow.right, 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₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max.{v₁, u₁} f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
refine_1 : f ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))
refine_1₁ : g ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))
⊢ ∃ (Z : StructuredArrow d F) (x : f ⟶ Z) (x : g ⟶ Z), True

Tactic:
refine ⟨.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t)), ?_, ?_, 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₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max.{v₁, u₁} f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ f ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))

Tactic:
exact StructuredArrow.homMk (IsFiltered.leftToMax _ _ ≫ t) rfl

Premises used: CategoryTheory.StructuredArrow.homMk, 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₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max.{v₁, u₁} f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right ≫ t) =
    (StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))).hom

Tactic:
simpa using ht.symm

Premises used: Eq.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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max.{v₁, u₁} f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ g ⟶ StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))

Tactic:
exact StructuredArrow.homMk (IsFiltered.rightToMax _ _ ≫ t) (by simpa using ht.symm)

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.IsFiltered.rightToMax, 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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ g.hom ≫ F.map (IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)) =
    (StructuredArrow.mk (Y := IsFiltered.coeq (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ))
        (f.hom ≫
          F.map
            (StructuredArrow.Hom.right η ≫
              IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)))).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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
refine_2 :
  Eq (α :=
    f ⟶
      StructuredArrow.mk (Y := IsFiltered.coeq (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ))
        (f.hom ≫
          F.map
            (StructuredArrow.Hom.right η ≫
              IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ))))
    (η ≫ StructuredArrow.homMk (IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)) ⋯)
    (μ ≫ StructuredArrow.homMk (IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)) ⋯)
⊢ ∃ (Z : StructuredArrow d F) (h : g ⟶ Z), η ≫ h = μ ≫ h

Tactic:
refine ⟨.mk (f.hom ≫ F.map (η.right ≫ IsFiltered.coeqHom η.right μ.right)),
      StructuredArrow.homMk (IsFiltered.coeqHom η.right μ.right) (by 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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ Eq (α :=
    f ⟶
      StructuredArrow.mk (Y := IsFiltered.coeq (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ))
        (f.hom ≫
          F.map
            (StructuredArrow.Hom.right η ≫
              IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ))))
    (η ≫ StructuredArrow.homMk (IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)) ⋯)
    (μ ≫ StructuredArrow.homMk (IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)) ⋯)

Tactic:
simpa using 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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {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
suffices : IsFiltered (CostructuredArrow F d)ᵒᵖ
⊢ IsCofiltered (CostructuredArrow F d)

Tactic:
suffices IsFiltered (CostructuredArrow F d)ᵒᵖ from isCofiltered_of_isFiltered_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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {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
suffices : IsFiltered (StructuredArrow (op d) F.op)
⊢ IsFiltered (CostructuredArrow F d)ᵒᵖ

Tactic:
suffices IsFiltered (StructuredArrow (op d) F.op) from
    IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).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 : IsCofilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {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
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
⊢ IsFiltered (StructuredArrow (op d) F.op)

Tactic:
apply isFiltered_structuredArrow_of_isFiltered_of_exists

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

Tactic:
⟨op c, ⟨Quiver.Hom.op t⟩⟩

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

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

Tactic:
obtain ⟨c', t, ht⟩ := h₂ s.unop s'.unop

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

Tactic:
⟨op c', Quiver.Hom.op t, Quiver.Hom.unop_inj ht⟩

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

Tactic:
exact ⟨op c', Quiver.Hom.op t, Quiver.Hom.unop_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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t
suffices : ∀ (d : D), IsFiltered (StructuredArrow d F)
⊢ F.Final

Tactic:
suffices ∀ d, IsFiltered (StructuredArrow d F) from 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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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:
isFiltered_structuredArrow_of_isFiltered_of_exists F h₁ h₂

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 : IsFilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (d ⟶ F.obj c)
h₂ : ∀ {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 isFiltered_structuredArrow_of_isFiltered_of_exists F h₁ h₂

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

Tactic:
Functor.final_of_exists_of_isFiltered _ (fun _ => ⟨IsFiltered.nonempty.some, ⟨hX.from _⟩⟩)
    (fun {_ c} _ _ => ⟨c, 𝟙 _, hX.hom_ext _ _⟩)

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.CategoryStruct.id, Nonempty.some, CategoryTheory.Functor.final_of_exists_of_isFiltered, Nonempty.intro, CategoryTheory.Functor.map, CategoryTheory.IsFiltered.nonempty, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.IsTerminal.hom_ext, 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 : IsFiltered.{v₁, u₁} C
inst_3 : HasTerminal.{v₂, u₂} D
⊢ Final.{v₁, v₂, u₁, u₂} (obj (const C) (terminal.{v₂, u₂} D))

Tactic:
Functor.final_const_of_isTerminal terminalIsTerminal

Premises used: CategoryTheory.Functor.final_const_of_isTerminal, CategoryTheory.Limits.terminalIsTerminal
-- 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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ (c' : C) (t : c' ⟶ c), F.map t ≫ s = F.map t ≫ s'
suffices : ∀ (d : D), IsCofiltered (CostructuredArrow F d)
⊢ F.Initial

Tactic:
suffices ∀ d, IsCofiltered (CostructuredArrow F d) from
    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
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {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:
isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h₁ h₂

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 : IsCofilteredOrEmpty.{v₁, u₁} C
h₁ : ∀ (d : D), ∃ (c : C), Nonempty.{v₂ + 1} (F.obj c ⟶ d)
h₂ : ∀ {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 isCofiltered_costructuredArrow_of_isCofiltered_of_exists F h₁ h₂

Premises used: CategoryTheory.isCofiltered_costructuredArrow_of_isCofiltered_of_exists