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 : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
f : j ⟶ 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)) ''
      F.eventualRange j

Tactic:
(h.subset_image_eventualRange F f).antisymm <| mapsTo_iff_image_subset.1
    (F.eventualRange_mapsTo f)

Premises used: CategoryTheory.Functor.IsMittagLeffler.subset_image_eventualRange, Set.mapsTo_iff_image_subset, CategoryTheory.Functor.eventualRange_mapsTo, HasSubset.Subset.antisymm, 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)
i j : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : i ⟶ j
rw :
  (∀ (i_1 : J) (j_1 : i_1 ⟶ 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 i_1))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map j_1)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i_1)) → (fun (X : Type v) ↦ X) (F.obj j)))) ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i),
      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 ≫ f))) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj 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)) ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i),
      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 ≫ f))) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))

Tactic:
rw [subset_antisymm_iff, eventualRange, and_iff_right (iInter₂_subset _ _), subset_iInter₂_iff]

Premises used: Set.iInter₂_subset, Set.subset_iInter₂_iff, and_iff_right, subset_antisymm_iff, 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)
i j : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : i ⟶ j
⊢ (∀ (i_1 : J) (j_1 : i_1 ⟶ 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 i_1))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map j_1)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i_1)) → (fun (X : Type v) ↦ X) (F.obj j)))) ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i),
      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 ≫ f))) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))

Tactic:
⟨fun h k g => h _ _, fun h j' f' => ?_⟩

Premises used: Iff.intro, 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 : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : i ⟶ j
refine :
  ∀
    (h :
      ∀ ⦃k : J⦄ (g : k ⟶ i),
        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 ≫ f))) :
              (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j))))
    (j' : J) (f' : j' ⟶ 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 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)))
⊢ (∀ (i_1 : J) (j_1 : i_1 ⟶ 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 i_1))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map j_1)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i_1)) → (fun (X : Type v) ↦ X) (F.obj j)))) ↔
    ∀ ⦃k : J⦄ (g : k ⟶ i),
      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 ≫ f))) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))

Tactic:
refine ⟨fun h k g => h _ _, fun h j' f' => ?_⟩
-- 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 : i ⟶ j
h :
  ∀ ⦃k : J⦄ (g : k ⟶ i),
    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 ≫ f))) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
j' : J
f' : j' ⟶ j
obtain :
  ∀ (k : J) (g : k ⟶ i) (g' : k ⟶ j') (he : g ≫ f = g' ≫ f'),
    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 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)))
⊢ 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 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)))

Tactic:
obtain ⟨k, 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 : i ⟶ j
h :
  ∀ ⦃k : J⦄ (g : k ⟶ i),
    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 ≫ f))) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
⊢ 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 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)))

Tactic:
(h g).trans ?_

Premises used: HasSubset.Subset.trans
-- 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 : i ⟶ j
h :
  ∀ ⦃k : J⦄ (g : k ⟶ i),
    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 ≫ f))) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
refine :
  Subset (α := Set ((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 ≫ f))) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (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)))
⊢ 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 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)))

Tactic:
refine (h g).trans ?_

Premises used: HasSubset.Subset.trans
-- 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 : i ⟶ j
h :
  ∀ ⦃k : J⦄ (g : k ⟶ i),
    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 ≫ f))) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
rw :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (Function.comp (β := (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 g')) :
          (a : (fun (X : Type v) ↦ X) ((fun (X : Type v) ↦ X) (F.obj k))) → (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)))
⊢ Subset (α := Set ((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 ≫ f))) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (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)))

Tactic:
rw [he, 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 : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : i ⟶ j
h :
  ∀ ⦃k : J⦄ (g : k ⟶ i),
    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 ≫ f))) :
          (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
j' : J
f' : j' ⟶ j
k : J
g : k ⟶ i
g' : k ⟶ j'
he : g ≫ f = g' ≫ f'
⊢ Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (Function.comp (β := (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 g')) :
          (a : (fun (X : Type v) ↦ X) ((fun (X : Type v) ↦ X) (F.obj k))) → (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)))

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)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
simp_rw simp_rw₁ :
  F.IsMittagLeffler ↔
    ∀ (j : J),
      ∃ (i : J) (f : i ⟶ j),
        ∀ ⦃k : J⦄ (g : k ⟶ i),
          Subset (α := Set (F.obj j))
            (range (ι := F.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) : (a : F.obj i) → F.obj j))
            (range (ι := F.obj k)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f))) : (a : F.obj k) → F.obj j))
