awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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
⊢ Membership.mem (γ := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) x
have 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)
Tactic: obtain ⟨i, x, rfl⟩ := 𝒰.exists_eq x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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)
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) ((𝒰.f i) x : ↥Y)
have inst : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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) (γ := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) ((𝒰.f i) x : ↥Y)
have 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)
Tactic: have := this (𝒰.pullbackHom f i) ⟨_, rfl⟩
        ((coe_support_inter _ ⟨⊤, isAffineOpen_top _⟩).ge ⟨?_, Set.mem_univ x⟩).1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
⊢ Membership.mem (α := ↥Y) (γ := Set ↥Y) (closure (Set.range (ι := ↥X) ⇑f)) ((𝒰.f i) x : ↥Y)
have 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) ⊤
            sorry)) :
      Set (↑Γ(𝒰.X i, (↑⟨⊤, sorry⟩ : (𝒰.X i).Opens)) : Type u))
Tactic: have := this (𝒰.pullbackHom f i) ⟨_, rfl⟩
        ((coe_support_inter _ ⟨⊤, isAffineOpen_top _⟩).ge ⟨?_, Set.mem_univ x⟩).1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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 (ι := ↥X) ⇑f)) ((𝒰.f i) x : ↥Y)
have 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)
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, 𝒰.pullbackHom_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
⊢ 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))
have a : 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) ⊤ sorry) :
                  (𝒰.X i).Opens))
              sorry)) :
        Set (↑Γ(Y, (↑⟨𝒰.f i ''ᵁ (↑⟨⊤, sorry⟩ : (𝒰.X i).Opens), sorry⟩ : Y.Opens)) : Type u)) ∩
    Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))
  ((𝒰.f i) x : ↥Y)
Tactic: rw [← (𝒰.f i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
          ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i)
            ((𝒰.pullback₁ f).f i) (𝒰.f i),
          Ideal.coe_comap, Set.image_preimage_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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 :
  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)
⊢ 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))
have a₁ : Function.Surjective (α :=
  (↑Γ(𝒰.X i,
        (↑(Subtype.mk (p := fun (x : (𝒰.X i).Opens) ↦ Membership.mem (γ := Set (𝒰.X i).Opens) (𝒰.X i).affineOpens x) ⊤
              sorry) :
          (𝒰.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) ⊤
                sorry) :
            (𝒰.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)
                  ⊤ sorry) :
              (𝒰.X i).Opens)))) :
    (a : (↑Γ(𝒰.X i, (↑⟨⊤, sorry⟩ : (𝒰.X i).Opens)) : Type u)) → (↑Γ(Y, 𝒰.f i ''ᵁ (↑⟨⊤, sorry⟩ : (𝒰.X i).Opens)) : Type u))
Tactic: rw [← (𝒰.f i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
          ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i)
            ((𝒰.pullback₁ f).f i) (𝒰.f i),
          Ideal.coe_comap, Set.image_preimage_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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 :
  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)
a₁ :
  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))
⊢ 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))
have a₂ : IsPullback (Cover.pullbackHom (P := IsOpenImmersion) 𝒰 f i) ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i) (𝒰.f i) f
Tactic: rw [← (𝒰.f i).isOpenEmbedding.injective.mem_set_image, Scheme.image_zeroLocus,
          ker_ideal_of_isPullback_of_isOpenImmersion f (𝒰.pullbackHom f i)
            ((𝒰.pullback₁ f).f i) (𝒰.f i),
          Ideal.coe_comap, Set.image_preimage_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X_1 Y_1 X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
hY : ∃ (S : CommRingCat.{u}), Y = Spec S
⊢ (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
have obtain : ∀ (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f],
  (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
Tactic: obtain ⟨S, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X_1 Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
⊢ (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
have 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)
Tactic: wlog hX : ∃ R, X = Spec R generalizing X S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
⊢ (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
have 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)
Tactic: wlog hX : ∃ R, X = Spec R generalizing X S
Cleared hypotheses: X, S, f, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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))
⊢ Membership.mem (γ := Set ↥(Spec S)) (closure (Set.range (ι := ↥X) ⇑f)) x
have inst : CompactSpace.{u} ↥X
Tactic: have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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
⊢ Membership.mem (γ := Set ↥(Spec S)) (closure (Set.range (ι := ↥X) ⇑f)) x
have 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
Tactic: obtain ⟨_, ⟨i, rfl⟩, hx⟩ := (f.iUnion_support_ker_openCover_map_comp 𝒰).ge hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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
⊢ Membership.mem (γ := Set ↥(Spec S)) (closure (Set.range (ι := ↥X) ⇑f)) x
have inst₁ : QuasiCompact (𝒰.f i ≫ f)
Tactic: have inst : QuasiCompact (𝒰.f i ≫ f) := HasAffineProperty.iff_of_isAffine.mpr
        (inferInstanceAs <| CompactSpace (Spec _))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X_1 Y X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
hX : ∃ (R : CommRingCat.{u}), X = Spec R
⊢ (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥X) ⇑f)
have obtain : ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ Spec S) [QuasiCompact f],
  (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥(Spec R)) ⇑f)
Tactic: obtain ⟨R, rfl⟩ := hX
Cleared hypotheses: X, f, inst, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
S R : CommRingCat
f : Spec R ⟶ Spec S
inst : QuasiCompact f
⊢ (↑(ker f).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥(Spec R)) ⇑f)
have obtain : ∀ (φ : S ⟶ R) [QuasiCompact (Spec.map φ)],
  (↑(ker (Spec.map φ)).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst : QuasiCompact (Spec.map φ)
⊢ (↑(ker (Spec.map φ)).support : Set ↥(Spec S)) ⊆ closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))
have rw : closure (Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom (φ ≫ (ΓSpecIso R).inv)))) ⊆
  closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))
