-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
this_1 :
  I.subschemeCover.f (P := IsOpenImmersion) U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
this :
  (((Hom.app I.subschemeι (↑U : X.Opens) ≫
            Hom.app (I.subschemeCover.f (P := IsOpenImmersion) U) (I.subschemeι ⁻¹ᵁ (↑U : X.Opens))) ≫
          inv ((Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map (eqToHom ⋯))) ≫
        inv
          ((Spec (I.subschemeCover.X (P := IsOpenImmersion) U)).presheaf.map
            (Quiver.Hom.op
              ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map
                (Quiver.Hom.unop (eqToHom ⋯)))))) ≫
      inv (Iso.inv (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)))) =
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ Eq (α := Γ(X, (↑U : X.Opens)) ⟶ Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens))) (Hom.app I.subschemeι (↑U : X.Opens))
    (Hom.app I.subschemeι (↑U : X.Opens) ≫
      I.subscheme.presheaf.map
        (CategoryStruct.comp (Y :=
          Opposite.op
            (I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ
              I.subschemeCover.f (P := IsOpenImmersion) U ⁻¹ᵁ I.subschemeι ⁻¹ᵁ (↑U : X.Opens)))
          (Quiver.Hom.op (X :=
            Set.image (α := ↥(Spec (I.subschemeCover.X (P := IsOpenImmersion) U)))
              (⇑(I.subschemeCover.f (P := IsOpenImmersion) U))
              (Set.preimage (β := ↥I.subscheme) (⇑(I.subschemeCover.f (P := IsOpenImmersion) U))
                (⇑I.subschemeι ⁻¹' (↑(↑U : X.Opens) : Set ↥X))))
            (Y := ⇑I.subschemeι ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
            (homOfLE (x :=
              Set.image (α := ↥(Spec (I.subschemeCover.X (P := IsOpenImmersion) U)))
                (⇑(I.subschemeCover.f (P := IsOpenImmersion) U))
                (Set.preimage (β := ↥I.subscheme) (⇑(I.subschemeCover.f (P := IsOpenImmersion) U))
                  (⇑I.subschemeι ⁻¹' (↑(↑U : X.Opens) : Set ↥X))))
              (y := ⇑I.subschemeι ⁻¹' (↑(↑U : X.Opens) : Set ↥X)) ⋯))
          (CategoryStruct.comp (Y := Opposite.op (I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ ⊤))
            (Quiver.Hom.op
                ((Hom.opensFunctor (I.subschemeCover.f (P := IsOpenImmersion) U)).map
                  (CategoryStruct.comp (Y :=
                    (Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).obj
                      ((Opens.map (IsAffineOpen.fromSpec ⋯).base).obj (↑U : X.Opens)))
                    ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map (eqToHom ⋯))
                    (eqToHom ⋯))) :
              Opposite.op
                  (I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ
                    (Opens.map (I.subschemeCover.f (P := IsOpenImmersion) U).base).obj
                      ((Opens.map I.subschemeι.base).obj (↑U : X.Opens))) ⟶
                Opposite.op (I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ ⊤))
            (eqToHom ⋯ :
              Opposite.op (I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ ⊤) ⟶
                Opposite.op (I.subschemeι ⁻¹ᵁ (↑U : X.Opens))))))
have h : I.subscheme.presheaf.map
    (CategoryStruct.comp (Y :=
      Opposite.op
        (I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ
          I.subschemeCover.f (P := IsOpenImmersion) U ⁻¹ᵁ I.subschemeι ⁻¹ᵁ (↑U : X.Opens)))
      (Quiver.Hom.op (X :=
        Set.image (α := ↥(Spec (I.subschemeCover.X (P := IsOpenImmersion) U)))
          (⇑(I.subschemeCover.f (P := IsOpenImmersion) U))
          (Set.preimage (β := ↥I.subscheme) (⇑(I.subschemeCover.f (P := IsOpenImmersion) U))
            (⇑I.subschemeι ⁻¹' (↑(↑U : X.Opens) : Set ↥X))))
        (Y := ⇑I.subschemeι ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
        (homOfLE (x :=
          Set.image (α := ↥(Spec (I.subschemeCover.X (P := IsOpenImmersion) U)))
            (⇑(I.subschemeCover.f (P := IsOpenImmersion) U))
            (Set.preimage (β := ↥I.subscheme) (⇑(I.subschemeCover.f (P := IsOpenImmersion) U))
              (⇑I.subschemeι ⁻¹' (↑(↑U : X.Opens) : Set ↥X))))
          (y := ⇑I.subschemeι ⁻¹' (↑(↑U : X.Opens) : Set ↥X)) sorry))
      (CategoryStruct.comp (Y := Opposite.op (I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ ⊤))
        (Quiver.Hom.op
            ((Hom.opensFunctor (I.subschemeCover.f (P := IsOpenImmersion) U)).map
              (CategoryStruct.comp (Y :=
                (Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).obj
                  ((Opens.map (IsAffineOpen.fromSpec sorry).base).obj (↑U : X.Opens)))
                ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map (eqToHom sorry))
                (eqToHom sorry))) :
          Opposite.op
              (I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ
                (Opens.map (I.subschemeCover.f (P := IsOpenImmersion) U).base).obj
                  ((Opens.map I.subschemeι.base).obj (↑U : X.Opens))) ⟶
            Opposite.op (I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ ⊤))
        (eqToHom sorry :
          Opposite.op (I.subschemeCover.f (P := IsOpenImmersion) U ''ᵁ ⊤) ⟶
            Opposite.op (I.subschemeι ⁻¹ᵁ (↑U : X.Opens))))) =
  𝟙 Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens))
Tactic: convert! (Category.comp_id _).symm