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 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))
⊢ 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))
have 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
Tactic: apply subset_antisymm
-- 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 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))
⊢ 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
have a : Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj k)))
  (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
    (Function.comp (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) ((fun (X : Type v) ↦ X) (F.obj i))) → (fun (X : Type v) ↦ X) (F.obj j))))
  (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
      (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj k)))
Tactic: rw [h, 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)
h :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
j k : J
g : k ⟶ j
⊢ Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j))) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
have rw : Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
  (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj j))) :
      (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j)))
  (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
      (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
Tactic: rw [map_id, types_id, range_id, (h g).range_eq]
-- 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)
h :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
j k : J
g : k ⟶ j
rw :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj j))) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
⊢ Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j))) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
have rw₁ : Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j))) (range id)
  (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
      (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
Tactic: rw [map_id, types_id, range_id, (h g).range_eq]
-- 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)
h :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
j k : J
g : k ⟶ j
rw :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj j))) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
rw₁ :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j))) (range id)
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
⊢ Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j))) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
have rw₂ : Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j))) univ
  (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
      (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
Tactic: rw [map_id, types_id, range_id, (h g).range_eq]
-- 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)
h :
  ∀ ⦃i j : J⦄ (f : i ⟶ j),
    Function.Surjective (α := (fun (X : Type v) ↦ X) (F.obj i)) (β := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))
j k : J
g : k ⟶ j
rw :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj j))) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
rw₁ :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j))) (range id)
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
rw₂ :
  Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j))) univ
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
⊢ Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj j))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 j))) :
        (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
have rw₃ : Subset.{v} (α := Set ((fun (X : Type v) ↦ X) (F.obj j))) univ univ
Tactic: rw [map_id, types_id, range_id, (h g).range_eq]
-- 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 k : J
s : Set (F.obj i)
X Y : J
g : X ⟶ Y
x : (fun (X : Type v) ↦ X) (F.obj X)
h :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
    (⋂ (f : X ⟶ i),
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
    x
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj Y)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj Y)))
    (⋂ (f : Y ⟶ i),
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
        x :
      (fun (X : Type v) ↦ X) (F.obj Y))
have rw : ∀
  (h :
    ∀ (i_1 : X ⟶ i),
      Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
        ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
            (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
          s)
        x)
  (i_1 : Y ⟶ i),
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj Y)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj Y)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
        (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
        x :
      (fun (X : Type v) ↦ X) (F.obj Y))
Tactic: rw [mem_iInter] at h ⊢
Cleared hypotheses: h
-- 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 k : J
s : Set (F.obj i)
X Y : J
g : X ⟶ Y
x : (fun (X : Type v) ↦ X) (F.obj X)
h :
  ∀ (i_1 : X ⟶ i),
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
f : Y ⟶ i
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj Y)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj Y)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
        x :
      (fun (X : Type v) ↦ X) (F.obj Y))
have rw : Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
          x :
        (fun (X : Type v) ↦ X) (F.obj Y)) :
    (fun (X : Type v) ↦ X) (F.obj i))
Tactic: rw [← mem_preimage, preimage_preimage, mem_preimage]
-- 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 k : J
s : Set (F.obj i)
X Y : J
g : X ⟶ Y
x : (fun (X : Type v) ↦ X) (F.obj X)
h :
  ∀ (i_1 : X ⟶ i),
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
f : Y ⟶ i
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
            x :
          (fun (X : Type v) ↦ X) (F.obj Y)) :
      (fun (X : Type v) ↦ X) (F.obj i))
