awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite.{u + 1} (F.obj j)
hne : ∀ (j : J), Nonempty.{u + 1} (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this_1 : ∀ (j : J), DiscreteTopology.{u} (↑(F'.obj j) : Type u)
this_2 : ∀ (j : J), Finite.{u + 1} (↑(F'.obj j) : Type u)
this : ∀ (j : J), Nonempty.{u + 1} (↑(F'.obj j) : Type u)
u : (j : J) → (↑(F'.obj j) : Type u)
hu :
  Membership.mem (γ := Set ((j : J) → (↑(F'.obj j) : Type u)))
    {u : (j : J) → (↑(F'.obj j) : Type u) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (F'.map f) :
              (a : (↑(F'.obj i) : Type u)) → (↑(F'.obj j) : Type u))
            (u i) =
          u j}
    u
⊢ F.sections.Nonempty

Tactic:
⟨u, hu⟩

Premises used: Set.Nonempty, Exists.intro
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsCofilteredOrEmpty J
F : J ⥤ Type u
hf : ∀ (j : J), Finite.{u + 1} (F.obj j)
hne : ∀ (j : J), Nonempty.{u + 1} (F.obj j)
F' : J ⥤ TopCat := F ⋙ TopCat.discrete
this_1 : ∀ (j : J), DiscreteTopology.{u} (↑(F'.obj j) : Type u)
this_2 : ∀ (j : J), Finite.{u + 1} (↑(F'.obj j) : Type u)
this : ∀ (j : J), Nonempty.{u + 1} (↑(F'.obj j) : Type u)
u : (j : J) → (↑(F'.obj j) : Type u)
hu :
  Membership.mem (γ := Set ((j : J) → (↑(F'.obj j) : Type u)))
    {u : (j : J) → (↑(F'.obj j) : Type u) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (F'.map f) :
              (a : (↑(F'.obj i) : Type u)) → (↑(F'.obj j) : Type u))
            (u i) =
          u j}
    u
⊢ F.sections.Nonempty

Tactic:
exact ⟨u, hu⟩
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
⊢ ∀ (i : J'), Nonempty (F'.obj i)

Tactic:
haveI : ∀ i, Nonempty (F'.obj i) := fun i => ⟨⟨Classical.arbitrary (F.obj (down.obj i))⟩⟩
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this : ∀ (i : J'), Nonempty (F'.obj i)
⊢ ∀ (i : J'), Finite (F'.obj i)

Tactic:
haveI : ∀ i, Finite (F'.obj i) := fun i => Finite.of_equiv (F.obj (down.obj i)) Equiv.ulift.symm
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
inl : IsEmpty J → F.sections.Nonempty
inr : Nonempty J → F.sections.Nonempty
⊢ F.sections.Nonempty

Tactic:
cases isEmpty_or_nonempty J

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h : IsEmpty J
inl : (j : J) → F.obj j
inl₁ : isEmptyElim (p := F.obj) ∈ F.sections
⊢ F.sections.Nonempty

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h : IsEmpty J
⊢ (j : J) → F.obj j

Tactic:
apply isEmptyElim
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h : IsEmpty J
⊢ isEmptyElim (p := F.obj) ∈ F.sections

Tactic:
apply isEmptyElim
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this : ∀ (i : J'), Finite (F'.obj i)
h : Nonempty J
⊢ IsCofiltered.{w, u} J

Tactic:
haveI : IsCofiltered J := ⟨⟩
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this_2 : ∀ (i : J'), Finite (F'.obj i)
h : Nonempty J
this : IsCofiltered.{w, u} J
inr : ∀ (u : (j : J') → F'.obj j) (hu : u ∈ F'.sections), F.sections.Nonempty
⊢ F.sections.Nonempty

Tactic:
obtain ⟨u, hu⟩ := nonempty_sections_of_finite_cofiltered_system.init F'

Premises used: nonempty_sections_of_finite_cofiltered_system.init
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this_2 : ∀ (i : J'), Finite (F'.obj i)
h_1 : Nonempty J
this : IsCofiltered.{w, u} J
u : (j : J') → F'.obj j
hu : u ∈ F'.sections
h : (fun (j : J) ↦ ULift.down (u { down := j })) ∈ F.sections
⊢ F.sections.Nonempty

Tactic:
use fun j => (u ⟨j⟩).down

Premises used: ULift.up, ULift.down
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this_2 : ∀ (i : J'), Finite (F'.obj i)
h : Nonempty J
this : IsCofiltered.{w, u} J
u : (j : J') → F'.obj j
hu : u ∈ F'.sections
j j' : J
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type (max (max u v) w)) ↦ X) (F'.obj { down := j' }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F'.map
              { down := f :
                ULift.{max (max u v) w, w}
                  ({ down := j : ULift.{max v w, u} J }.down ⟶ { down := j' : ULift.{max v w, u} J }.down) }) :
          (a : (fun (X : Type (max (max u v) w)) ↦ X) (F'.obj { down := j })) →
            (fun (X : Type (max (max u v) w)) ↦ X) (F'.obj { down := j' }))
        (u { down := j }) :
      (fun (X : Type (max (max u v) w)) ↦ X) (F'.obj { down := j' }))
    (u { down := j' } : F'.obj { down := j' })

Tactic:
have h := @hu (⟨j⟩ : J') (⟨j'⟩ : J') (ULift.up f)
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Category.{w, u} J
inst_1 : IsCofilteredOrEmpty.{w, u} J
F : CategoryTheory.Functor.{w, v, u, v + 1} J (Type v)
inst_2 : ∀ (j : J), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
J' : Type (max w v u) := AsSmall J
down : J' ⥤ J := AsSmall.down
F' : J' ⥤ Type (max u v w) := down ⋙ F ⋙ uliftFunctor.{max u w, v}
this_1 : ∀ (i : J'), Nonempty (F'.obj i)
this_2 : ∀ (i : J'), Finite (F'.obj i)
h_1 : Nonempty J
this : IsCofiltered.{w, u} J
u : (j : J') → F'.obj j
hu : u ∈ F'.sections
j j' : J
f : j ⟶ j'
h :
  Eq (α :=
    ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := ⋯,
            map_comp := ⋯ : AsSmall J ⥤ J } ⋙
          F ⋙ uliftFunctor.{max u w, v}).obj
      { down := j' })
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (x : ULift.{max u w, v} (F.obj j)) ↦
              { down := (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj j') x.down :
                ULift.{max u w, v} (F.obj j') }) :
          (a :
              ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    F ⋙ uliftFunctor.{max u w, v}).obj
                { down := j }) →
            ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := ⋯,
                    map_comp := ⋯ } ⋙
                  F ⋙ uliftFunctor.{max u w, v}).obj
              { down := j' })
        (u { down := j }) :
      ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := ⋯,
              map_comp := ⋯ : AsSmall J ⥤ J } ⋙
            F ⋙ uliftFunctor.{max u w, v}).obj
        { down := j' })
    (u { down := j' } : F'.obj { down := j' })
⊢ Eq (α := F.obj j')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj j') (ULift.down (u { down := j })) :
      F.obj j')
    (ULift.down
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾fun (x : ULift.{max u w, v} (F.obj j)) ↦
                { down := (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj j') x.down :
                  ULift.{max u w, v} (F.obj j') }) :
            (a :
                ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := ⋯,
                        map_comp := ⋯ } ⋙
                      F ⋙ uliftFunctor.{max u w, v}).obj
                  { down := j }) →
              ({ obj := fun (X : AsSmall J) ↦ X.down, map := fun {X Y : AsSmall J} (f : X ⟶ Y) ↦ f.down, map_id := ⋯,
                      map_comp := ⋯ } ⋙
                    F ⋙ uliftFunctor.{max u w, v}).obj
                { down := j' })
          (u { down := j })) :
      F.obj (down.obj { down := j' }))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.CofilteredSystem
Goal:
J : Type u
inst : Preorder J
inst_1 : IsDirectedOrder J
F : CategoryTheory.Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
inst_2 : ∀ (j : Jᵒᵖ), Finite.{v + 1} (F.obj j)
inst_3 : ∀ (j : Jᵒᵖ), Nonempty.{v + 1} (F.obj j)
⊢ F.sections.Nonempty

Tactic:
nonempty_sections_of_finite_cofiltered_system F

Premises used: nonempty_sections_of_finite_cofiltered_system
-- 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)
j : J
x : F.obj j
⊢ x ∈ F.eventualRange j ↔
    ∀ ⦃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

Tactic:
mem_iInter₂

Premises used: Set.Mem, Set.mem_iInter₂, CategoryTheory.Functor.eventualRange
-- 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)
⊢ F.IsMittagLeffler ↔
    ∀ (j : J),
      ∃ (i : J) (f : i ⟶ j),
        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))

Tactic:
forall_congr' fun _ =>
    exists₂_congr fun _ _ =>
      ⟨fun h => (iInter₂_subset _ _).antisymm <| subset_iInter₂ h, fun h => h ▸ iInter₂_subset⟩

Premises used: Set.iInter₂_subset, Eq.rec, Set.subset_iInter₂, CategoryTheory.Functor.IsMittagLeffler, exists₂_congr, HasSubset.Subset.antisymm, Iff.intro, forall_congr'
-- 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
h : F.IsMittagLeffler
f : j ⟶ i
obtain :
  ∀ (k : J) (g : k ⟶ j)
    (hg :
      F.eventualRange 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))),
    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)) ''
        F.eventualRange j
⊢ 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)) ''
      F.eventualRange j

Tactic:
obtain ⟨k, g, hg⟩ := F.isMittagLeffler_iff_eventualRange.1 h j

Premises used: Iff.mp, CategoryTheory.Functor.isMittagLeffler_iff_eventualRange
-- 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
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg :
  F.eventualRange 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 :
  F.eventualRange i ⊆
    image (α := (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 i))
      (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)))
⊢ 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)) ''
      F.eventualRange j

Tactic:
rw [hg]
-- 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
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg :
  F.eventualRange 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))
x : F.obj i
hx : x ∈ F.eventualRange i
obtain :
  ∀ (x : F.obj k)
    (hx :
      Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) (F.eventualRange i)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
              (a : (fun (X : Type v) ↦ X) (F.obj k)) → (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)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
      (image (α := (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 i))
        (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))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
          x :
        (fun (X : Type v) ↦ X) (F.obj i))
⊢ Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (image (α := (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 i))
      (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))))
    x

Tactic:
obtain ⟨x, rfl⟩ := F.mem_eventualRange_iff.1 hx (g ≫ f)

Premises used: CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.Functor.mem_eventualRange_iff, 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
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg :
  F.eventualRange 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))
x : F.obj k
hx :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) (F.eventualRange i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
rw :
  Eq (α := (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 k)) → (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))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g ≫ F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
rw₁ rw₂ :
  Eq (α := (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 k)) → (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))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) : (a : F.obj j) → F.obj i)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) : (a : F.obj k) → F.obj j) x : F.obj j) :
      F.obj i)
⊢ Eq (α := (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 k)) → (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))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))

Tactic:
rw [map_comp, comp_apply]

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
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg :
  F.eventualRange 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))
x : F.obj k
hx :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) (F.eventualRange i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (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)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (image (α := (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 i))
      (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))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))

Tactic:
exact ⟨_, ⟨x, rfl⟩, by rw [map_comp, comp_apply]⟩
-- 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 :
  F.eventualRange 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))
a₁ :
  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
⊢ F.eventualRange 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))

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- 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))
⊢ F.eventualRange 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))

Tactic:
apply iInter₂_subset

Premises used: Set.iInter₂_subset