awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
x₁ x₂ : t.pt
obtain :
  ∀ (j₁ : J) (x₁ : F.obj j₁),
    ∃ (j : J) (x₁' : F.obj j) (x₂' : F.obj j),
      Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
          ((hom (FC := TypeCat.Fun) (t.ι.app j) :
                (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
              x₁' :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
          ((hom (FC := TypeCat.Fun) (t.ι.app j₁) :
                (a : (fun (X : Type u) ↦ X) (F.obj j₁)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j₁))
              x₁ :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j₁)) ∧
        (hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            x₂' =
          x₂
⊢ ∃ (j : J) (x₁' : F.obj j) (x₂' : F.obj j),
    (hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          x₁' =
        x₁ ∧
      (hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          x₂' =
        x₂

Tactic:
obtain ⟨j₁, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit ht x₁

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
x₂ : t.pt
j₁ : J
x₁ : F.obj j₁
obtain :
  ∀ (j₂ : J) (x₂ : F.obj j₂),
    ∃ (j : J) (x₁' : F.obj j) (x₂' : F.obj j),
      Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
          ((hom (FC := TypeCat.Fun) (t.ι.app j) :
                (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
              x₁' :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
          ((hom (FC := TypeCat.Fun) (t.ι.app j₁) :
                (a : (fun (X : Type u) ↦ X) (F.obj j₁)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j₁))
              x₁ :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j₁)) ∧
        Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
          ((hom (FC := TypeCat.Fun) (t.ι.app j) :
                (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
              x₂' :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
          ((hom (FC := TypeCat.Fun) (t.ι.app j₂) :
                (a : (fun (X : Type u) ↦ X) (F.obj j₂)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j₂))
              x₂ :
            (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j₂))
⊢ ∃ (j : J) (x₁' : F.obj j) (x₂' : F.obj j),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            x₁' :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j₁) :
              (a : (fun (X : Type u) ↦ X) (F.obj j₁)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j₁))
            x₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j₁)) ∧
      (hom (FC := TypeCat.Fun) (t.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
          x₂' =
        x₂

Tactic:
obtain ⟨j₂, x₂, rfl⟩ := Types.jointly_surjective_of_isColimit ht x₂

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
j₁ : J
x₁ : F.obj j₁
j₂ : J
x₂ : F.obj j₂
⊢ ∃ (j : J) (x₁' : F.obj j) (x₂' : F.obj j),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            x₁' :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j₁) :
              (a : (fun (X : Type u) ↦ X) (F.obj j₁)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j₁))
            x₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j₁)) ∧
      Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            x₂' :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j₂) :
              (a : (fun (X : Type u) ↦ X) (F.obj j₂)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j₂))
            x₂ :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j₂))

Tactic:
⟨max j₁ j₂, F.map (leftToMax _ _) x₁, F.map (rightToMax _ _) x₂,
    congr_hom (t.w (leftToMax j₁ j₂)) x₁, congr_hom (t.w (rightToMax j₁ j₂)) x₂⟩

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.ConcreteCategory.hom, CategoryTheory.IsFiltered.max, CategoryTheory.Functor.map, And.intro, Exists.intro, CategoryTheory.IsFiltered.leftToMax, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Filtered
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : IsFilteredOrEmpty.{w, v} J
t : Cocone F
ht : IsColimit t
j₁ : J
x₁ : F.obj j₁
j₂ : J
x₂ : F.obj j₂
⊢ ∃ (j : J) (x₁' : F.obj j) (x₂' : F.obj j),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            x₁' :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j₁) :
              (a : (fun (X : Type u) ↦ X) (F.obj j₁)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j₁))
            x₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j₁)) ∧
      Eq (α := (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j))
            x₂' :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j))
        ((hom (FC := TypeCat.Fun) (t.ι.app j₂) :
              (a : (fun (X : Type u) ↦ X) (F.obj j₂)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj t.pt).obj j₂))
            x₂ :
          (fun (X : Type u) ↦ X) (Functor.obj.{w, u, v, u + 1} (Functor.obj (Functor.const J) t.pt) j₂))

Tactic:
exact ⟨max j₁ j₂, F.map (leftToMax _ _) x₁, F.map (rightToMax _ _) x₂,
    congr_hom (t.w (leftToMax j₁ j₂)) x₁, congr_hom (t.w (rightToMax j₁ j₂)) x₂⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
α β : Type u
f : α ⟶ β
⊢ Mono (Image.ι f)

Tactic:
(mono_iff_injective _).2 Subtype.val_injective

Premises used: Iff.mpr, Subtype.val_injective, CategoryTheory.mono_iff_injective
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
h :
  ∀ (x : Image f),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (lift F' ≫ F'.m)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (ι f)).toFun x
⊢ lift F' ≫ F'.m = ι f

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F'.e ≫ F'.m) : (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) β)
      (↑(Classical.indefiniteDescription
            (fun (x_1 : α) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) β)
                  x_1 =
                (↑x : (fun (X : Type u) ↦ X) β))
            ⋯) :
        (fun (X : Type u) ↦ X) α) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ι f)).toFun x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (lift F' ≫ F'.m)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ι f)).toFun x