simp_rw₂ :
  (∀ (j : J),
      ∃ (i : J) (f : i ⟶ j),
        F.eventualRange j =
          range (ι := F.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) : (a : F.obj i) → F.obj j)) ↔
    ∀ (j : J),
      ∃ (i : J) (f : i ⟶ j),
        ∀ ⦃k : J⦄ (g : k ⟶ i),
          Subset (α := Set (F.obj j))
            (range (ι := F.obj i) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) : (a : F.obj i) → F.obj j))
            (range (ι := F.obj k)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f))) : (a : F.obj k) → F.obj j))
⊢ F.IsMittagLeffler ↔
    ∀ (j : J),
      ∃ (i : J) (f : i ⟶ j),
        ∀ ⦃k : J⦄ (g : k ⟶ i),
          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 ≫ f))) :
                (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))

Tactic:
simp_rw [isMittagLeffler_iff_eventualRange, eventualRange_eq_iff]

Premises used: CategoryTheory.Functor.eventualRange_eq_iff, 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
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j : J
obtain :
  ∀ (j₁ : J) (g₁ : j₁ ⟶ i) (f₁ : j₁ ⟶ j),
    ∃ (i_1 : J) (f : i_1 ⟶ j),
      ∀ ⦃k : J⦄ (g : k ⟶ i_1),
        Subset (α := Set ((fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
          (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map f)) :
              (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1)) →
                (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
          (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (g ≫ f))) :
              (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k)) →
                (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
⊢ ∃ (i_1 : J) (f : i_1 ⟶ j),
    ∀ ⦃k : J⦄ (g : k ⟶ i_1),
      Subset (α := Set ((fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
        (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map f)) :
            (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1)) →
              (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
        (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (g ≫ f))) :
            (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k)) → (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))

Tactic:
obtain ⟨j₁, g₁, f₁, -⟩ := IsCofilteredOrEmpty.cone_objs i j

Premises used: CategoryTheory.IsCofilteredOrEmpty.cone_objs
-- 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
obtain :
  ∀ (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₁))),
    ∃ (i_1 : J) (f : i_1 ⟶ j),
      ∀ ⦃k : J⦄ (g : k ⟶ i_1),
        Subset (α := Set ((fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
          (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map f)) :
              (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1)) →
                (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
          (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (g ≫ f))) :
              (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k)) →
                (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
⊢ ∃ (i_1 : J) (f : i_1 ⟶ j),
    ∀ ⦃k : J⦄ (g : k ⟶ i_1),
      Subset (α := Set ((fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
        (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map f)) :
            (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1)) →
              (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
        (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (g ≫ f))) :
            (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k)) → (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))

Tactic:
obtain ⟨j₂, f₂, h₂⟩ := 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
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₁))
⊢ ∃ (i_1 : J) (f : i_1 ⟶ j),
    ∀ ⦃k : J⦄ (g : k ⟶ i_1),
      Subset (α := Set ((fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
        (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map f)) :
            (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1)) →
              (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
        (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (g ≫ f))) :
            (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k)) → (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))

Tactic:
⟨j₂, f₂ ≫ f₁, fun j₃ f₃ => ?_⟩

Premises used: Exists.intro, 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
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₁))
refine :
  ∀ (j₃ : J) (f₃ : j₃ ⟶ j₂),
    Subset (α := 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₁))) :
          (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j₂)) → (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)))
⊢ ∃ (i_1 : J) (f : i_1 ⟶ j),
    ∀ ⦃k : J⦄ (g : k ⟶ i_1),
      Subset (α := Set ((fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
        (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map f)) :
            (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj i_1)) →
              (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))
        (range (ι := (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((F.toPreimages s).map (g ≫ f))) :
            (a : (fun (X : Type v) ↦ X) ((F.toPreimages s).obj k)) → (fun (X : Type v) ↦ X) ((F.toPreimages s).obj j)))

Tactic:
refine ⟨j₂, f₂ ≫ f₁, fun j₃ f₃ => ?_⟩