have a : Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
            x :
          (fun (X : Type v) ↦ X) (F.obj Y)) :
      (fun (X : Type v) ↦ X) (F.obj i)) ↔
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f))) :
        (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    x
Tactic: convert! h (g ≫ 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 k : J
s : Set (F.obj i)
X Y : J
g : X ⟶ Y
x : (fun (X : Type v) ↦ X) (F.obj X)
h :
  ∀ (i_1 : X ⟶ i),
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i_1)) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
f : Y ⟶ i
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
                (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
              x :
            (fun (X : Type v) ↦ X) (F.obj Y)) :
        (fun (X : Type v) ↦ X) (F.obj i)) ↔
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
      ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (g ≫ f))) :
          (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
      x
have a : Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj Y)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj Y))
            x :
          (fun (X : Type v) ↦ X) (F.obj Y)) :
      (fun (X : Type v) ↦ X) (F.obj i)) ↔
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj X)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g ≫ F.map f)) :
        (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    x
Tactic: rw [F.map_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)
i j : J
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
f : j ⟶ i
x : (fun (X : Type v) ↦ X) (F.obj j)
hx : x ∈ F.eventualRange j
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) (F.eventualRange i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
have rw : ∀
  (hx :
    ∀ ⦃i : J⦄ (f : i ⟶ j),
      Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
        x)
  ⦃i_1 : J⦄ (f_1 : i_1 ⟶ i),
  Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj i_1))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f_1)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i_1)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
Tactic: rw [mem_eventualRange_iff] at hx ⊢
Cleared hypotheses: hx
-- 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 : j ⟶ i
x : (fun (X : Type v) ↦ X) (F.obj j)
hx :
  ∀ ⦃i : J⦄ (f : i ⟶ j),
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j)))
      (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
      x
k : J
f' : k ⟶ i
⊢ Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
have obtain : ∀ (l : J) (g : l ⟶ j) (g' : l ⟶ k) (he : g ≫ f = g' ≫ f'),
  Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
Tactic: obtain ⟨l, 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 : j ⟶ i
x : (fun (X : Type v) ↦ X) (F.obj j)
hx :
  ∀ ⦃i : J⦄ (f : i ⟶ j),
    Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j)))
      (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
      x
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
⊢ Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        x :
      (fun (X : Type v) ↦ X) (F.obj i))
have obtain : ∀ (x : F.obj l)
  (hx :
    ∀ ⦃i : J⦄ (f : i ⟶ j),
      Membership.mem (α := F.obj j) (γ := Set ((fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj l)) → (fun (X : Type v) ↦ X) (F.obj j))
            x :
          (fun (X : Type v) ↦ X) (F.obj j))),
  Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj l)) → (fun (X : Type v) ↦ X) (F.obj j))
            x :
          (fun (X : Type v) ↦ X) (F.obj j)) :
      (fun (X : Type v) ↦ X) (F.obj i))
Tactic: obtain ⟨x, rfl⟩ := hx g
Cleared hypotheses: x, hx
-- 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 : j ⟶ i
k : J
f' : k ⟶ i
l : J
g : l ⟶ j
g' : l ⟶ k
he : g ≫ f = g' ≫ f'
x : F.obj l
hx :
  ∀ ⦃i : J⦄ (f : i ⟶ j),
    Membership.mem (α := F.obj j) (γ := Set ((fun (X : Type v) ↦ X) (F.obj j)))
      (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type v) ↦ X) (F.obj l)) → (fun (X : Type v) ↦ X) (F.obj j))
          x :
        (fun (X : Type v) ↦ X) (F.obj j))
⊢ Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
        (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type v) ↦ X) (F.obj l)) → (fun (X : Type v) ↦ X) (F.obj j))
            x :
          (fun (X : Type v) ↦ X) (F.obj j)) :
      (fun (X : Type v) ↦ X) (F.obj i))
have rw : Membership.mem (α := F.obj i) (γ := Set ((fun (X : Type v) ↦ X) (F.obj i)))
  (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f')) :
      (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g' ≫ F.map f') : (a : (fun (X : Type v) ↦ X) (F.obj l)) → F.obj i)
      x :
    F.obj i)
Tactic: rw [← comp_apply, ← map_comp, he, F.map_comp]