-- Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
U : Y.Opens
this :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U),
    Function.Injective (α := (↑Γ(Y, U) : Type u_1)) (β := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U)) :
        (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
hU : ¬IsAffineOpen U
s : (↑Γ(Y, U) : Type u_1)
hs :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f U) :
          (a : (↑Γ(Y, U) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
        s :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
    (0 : (↑Γ(X, f ⁻¹ᵁ U) : Type u_1))
x : ↥Y
hx : x ∈ Opposite.unop (Opposite.op U)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : x ∈ (↑V : Set ↥Y)
hVU : V ≤ U
inr :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier)
            (app f (Opposite.unop (Opposite.op U)) ≫
              X.presheaf.map ((TopologicalSpace.Opens.map f.base).map (homOfLE hVU).op.unop).op) :
          (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
            (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
        s :
      (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f V) :
          (a : (↑Γ(Y, V) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hVU).op) :
              (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
            0 :
          (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1)) :
      (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
⊢ Eq (α := (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f V) :
          (a : (↑Γ(Y, V) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hVU).op) :
              (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
            s :
          (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1)) :
      (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (app f V) :
          (a : (↑Γ(Y, V) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hVU).op) :
              (a : (↑(Y.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op U)))) : Type u_1)) →
                (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1))
            0 :
          (↑(Y.presheaf.obj (Opposite.op V)) : Type u_1)) :
      (↑Γ(X, f ⁻¹ᵁ V) : Type u_1))

Tactic:
rw [← ConcreteCategory.comp_apply, f.naturality]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, AlgebraicGeometry.Scheme.Hom.naturality