-- Module: Mathlib.AlgebraicGeometry.Properties
Goal:
X : Scheme
hX : IsReduced X
U : X.Opens
s : (↑Γ(X, U) : Type u_1)
hs : X.basicOpen s = ⊥
x : ↥X
hx : x ∈ U
h :
  ∀ (X : Scheme.{u_1}) (U : X.Opens)
    (H :
      ∀ (x : ↥U),
        ∃ (V : X.Opens) (_ : (↑x : ↥X) ∈ V) (x : V ⟶ U),
          ∀ [hX : IsReduced X] (s : (↑Γ(X, V) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X) (hx : x ∈ V),
            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 V x hx) :
                    (a : (↑(X.sheaf.presheaf.obj (op V)) : 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 X] (s : (↑Γ(X, U) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X) (hx : x ∈ U),
    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 U x hx) :
            (a : (↑(X.sheaf.presheaf.obj (op U)) : 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))
h₁ :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) [inst : IsOpenImmersion f],
    ∃ (U : X.Opens) (V : Y.Opens),
      U = ⊤ ∧
        V = Scheme.Hom.opensRange f ∧
          ((∀ [hX : IsReduced X] (s : (↑Γ(X, U) : Type u_1)) (hs : X.basicOpen s = ⊥) (x : ↥X) (hx : x ∈ U),
              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 U x hx) :
                      (a : (↑(X.sheaf.presheaf.obj (op U)) : 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, V) : Type u_1)) (hs : Y.basicOpen s = ⊥) (x : ↥Y) (hx : x ∈ V),
              Eq (α := (↑(Y.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 := Y.sheaf.presheaf.stalk x) (Y.sheaf.presheaf.germ V x hx) :
                      (a : (↑(Y.sheaf.presheaf.obj (op V)) : Type u_1)) → (↑(Y.sheaf.presheaf.stalk x) : Type u_1))
                    s :
                  (↑(Y.sheaf.presheaf.stalk x) : Type u_1))
                (0 : (↑(Y.sheaf.presheaf.stalk x) : Type u_1)))
h₂ :
  ∀ (R : CommRingCat.{u_1}) [hX : IsReduced.{u_1} (Spec R)] (s : (↑Γ(Spec R, ⊤) : Type u_1))
    (hs : (Spec R).basicOpen s = ⊥) (x : ↥(Spec R)) (hx : Membership.mem (γ := Opens ↥(Spec R)) ⊤ x),
    Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) 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 := Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ) (Sheaf.presheaf (Spec R).sheaf) (op ⊤))
              (Y := Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x)
              (Presheaf.germ (Sheaf.presheaf (Spec R).sheaf) ⊤ x hx) :
            (a : (↑((Spec R).sheaf.presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).sheaf.presheaf.stalk x) : Type u_1))
          s :
        (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_1))
      (0 : (↑(Presheaf.stalk (Sheaf.presheaf (Spec R).sheaf) x) : Type u_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) (Y := X.sheaf.presheaf.stalk x) (X.sheaf.presheaf.germ U x hx) :
          (a : (↑(X.sheaf.presheaf.obj (op U)) : 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))

Tactic:
induction U using reduce_to_affine_global generalizing hX with
  | h₁ X U H =>
    obtain ⟨V, hx, i, H⟩ := H ⟨x, hx⟩
    specialize H (X.presheaf.map i.op s)
    rw [Scheme.basicOpen_res, hs] at H
    specialize H (inf_bot_eq _) x hx
    rw [← X.sheaf.presheaf.germ_res_apply i x hx s]
    exact H
  | h₂ X Y f =>
    refine ⟨f ⁻¹ᵁ f.opensRange, f.opensRange, by simp, rfl, ?_⟩
    rintro H hX s hs _ ⟨x, rfl⟩
    haveI := isReduced_of_isOpenImmersion f
    specialize H (f.app _ s) _ x ⟨x, rfl⟩
    · rw [← Scheme.preimage_basicOpen, hs]; ext1; simp [Opens.map]
    · have H : (X.presheaf.germ _ x _).hom _ = 0 := H
      rw [← Scheme.Hom.germ_stalkMap_apply f ⟨_, _⟩ x] at H
      apply_fun inv <| f.stalkMap x at H
      rw [← CommRingCat.comp_apply, CategoryTheory.IsIso.hom_inv_id, map_zero] at H
      exact H
  | h₃ R =>
    rw [basicOpen_eq_of_affine', PrimeSpectrum.basicOpen_eq_bot_iff] at hs
    replace hs := (hs.map (Scheme.ΓSpecIso R).inv.hom).eq_zero
    rw [← CommRingCat.comp_apply, Iso.hom_inv_id, CommRingCat.id_apply] at hs
    rw [hs, map_zero]

Premises used: CommRingCat.id_apply, CategoryTheory.Iso.hom_inv_id, map_zero, CommRingCat.comp_apply, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.Scheme.basicOpen_res, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.inv, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.preimage_basicOpen, rfl, PrimeSpectrum.basicOpen_eq_bot_iff