-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H_1 :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
e : U = ⨆ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)
h₁ : ∀ (i : (↑s : Type u)), (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens) ≤ U
i : (↑s : Type u)
H :
  Eq (α := (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
        x :
      (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
    (0 : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
h :
  Eq (α :=
    (↑(X.presheaf.obj
          (op
            (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                  (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                f)))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) (Y :=
            X.presheaf.obj
              (op
                (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                      (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                    f))))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(X.presheaf.obj (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) : Type u)) →
            (↑(X.presheaf.obj
                  (op
                    (X.basicOpen
                      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op) :
                          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                        f)))) :
              Type u))
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) →
                (↑(X.presheaf.obj (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) : Type u))
            x :
          (↑(X.presheaf.obj (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) : Type u)) :
      (↑(X.presheaf.obj
            (op
              (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                    (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                  f)))) :
        Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u)) →
            (↑(X.presheaf.obj
                  (op
                    (X.basicOpen
                      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op) :
                          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                        f)))) :
              Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u))
            x :
          (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u)) :
      (↑(X.presheaf.obj
            (op
              (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                    (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                  f)))) :
        Type u))
h₂ :
  Eq (α :=
    (↑(X.presheaf.obj
          (op
            (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                  (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                f)))) :
      Type u))
    (0 :
      (↑(X.presheaf.obj
            (op
              (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                    (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                  f)))) :
        Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑(X.presheaf.obj (op (X.basicOpen f))) : Type u)) →
            (↑(X.presheaf.obj
                  (op
                    (X.basicOpen
                      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op) :
                          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                        f)))) :
              Type u))
        0 :
      (↑(X.presheaf.obj
            (op
              (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                    (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                  f)))) :
        Type u))
refine_1 :
  X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        f) ≤
    X.basicOpen f
⊢ Eq (α :=
    (↑(X.presheaf.obj
          (op
            (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                  (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                f)))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) (Y :=
            X.presheaf.obj
              (op
                (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                      (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                    f))))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(X.presheaf.obj (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) : Type u)) →
            (↑(X.presheaf.obj
                  (op
                    (X.basicOpen
                      ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op) :
                          (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                        f)))) :
              Type u))
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) →
                (↑(X.presheaf.obj (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) : Type u))
            x :
          (↑(X.presheaf.obj (op (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))) : Type u)) :
      (↑(X.presheaf.obj
            (op
              (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                    (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                  f)))) :
        Type u))
    (0 :
      (↑(X.presheaf.obj
            (op
              (X.basicOpen (U := (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
                    (a : (↑Γ(X, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
                  f)))) :
        Type u))

Tactic:
convert! congr_arg (X.presheaf.map (homOfLE _).op).hom H

Premises used: CommRingCat.Hom.hom, Quiver.Hom.op, CategoryTheory.Functor.map, congr_arg, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace