-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma Hom.iUnion_support_ker_openCover_map_comp
    (f : X.Hom Y) [QuasiCompact f] (𝒰 : X.OpenCover) [Finite 𝒰.J] :
    ⋃ i, (𝒰.map i ≫ f).ker.support = f.ker.support

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
this : ∀ (U : ↑Y.affineOpens), (⋃ i, (ker (𝒰.map i ≫ f)).support) ∩ ↑↑U = f.ker.support ∩ ↑↑U
⊢ ⋃ i, (ker (𝒰.map i ≫ f)).support = f.ker.support

Tactic:
ext x

Result:
case h
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
this : ∀ (U : ↑Y.affineOpens), (⋃ i, (ker (𝒰.map i ≫ f)).support) ∩ ↑↑U = f.ker.support ∩ ↑↑U
x : ↑↑Y.toPresheafedSpace
⊢ x ∈ ⋃ i, (ker (𝒰.map i ≫ f)).support ↔ x ∈ f.ker.support

Proof state:
case inr
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
U : ↑Y.affineOpens
⊢ (⋃ i, (ker (𝒰.map i ≫ f)).support) ∩ ↑↑U = f.ker.support ∩ ↑↑U

Tactic:
simp only [Set.iUnion_inter, support_inter, ← f.iInf_ker_openCover_map_comp_apply 𝒰,
  Scheme.zeroLocus_iInf_of_nonempty]

Result:
no goals

Proof state:
case inr
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
⊢ ⋃ i, (ker (𝒰.map i ≫ f)).support = f.ker.support

Tactic:
suffices ∀ U : Y.affineOpens, (⋃ i, (𝒰.map i ≫ f).ker.support) ∩ U = f.ker.support ∩ U by
  ext x
  obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    (isBasis_affine_open Y).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
  simpa [hxU] using congr(x ∈ $(this ⟨U, hU⟩))

Result:
case inr
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
⊢ ∀ (U : ↑Y.affineOpens), (⋃ i, (ker (𝒰.map i ≫ f)).support) ∩ ↑↑U = f.ker.support ∩ ↑↑U

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
⊢ ⋃ i, (ker (𝒰.map i ≫ f)).support = f.ker.support

Tactic:
cases isEmpty_or_nonempty 𝒰.J

Result:
case inl
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : IsEmpty 𝒰.J
⊢ ⋃ i, (ker (𝒰.map i ≫ f)).support = f.ker.support

case inr
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
⊢ ⋃ i, (ker (𝒰.map i ≫ f)).support = f.ker.support

Proof state:
case inl
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : IsEmpty 𝒰.J
⊢ ⋃ i, (ker (𝒰.map i ≫ f)).support = f.ker.support

Tactic:
have : IsEmpty X := Function.isEmpty 𝒰.f

Result:
case inl
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : IsEmpty 𝒰.J
this : IsEmpty ↑↑X.toPresheafedSpace
⊢ ⋃ i, (ker (𝒰.map i ≫ f)).support = f.ker.support

Proof state:
case inl
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : IsEmpty 𝒰.J
this : IsEmpty ↑↑X.toPresheafedSpace
⊢ ⋃ i, (ker (𝒰.map i ≫ f)).support = f.ker.support

Tactic:
simp [ker_eq_top_of_isEmpty]

Result:
no goals

Proof state:
case h
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
this : ∀ (U : ↑Y.affineOpens), (⋃ i, (ker (𝒰.map i ≫ f)).support) ∩ ↑↑U = f.ker.support ∩ ↑↑U
x : ↑↑Y.toPresheafedSpace
⊢ x ∈ ⋃ i, (ker (𝒰.map i ≫ f)).support ↔ x ∈ f.ker.support

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
  (isBasis_affine_open Y).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Result:
case h.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
this : ∀ (U : ↑Y.affineOpens), (⋃ i, (ker (𝒰.map i ≫ f)).support) ∩ ↑↑U = f.ker.support ∩ ↑↑U
x : ↑↑Y.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ ⋃ i, (ker (𝒰.map i ≫ f)).support ↔ x ∈ f.ker.support

Proof state:
case h.intro.intro.intro.intro.intro
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
this : ∀ (U : ↑Y.affineOpens), (⋃ i, (ker (𝒰.map i ≫ f)).support) ∩ ↑↑U = f.ker.support ∩ ↑↑U
x : ↑↑Y.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace
hU : U ∈ Y.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ ⋃ i, (ker (𝒰.map i ≫ f)).support ↔ x ∈ f.ker.support

Tactic:
simpa [hxU] using congr(x ∈ $(this ⟨U, hU⟩))

Result:
no goals

Proof state:
case inr
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
⊢ ∀ (U : ↑Y.affineOpens), (⋃ i, (ker (𝒰.map i ≫ f)).support) ∩ ↑↑U = f.ker.support ∩ ↑↑U

Tactic:
intro U

Result:
case inr
X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
h✝ : Nonempty 𝒰.J
U : ↑Y.affineOpens
⊢ (⋃ i, (ker (𝒰.map i ≫ f)).support) ∩ ↑↑U = f.ker.support ∩ ↑↑U