awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst : IsOpenImmersion iV
inst_1 : QuasiCompact f
H : IsPullback f' iU iV f
W : (↑V.affineOpens : Type u)
this_1 : QuasiCompact f'
this_2 : IsOpenImmersion iU
x : (↑Γ(V, (↑W : V.Opens)) : Type u)
this_3 : iU ''ᵁ f' ⁻¹ᵁ (↑W : V.Opens) = f ⁻¹ᵁ iV ''ᵁ (↑W : V.Opens)
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ (↑W : V.Opens)) ≅ Γ(U, f' ⁻¹ᵁ (↑W : V.Opens)) :=
  Functor.mapIso X.presheaf (Iso.op (eqToIso this_3)) ≪≫ Hom.appIso iU (f' ⁻¹ᵁ (↑W : V.Opens))
this : Iso.inv (Hom.appIso iV (↑W : V.Opens)) ≫ Hom.app f (iV ''ᵁ (↑W : V.Opens)) = Hom.app f' (↑W : V.Opens) ≫ e.inv
⊢ Eq (α := (↑Γ(U, f' ⁻¹ᵁ (↑W : V.Opens)) : Type u))
      ((CommRingCat.Hom.hom (Hom.app f' (↑W : V.Opens)) :
            (a : (↑Γ(V, (↑W : V.Opens)) : Type u)) → (↑Γ(U, f' ⁻¹ᵁ (↑W : V.Opens)) : Type u))
          x :
        (↑Γ(U, f' ⁻¹ᵁ (↑W : V.Opens)) : Type u))
      (0 : (↑Γ(U, f' ⁻¹ᵁ (↑W : V.Opens)) : Type u)) ↔
    Eq (α := (↑Γ(X, f ⁻¹ᵁ iV ''ᵁ (↑W : V.Opens)) : Type u))
      ((CommRingCat.Hom.hom (Hom.app f' (↑W : V.Opens) ≫ e.inv) :
            (a : (↑Γ(V, (↑W : V.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ iV ''ᵁ (↑W : V.Opens)) : Type u))
          x :
        (↑Γ(X, f ⁻¹ᵁ iV ''ᵁ (↑W : V.Opens)) : Type u))
      (0 : (↑Γ(X, f ⁻¹ᵁ iV ''ᵁ (↑W : V.Opens)) : Type u))

Tactic:
simpa using (map_eq_zero_iff _ (ConcreteCategory.bijective_of_isIso e.inv).1).symm

Premises used: And.left, map_eq_zero_iff, CategoryTheory.Iso.inv, Iff.symm, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
a : (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
a₁ : closure (Set.range (ι := ↥X) ⇑f) ⊆ (↑(ker f).support : Set ↥Y)
⊢ (↑(ker f).support : Set ↥Y) = closure (Set.range (ι := ↥X) ⇑f)

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
a :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
        (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f))
    (hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S), (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
⊢ (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)

Tactic:
wlog hY : ∃ S, Y = Spec S
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
x : ↥Y
hx : x ∈ (↑(ker f).support : Set ↥Y)
𝒰 : Y.OpenCover := Y.affineCover
a :
  ∀ (i : 𝒰.I₀) (x : ↥(𝒰.X i)) (hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)),
    Membership.mem (α := ↥Y) (γ := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) ((𝒰.f i) x : ↥Y)
⊢ Membership.mem (γ := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) x

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x

Premises used: AlgebraicGeometry.Scheme.Cover.exists_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
⊢ QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)

Tactic:
have inst : QuasiCompact (𝒰.pullbackHom f i) :=
        MorphismProperty.pullback_snd _ _ inferInstance
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
a :
  ∀
    (this :
      Membership.mem (γ := Set ↥(𝒰.X i))
        (closure
          (Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i))
            ⇑(Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)))
        x),
    Membership.mem (α := ↥Y) (γ := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) ((𝒰.f i) x : ↥Y)
a₁ :
  x ∈
    (𝒰.X i).zeroLocus
      (↑((ker (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
                (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i :
                  (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)).ideal
            (Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦ Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤
              ⋯)) :
        Set (↑Γ(𝒰.X i, (↑⟨⊤, ⋯⟩ : (𝒰.X i).Opens)) : Type u))
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) ((𝒰.f i) x : ↥Y)

Tactic:
have := this (𝒰.pullbackHom f i) ⟨_, rfl⟩
        ((coe_support_inter _ ⟨⊤, isAffineOpen_top _⟩).ge ⟨?_, Set.mem_univ x⟩).1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
this_2 :
  Membership.mem (γ := Set ↥(𝒰.X i))
    (closure
      (Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i))
        ⇑(Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)))
    x
this :
  Membership.mem (α := ↥Y) (γ := Set ↥Y)
    (closure
      (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i))
        (Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i))
          ⇑(Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i))))
    ((𝒰.f i) x : ↥Y)
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y)
    (closure
      (Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i))
        ⇑((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f)))
    ((𝒰.f i) x : ↥Y)

Tactic:
rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, 𝒰.pullbackHom_map] at this

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, AlgebraicGeometry.Scheme.Cover.pullbackHom_map
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
this_2 :
  Membership.mem (γ := Set ↥(𝒰.X i))
    (closure
      (Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i))
        ⇑(Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)))
    x
this :
  Membership.mem (α := ↥Y) (γ := Set ↥Y)
    (closure
      (Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i))
        ⇑((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f)))
    ((𝒰.f i) x : ↥Y)
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) ((𝒰.f i) x : ↥Y)

Tactic:
closure_mono (Set.range_comp_subset_range _ _) this

Premises used: Set.range_comp_subset_range, closure_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
this_2 :
  Membership.mem (γ := Set ↥(𝒰.X i))
    (closure
      (Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i))
        ⇑(Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i)))
    x
this :
  Membership.mem (α := ↥Y) (γ := Set ↥Y)
    (closure
      (Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i))
        ⇑((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f)))
    ((𝒰.f i) x : ↥Y)
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) ((𝒰.f i) x : ↥Y)

