-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
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
⊢ 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))
have 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))
Tactic: rw [← ConcreteCategory.comp_apply, f.naturality]