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

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 (Cocone F)
this✝ : Nonempty C
this : IsFilteredOrEmpty C
⊢ IsFiltered C

Tactic:
apply IsFiltered.mk

Result:
no goals

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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
⊢ ∃ Z h, f ≫ h = g ≫ h

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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ Z h, f ≫ h = g ≫ h

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 (Cocone F)
⊢ IsFiltered 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 (Cocone F)
this : Nonempty C
⊢ IsFiltered 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 (Cocone F)
this : Nonempty C
X Y : C
⊢ ∃ Z 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 (Cocone F)
this : Nonempty C
X Y : C
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ pair X Y)
⊢ ∃ Z 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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ f ≫ c.ι.app { down := WalkingParallelPair.one } = g ≫ c.ι.app { down := WalkingParallelPair.one }

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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.left } ≫
      c.ι.app { down := WalkingParallelPair.one } =
    c.ι.app { down := WalkingParallelPair.zero } ≫
      ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.left }
⊢ f ≫ c.ι.app { down := WalkingParallelPair.one } = g ≫ c.ι.app { down := WalkingParallelPair.one }

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 (Cocone F)
c : Cocone (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 (Cocone F)
this : Nonempty C
⊢ IsFilteredOrEmpty 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 (Cocone F)
this : Nonempty C
⊢ ∀ (X Y : C), ∃ Z 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 (Cocone F)
this : Nonempty C
⊢ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h

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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.left } ≫
      c.ι.app { down := WalkingParallelPair.one } =
    c.ι.app { down := WalkingParallelPair.zero } ≫
      ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.left }
⊢ f ≫ c.ι.app { down := WalkingParallelPair.one } = g ≫ c.ι.app { down := WalkingParallelPair.one }

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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
h₁ :
  (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.left } ≫
      c.ι.app { down := WalkingParallelPair.one } =
    c.ι.app { down := WalkingParallelPair.zero } ≫
      ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.left }
h₂ :
  (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g).map { down := WalkingParallelPairHom.right } ≫
      c.ι.app { down := WalkingParallelPair.one } =
    c.ι.app { down := WalkingParallelPair.zero } ≫
      ((Functor.const (ULiftHom (ULift.{w, 0} WalkingParallelPair))).obj c.pt).map
        { down := WalkingParallelPairHom.right }
⊢ f ≫ c.ι.app { down := WalkingParallelPair.one } = g ≫ c.ι.app { down := WalkingParallelPair.one }

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 (Cocone 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 (Cocone F)
c : Cocone (Functor.empty C)
⊢ Nonempty 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 (Cocone F)
this : Nonempty C
⊢ ∀ (X Y : C), ∃ Z 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 (Cocone F)
this : Nonempty C
X Y : C
⊢ ∃ Z 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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ Z h, f ≫ h = g ≫ h

Tactic:
refine ⟨c.pt, c.ι.app ⟨WalkingParallelPair.one⟩, ?_⟩

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 (Cocone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cocone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ f ≫ c.ι.app { down := WalkingParallelPair.one } = g ≫ c.ι.app { down := WalkingParallelPair.one }