-- 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 : IsCofilteredOrEmpty I
inst_2 : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
Z : (i : I) → Set ↥(D.obj i)
hZc : ∀ (i : I), IsClosed (Z i)
hZne : ∀ (i : I), (Z i).Nonempty
hZcpt : ∀ (i : I), IsCompact (Z i)
hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (⇑(D.map f)) (Z i) (Z i')
D' : I ⥤ Scheme :=
  {
    obj := fun (i : I) ↦
      (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).subscheme,
    map := fun {X Y : I} (f : X ⟶ Y) ↦
      (vanishingIdeal { carrier := Z X, isClosed' := ⋯ }).subschemeMap
        (vanishingIdeal { carrier := Z Y, isClosed' := ⋯ }) (D.map f) ⋯,
    map_id := ⋯, map_comp := ⋯ }
ι : D' ⟶ D := { app := fun (i : I) ↦ (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }).subschemeι, naturality := ⋯ }
this : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D'.map f)
h : ∀ (i : I), Nonempty.{u + 1} ↥(D'.obj i)
h_1 : ∀ (i : I), CompactSpace.{u} ↥(D'.obj i)
c' : Cone D' :=
  {
    pt :=
      subscheme (X := c.1)
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)),
    π :=
      {
        app := fun (i : I) ↦
          subschemeMap
            (⨆ (i : I),
              (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
                (c.π.app i))
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ }) (c.π.app i) ⋯,
        naturality := ⋯ } }
s : Cone D'
m : s.pt ⟶ c'.pt
hm : ∀ (j : I), m ≫ c'.π.app j = s.π.app j
⊢ m ≫
      subschemeι
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)) =
    CategoryStruct.comp (Y :=
      subscheme (X := c.1)
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
      (IsClosedImmersion.lift
        (subschemeι
          (⨆ (i : I),
            (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap
              (c.π.app i)))
        (hc.lift ((Cone.postcompose ι).obj s)) ⋯)
      (subschemeι
        (⨆ (i : I),
          (vanishingIdeal { carrier := Z i, isClosed' := ⋯ : TopologicalSpace.Closeds ↥(D.obj i) }).comap (c.π.app i)))
have refine : ∀ (i : I),
  (m ≫
        subschemeι
          (⨆ (i : I),
            (vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) }).comap
              (c.π.app i))) ≫
      c.π.app i =
    CategoryStruct.comp (Y :=
        subscheme (X := c.1)
          (⨆ (i : I),
            (vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) }).comap
              (c.π.app i)))
        (IsClosedImmersion.lift
          (subschemeι
            (⨆ (i : I),
              (vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) }).comap
                (c.π.app i)))
          (hc.lift ((Cone.postcompose ι).obj s)) sorry)
        (subschemeι
          (⨆ (i : I),
            (vanishingIdeal { carrier := Z i, isClosed' := sorry : TopologicalSpace.Closeds ↥(D.obj i) }).comap
              (c.π.app i))) ≫
      c.π.app i
Tactic: refine hc.hom_ext fun i ↦ ?_