Tactic:
exact closure_mono (Set.range_comp_subset_range _ _) this

Premises used: Set.range_comp_subset_range, closure_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ Membership.mem (α := ↥Y)
    (↑(↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens)
              (𝒰.f i ''ᵁ
                (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦
                      Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤ ⋯) :
                  (𝒰.X i).Opens))
              ⋯) :
          Y.Opens) :
      Set ↥Y)
    ((𝒰.f i) x : ↥Y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ Membership.mem (α := ↥Y)
    (Y.zeroLocus
        (↑((ker f).ideal
              (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens)
                (𝒰.f i ''ᵁ
                  (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦
                        Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤ ⋯) :
                    (𝒰.X i).Opens))
                ⋯)) :
          Set (↑Γ(Y, (↑⟨𝒰.f i ''ᵁ (↑⟨⊤, ⋯⟩ : (𝒰.X i).Opens), ⋯⟩ : Y.Opens)) : Type u)) ∩
      Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))
    ((𝒰.f i) x : ↥Y)

Tactic:
exact ⟨((coe_support_inter _ _).le ⟨hx, by simp⟩).1, ⟨_, rfl⟩⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ Function.Surjective (α :=
    (↑Γ(𝒰.X i,
          (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦ Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤
                ⋯) :
            (𝒰.X i).Opens)) :
      Type u))
    (β :=
    (↑Γ(Y,
          𝒰.f i ''ᵁ
            (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦ Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x)
                  ⊤ ⋯) :
              (𝒰.X i).Opens)) :
      Type u))
    (⇑(CommRingCat.Hom.hom
          (Iso.inv
            (appIso (𝒰.f i)
              (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦
                    Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤ ⋯) :
                (𝒰.X i).Opens)))) :
      (a : (↑Γ(𝒰.X i, (↑⟨⊤, ⋯⟩ : (𝒰.X i).Opens)) : Type u)) → (↑Γ(Y, 𝒰.f i ''ᵁ (↑⟨⊤, ⋯⟩ : (𝒰.X i).Opens)) : Type u))

Tactic:
(ConcreteCategory.bijective_of_isIso ((𝒰.f i).appIso ⊤).inv).2

Premises used: CategoryTheory.PreZeroHypercover.f, Set.Mem, And.right, AlgebraicGeometry.Scheme.Hom.appIso, Top.top, CategoryTheory.Iso.inv, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ Function.Surjective (α :=
    (↑Γ(𝒰.X i,
          (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦ Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤
                ⋯) :
            (𝒰.X i).Opens)) :
      Type u))
    (β :=
    (↑Γ(Y,
          𝒰.f i ''ᵁ
            (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦ Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x)
                  ⊤ ⋯) :
              (𝒰.X i).Opens)) :
      Type u))
    (⇑(CommRingCat.Hom.hom
          (Iso.inv
            (appIso (𝒰.f i)
              (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦
                    Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤ ⋯) :
                (𝒰.X i).Opens)))) :
      (a : (↑Γ(𝒰.X i, (↑⟨⊤, ⋯⟩ : (𝒰.X i).Opens)) : Type u)) → (↑Γ(Y, 𝒰.f i ''ᵁ (↑⟨⊤, ⋯⟩ : (𝒰.X i).Opens)) : Type u))

Tactic:
exact (ConcreteCategory.bijective_of_isIso ((𝒰.f i).appIso ⊤).inv).2

Premises used: CategoryTheory.PreZeroHypercover.f, And.right, AlgebraicGeometry.Scheme.Hom.appIso, Top.top, CategoryTheory.Iso.inv, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f

