awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J_1 : Type u_2
inst_1 : Countable J_1
inst_2 : HasCountableCoproducts.{v_1, u_1} C
J : Type u_3
inst_3 : Countable J
⊢ HasCoproductsOfShape.{u_3, u_1, v_1} J C

Tactic:
have : Countable (Shrink.{0} J) := Countable.of_equiv _ (equivShrink.{0} J)
  have : HasColimitsOfShape (Discrete (Shrink.{0} J)) C := HasCountableCoproducts.out _
  hasColimitsOfShape_of_equivalence (Discrete.equivalence (equivShrink.{0} J)).symm

Premises used: Countable.of_equiv, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, Shrink, CategoryTheory.Limits.HasCountableCoproducts.out, equivShrink, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
⊢ Monotone (sequentialFunctor_obj J)

Tactic:
monotone_nat_of_le_succ fun n ↦
    leOfHom (IsFilteredOrEmpty.cocone_objs ((exists_surjective_nat _).choose n)
      (sequentialFunctor_obj J n)).choose_spec.choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj, exists_surjective_nat, CategoryTheory.IsFilteredOrEmpty.cocone_objs, Exists.choose, CategoryTheory.leOfHom, monotone_nat_of_le_succ
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
j : J
obtain : ∀ (m : ℕ) (h : ⋯.choose (p := Function.Surjective) m = j), ∃ (n : ℕ), j ≤ sequentialFunctor_obj J n
⊢ ∃ (n : ℕ), j ≤ sequentialFunctor_obj J n

Tactic:
obtain ⟨m, h⟩ := (exists_surjective_nat _).choose_spec j

Premises used: Exists.choose_spec, exists_surjective_nat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
j : J
m : ℕ
h : ⋯.choose (p := Function.Surjective) m = j
⊢ ∃ (n : ℕ), j ≤ sequentialFunctor_obj J n

Tactic:
⟨m + 1, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
j : J
m : ℕ
h : ⋯.choose (p := Function.Surjective) m = j
refine : j ≤ sequentialFunctor_obj J (m + 1)
⊢ ∃ (n : ℕ), j ≤ sequentialFunctor_obj J n

Tactic:
refine ⟨m + 1, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
j : J
m : ℕ
h : ⋯.choose (p := Function.Surjective) m = j
⊢ j ≤ sequentialFunctor_obj J (m + 1)

Tactic:
simpa only [h] using leOfHom (IsFilteredOrEmpty.cocone_objs ((exists_surjective_nat _).choose m)
    (sequentialFunctor_obj J m)).choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj, exists_surjective_nat, CategoryTheory.IsFilteredOrEmpty.cocone_objs, Exists.choose, CategoryTheory.leOfHom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
obtain :
  ∀ (n : ℕ) (g : d ≤ Functor.obj (sequentialFunctor J) n),
    IsConnected.{0, u_2} (StructuredArrow d (sequentialFunctor J))
⊢ IsConnected.{0, u_2} (StructuredArrow d (sequentialFunctor J))

Tactic:
obtain ⟨n, (g : d ≤ (sequentialFunctor J).obj n)⟩ := sequentialFunctor_final_aux J d

Premises used: CategoryTheory.Limits.IsFiltered.sequentialFunctor_final_aux
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
⊢ Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))

Tactic:
have : Nonempty (StructuredArrow d (sequentialFunctor J)) :=
      ⟨StructuredArrow.mk (homOfLE g)⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
h :
  ∀ (j₁ j₂ : StructuredArrow d (sequentialFunctor J)),
    ∃ (l : List (StructuredArrow d (sequentialFunctor J))), List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ IsConnected.{0, u_2} (StructuredArrow d (sequentialFunctor J))

Tactic:
apply isConnected_of_zigzag

Premises used: CategoryTheory.isConnected_of_zigzag
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
⊢ ∀ (j₁ j₂ : StructuredArrow d (sequentialFunctor J)),
    ∃ (l : List (StructuredArrow d (sequentialFunctor J))), List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
fun i j ↦ ⟨[j], ?_⟩

Premises used: List.cons, Exists.intro, List.nil
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
h : ∀ (i j : StructuredArrow d (sequentialFunctor J)), List.IsChain Zag [i, j] ∧ [i, j].getLast ⋯ = j
⊢ ∀ (j₁ j₂ : StructuredArrow d (sequentialFunctor J)),
    ∃ (l : List (StructuredArrow d (sequentialFunctor J))), List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
refine fun i j ↦ ⟨[j], ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h : Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
⊢ List.IsChain Zag [i, j] ∧ [i, j].getLast ⋯ = j

Tactic:
simp only [List.isChain_cons_cons, Zag, List.isChain_singleton, and_true, ne_eq,
      not_false_eq_true, List.getLast_cons, List.getLast_singleton', reduceCtorEq]

Premises used: reduceCtorEq, List.isChain_singleton, and_true, List.getLast_singleton', ne_eq, List.isChain_cons_cons, List.getLast_cons, CategoryTheory.Zag, not_false_eq_true
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h :
  ∀
    (this :
      ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsFiltered J] (d : J) (n : ℕ)
        (g : d ≤ Functor.obj (sequentialFunctor J) n)
        (this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J)))
        (i j : StructuredArrow d (sequentialFunctor J)) (h : j.right ≤ i.right), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i))
    (h : i.right < j.right), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
wlog! :
  ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsFiltered J] (d : J) (n : ℕ)
    (g : d ≤ Functor.obj (sequentialFunctor J) n)
    (this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J)))
    (i j : StructuredArrow d (sequentialFunctor J)) (h : j.right ≤ i.right), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
wlog! h : j.right ≤ i.right

Premises used: CategoryTheory.StructuredArrow.right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this_1 : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
this :
  ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsFiltered J] (d : J) (n : ℕ)
    (g : d ≤ Functor.obj (sequentialFunctor J) n)
    (this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J)))
    (i j : StructuredArrow d (sequentialFunctor J)) (h : j.right ≤ i.right), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
h : i.right < j.right
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
exact or_comm.1 (this J d n g inferInstance j i (le_of_lt h))

Premises used: le_of_lt, inferInstance, Iff.mp, or_comm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J_1 : Type u_2
inst : Countable J_1
inst_1 : Preorder J_1
inst_2 : IsFiltered J_1
J : Type u_2
inst_3 : Countable J
inst_4 : Preorder J
inst_5 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h : j.right ≤ i.right
h₁ : Nonempty (j ⟶ i)
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J_1 : Type u_2
inst : Countable J_1
inst_1 : Preorder J_1
inst_2 : IsFiltered J_1
J : Type u_2
inst_3 : Countable J
inst_4 : Preorder J
inst_5 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h : j.right ≤ i.right
⊢ Nonempty (j ⟶ i)

Tactic:
⟨StructuredArrow.homMk (homOfLE h) rfl⟩

Premises used: CategoryTheory.StructuredArrow.homMk, Nonempty.intro, CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J_1 : Type u_2
inst : Countable J_1
inst_1 : Preorder J_1
inst_2 : IsFiltered J_1
J : Type u_2
inst_3 : Countable J
inst_4 : Preorder J
inst_5 : IsFiltered J
d : J
n : ℕ
g : d ≤ Functor.obj (sequentialFunctor J) n
this : Nonempty.{max 1 (u_2 + 1)} (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h : j.right ≤ i.right
⊢ Nonempty (j ⟶ i)

Tactic:
exact ⟨StructuredArrow.homMk (homOfLE h) rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
⊢ Antitone (sequentialFunctor_obj J)

Tactic:
antitone_nat_of_succ_le fun n ↦
    leOfHom (IsCofilteredOrEmpty.cone_objs ((exists_surjective_nat _).choose n)
      (sequentialFunctor_obj J n)).choose_spec.choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.IsCofilteredOrEmpty.cone_objs, antitone_nat_of_succ_le, exists_surjective_nat, Exists.choose, CategoryTheory.leOfHom, CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
j : J
obtain : ∀ (m : ℕ) (h : ⋯.choose (p := Function.Surjective) m = j), ∃ (n : ℕ), sequentialFunctor_obj J n ≤ j
⊢ ∃ (n : ℕ), sequentialFunctor_obj J n ≤ j

Tactic:
obtain ⟨m, h⟩ := (exists_surjective_nat _).choose_spec j

Premises used: Exists.choose_spec, exists_surjective_nat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose (p := Function.Surjective) m = j
⊢ ∃ (n : ℕ), sequentialFunctor_obj J n ≤ j

Tactic:
⟨m + 1, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose (p := Function.Surjective) m = j
refine : sequentialFunctor_obj J (m + 1) ≤ j
⊢ ∃ (n : ℕ), sequentialFunctor_obj J n ≤ j

Tactic:
refine ⟨m + 1, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
j : J
m : ℕ
h : ⋯.choose (p := Function.Surjective) m = j
⊢ sequentialFunctor_obj J (m + 1) ≤ j

Tactic:
simpa only [h] using leOfHom (IsCofilteredOrEmpty.cone_objs ((exists_surjective_nat _).choose m)
    (sequentialFunctor_obj J m)).choose_spec.choose

Premises used: Exists.choose_spec, CategoryTheory.IsCofilteredOrEmpty.cone_objs, exists_surjective_nat, Exists.choose, CategoryTheory.leOfHom, CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
obtain :
  ∀ (n : ℕ) (g : Functor.obj (sequentialFunctor J) (op n) ≤ d),
    IsConnected.{0, u_2} (CostructuredArrow (sequentialFunctor J) d)
⊢ IsConnected.{0, u_2} (CostructuredArrow (sequentialFunctor J) d)

Tactic:
obtain ⟨n, (g : (sequentialFunctor J).obj ⟨n⟩ ≤ d)⟩ := sequentialFunctor_initial_aux J d

Premises used: CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial_aux
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
⊢ Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)