Tactic:
change (F'.e ≫ F'.m) _ = _

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.MonoFactorisation.e, CategoryTheory.Limits.MonoFactorisation.m, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
h : (↑x : (fun (X : Type u) ↦ X) β) = (ConcreteCategory.hom (FC := TypeCat.Fun) (ι f)).toFun x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F'.e ≫ F'.m) : (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) β)
      (↑(Classical.indefiniteDescription
            (fun (x_1 : α) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) β)
                  x_1 =
                (↑x : (fun (X : Type u) ↦ X) β))
            ⋯) :
        (fun (X : Type u) ↦ X) α) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ι f)).toFun x

Tactic:
rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac, Classical.indefiniteDescription, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (↑x : (fun (X : Type u) ↦ X) β) = (ConcreteCategory.hom (FC := TypeCat.Fun) (ι f)).toFun x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
α β : Type u
f : α ⟶ β
⊢ HasImage f

Tactic:
HasImage.mk ⟨_, isImage f⟩

Premises used: CategoryTheory.Limits.ImageFactorisation.mk, CategoryTheory.Limits.HasImage.mk, CategoryTheory.Limits.Types.isImage
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
α β : Type u
f : α ⟶ β
⊢ ∀ {X Y : Type u} (f : X ⟶ Y), HasImage f

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
α β : Type u
f_1 : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
rw :
  Eq (α := (fun (X : Type u) ↦ X) g.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Arrow.Hom.right st) : (a : f.right) → g.right)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f.hom : (a : f.left) → f.right)
            (Classical.choose (p := fun (x_1 : f.left) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f.hom :
                    (a : (fun (X : Type u) ↦ X) f.left) → (fun (X : Type u) ↦ X) f.right)
                  x_1 =
                (↑x : (fun (X : Type u) ↦ X) f.right))
              ⋯) :
          f.right) :
      g.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Arrow.Hom.right st) :
          (a : (fun (X : Type u) ↦ X) f.right) → (fun (X : Type u) ↦ X) g.right)
        (↑x : (fun (X : Type u) ↦ X) f.right) :
      (fun (X : Type u) ↦ X) g.right)
⊢ Eq (α := (fun (X : Type u) ↦ X) g.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g.hom :
          (a : (fun (X : Type u) ↦ X) g.left) → (fun (X : Type u) ↦ X) g.right)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Arrow.Hom.left st) :
              (a : (fun (X : Type u) ↦ X) f.left) → (fun (X : Type u) ↦ X) g.left)
            (Classical.choose (p := fun (x_1 : f.left) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f.hom :
                    (a : (fun (X : Type u) ↦ X) f.left) → (fun (X : Type u) ↦ X) f.right)
                  x_1 =
                (↑x : (fun (X : Type u) ↦ X) f.right))
              ⋯) :
          (fun (X : Type u) ↦ X) g.left) :
      (fun (X : Type u) ↦ X) g.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Arrow.Hom.right st) :
          (a : (fun (X : Type u) ↦ X) f.right) → (fun (X : Type u) ↦ X) g.right)
        (↑x : (fun (X : Type u) ↦ X) f.right) :
      (fun (X : Type u) ↦ X) g.right)

Tactic:
rw [elementwise_of% st.w]

Premises used: CategoryTheory.Arrow.Hom.w
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
α β : Type u
f_1 : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
rw rw₁ :
  Eq (α := (fun (X : Type u) ↦ X) g.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Arrow.Hom.right st) : (a : f.right) → g.right)
        (↑x : (fun (X : Type u) ↦ X) f.right) :
      g.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Arrow.Hom.right st) :
          (a : (fun (X : Type u) ↦ X) f.right) → (fun (X : Type u) ↦ X) g.right)
        (↑x : (fun (X : Type u) ↦ X) f.right) :
      (fun (X : Type u) ↦ X) g.right)
⊢ Eq (α := (fun (X : Type u) ↦ X) g.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Arrow.Hom.right st) : (a : f.right) → g.right)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f.hom : (a : f.left) → f.right)
            (Classical.choose (p := fun (x_1 : f.left) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f.hom :
                    (a : (fun (X : Type u) ↦ X) f.left) → (fun (X : Type u) ↦ X) f.right)
                  x_1 =
                (↑x : (fun (X : Type u) ↦ X) f.right))
              ⋯) :
          f.right) :
      g.right)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Arrow.Hom.right st) :
          (a : (fun (X : Type u) ↦ X) f.right) → (fun (X : Type u) ↦ X) g.right)
        (↑x : (fun (X : Type u) ↦ X) f.right) :
      (fun (X : Type u) ↦ X) g.right)

Tactic:
rw [Classical.choose_spec x.property]

