-- 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))
simp :
  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))))))
⊢ Hom.app I.subschemeι (↑U : X.Opens) = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv

Tactic:
simp only [← this, ← Functor.map_inv, inv_eqToHom, Category.assoc, eqToHom_unop,
    ← Functor.map_comp, IsIso.Iso.inv_inv, subschemeObjIso, Iso.trans_inv, Functor.mapIso_inv,
    Iso.op_inv, eqToIso.inv, eqToHom_op, Iso.hom_inv_id_assoc, Hom.appIso_inv_naturality_assoc,
    Functor.op_obj, Functor.op_map, unop_comp, unop_inv, Quiver.Hom.unop_op,
    Hom.app_appIso_inv_assoc, TopologicalSpace.Opens.carrier_eq_coe, TopologicalSpace.Opens.map_coe,
    homOfLE_leOfHom]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIso, TopologicalSpace.Opens.map_coe, CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.Iso.op_inv, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, CategoryTheory.unop_comp, CategoryTheory.Functor.map_inv, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc, TopologicalSpace.Opens.carrier_eq_coe, CategoryTheory.eqToHom_op, CategoryTheory.unop_inv, CategoryTheory.inv_eqToHom, CategoryTheory.IsIso.Iso.inv_inv, CategoryTheory.Functor.mapIso_inv, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.trans_inv, CategoryTheory.eqToHom_unop, CategoryTheory.Functor.op_obj, CategoryTheory.eqToIso.inv, CategoryTheory.Functor.op_map