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
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ i),
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
    x
this :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₁)) (F.eventualRange j₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
y : F.obj j₃
hy : y ∈ F.eventualRange j₃
h₃ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
g₂ : j₃ ⟶ i
⊢ 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
have refine_1 : ∀ (j₄ : J) (f₄ : j₄ ⟶ j₃) (h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁),
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₃)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    y
Tactic: obtain ⟨j₄, f₄, h₄⟩ := IsCofilteredOrEmpty.cone_maps g₂ ((f₃ ≫ f₂) ≫ g₁)
-- 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
this :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₁)) (F.eventualRange j₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₃)) (F.eventualRange j₃)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₄) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → (fun (X : Type v) ↦ X) (F.obj j₃))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₃))
h₃ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₄) :
              (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → (fun (X : Type v) ↦ X) (F.obj j₃))
            y :
          (fun (X : Type v) ↦ X) (F.obj j₃)) :
      (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₃)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₃)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₄) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → (fun (X : Type v) ↦ X) (F.obj j₃))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₃))
have h₅ : Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₄ ≫ f₃ ≫ f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → F.obj j₁)
      y :
    F.obj j₁)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
      x :
    (fun (X : Type v) ↦ X) (F.obj j₁))
Tactic: rw [← comp_apply, ← map_comp] 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
s : Set (F.obj i)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
j j₁ : J
g₁ : j₁ ⟶ i
f₁ : j₁ ⟶ j
j₂ : J
f₂ : j₂ ⟶ j₁
h₂ :
  F.eventualRange j₁ =
    range (ι := (fun (X : Type v) ↦ X) (F.obj j₂))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
j₃ : J
f₃ : j₃ ⟶ j₂
x : F.obj j₂
hx :
  Membership.mem (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₂)))
    (⋂ (f : j₂ ⟶ i),
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
        s)
    x
this :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₁)) (F.eventualRange j₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
g₂ : j₃ ⟶ i
j₄ : J
f₄ : j₄ ⟶ j₃
h₄ : f₄ ≫ g₂ = f₄ ≫ (f₃ ≫ f₂) ≫ g₁
y : F.obj j₄
hy :
  Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₃)) (F.eventualRange j₃)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₄) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → (fun (X : Type v) ↦ X) (F.obj j₃))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₃))
h₃ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj j₁))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₄ ≫ f₃ ≫ f₂)) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → F.obj j₁)
        y :
      F.obj j₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₂) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → (fun (X : Type v) ↦ X) (F.obj j₁))
        x :
      (fun (X : Type v) ↦ X) (F.obj j₁))
⊢ Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj j₃)) (γ := Set ((fun (X : Type v) ↦ X) (F.obj j₃)))
    ((⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g₂)) :
        (a : (fun (X : Type v) ↦ X) (F.obj j₃)) → (fun (X : Type v) ↦ X) (F.obj i)) ⁻¹'
      s)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₄) :
          (a : (fun (X : Type v) ↦ X) (F.obj j₄)) → (fun (X : Type v) ↦ X) (F.obj j₃))
        y :
      (fun (X : Type v) ↦ X) (F.obj j₃))
have refine_1 : Membership.mem (α := (fun (X : Type v) ↦ X) (F.obj i)) s
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ g₁)) : (a : (fun (X : Type v) ↦ X) (F.obj j₂)) → F.obj i) x :
    F.obj i)
Tactic: rw [mem_preimage, ← comp_apply, ← map_comp, h₄, ← Category.assoc, map_comp, comp_apply, h₃,
        ← comp_apply, ← 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
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₁))
⊢ Eq (α := F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂ ≫ f₁)) : (a : F.obj j₃) → F.obj j) y : F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ f₁)) : (a : F.obj j₂) → F.obj j) x : F.obj j)
have refine_2 : Eq (α := F.obj j)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((f₃ ≫ f₂) ≫ f₁)) : (a : F.obj j₃) → F.obj j) y : F.obj j)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ f₁)) : (a : F.obj j₂) → F.obj j) x : F.obj j)
Tactic: rw [← Category.assoc, map_comp, comp_apply, h₃, map_comp, comp_apply]
-- 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₁))
refine_2 :
  Eq (α := F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((f₃ ≫ f₂) ≫ f₁)) : (a : F.obj j₃) → F.obj j) y : F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ f₁)) : (a : F.obj j₂) → F.obj j) x : F.obj j)
⊢ Eq (α := F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂ ≫ f₁)) : (a : F.obj j₃) → F.obj j) y : F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ f₁)) : (a : F.obj j₂) → F.obj j) x : F.obj j)
have refine_2₁ : Eq (α := F.obj j)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂) ≫ F.map f₁) : (a : F.obj j₃) → F.obj j) y : F.obj j)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ f₁)) : (a : F.obj j₂) → F.obj j) x : F.obj j)
Tactic: rw [← Category.assoc, map_comp, comp_apply, h₃, map_comp, comp_apply]
-- 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₁))
refine_2 :
  Eq (α := F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((f₃ ≫ f₂) ≫ f₁)) : (a : F.obj j₃) → F.obj j) y : F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ f₁)) : (a : F.obj j₂) → F.obj j) x : F.obj j)
refine_2₁ :
  Eq (α := F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂) ≫ F.map f₁) : (a : F.obj j₃) → F.obj j) y : F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ f₁)) : (a : F.obj j₂) → F.obj j) x : F.obj j)
⊢ Eq (α := F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂ ≫ f₁)) : (a : F.obj j₃) → F.obj j) y : F.obj j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ f₁)) : (a : F.obj j₂) → F.obj j) x : F.obj j)
have refine_2₂ : Eq (α := F.obj j)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f₁) : (a : F.obj j₁) → F.obj j)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₃ ≫ f₂)) : (a : F.obj j₃) → F.obj j₁) y : F.obj j₁) :
    F.obj j)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (f₂ ≫ f₁)) : (a : F.obj j₂) → F.obj j) x : F.obj j)