Tactic:
(IsPullback.of_hasPullback _ _).flip

Premises used: CategoryTheory.Limits.limit.π, AlgebraicGeometry.Scheme.Cover.pullbackHom, CategoryTheory.Limits.limit, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (hY : ∃ (S : CommRingCat.{u}), Y = Spec S),
    (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) ((𝒰.f i) x : ↥Y)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i)
⊢ IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f

Tactic:
exact (IsPullback.of_hasPullback _ _).flip

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X_1 Y_1 X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
hY : ∃ (S : CommRingCat.{u}), Y = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f],
    (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
⊢ (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)

Tactic:
obtain ⟨S, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X_1 Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f]
        (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
        (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f))
    (hX : ¬∃ (R : CommRingCat.{u}), X = Spec R), (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
wlog :
  ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
    (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
⊢ (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)

Tactic:
wlog hX : ∃ R, X = Spec R generalizing X S
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X_1 Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
    (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
x : ↥(Spec S)
hx : x ∈ (↑(ker f).support : Set ↥(Spec S))
⊢ CompactSpace.{u} ↥X

Tactic:
have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X_1 Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
    (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
x : ↥(Spec S)
hx : x ∈ (↑(ker f).support : Set ↥(Spec S))
inst : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
inr :
  ∀ (i : 𝒰.I₀)
    (hx : Membership.mem (γ := Set ↥(Spec S)) ((fun (i : 𝒰.I₀) ↦ (↑(ker (𝒰.f i ≫ f)).support : Set ↥(Spec S))) i) x),
    Membership.mem (γ := Set ↥(Spec S)) (closure (Set.range (ι := ↥X) ⇑f)) x
⊢ Membership.mem (γ := Set ↥(Spec S)) (closure (Set.range (ι := ↥X) ⇑f)) x

Tactic:
obtain ⟨_, ⟨i, rfl⟩, hx⟩ := (f.iUnion_support_ker_openCover_map_comp 𝒰).ge hx

Premises used: Eq.ge, AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X_1 Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
    (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
x : ↥(Spec S)
hx_1 : x ∈ (↑(ker f).support : Set ↥(Spec S))
inst : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
hx : Membership.mem (γ := Set ↥(Spec S)) ((fun (i : 𝒰.I₀) ↦ (↑(ker (𝒰.f i ≫ f)).support : Set ↥(Spec S))) i) x
⊢ QuasiCompact (𝒰.f i ≫ f)

Tactic:
have inst : QuasiCompact (𝒰.f i ≫ f) := HasAffineProperty.iff_of_isAffine.mpr
        (inferInstanceAs <| CompactSpace (Spec _))
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X_1 Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
    (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
x : ↥(Spec S)
hx_1 : x ∈ (↑(ker f).support : Set ↥(Spec S))
inst_2 : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
hx : Membership.mem (γ := Set ↥(Spec S)) ((fun (i : 𝒰.I₀) ↦ (↑(ker (𝒰.f i ≫ f)).support : Set ↥(Spec S))) i) x
inst : QuasiCompact (𝒰.f i ≫ f)
⊢ Membership.mem (γ := Set ↥(Spec S)) (closure (Set.range (ι := ↥X) ⇑f)) x

Tactic:
closure_mono (Set.range_comp_subset_range _ _) (this S (𝒰.f i ≫ f) ⟨_, rfl⟩ hx)

Premises used: Set.range_comp_subset_range, CategoryTheory.PreZeroHypercover.f, closure_mono, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X_1 Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
    (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
x : ↥(Spec S)
hx_1 : x ∈ (↑(ker f).support : Set ↥(Spec S))
inst_2 : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
hx : Membership.mem (γ := Set ↥(Spec S)) ((fun (i : 𝒰.I₀) ↦ (↑(ker (𝒰.f i ≫ f)).support : Set ↥(Spec S))) i) x
inst : QuasiCompact (𝒰.f i ≫ f)
⊢ Membership.mem (γ := Set ↥(Spec S)) (closure (Set.range (ι := ↥X) ⇑f)) x

Tactic:
exact closure_mono (Set.range_comp_subset_range _ _) (this S (𝒰.f i ≫ f) ⟨_, rfl⟩ hx)

Premises used: Set.range_comp_subset_range, CategoryTheory.PreZeroHypercover.f, closure_mono, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X_1 Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
hX : ∃ (R : CommRingCat.{u}), X = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ Spec S) [QuasiCompact f],
    (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥(Spec R)) ⇑f)
⊢ (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)

Tactic:
obtain ⟨R, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
S R : CommRingCat
f : Spec R ⟶ Spec S
inst : QuasiCompact f
obtain :
  ∀ (φ : S ⟶ R) [QuasiCompact (Spec.map φ)],
    (↑(ker (Spec.map φ)).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))
⊢ (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥(Spec R)) ⇑f)

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl