awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h :
  ∀ (j : J),
    ∃ (i : J) (f : i ⟶ j),
      Set.Finite (α := (fun (X : Type v) ↦ X) (F.obj j))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
j i_1 : J
hi : i_1 ⟶ j
hf :
  Set.Finite (α := (fun (X : Type v) ↦ X) (F.obj j))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj i_1))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map hi)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i_1)) → (fun (X : Type v) ↦ X) (F.obj j)))
m : Finset (F.obj j)
hmin :
  ∀ (x : Finset (F.obj j)),
    Membership.mem (γ := Set (Finset (F.obj j)))
        {s : Finset (F.obj j) |
          ∃ (i : J) (f : i ⟶ j),
            (↑s : Set ((fun (X : Type v) ↦ X) (F.obj j))) =
              range (ι := (fun (X : Type v) ↦ X) (F.obj i))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
                  (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))}
        x →
      ¬x < m
i : J
f : i ⟶ j
hm :
  (↑m : Set ((fun (X : Type v) ↦ X) (F.obj j))) =
    range (ι := (fun (X : Type v) ↦ X) (F.obj i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
⊢ ∃ (i : J) (f : i ⟶ j),
    ∀ ⦃k : J⦄ (g : k ⟶ j),
      Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))

Tactic:
⟨i, f, fun k g =>
    (F.ranges_directed j).directedOn_range.is_bot_of_is_min ⟨⟨i, f⟩, rfl⟩ ?_ _ ⟨⟨k, g⟩, rfl⟩⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Directed.directedOn_range, DirectedOn.is_bot_of_is_min, CategoryTheory.Functor.map, CategoryTheory.Functor.ranges_directed, Exists.intro, PSigma.mk, Set.range, DFunLike.coe, rfl
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h :
  ∀ (j : J),
    ∃ (i : J) (f : i ⟶ j),
      Set.Finite (α := (fun (X : Type v) ↦ X) (F.obj j))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
j i_1 : J
hi : i_1 ⟶ j
hf :
  Set.Finite (α := (fun (X : Type v) ↦ X) (F.obj j))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj i_1))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map hi)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i_1)) → (fun (X : Type v) ↦ X) (F.obj j)))
m : Finset (F.obj j)
hmin :
  ∀ (x : Finset (F.obj j)),
    Membership.mem (γ := Set (Finset (F.obj j)))
        {s : Finset (F.obj j) |
          ∃ (i : J) (f : i ⟶ j),
            (↑s : Set ((fun (X : Type v) ↦ X) (F.obj j))) =
              range (ι := (fun (X : Type v) ↦ X) (F.obj i))
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
                  (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))}
        x →
      ¬x < m
i : J
f : i ⟶ j
hm :
  (↑m : Set ((fun (X : Type v) ↦ X) (F.obj j))) =
    range (ι := (fun (X : Type v) ↦ X) (F.obj i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
k : J
g : k ⟶ j
k' : J
g' : k' ⟶ j
hl :
  LE.le.{v} (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    ((fun (f : (i : J) ×' (i ⟶ j)) ↦
        (range (ι := (fun (X : Type v) ↦ X) (F.obj (f.fst (β := fun (i : J) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : J) ↦ i ⟶ j)))) :
              (a : (fun (X : Type v) ↦ X) (F.obj f.fst)) → (fun (X : Type v) ↦ X) (F.obj j)) :
          Set ((fun (X : Type v) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : J) ↦ i ⟶ j) k' g'))
    ((fun (f : (i : J) ×' (i ⟶ j)) ↦
        (range (ι := (fun (X : Type v) ↦ X) (F.obj (f.fst (β := fun (i : J) ↦ i ⟶ j))))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f.snd (β := fun (i : J) ↦ i ⟶ j)))) :
              (a : (fun (X : Type v) ↦ X) (F.obj f.fst)) → (fun (X : Type v) ↦ X) (F.obj j)) :
          Set ((fun (X : Type v) ↦ X) (F.obj j))))
      (PSigma.mk (β := fun (i : J) ↦ i ⟶ j) i f))
