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
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ 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)) ⁻¹'
        s)
    x
rw :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₁)) (γ := 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 f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
⊢ 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 j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))

Tactic:
rw [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)
i : J
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ 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)) ⁻¹'
        s)
    x
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₁)) (γ := 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 f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))

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
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ 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)) ⁻¹'
        s)
    x
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₁)) (γ := 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 f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))

Tactic:
exact ⟨_, 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
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ 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)) ⁻¹'
        s)
    x
⊢ 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 j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))

Tactic:
have : F.map f₂ x ∈ F.eventualRange j₁ := by
      rw [h₂]
      exact ⟨_, 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
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ 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)) ⁻¹'
        s)
    x
this :
  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 j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
y : F.obj j₃
hy : y ∈ F.eventualRange j₃
h₃ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)) (γ :=
    Set ((fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
    (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j₃))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))) :
        (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j₃)) → (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (f₂ ≫ f₁)) :
          (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j₂)) → (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j))
        (Subtype.mk (p := fun (x : (fun (X : Type v) ↦ X) (F.obj j₂)) ↦
          Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
            (⋂ (f : j₂ ⟶ 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)) ⁻¹'
                s)
            x)
          x hx) :
      (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j))

Tactic:
⟨⟨y, mem_iInter.2 fun g₂ => ?_⟩, Subtype.ext ?_⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.mem_iInter, Subtype.mk, Exists.intro, Set.range, Subtype.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)
i : J
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ 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)) ⁻¹'
        s)
    x
this :
  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 j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
y : F.obj j₃
hy : y ∈ F.eventualRange j₃
h₃ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
g₂ : j₃ ⟶ i
refine_1 :
  ∀ (j₄ : J) (f₄ : j₄ ⟶ j₃) (h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁),
    Membership.mem (γ := Set ((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 i)) ⁻¹'
        s)
      y
⊢ Membership.mem (γ := Set ((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 i)) ⁻¹'
      s)
    y

Tactic:
obtain ⟨j₄, f₄, h₄⟩ := IsCofilteredOrEmpty.cone_maps g₂ ((f₃ ≫ f₂) ≫ g₁)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.IsCofilteredOrEmpty.cone_maps
-- 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
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ 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)) ⁻¹'
        s)
    x
this :
  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 j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy :
  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 j₄)) → (fun (X : Type v) ↦ X) (F.obj j₃))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₃))
h₃ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₄) :
              (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → (fun (X : Type v) ↦ X) (F.obj j₃))
            y :
          (fun (X : Type v) ↦ X) (F.obj j₃)) :
      (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₄ ≫ f₃ ≫ f₂)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → F.obj j₁)
        y :
      F.obj j₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))

Tactic:
rw [← comp_apply, ← map_comp] at h₃

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
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ 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)) ⁻¹'
        s)
    x
this :
  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 j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy :
  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 j₄)) → (fun (X : Type v) ↦ X) (F.obj j₃))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₃))
h₃ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₄ ≫ f₃ ≫ f₂)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → F.obj j₁)
        y :
      F.obj j₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
refine_1 :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ g₁)) : (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → F.obj i)
        x :
      F.obj i)
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₃)) (γ := Set ((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 i)) ⁻¹'
      s)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₄) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → (fun (X : Type v) ↦ X) (F.obj j₃))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₃))

Tactic:
rw [mem_preimage, ← comp_apply, ← map_comp, h₄, ← Category.assoc, map_comp, comp_apply, h₃,
        ← comp_apply, ← map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp, 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
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ 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)) ⁻¹'
        s)
    x
this :
  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 j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy :
  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 j₄)) → (fun (X : Type v) ↦ X) (F.obj j₃))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₃))
h₃ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₄ ≫ f₃ ≫ f₂)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → F.obj j₁)
        y :
      F.obj j₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ g₁)) : (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → F.obj i)
        x :
      F.obj i)

Tactic:
apply mem_iInter.1 hx

Premises used: Set.mem_iInter, Iff.mp
-- 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 : J
obtain :
  ∀ (i : J) (hi : i ⟶ j)
    (hf :
      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 hi)) :
            (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)))
⊢ ∃ (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:
obtain ⟨i, hi, hf⟩ := 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 :
  ∀ (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 : J
hi : i ⟶ j
hf :
  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 hi)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
obtain :
  ∀ (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)))
⊢ ∃ (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:
obtain ⟨m, ⟨i, f, hm⟩, hmin⟩ := Finset.wellFoundedLT.wf.has_min
    { s : Finset (F.obj j) | ∃ (i : _) (f : i ⟶ j), ↑s = range (F.map f) }
    ⟨_, i, hi, hf.coe_toFinset⟩

Premises used: CategoryTheory.ConcreteCategory.hom, setOf, Exists, Set.Finite.coe_toFinset, IsWellFounded.wf, CategoryTheory.Functor.map, SetLike.coe, Exists.intro, Set.range, WellFounded.has_min, Eq, DFunLike.coe