-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : (↑Γ(X, U) : Type u)
H :
  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
n : (i : (↑s : Type u)) → ℕ
hn :
  ∀ (i : (↑s : Type u)),
    HMul.hMul (β := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (HPow.hPow (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : 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, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              f :
            (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (n i))
        ((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))
            x :
          (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) =
      0
this : Finite.{u + 1} (↑s : Type u)
val : Fintype (↑s : Type u)
i : (↑s : Type u)
⊢ Eq.{u + 1} (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
    ((fun (x : (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) ↦
        HMul.hMul (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : 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, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              (f ^ (Finset.sup Finset.univ n - n i)) :
            (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          x)
      (HMul.hMul (β := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
        (HPow.hPow (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : 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, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              f :
            (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          (n i))
        ((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))
            x :
          (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))))
    ((fun (x : (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u)) ↦
        HMul.hMul (α := (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : 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, U) : Type u)) → (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
              (f ^ (Finset.sup Finset.univ n - n i)) :
            (↑Γ(X, (↑(↑i : (↑X.affineOpens : Type u)) : X.Opens)) : Type u))
          x)
      0)

Tactic:
replace hn :=
    congr_arg (fun x => X.presheaf.map (homOfLE (h₁ i)).op (f ^ (Finset.univ.sup n - n i)) * x)
      (hn i)