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)
i j k : J
f : i ⟶ j
g : j ⟶ k
h :
  F.eventualRange k =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj k))
a :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj k)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
      (Function.comp (β := (fun (X : Type v) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj k))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) ((fun (X : Type v) ↦ X) (F.obj i))) → (fun (X : Type v) ↦ X) (F.obj j))))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj k)))
⊢ range (ι := (fun (X : Type v) ↦ X) (F.obj i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f ≫ g))) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj k)) ⊆
    F.eventualRange k

Tactic:
rw [h, F.map_comp, types_comp]

Premises used: CategoryTheory.types_comp, 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)
i j k : J
f : i ⟶ j
g : j ⟶ k
h :
  F.eventualRange k =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj k))
⊢ Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj k)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
      (Function.comp (β := (fun (X : Type v) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj k))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) ((fun (X : Type v) ↦ X) (F.obj i))) → (fun (X : Type v) ↦ X) (F.obj j))))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj k)))

Tactic:
apply range_comp_subset_range

Premises used: Set.range_comp_subset_range
-- 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)
h :
  ∀ ⦃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 k : J
g : k ⟶ j
rw :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj j))) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (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)))
rw₁ :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j))) (range id)
    (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)))
rw₂ :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j))) univ
    (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)))
rw₃ rw₄ : Subset.{v} (α := Set ((fun (X : Type v) ↦ X) (F.obj j))) univ univ
⊢ Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j))) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (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:
rw [map_id, types_id, range_id, (h g).range_eq]

Premises used: CategoryTheory.types_id, Function.Surjective.range_eq, CategoryTheory.Functor.map_id, Set.range_id
-- 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)
X Y : J
g : X ⟶ Y
x : (fun (X : Type v) ↦ X) (F.obj X)
h :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
    (⋂ (f : X ⟶ i),
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
    x
rw :
  ∀
    (h :
      ∀ (i_1 : X ⟶ i),
        Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
          ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
              (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
            s)
          x)
    (i_1 : Y ⟶ i),
    Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj Y)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj Y)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
          (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
          x :
        (fun (X : Type v) ↦ X) (F.obj Y))
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj Y)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj Y)))
    (⋂ (f : Y ⟶ i),
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
        x :
      (fun (X : Type v) ↦ X) (F.obj Y))

Tactic:
rw [mem_iInter] at h ⊢

Premises used: Set.mem_iInter
-- 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)
X Y : J
g : X ⟶ Y
x : (fun (X : Type v) ↦ X) (F.obj X)
h :
  ∀ (i_1 : X ⟶ i),
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
f : Y ⟶ i
rw :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
            x :
          (fun (X : Type v) ↦ X) (F.obj Y)) :
      (fun (X : Type v) ↦ X) (F.obj i))
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj Y)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj Y)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
        x :
      (fun (X : Type v) ↦ X) (F.obj Y))

Tactic:
rw [← mem_preimage, preimage_preimage, mem_preimage]

Premises used: Set.preimage_preimage, 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 k : J
s : Set (F.obj i)
X Y : J
g : X ⟶ Y
x : (fun (X : Type v) ↦ X) (F.obj X)
h :
  ∀ (i_1 : X ⟶ i),
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
f : Y ⟶ i
⊢ Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f))) :
        (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    x

Tactic:
h (g ≫ f)

Premises used: CategoryTheory.CategoryStruct.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)
i j k : J
s : Set (F.obj i)
X Y : J
g : X ⟶ Y
x : (fun (X : Type v) ↦ X) (F.obj X)
h :
  ∀ (i_1 : X ⟶ i),
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
f : Y ⟶ i
a :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
              x :
            (fun (X : Type v) ↦ X) (F.obj Y)) :
        (fun (X : Type v) ↦ X) (F.obj i)) ↔
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f))) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
            x :
          (fun (X : Type v) ↦ X) (F.obj Y)) :
      (fun (X : Type v) ↦ X) (F.obj i))

Tactic:
convert! h (g ≫ f)

Premises used: CategoryTheory.CategoryStruct.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)
i j k : J
s : Set (F.obj i)
X Y : J
g : X ⟶ Y
x : (fun (X : Type v) ↦ X) (F.obj X)
h :
  ∀ (i_1 : X ⟶ i),
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
f : Y ⟶ i
a :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
              x :
            (fun (X : Type v) ↦ X) (F.obj Y)) :
        (fun (X : Type v) ↦ X) (F.obj i)) ↔
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g ≫ F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
              x :
            (fun (X : Type v) ↦ X) (F.obj Y)) :
        (fun (X : Type v) ↦ X) (F.obj i)) ↔
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f))) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x

Tactic:
rw [F.map_comp]

