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