Premises used: Classical.choose_spec, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
a : F.obj (Opposite.op 0)
⊢ ∃ (a_1 :
    (fun (X : Type u) ↦ X) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) (limitCone F).pt) (Opposite.op 0))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((limitCone F).π.app (Opposite.op 0)) :
          (a : (fun (X : Type u) ↦ X) (((Functor.const ℕᵒᵖ).obj (limitCone F).pt).obj (Opposite.op 0))) →
            (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
        a_1 =
      a

Tactic:
⟨⟨fun ⟨n⟩ ↦ preimage hF a n, ?_⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, _private.0.CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux.match_1, _private.0.CategoryTheory.Limits.Types.limitOfSurjectionsSurjective.preimage, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
a : F.obj (Opposite.op 0)
refine :
  (fun (x : ℕᵒᵖ) ↦
      match (motive := (x : ℕᵒᵖ) → F.obj x) x with
      | Opposite.op n => preimage hF a n) ∈
    F.sections
⊢ ∃ (a_1 :
    (fun (X : Type u) ↦ X) (Functor.obj (C := ℕᵒᵖ) (Functor.obj (Functor.const ℕᵒᵖ) (limitCone F).pt) (Opposite.op 0))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((limitCone F).π.app (Opposite.op 0)) :
          (a : (fun (X : Type u) ↦ X) (((Functor.const ℕᵒᵖ).obj (limitCone F).pt).obj (Opposite.op 0))) →
            (fun (X : Type u) ↦ X) (F.obj (Opposite.op 0)))
        a_1 =
      a

Tactic:
refine ⟨⟨fun ⟨n⟩ ↦ preimage hF a n, ?_⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
a : F.obj (Opposite.op 0)
n : ℕ
this :
  ∀ (m : ℕ) (f : Opposite.op n ⟶ Opposite.op m),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
          ((fun (x : ℕᵒᵖ) ↦
              (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
                | Opposite.op n => preimage hF a n :
                F.obj x))
            (Opposite.op n)) :
        (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
      ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op m) :
        F.obj (Opposite.op m))
⊢ ∀ {j' : ℕᵒᵖ} (f : Opposite.op n ⟶ j'),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n))) → (fun (X : Type u) ↦ X) (F.obj j'))
          ((fun (x : ℕᵒᵖ) ↦
              (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
                | Opposite.op n => preimage hF a n :
                F.obj x))
            (Opposite.op n)) :
        (fun (X : Type u) ↦ X) (F.obj j'))
      ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          j' :
        F.obj j')

Tactic:
⟨m⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
a : F.obj (Opposite.op 0)
n m : ℕ
m₁ :
  ∀ (h : m ≤ n),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.map
                (Opposite.op
                  { down := { down := h : PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op n)) } :
                    ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op n))) })) :
            (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
          ((fun (x : ℕᵒᵖ) ↦
              (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
                | Opposite.op n => preimage hF a n :
                F.obj x))
            (Opposite.op n)) :
        (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
      ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op m) :
        F.obj (Opposite.op m))
⊢ ∀ (f : Opposite.op n ⟶ Opposite.op m),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
          ((fun (x : ℕᵒᵖ) ↦
              (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
                | Opposite.op n => preimage hF a n :
                F.obj x))
            (Opposite.op n)) :
        (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
      ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op m) :
        F.obj (Opposite.op m))

Tactic:
⟨⟨⟨(h : m ≤ n)⟩⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Images
Goal:
F : ℕᵒᵖ ⥤ Type u
hF :
  ∀ (n : ℕ),
    Function.Surjective (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) (β :=
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op)) :
        (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op n.succ))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op n)))
a : F.obj (Opposite.op 0)
n m : ℕ
refl :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj (Opposite.op m))) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op m))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
        ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op m)) :
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((fun (x : ℕᵒᵖ) ↦
          (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
            | Opposite.op n => preimage hF a n :
            F.obj x))
        (Opposite.op m) :
      F.obj (Opposite.op m))
refl₁ refl₂ :
  Eq.{u + 1} (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((fun (x : ℕᵒᵖ) ↦
        (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
          | Opposite.op n => preimage hF a n :
          F.obj x))
      (Opposite.op m))
    ((fun (x : ℕᵒᵖ) ↦
        (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
          | Opposite.op n => preimage hF a n :
          F.obj x))
      (Opposite.op m))
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (Opposite.op
                { down := { down := ⋯ : PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op m)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op m))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op m))) → (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
        ((fun (x : ℕᵒᵖ) ↦
            (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
              | Opposite.op n => preimage hF a n :
              F.obj x))
          (Opposite.op m)) :
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
    ((fun (x : ℕᵒᵖ) ↦
          (match (motive := (x : ℕᵒᵖ) → F.obj x) x with
            | Opposite.op n => preimage hF a n :
            F.obj x))
        (Opposite.op m) :
      F.obj (Opposite.op m))

Tactic:
erw [CategoryTheory.Functor.map_id, id_apply]

Premises used: CategoryTheory.id_apply, CategoryTheory.Functor.map_id