-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
lemma image_zeroLocus {U : X.Opens} (s : Set Γ(X, U)) :
    f.base '' X.zeroLocus s =
      Y.zeroLocus (U := f ''ᵁ U) ((f.appIso U).inv.hom '' s) ∩ Set.range f.base

Proof state:
case neg
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑Y.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ x ∉ (fun a => (ConcreteCategory.hom f.base) a) '' X.zeroLocus s

Tactic:
exact fun H ↦ hx (Set.image_subset_range _ _ H)

Result:
no goals

Proof state:
case pos
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑Y.toPresheafedSpace
hx : x ∈ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ x ∈ ⇑(ConcreteCategory.hom f.base) '' X.zeroLocus s ↔
    x ∈ Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
obtain ⟨x, rfl⟩ := hx

Result:
case pos.intro
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom f.base) x ∈ ⇑(ConcreteCategory.hom f.base) '' X.zeroLocus s ↔
    (ConcreteCategory.hom f.base) x ∈
      Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑(ConcreteCategory.hom f.base)

Proof state:
case h
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑Y.toPresheafedSpace
⊢ x ∈ ⇑(ConcreteCategory.hom f.base) '' X.zeroLocus s ↔
    x ∈ Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
by_cases hx : x ∈ Set.range f.base

Result:
case pos
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑Y.toPresheafedSpace
hx : x ∈ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ x ∈ ⇑(ConcreteCategory.hom f.base) '' X.zeroLocus s ↔
    x ∈ Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑(ConcreteCategory.hom f.base)

case neg
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑Y.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ x ∈ ⇑(ConcreteCategory.hom f.base) '' X.zeroLocus s ↔
    x ∈ Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑(ConcreteCategory.hom f.base)

Proof state:
case pos.intro
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑X.toPresheafedSpace
⊢ (ConcreteCategory.hom f.base) x ∈ ⇑(ConcreteCategory.hom f.base) '' X.zeroLocus s ↔
    (ConcreteCategory.hom f.base) x ∈
      Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
simp only [f.isOpenEmbedding.injective.mem_set_image, Scheme.mem_zeroLocus_iff,
  ← SetLike.mem_coe, Set.mem_inter_iff, Set.forall_mem_image, ← Scheme.image_basicOpen,
  IsOpenMap.coe_functor_obj, Set.mem_range, exists_apply_eq_apply, and_true]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
⊢ ⇑(ConcreteCategory.hom f.base) '' X.zeroLocus s =
    Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
ext x

Result:
case h
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑Y.toPresheafedSpace
⊢ x ∈ ⇑(ConcreteCategory.hom f.base) '' X.zeroLocus s ↔
    x ∈ Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑(ConcreteCategory.hom f.base)

Proof state:
case neg
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑Y.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ x ∈ ⇑(ConcreteCategory.hom f.base) '' X.zeroLocus s ↔
    x ∈ Y.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.appIso f U).inv) '' s) ∩ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
simp only [Set.mem_inter_iff, hx, and_false, iff_false]

Result:
case neg
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set ↑Γ(X, U)
x : ↑↑Y.toPresheafedSpace
hx : x ∉ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ x ∉ (fun a => (ConcreteCategory.hom f.base) a) '' X.zeroLocus s