-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X_1 X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IsReduced Y
s : (↑Γ(Y, Scheme.Hom.opensRange f) : Type u_1)
hs : Y.basicOpen s = ⊥
x : ↥X
this : IsReduced X
H_1 :
  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))
H :
  Eq (α := (↑(Y.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) (inv (Scheme.Hom.stalkMap f x)) :
          (a : (↑(X.presheaf.stalk x) : Type u_1)) → (↑(Y.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) (Scheme.Hom.stalkMap f x) :
              (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(X.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.presheaf.obj (op { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ })) (Y :=
                    Y.presheaf.stalk (f x))
                    (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } (f x) ⋯) :
                  (a :
                      (↑(Y.presheaf.obj (op { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ })) :
                        Type u_1)) →
                    (↑(Y.presheaf.stalk (f x)) : Type u_1))
                s :
              (↑(Y.presheaf.stalk (f x)) : Type u_1)) :
          (↑(X.presheaf.stalk x) : Type u_1)) :
      (↑(Y.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) (inv (Scheme.Hom.stalkMap f x)) :
          (a : (↑(X.presheaf.stalk x) : Type u_1)) → (↑(Y.presheaf.stalk (f x)) : Type u_1))
        0 :
      (↑(Y.presheaf.stalk (f x)) : Type u_1))
⊢ Eq (α := (↑(Y.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) (𝟙 (Y.presheaf.stalk (f x))) :
          (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(Y.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.presheaf.obj (op { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ })) (Y :=
                Y.presheaf.stalk (f x))
                (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } (f x) ⋯) :
              (a :
                  (↑(Y.presheaf.obj (op { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ })) : Type u_1)) →
                (↑(Y.presheaf.stalk (f x)) : Type u_1))
            s :
          (↑(Y.presheaf.stalk (f x)) : Type u_1)) :
      (↑(Y.presheaf.stalk (f x)) : Type u_1))
    (0 : (↑(Y.presheaf.stalk (f x)) : Type u_1))

Tactic:
rw [← CommRingCat.comp_apply, CategoryTheory.IsIso.hom_inv_id, map_zero] at H

Premises used: map_zero, CommRingCat.comp_apply, CategoryTheory.IsIso.hom_inv_id