Tactic: rw [ker_of_isAffine, coe_support_ofIdealTop, Spec_zeroLocus, ← Ideal.coe_comap,
      RingHom.comap_ker, ← PrimeSpectrum.closure_range_comap, ← CommRingCat.hom_comp,
      ← Scheme.ΓSpecIso_inv_naturality]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
S R : CommRingCat
φ : S ⟶ R
inst : QuasiCompact (Spec.map φ)
⊢ closure (Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom (φ ≫ (ΓSpecIso R).inv)))) ⊆
    closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))
have simp : closure
    (Set.range
      (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) ∘ PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv))) ⊆
  closure (Set.range (ι := ↥(Spec R)) ⇑(Spec.map φ))
Tactic: simp only [CommRingCat.hom_comp, PrimeSpectrum.comap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
⊢ closure (Set.range (ι := ↥X) ⇑f) ⊆ (↑(ker f).support : Set ↥Y)
have a : Set.range (ι := ↥X) ⇑f ⊆ (↑(ker f).support : Set ↥Y)
Tactic: rw [(support _).isClosed.closure_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
⊢ Hom.ker X.toSpecΓ = ⊥
have H : Eq (α :=
  Ideal
    (↑Γ(Spec Γ(X, ⊤),
          (↑(Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x) ⊤ sorry) :
            (Spec Γ(X, ⊤)).Opens)) :
      Type u))
  ((Hom.ker X.toSpecΓ).ideal
    (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
      Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x) ⊤ sorry))
  (ideal ⊥
    (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
      Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x) ⊤ sorry))
Tactic: apply IdealSheafData.ext_of_isAffine
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
⊢ (I.comapIso f).hom ≫ pullback.fst f I.subschemeι = (I.comap f).subschemeι
have rw : (I.comapIso f).hom ≫ (I.comapIso f).inv ≫ (I.comap f).subschemeι = (I.comap f).subschemeι
Tactic: rw [← comapIso_inv_subschemeι, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y : Scheme
I : Y.IdealSheafData
f : X ⟶ Y
rw : (I.comapIso f).hom ≫ (I.comapIso f).inv ≫ (I.comap f).subschemeι = (I.comap f).subschemeι
⊢ (I.comapIso f).hom ≫ pullback.fst f I.subschemeι = (I.comap f).subschemeι
have rw₁ : (I.comap f).subschemeι = (I.comap f).subschemeι
Tactic: rw [← comapIso_inv_subschemeι, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
X Y Z : Scheme
I : Z.IdealSheafData
f : X ⟶ Y
g : Y ⟶ Z
e : pullback f (I.comap g).subschemeι ≅ pullback (f ≫ g) I.subschemeι :=
  Iso.trans (Y := pullback (Y := pullback g I.subschemeι) f (pullback.fst g I.subschemeι))
    (asIso (pullback.map f (I.comap g).subschemeι f (pullback.fst g I.subschemeι) (𝟙 X) (I.comapIso g).hom (𝟙 Y) ⋯ ⋯))
    (pullbackRightPullbackFstIso g I.subschemeι f)
⊢ I.comap (f ≫ g) = (I.comap g).comap f
have rw : Hom.ker (e.hom ≫ pullback.fst (f ≫ g) I.subschemeι) =
  Hom.ker (X := pullback f (I.comap g).subschemeι) (pullback.fst f (I.comap g).subschemeι)
Tactic: rw [comap, comap, ← Scheme.Hom.ker_comp_of_isIso e.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
Z : Scheme
I : Z.IdealSheafData
⊢ I.comap (𝟙 Z) = I
have rw : Hom.ker (X := pullback (𝟙 Z) I.subschemeι) (pullback.fst (𝟙 Z) I.subschemeι) = I
Tactic: rw [comap, ← Scheme.Hom.ker_comp_of_isIso (inv (pullback.snd _ _)),
    pullback_inv_snd_fst_of_left_isIso, IsIso.inv_id, Category.comp_id, ker_subschemeι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
Z : Scheme
I : Z.IdealSheafData
rw : Hom.ker (X := pullback (𝟙 Z) I.subschemeι) (pullback.fst (𝟙 Z) I.subschemeι) = I
⊢ I.comap (𝟙 Z) = I
have rw₁ : Hom.ker
    (CategoryStruct.comp (Y := pullback (𝟙 Z) I.subschemeι) (inv (pullback.snd (𝟙 Z) I.subschemeι))
      (pullback.fst (𝟙 Z) I.subschemeι)) =
  I
Tactic: rw [comap, ← Scheme.Hom.ker_comp_of_isIso (inv (pullback.snd _ _)),
    pullback_inv_snd_fst_of_left_isIso, IsIso.inv_id, Category.comp_id, ker_subschemeι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Functorial (goal)
Goal:
Z : Scheme
I : Z.IdealSheafData
rw : Hom.ker (X := pullback (𝟙 Z) I.subschemeι) (pullback.fst (𝟙 Z) I.subschemeι) = I
rw₁ :
  Hom.ker
      (CategoryStruct.comp (Y := pullback (𝟙 Z) I.subschemeι) (inv (pullback.snd (𝟙 Z) I.subschemeι))
        (pullback.fst (𝟙 Z) I.subschemeι)) =
    I
⊢ I.comap (𝟙 Z) = I
have rw₂ : Hom.ker (I.subschemeι ≫ inv (𝟙 Z)) = I
Tactic: rw [comap, ← Scheme.Hom.ker_comp_of_isIso (inv (pullback.snd _ _)),
    pullback_inv_snd_fst_of_left_isIso, IsIso.inv_id, Category.comp_id, ker_subschemeι]