-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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))
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)) ⋯))
        (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))))) =
    𝟙 Γ(I.subscheme, I.subschemeι ⁻¹ᵁ (↑U : X.Opens))
⊢ 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))))))

Tactic:
convert! (Category.comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.symm