Premises used: 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)
i j k : J
s : Set (F.obj i)
X Y : J
g : X ⟶ Y
x : (fun (X : Type v) ↦ X) (F.obj X)
h :
  ∀ (i_1 : X ⟶ i),
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
f : Y ⟶ i
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
              x :
            (fun (X : Type v) ↦ X) (F.obj Y)) :
        (fun (X : Type v) ↦ X) (F.obj i)) ↔
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g ≫ F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x

Tactic:
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)
i j k : J
s : Set (F.obj i)
inst_1 : ∀ (j : J), Finite.{v + 1} (F.obj j)
⊢ ∀ (j : J), Finite.{v + 1} ((F.toPreimages s).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)
i j : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : j ⟶ i
x : (fun (X : Type v) ↦ X) (F.obj j)
hx : x ∈ F.eventualRange j
rw :
  ∀
    (hx :
      ∀ ⦃i : J⦄ (f : i ⟶ j),
        Membership.mem (γ := 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)
    ⦃i_1 : J⦄ (f_1 : i_1 ⟶ i),
    Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
      (range (ι := (fun (X : Type v) ↦ X) (F.obj i_1))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i_1)) → (fun (X : Type v) ↦ X) (F.obj i)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (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))
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) (F.eventualRange i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (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))

Tactic:
rw [mem_eventualRange_iff] at hx ⊢

Premises used: CategoryTheory.Functor.mem_eventualRange_iff
-- 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 : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : j ⟶ i
x : (fun (X : Type v) ↦ X) (F.obj j)
hx :
  ∀ ⦃i : J⦄ (f : i ⟶ j),
    Membership.mem (γ := 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
k : J
f' : k ⟶ i
obtain :
  ∀ (l : J) (g : l ⟶ j) (g' : l ⟶ k) (he : g ≫ f = g' ≫ f'),
    Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
      (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (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))
⊢ Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (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))

Tactic:
obtain ⟨l, g, g', he⟩ := cospan f f'

Premises used: CategoryTheory.IsCofiltered.cospan
-- 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 : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : j ⟶ i
x : (fun (X : Type v) ↦ X) (F.obj j)
hx :
  ∀ ⦃i : J⦄ (f : i ⟶ j),
    Membership.mem (γ := 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
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
obtain :
  ∀ (x : F.obj l)
    (hx :
      ∀ ⦃i : J⦄ (f : i ⟶ j),
        Membership.mem (α := F.obj j) (γ := 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)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                (a : (fun (X : Type v) ↦ X) (F.obj l)) → (fun (X : Type v) ↦ X) (F.obj j))
              x :
            (fun (X : Type v) ↦ X) (F.obj j))),
    Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
      (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                (a : (fun (X : Type v) ↦ X) (F.obj l)) → (fun (X : Type v) ↦ X) (F.obj j))
              x :
            (fun (X : Type v) ↦ X) (F.obj j)) :
        (fun (X : Type v) ↦ X) (F.obj i))
⊢ Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (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))

Tactic:
obtain ⟨x, rfl⟩ := hx g

Premises used: 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)
i j : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : j ⟶ i
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
x : F.obj l
hx :
  ∀ ⦃i : J⦄ (f : i ⟶ j),
    Membership.mem (α := F.obj j) (γ := 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)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj l)) → (fun (X : Type v) ↦ X) (F.obj j))
          x :
        (fun (X : Type v) ↦ X) (F.obj j))
rw :
  Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g' ≫ F.map f') : (a : (fun (X : Type v) ↦ X) (F.obj l)) → F.obj i)
        x :
      F.obj i)
⊢ Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj l)) → (fun (X : Type v) ↦ X) (F.obj j))
            x :
          (fun (X : Type v) ↦ X) (F.obj j)) :
      (fun (X : Type v) ↦ X) (F.obj i))

Tactic:
rw [← comp_apply, ← map_comp, he, F.map_comp]

Premises used: 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)
i j : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : j ⟶ i
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
x : F.obj l
hx :
  ∀ ⦃i : J⦄ (f : i ⟶ j),
    Membership.mem (α := F.obj j) (γ := 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)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj l)) → (fun (X : Type v) ↦ X) (F.obj j))
          x :
        (fun (X : Type v) ↦ X) (F.obj j))
⊢ Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g' ≫ F.map f') : (a : (fun (X : Type v) ↦ X) (F.obj l)) → F.obj i)
        x :
      F.obj i)

Tactic:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, 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)
i j : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : j ⟶ i
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
x : F.obj l
hx :
  ∀ ⦃i : J⦄ (f : i ⟶ j),
    Membership.mem (α := F.obj j) (γ := 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)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj l)) → (fun (X : Type v) ↦ X) (F.obj j))
          x :
        (fun (X : Type v) ↦ X) (F.obj j))
⊢ Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g' ≫ F.map f') : (a : (fun (X : Type v) ↦ X) (F.obj l)) → F.obj i)
        x :
      F.obj i)

Tactic:
exact ⟨_, rfl⟩