-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X_1 X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X)
    (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
    Eq (α := (↑(X.sheaf.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.sheaf.presheaf.stalk x)
              (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) : Type u_1)) →
              (↑(X.sheaf.presheaf.stalk x) : Type u_1))
          s :
        (↑(X.sheaf.presheaf.stalk x) : Type u_1))
      (0 : (↑(X.sheaf.presheaf.stalk x) : Type u_1))
hX : IsReduced Y
s : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
h :
  X.basicOpen (U := f ⁻¹ᵁ Scheme.Hom.opensRange f)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, Scheme.Hom.opensRange f)) (Scheme.Hom.app f (Scheme.Hom.opensRange f)) :
          (a : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1))
        s) =
    ⊥
h₁ :
  ∀
    (H :
      Eq (α := (↑(X.sheaf.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X := X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) (Y :=
                X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯) :
              (a : (↑(X.sheaf.presheaf.obj (op (f ⁻¹ᵁ Scheme.Hom.opensRange f))) : Type u_1)) →
                (↑(X.sheaf.presheaf.stalk x) : Type u_1))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (X := Γ(Y, Scheme.Hom.opensRange f))
                    (Scheme.Hom.app f (Scheme.Hom.opensRange f)) :
                  (a : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1))
                s :
              (↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f) : Type u_1)) :
          (↑(X.sheaf.presheaf.stalk x) : Type u_1))
        (0 : (↑(X.sheaf.presheaf.stalk x) : Type u_1))),
    Eq (α := (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X := Y.sheaf.presheaf.obj (op (Scheme.Hom.opensRange f))) (Y :=
              Y.sheaf.presheaf.stalk (f x)) (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯) :
            (a : (↑(Y.sheaf.presheaf.obj (op (Scheme.Hom.opensRange f))) : Type u_1)) →
              (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
          s :
        (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
      (0 : (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
⊢ Eq (α := (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := Y.sheaf.presheaf.obj (op (Scheme.Hom.opensRange f))) (Y :=
            Y.sheaf.presheaf.stalk (f x)) (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) (f x) ⋯) :
          (a : (↑(Y.sheaf.presheaf.obj (op (Scheme.Hom.opensRange f))) : Type u_1)) →
            (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
        s :
      (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))
    (0 : (↑(Y.sheaf.presheaf.stalk (f x)) : Type u_1))

Tactic:
specialize H (f.app _ s) _ x ⟨x, rfl⟩

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.app, Exists.intro, DFunLike.coe, rfl