-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U) s
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : Membership.mem (α := ↥X) (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) ((𝒰.f i) x : ↥X)
a :
  Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((CommRingCat.Hom.hom
            (appLE (𝒰.f i) (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) :
          (a : (↑Γ(X, 𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
            (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.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.presheaf.obj (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) →
                (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
            ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
                  (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
                s :
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
          (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
⊢ Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((Iso.commRingCatIsoToRingEquiv (appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens))) :
          (a : (↑Γ(X, 𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
            (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.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.presheaf.obj (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) →
                (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
            ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
                  (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
                s :
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
          (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((Iso.commRingCatIsoToRingEquiv (appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens))) :
          (a : (↑Γ(X, 𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
            (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        0 :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))

Tactic:
rw [map_zero, ← RingEquiv.coe_toRingHom, Iso.commRingCatIsoToRingEquiv_toRingHom,
    Scheme.Hom.appIso_hom']

Premises used: map_zero, AlgebraicGeometry.Scheme.Hom.appIso_hom', CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom, RingEquiv.coe_toRingHom