-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U_1 : (↑Y.affineOpens : Type u)
U V :
  (Precoverage.ZeroHypercover.pullback₁ f
      (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀
⊢ Eq (α :=
    pullback
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
          U)
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
          V) ⟶
      image f)
    (pullback.fst
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
          U)
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
          V) ≫
      (fun
            (U :
              (Precoverage.ZeroHypercover.pullback₁ f
                  (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀) ↦
          liftQuotient (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ) ((ker f).ideal U) ⋯ ≫
            (ker f).subschemeCover.f (P := IsOpenImmersion) U)
        U)
    (pullback.snd
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
          U)
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).f
          V) ≫
      (fun
            (U :
              (Precoverage.ZeroHypercover.pullback₁ f
                  (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) ⋯)).I₀) ↦
          liftQuotient (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ) ((ker f).ideal U) ⋯ ≫
            (ker f).subschemeCover.f (P := IsOpenImmersion) U)
        V)
have rw : Eq (α :=
  pullback
      ((Precoverage.ZeroHypercover.pullback₁ f
            (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).f
        U)
      ((Precoverage.ZeroHypercover.pullback₁ f
            (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).f
        V) ⟶
    Y)
  ((pullback.fst
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).f
          U)
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).f
          V) ≫
      (fun
            (U :
              (Precoverage.ZeroHypercover.pullback₁ f
                  (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).I₀) ↦
          liftQuotient (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ) ((ker f).ideal U) sorry ≫
            (ker f).subschemeCover.f (P := IsOpenImmersion) U)
        U) ≫
    imageι f)
  ((pullback.snd
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).f
          U)
        ((Precoverage.ZeroHypercover.pullback₁ f
              (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).f
          V) ≫
      (fun
            (U :
              (Precoverage.ZeroHypercover.pullback₁ f
                  (Y.openCoverOfIsOpenCover (fun (i : (↑Y.affineOpens : Type u)) ↦ (↑i : Y.Opens)) sorry)).I₀) ↦
          liftQuotient (pullback.snd f (↑U : Y.Opens).ι ≫ (↑U : Y.Opens).toSpecΓ) ((ker f).ideal U) sorry ≫
            (ker f).subschemeCover.f (P := IsOpenImmersion) U)
        V) ≫
    imageι f)
Tactic: rw [← cancel_mono f.imageι]