-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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₀
rw :
  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) ⟶
      Y)
    ((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) ≫
      imageι f)
    ((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) ≫
      imageι f)
⊢ 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)

Tactic:
rw [← cancel_mono f.imageι]

Premises used: AlgebraicGeometry.Scheme.Hom.imageι, CategoryTheory.cancel_mono