Tactic:
have : Nonempty (CostructuredArrow (sequentialFunctor J) d) :=
      ⟨CostructuredArrow.mk (homOfLE g)⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
h :
  ∀ (j₁ j₂ : CostructuredArrow (sequentialFunctor J) d),
    ∃ (l : List (CostructuredArrow (sequentialFunctor J) d)), List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
⊢ IsConnected.{0, u_2} (CostructuredArrow (sequentialFunctor J) d)

Tactic:
apply isConnected_of_zigzag

Premises used: CategoryTheory.isConnected_of_zigzag
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
⊢ ∀ (j₁ j₂ : CostructuredArrow (sequentialFunctor J) d),
    ∃ (l : List (CostructuredArrow (sequentialFunctor J) d)), List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
fun i j ↦ ⟨[j], ?_⟩

Premises used: List.cons, Exists.intro, List.nil
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
h : ∀ (i j : CostructuredArrow (sequentialFunctor J) d), List.IsChain Zag [i, j] ∧ [i, j].getLast ⋯ = j
⊢ ∀ (j₁ j₂ : CostructuredArrow (sequentialFunctor J) d),
    ∃ (l : List (CostructuredArrow (sequentialFunctor J) d)), List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂

Tactic:
refine fun i j ↦ ⟨[j], ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u_2
inst_1 : Countable J
inst_2 : Preorder J
inst_3 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
⊢ List.IsChain Zag [i, j] ∧ [i, j].getLast ⋯ = j

Tactic:
simp only [List.isChain_cons_cons, Zag, List.isChain_singleton, and_true, ne_eq,
      not_false_eq_true, List.getLast_cons, List.getLast_singleton', reduceCtorEq]

Premises used: reduceCtorEq, List.isChain_singleton, and_true, List.getLast_singleton', ne_eq, List.isChain_cons_cons, List.getLast_cons, CategoryTheory.Zag, not_false_eq_true
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h :
  ∀
    (this :
      ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsCofiltered J] (d : J) (n : ℕ)
        (g : Functor.obj (sequentialFunctor J) (op n) ≤ d)
        (this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d))
        (i j : CostructuredArrow (sequentialFunctor J) d) (h : unop i.left ≤ unop j.left),
        Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i))
    (h : unop j.left < unop i.left), Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
wlog! :
  ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsCofiltered J] (d : J) (n : ℕ)
    (g : Functor.obj (sequentialFunctor J) (op n) ≤ d)
    (this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d))
    (i j : CostructuredArrow (sequentialFunctor J) d) (h : unop i.left ≤ unop j.left),
    Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
wlog! h : (unop i.left) ≤ (unop j.left)

Premises used: CategoryTheory.CostructuredArrow.left, Opposite.unop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this_1 : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
this :
  ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsCofiltered J] (d : J) (n : ℕ)
    (g : Functor.obj (sequentialFunctor J) (op n) ≤ d)
    (this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d))
    (i j : CostructuredArrow (sequentialFunctor J) d) (h : unop i.left ≤ unop j.left),
    Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
h : unop j.left < unop i.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
or_comm.1 (this J d n g inferInstance j i (le_of_lt h))