⊢ ¬⋯.toFinset (s :=
        range (ι := (fun (X : Type v) ↦ X) (F.obj k'))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g')) :
            (a : (fun (X : Type v) ↦ X) (F.obj k')) → (fun (X : Type v) ↦ X) (F.obj j))) <
      m

Tactic:
have := hmin _ ⟨k', g', (m.finite_toSet.subset <| hm.substr hl).coe_toFinset⟩
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
i j k : J
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
⊢ ∀ (j : J), Finite.{v + 1} (F.toEventualRanges.obj j)

Tactic:
fun _ => Subtype.finite

Premises used: Subtype.finite
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
i j : J
f : i ⟶ j
x_1 : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j)
x : (fun (X : Type v) ↦ X) (F.obj j)
hx : x ∈ F.eventualRange j
obtain :
  ∀ (y : F.obj i) (hy : y ∈ F.eventualRange i)
    (hx :
      Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j)) (F.eventualRange j)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
            y :
          (fun (X : Type v) ↦ X) (F.obj j))),
    ∃ (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)),
      Eq (α := (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.toEventualRanges.map f) :
              (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)) →
                (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
            a :
          (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
        (Subtype.mk (p := fun (x : (fun (X : Type v) ↦ X) (F.obj j)) ↦ x ∈ F.eventualRange j)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
              y)
            hx :
          { x : (fun (X : Type v) ↦ X) (F.obj j) // x ∈ F.eventualRange j })
⊢ ∃ (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.toEventualRanges.map f) :
          (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)) → (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
        a =
      Subtype.mk (p := fun (x : (fun (X : Type v) ↦ X) (F.obj j)) ↦ x ∈ F.eventualRange j) x hx

Tactic:
obtain ⟨y, hy, rfl⟩ := h.subset_image_eventualRange F f hx

Premises used: CategoryTheory.Functor.IsMittagLeffler.subset_image_eventualRange, rfl
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
i j : J
f : i ⟶ j
x : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j)
y : F.obj i
hy : y ∈ F.eventualRange i
hx :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j)) (F.eventualRange j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
        y :
      (fun (X : Type v) ↦ X) (F.obj j))
⊢ ∃ (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)),
    Eq (α := (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.toEventualRanges.map f) :
            (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)) → (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
          a :
        (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
      (Subtype.mk (p := fun (x : (fun (X : Type v) ↦ X) (F.obj j)) ↦ x ∈ F.eventualRange j)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
            y)
          hx :
        { x : (fun (X : Type v) ↦ X) (F.obj j) // x ∈ F.eventualRange j })

Tactic:
⟨⟨y, hy⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
i j : J
f : i ⟶ j
x : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j)
y : F.obj i
hy : y ∈ F.eventualRange i
hx :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j)) (F.eventualRange j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
        y :
      (fun (X : Type v) ↦ X) (F.obj j))
⊢ ∃ (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)),
    Eq (α := (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.toEventualRanges.map f) :
            (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)) → (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
          a :
        (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
      (Subtype.mk (p := fun (x : (fun (X : Type v) ↦ X) (F.obj j)) ↦ x ∈ F.eventualRange j)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
            y)
          hx :
        { x : (fun (X : Type v) ↦ X) (F.obj j) // x ∈ F.eventualRange j })

Tactic:
exact ⟨⟨y, hy⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
j : J
let :
  ∀ (i : J) (f : i ⟶ j)
    (h :
      F.eventualRange j =
        range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))),
    Nonempty.{v + 1} (F.toEventualRanges.obj j)
⊢ Nonempty.{v + 1} (F.toEventualRanges.obj j)

Tactic:
let ⟨i, f, h⟩ := F.isMittagLeffler_iff_eventualRange.1 h j
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h_1 : F.IsMittagLeffler
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
j i : J
f : i ⟶ j
h :
  F.eventualRange j =
    range (ι := (fun (X : Type v) ↦ X) (F.obj i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
rw :
  Nonempty.{v + 1}
    (↑(range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))) :
      Type v)
⊢ Nonempty.{v + 1} (F.toEventualRanges.obj j)

Tactic:
rw [toEventualRanges_obj, h]

Premises used: CategoryTheory.Functor.toEventualRanges_obj
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h_1 : F.IsMittagLeffler
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
j i : J
f : i ⟶ j
h :
  F.eventualRange j =
    range (ι := (fun (X : Type v) ↦ X) (F.obj i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
⊢ Nonempty.{v + 1}
    (↑(range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))) :
      Type v)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
i j : J
f g : i ⟶ j
let : ∀ (k : J) (φ : k ⟶ i) (hφ : φ ≫ f = φ ≫ g), F.map f = F.map g
⊢ F.map f = F.map g

Tactic:
let ⟨k, φ, hφ⟩ := IsCofilteredOrEmpty.cone_maps f g
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
i j : J
f g : i ⟶ j
k : J
φ : k ⟶ i
hφ : φ ≫ f = φ ≫ g
h : ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) = ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)
⊢ F.map f = F.map g

Tactic:
apply ConcreteCategory.ext

Premises used: CategoryTheory.ConcreteCategory.ext
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
i j : J
f g : i ⟶ j
k : J
φ : k ⟶ i
hφ : φ ≫ f = φ ≫ g
⊢ F.map (φ ≫ f) = F.map (φ ≫ g)

Tactic:
have := congrArg F.map hφ
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
i j : J
f g : i ⟶ j
k : J
φ : k ⟶ i
hφ : φ ≫ f = φ ≫ g
this : F.map (φ ≫ f) = F.map (φ ≫ g)
⊢ Eq.{v + 1} (α := (x : F.obj k) → F.obj j)
    (fun (x : F.obj k) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj i) → F.obj j)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ) : (a : F.obj k) → F.obj i) x : F.obj i))
    fun (x : F.obj k) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj i) → F.obj j)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ) : (a : F.obj k) → F.obj i) x : F.obj i)

