awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [subset_antisymm_iff, eventualRange, and_iff_right (iInter₂_subset _ _), subset_iInter₂_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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)))
have 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)))
Tactic: refine ⟨fun h k g => h _ _, fun h j' f' => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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
⊢ 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)))
have 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)))
Tactic: obtain ⟨k, g, g', he⟩ := cospan f f'
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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)))
have 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)))
Tactic: refine (h g).trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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))
      (⇑(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)))
have 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)))
Tactic: rw [he, F.map_comp, types_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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))
⊢ 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)))
have 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))
Tactic: simp_rw [isMittagLeffler_iff_eventualRange, eventualRange_eq_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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
⊢ ∃ (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)))
have 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)))
Tactic: obtain ⟨j₁, g₁, f₁, -⟩ := IsCofilteredOrEmpty.cone_objs i j
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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
⊢ ∃ (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)))
have 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)))
Tactic: obtain ⟨j₂, f₂, h₂⟩ := F.isMittagLeffler_iff_eventualRange.1 h j₁
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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)))
have 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)))
Tactic: refine ⟨j₂, f₂ ≫ f₁, fun j₃ f₃ => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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₁))
have 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₁))
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (hypothesis)
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.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))
have 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₁))
Tactic: have : F.map f₂ x ∈ F.eventualRange j₁ := by
      rw [h₂]
      exact ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.CofilteredSystem (goal)
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))
have refine_1 : ∀ (g₂ : j₃ ⟶ i),
  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: refine ⟨⟨y, mem_iInter.2 fun g₂ => ?_⟩, Subtype.ext ?_⟩