awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Filtered (goal)
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₁
⊢ ∃ (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₂
have 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₂))
Tactic: obtain ⟨j₂, x₂, rfl⟩ := Types.jointly_surjective_of_isColimit ht x₂
Cleared hypotheses: x₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
Goal:
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
⊢ lift F' ≫ F'.m = ι f
have h : ∀ (x : Image f),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (lift F' ≫ F'.m)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ι f)).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
Goal:
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (lift F' ≫ F'.m)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ι f)).toFun x
have 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) β))
          sorry) :
      (fun (X : Type u) ↦ X) α) =
  (ConcreteCategory.hom (FC := TypeCat.Fun) (ι f)).toFun x
Tactic: change (F'.e ≫ F'.m) _ = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
Goal:
α β : Type u
f : α ⟶ β
F' : MonoFactorisation f
x : Image f
⊢ (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
have h : (↑x : (fun (X : Type u) ↦ X) β) = (ConcreteCategory.hom (FC := TypeCat.Fun) (ι f)).toFun x
Tactic: rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
Goal:
α β : Type u
f_1 : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
⊢ 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)
have 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))
            sorry) :
        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 [elementwise_of% st.w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
Goal:
α β : Type u
f_1 : α ⟶ β
f g : Arrow (Type u)
st : f ⟶ g
x : (monoFactorisation f.hom).I
⊢ 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)
have 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)
Tactic: rw [Classical.choose_spec x.property]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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
have refine : (fun (x : ℕᵒᵖ) ↦
    match (motive := (x : ℕᵒᵖ) → F.obj x) x with
    | Opposite.op n => preimage hF a n) ∈
  F.sections
Tactic: refine ⟨⟨fun ⟨n⟩ ↦ preimage hF a n, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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 : ℕ
⊢ ∀ {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')
have 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))
Tactic: ⟨m⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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 : ℕ
⊢ ∀ (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))
have 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))
Tactic: ⟨⟨⟨(h : m ≤ n)⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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 : ℕ
⊢ 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))
have 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))
Tactic: erw [CategoryTheory.Functor.map_id, id_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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))
⊢ 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))
have 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))
Tactic: erw [CategoryTheory.Functor.map_id, id_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (hypothesis)
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 p : ℕ
h : m.le p
ih :
  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 p)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op p))) → (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 p)) :
      (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))
⊢ 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 p.succ)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p.succ))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op p.succ))) → (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 p.succ)) :
      (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 p)) } :
                  ULift.{0, 0} (PLift (Opposite.unop (Opposite.op m) ≤ Opposite.unop (Opposite.op p))) })) :
          (a : (fun (X : Type u) ↦ X) (F.obj (Opposite.op p))) → (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 p)) :
      (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
have h' : m ≤ p
Tactic: have h' : m ≤ p := h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Images (goal)
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 : ℕ
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))
have refl : Eq (α := (fun (X : Type u) ↦ X) (F.obj (Opposite.op m)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (Opposite.op
              { down := { down := sorry : 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: induction h with
  | refl =>
    erw [CategoryTheory.Functor.map_id, id_apply]
  | @step p h ih =>
    rw [← ih]
    have h' : m ≤ p := h
    erw [CategoryTheory.Functor.map_comp (f := (homOfLE (Nat.le_succ p)).op) (g := (homOfLE h').op),
      comp_apply, (hF p _).choose_spec]
    rfl
Cleared hypotheses: h