Tactic:
simp only [map_comp, ConcreteCategory.ext_iff, DFunLike.ext_iff, comp_apply, ← funext_iff] at this

Premises used: funext_iff, DFunLike.ext_iff, CategoryTheory.ConcreteCategory.ext_iff, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
i j : J
f g : i ⟶ j
k : J
φ : k ⟶ i
hφ : φ ≫ f = φ ≫ g
this :
  Eq.{v + 1} (α := (x : F.obj k) → F.obj j)
    (fun (x : F.obj k) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj i) → F.obj j)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ) : (a : F.obj k) → F.obj i) x : F.obj i))
    fun (x : F.obj k) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj i) → F.obj j)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ) : (a : F.obj k) → F.obj i) x : F.obj i)
⊢ ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) = ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)

Tactic:
simpa using (Fsur φ).injective_comp_right <| this

Premises used: Function.Surjective.injective_comp_right
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
i : J
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
hFn : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
hs : s.Nonempty
j : J
simp :
  ∃ (x : F.obj j),
    ∀ (i_1 : j ⟶ i),
      Membership.mem (α := F.obj i) s
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj j) → F.obj i) x : F.obj i)
⊢ Nonempty.{v + 1} ((F.toPreimages s).obj j)

Tactic:
simp only [toPreimages_obj, nonempty_coe_sort, nonempty_iInter, mem_preimage]

Premises used: Set.nonempty_coe_sort, Set.nonempty_iInter, CategoryTheory.Functor.toPreimages_obj, Set.mem_preimage
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
i : J
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
hFn : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
hs : s.Nonempty
j : J
inl :
  ∀ (h : IsEmpty.{v_1 + 1} (j ⟶ i)),
    ∃ (x : F.obj j),
      ∀ (i_1 : j ⟶ i),
        Membership.mem (α := F.obj i) s
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj j) → F.obj i) x : F.obj i)
inr :
  ∀ (ji : j ⟶ i),
    ∃ (x : F.obj j),
      ∀ (i_1 : j ⟶ i),
        Membership.mem (α := F.obj i) s
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj j) → F.obj i) x : F.obj i)
⊢ ∃ (x : F.obj j),
    ∀ (i_1 : j ⟶ i),
      Membership.mem (α := F.obj i) s
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj j) → F.obj i) x : F.obj i)

Tactic:
obtain h | ⟨⟨ji⟩⟩ := isEmpty_or_nonempty (j ⟶ i)

Premises used: Quiver.Hom, isEmpty_or_nonempty
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
i : J
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
hFn : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
hs : s.Nonempty
j : J
h : IsEmpty.{v_1 + 1} (j ⟶ i)
⊢ ∃ (x : F.obj j),
    ∀ (i_1 : j ⟶ i),
      Membership.mem (α := F.obj i) s
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj j) → F.obj i) x : F.obj i)

Tactic:
⟨(hFn j).some, fun ji => h.elim ji⟩

Premises used: IsEmpty.elim, Nonempty.some, Exists.intro
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
i : J
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
hFn : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
hs : s.Nonempty
j : J
h : IsEmpty.{v_1 + 1} (j ⟶ i)
⊢ ∃ (x : F.obj j),
    ∀ (i_1 : j ⟶ i),
      Membership.mem (α := F.obj i) s
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj j) → F.obj i) x : F.obj i)

Tactic:
exact ⟨(hFn j).some, fun ji => h.elim ji⟩
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
i : J
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
hFn : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
hs : s.Nonempty
j : J
ji : j ⟶ i
inr :
  ∀ (y : F.obj i) (ys : y ∈ s),
    ∃ (x : F.obj j),
      ∀ (i_1 : j ⟶ i),
        Membership.mem (α := F.obj i) s
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj j) → F.obj i) x : F.obj i)
⊢ ∃ (x : F.obj j),
    ∀ (i_1 : j ⟶ i),
      Membership.mem (α := F.obj i) s
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj j) → F.obj i) x : F.obj i)

Tactic:
obtain ⟨y, ys⟩ := hs
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{v_1, u} J
F : Functor.{v_1, v, u, v + 1} J (Type v)
i : J
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
hFn : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
Fsur :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
j : J
ji : j ⟶ i
y : F.obj i
ys : y ∈ s
inr :
  ∀ (x : F.obj j)
    (ys :
      Membership.mem (α := F.obj i) s
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ji) :
              (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
            x :
          (fun (X : Type v) ↦ X) (F.obj i))),
    ∃ (x : F.obj j),
      ∀ (i_1 : j ⟶ i),
        Membership.mem (α := F.obj i) s
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj j) → F.obj i) x : F.obj i)
⊢ ∃ (x : F.obj j),
    ∀ (i_1 : j ⟶ i),
      Membership.mem (α := F.obj i) s
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1) : (a : F.obj j) → F.obj i) x : F.obj i)

Tactic:
obtain ⟨x, rfl⟩ := Fsur ji y

Premises used: rfl