-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineTransitionLimit (goal)
Goal:
I : Type u
inst : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst_1 : IsCofiltered I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst_3 : ∀ (i : I), CompactSpace.{u} ↥(D.obj i)
inst_4 : ∀ (i : I), QuasiSeparatedSpace.{u} ↥(D.obj i)
this :
  ReflectsFilteredColimits
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier))
refine_1 :
  ∀
    (x :
      Cocone.pt (F :=
        (D.op ⋙ Scheme.Γ) ⋙
          forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
        (Functor.mapCocone
          (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier))
          (Scheme.Γ.mapCocone c.op))),
    ∃ (i : Iᵒᵖ) (xi :
      (fun (X : Type u) ↦ X)
        (((D.op ⋙ Scheme.Γ) ⋙
              forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier)).obj
          i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                    (Scheme.Γ.mapCocone c.op)))
                i) :
            (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const Iᵒᵖ).obj ((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).pt).obj i))
          xi
⊢ Nonempty.{u + 2} (IsColimit (Scheme.Γ.mapCocone c.op))
have refine_2 : ∀ (i : Iᵒᵖ)
  (x y :
    (fun (X : Type u) ↦ X)
      (((D.op ⋙ Scheme.Γ) ⋙
            forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier)).obj
        i)),
  Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const Iᵒᵖ)
            (Cocone.pt (F :=
              (D.op ⋙ Scheme.Γ) ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier))
              (Functor.mapCocone
                (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier))
                (Scheme.Γ.mapCocone c.op))))
          i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                    (Scheme.Γ.mapCocone c.op)))
                i) :
            (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const Iᵒᵖ).obj ((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).pt).obj i))
          x :
        (fun (X : Type u) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const Iᵒᵖ)
              (Cocone.pt (F :=
                (D.op ⋙ Scheme.Γ) ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier))
                (Functor.mapCocone
                  (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier))
                  (Scheme.Γ.mapCocone c.op))))
            i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Functor.mapCocone
                    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier))
                    (Scheme.Γ.mapCocone c.op)))
                i) :
            (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
              (fun (X : Type u) ↦ X)
                (((Functor.const Iᵒᵖ).obj ((forget CommRingCat).mapCocone (Scheme.Γ.mapCocone c.op)).pt).obj i))
          y :
        (fun (X : Type u) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const Iᵒᵖ)
              (Cocone.pt (F :=
                (D.op ⋙ Scheme.Γ) ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier))
                (Functor.mapCocone
                  (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier))
                  (Scheme.Γ.mapCocone c.op))))
            i)) →
    ∃ (k : Iᵒᵖ) (f : i ⟶ k),
      Eq (α :=
        (fun (X : Type u) ↦ X)
          (((D.op ⋙ Scheme.Γ) ⋙
                forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier)).obj
            k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (((D.op ⋙ Scheme.Γ) ⋙
                      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier)).map
                  f) :
              (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
                (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj k))
            x :
          (fun (X : Type u) ↦ X)
            (((D.op ⋙ Scheme.Γ) ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier)).obj
              k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (((D.op ⋙ Scheme.Γ) ⋙
                      forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier)).map
                  f) :
              (a : (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj i)) →
                (fun (X : Type u) ↦ X) (((D.op ⋙ Scheme.Γ) ⋙ forget CommRingCat).obj k))
            y :
          (fun (X : Type u) ↦ X)
            (((D.op ⋙ Scheme.Γ) ⋙
                  forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier)).obj
              k))
Tactic: refine ReflectsColimit.reflects (F := forget _) (Types.FilteredColimit.isColimitOf' _ _ ?_ ?_)