Premises used: le_of_lt, inferInstance, Iff.mp, or_comm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J : Type u_2
inst : Countable J
inst_1 : Preorder J
inst_2 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this_1 : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
this :
  ∀ (J : Type u_2) [inst : Countable J] [inst_3 : Preorder J] [inst_4 : IsCofiltered J] (d : J) (n : ℕ)
    (g : Functor.obj (sequentialFunctor J) (op n) ≤ d)
    (this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d))
    (i j : CostructuredArrow (sequentialFunctor J) d) (h : unop i.left ≤ unop j.left),
    Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
h : unop j.left < unop i.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
exact or_comm.1 (this J d n g inferInstance j i (le_of_lt h))

Premises used: le_of_lt, inferInstance, Iff.mp, or_comm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J_1 : Type u_2
inst : Countable J_1
inst_1 : Preorder J_1
inst_2 : IsCofiltered J_1
J : Type u_2
inst_3 : Countable J
inst_4 : Preorder J
inst_5 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
h₁ : Nonempty (j ⟶ i)
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J_1 : Type u_2
inst : Countable J_1
inst_1 : Preorder J_1
inst_2 : IsCofiltered J_1
J : Type u_2
inst_3 : Countable J
inst_4 : Preorder J
inst_5 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (j ⟶ i)

Tactic:
⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩

Premises used: Quiver.Hom.op, CategoryTheory.CostructuredArrow.homMk, Nonempty.intro, CategoryTheory.homOfLE, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Countable
Goal:
J_1 : Type u_2
inst : Countable J_1
inst_1 : Preorder J_1
inst_2 : IsCofiltered J_1
J : Type u_2
inst_3 : Countable J
inst_4 : Preorder J
inst_5 : IsCofiltered J
d : J
n : ℕ
g : Functor.obj (sequentialFunctor J) (op n) ≤ d
this : Nonempty.{max 1 (u_2 + 1)} (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (j ⟶ i)

Tactic:
exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullback f f
⊢ CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (fst f f) = 𝟙 X

Tactic:
pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.pullback.diagonal, CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullback f f
⊢ CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (snd f f) = 𝟙 X

Tactic:
pullback.lift_snd _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.pullback.diagonal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
inst_1 : HasPullback f f
⊢ IsSplitMono (Y := diagonalObj f) (diagonal f)

Tactic:
⟨⟨⟨pullback.fst _ _, diagonal_fst f⟩⟩⟩

Premises used: CategoryTheory.SplitMono.mk, CategoryTheory.Limits.pullback.diagonal_fst, Nonempty.intro, CategoryTheory.Limits.pullback.fst, CategoryTheory.IsSplitMono.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
inst_1 : HasPullback f f
⊢ IsSplitEpi (X := pullback f f) (fst f f)

Tactic:
⟨⟨⟨diagonal f, diagonal_fst f⟩⟩⟩

Premises used: CategoryTheory.Limits.pullback.diagonal_fst, Nonempty.intro, CategoryTheory.SplitEpi.mk, CategoryTheory.IsSplitEpi.mk, CategoryTheory.Limits.pullback.diagonal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
inst_1 : HasPullback f f
⊢ IsSplitEpi (X := pullback f f) (snd f f)

Tactic:
⟨⟨⟨diagonal f, diagonal_snd f⟩⟩⟩

Premises used: CategoryTheory.Limits.pullback.diagonal_snd, Nonempty.intro, CategoryTheory.SplitEpi.mk, CategoryTheory.IsSplitEpi.mk, CategoryTheory.Limits.pullback.diagonal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
inst_1 : HasPullback f f
inst_2 : Mono f
rw : IsIso (Y := diagonalObj f) (inv (fst f f))
⊢ IsIso (Y := diagonalObj f) (diagonal f)

Tactic:
rw [(IsIso.inv_eq_of_inv_hom_id (diagonal_fst f)).symm]

Premises used: CategoryTheory.Limits.pullback.diagonal_fst, CategoryTheory.IsIso.inv_eq_of_inv_hom_id, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
inst_1 : HasPullback f f
inst_2 : Mono f
⊢ IsIso (Y := diagonalObj f) (inv (fst f f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullback f f
H : IsIso (Y := diagonalObj f) (diagonal f)
Z : C
x x_1 : Z ⟶ X
e : x ≫ f = x_1 ≫ f
⊢ CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (fst f f) =
    CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (snd f f)

Tactic:
simp