Tactic: rw [← Category.assoc, map_comp, comp_apply, h₃, map_comp, comp_apply]
-- 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
h :
  ∀ (j : J),
    ∃ (i : J) (f : i ⟶ j),
      Set.Finite (α := (fun (X : Type v) ↦ X) (F.obj j))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
j : J
⊢ ∃ (i : J) (f : i ⟶ j),
    ∀ ⦃k : J⦄ (g : k ⟶ j),
      Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
have obtain : ∀ (i : J) (hi : i ⟶ j)
  (hf :
    Set.Finite (α := (fun (X : Type v) ↦ X) (F.obj j))
      (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map hi)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))),
  ∃ (i : J) (f : i ⟶ j),
    ∀ ⦃k : J⦄ (g : k ⟶ j),
      Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
Tactic: obtain ⟨i, hi, hf⟩ := 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)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h :
  ∀ (j : J),
    ∃ (i : J) (f : i ⟶ j),
      Set.Finite (α := (fun (X : Type v) ↦ X) (F.obj j))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
j i : J
hi : i ⟶ j
hf :
  Set.Finite (α := (fun (X : Type v) ↦ X) (F.obj j))
    (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map hi)) :
        (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
⊢ ∃ (i : J) (f : i ⟶ j),
    ∀ ⦃k : J⦄ (g : k ⟶ j),
      Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
have obtain : ∀ (m : Finset (F.obj j))
  (hmin :
    ∀ (x : Finset (F.obj j)),
      Membership.mem (γ := Set (Finset (F.obj j)))
          {s : Finset (F.obj j) |
            ∃ (i : J) (f : i ⟶ j),
              (↑s : Set ((fun (X : Type v) ↦ X) (F.obj j))) =
                range (ι := (fun (X : Type v) ↦ X) (F.obj i))
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
                    (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))}
          x →
        ¬x < m)
  (i : J) (f : i ⟶ j)
  (hm :
    (↑m : Set ((fun (X : Type v) ↦ X) (F.obj j))) =
      range (ι := (fun (X : Type v) ↦ X) (F.obj i))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j))),
  ∃ (i : J) (f : i ⟶ j),
    ∀ ⦃k : J⦄ (g : k ⟶ j),
      Subset (α := Set ((fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj i))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
            (a : (fun (X : Type v) ↦ X) (F.obj i)) → (fun (X : Type v) ↦ X) (F.obj j)))
        (range (ι := (fun (X : Type v) ↦ X) (F.obj k))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g)) :
            (a : (fun (X : Type v) ↦ X) (F.obj k)) → (fun (X : Type v) ↦ X) (F.obj j)))
Tactic: obtain ⟨m, ⟨i, f, hm⟩, hmin⟩ := Finset.wellFoundedLT.wf.has_min
    { s : Finset (F.obj j) | ∃ (i : _) (f : i ⟶ j), ↑s = range (F.map f) }
    ⟨_, i, hi, hf.coe_toFinset⟩
-- 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
h : F.IsMittagLeffler
i j : J
f : i ⟶ j
x_1 : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j)
x : (fun (X : Type v) ↦ X) (F.obj j)
hx : x ∈ F.eventualRange j
⊢ ∃ (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.toEventualRanges.map f) :
          (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)) → (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
        a =
      Subtype.mk (p := fun (x : (fun (X : Type v) ↦ X) (F.obj j)) ↦ x ∈ F.eventualRange j) x hx
have obtain : ∀ (y : F.obj i) (hy : y ∈ F.eventualRange i)
  (hx :
    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 i)) → (fun (X : Type v) ↦ X) (F.obj j))
          y :
        (fun (X : Type v) ↦ X) (F.obj j))),
  ∃ (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)),
    Eq (α := (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.toEventualRanges.map f) :
            (a : (fun (X : Type v) ↦ X) (F.toEventualRanges.obj i)) → (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
          a :
        (fun (X : Type v) ↦ X) (F.toEventualRanges.obj j))
      (Subtype.mk (p := fun (x : (fun (X : Type v) ↦ X) (F.obj j)) ↦ x ∈ F.eventualRange 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))
            y)
          hx :
        { x : (fun (X : Type v) ↦ X) (F.obj j) // x ∈ F.eventualRange j })
Tactic: obtain ⟨y, hy, rfl⟩ := h.subset_image_eventualRange F f hx
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)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h : F.IsMittagLeffler
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
j : J
⊢ Nonempty.{v + 1} (F.toEventualRanges.obj j)
have let : ∀ (i : J) (f : i ⟶ j)
  (h :
    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))),
  Nonempty.{v + 1} (F.toEventualRanges.obj j)
Tactic: let ⟨i, 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)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
h_1 : F.IsMittagLeffler
inst_2 : ∀ (j : J), Nonempty.{v + 1} (F.obj j)
j i : J
f : i ⟶ j
h :
  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))
⊢ Nonempty.{v + 1} (F.toEventualRanges.obj j)
have rw : Nonempty.{v + 1}
  (↑(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))) :
    Type v)
Tactic: rw [toEventualRanges_obj, 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)
inst_1 : IsCofilteredOrEmpty.{v_1, u} J
Fsur :
  ∀ ⦃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))
i j : J
f g : i ⟶ j
⊢ F.map f = F.map g
have let : ∀ (k : J) (φ : k ⟶ i) (hφ : φ ≫ f = φ ≫ g), F.map f = F.map g
Tactic: let ⟨k, φ, hφ⟩ := IsCofilteredOrEmpty.cone_maps f g