-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem of_cone_nonempty (h : ∀ {J : Type w} [SmallCategory J] [FinCategory J] (F : J ⥤ C),
    Nonempty (Cone F)) : IsCofiltered C

Proof state:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
⊢ ∃ W h, h ≫ f = h ≫ g

Tactic:
obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)

Result:
case refine_2.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ W h, h ≫ f = h ≫ g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
⊢ IsCofilteredOrEmpty C

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
⊢ ∀ (X Y : C), ∃ W x x, True

case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
⊢ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ W h, h ≫ f = h ≫ g

Proof state:
case refine_1.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
⊢ ∃ W x x, True

Tactic:
exact ⟨c.pt, c.π.app ⟨⟨WalkingPair.left⟩⟩, c.π.app ⟨⟨WalkingPair.right⟩⟩, trivial⟩

Result:
no goals

Proof state:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
⊢ ∃ W x x, True

Tactic:
obtain ⟨c⟩ := h (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)

Result:
case refine_1.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
⊢ ∃ W x x, True

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
⊢ IsCofiltered C

Tactic:
have : Nonempty C := by
  obtain ⟨c⟩ := h (Functor.empty _)
  exact ⟨c.pt⟩

Result:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
⊢ IsCofiltered C

Proof state:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
⊢ ∀ (X Y : C), ∃ W x x, True

Tactic:
intros X Y

Result:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
⊢ ∃ W x x, True

Proof state:
case refine_2.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map { down := WalkingParallelPairHom.left } ≫
      c.π.app { down := WalkingParallelPair.one } =
    c.π.app { down := WalkingParallelPair.zero } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.left }
⊢ c.π.app { down := WalkingParallelPair.zero } ≫ f = c.π.app { down := WalkingParallelPair.zero } ≫ g

Tactic:
have h₂ := c.π.naturality ⟨WalkingParallelPairHom.right⟩

Result:
case refine_2.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map { down := WalkingParallelPairHom.left } ≫
      c.π.app { down := WalkingParallelPair.one } =
    c.π.app { down := WalkingParallelPair.zero } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.left }
h₂ :
  ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.right } ≫
      c.π.app { down := WalkingParallelPair.one } =
    c.π.app { down := WalkingParallelPair.zero } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.right }
⊢ c.π.app { down := WalkingParallelPair.zero } ≫ f = c.π.app { down := WalkingParallelPair.zero } ≫ g

Proof state:
case refine_2.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map { down := WalkingParallelPairHom.left } ≫
      c.π.app { down := WalkingParallelPair.one } =
    c.π.app { down := WalkingParallelPair.zero } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.left }
h₂ :
  ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.right } ≫
      c.π.app { down := WalkingParallelPair.one } =
    c.π.app { down := WalkingParallelPair.zero } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.right }
⊢ c.π.app { down := WalkingParallelPair.zero } ≫ f = c.π.app { down := WalkingParallelPair.zero } ≫ g

Tactic:
simp_all

Result:
no goals

Proof state:
case refine_2.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ c.π.app { down := WalkingParallelPair.zero } ≫ f = c.π.app { down := WalkingParallelPair.zero } ≫ g

Tactic:
have h₁ := c.π.naturality ⟨WalkingParallelPairHom.left⟩

Result:
case refine_2.intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map { down := WalkingParallelPairHom.left } ≫
      c.π.app { down := WalkingParallelPair.one } =
    c.π.app { down := WalkingParallelPair.zero } ≫
      (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.left }
⊢ c.π.app { down := WalkingParallelPair.zero } ≫ f = c.π.app { down := WalkingParallelPair.zero } ≫ g

Proof state:
case intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
c : Cone (Functor.empty C)
⊢ Nonempty C

Tactic:
exact ⟨c.pt⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
⊢ Nonempty C

Tactic:
obtain ⟨c⟩ := h (Functor.empty _)

Result:
case intro
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [inst_1 : FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
c : Cone (Functor.empty C)
⊢ Nonempty C