awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U) s
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : Membership.mem (α := ↥X) (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) ((𝒰.f i) x : ↥X)
⊢ Eq (α := (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑(X.presheaf.obj (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) →
            (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
        ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            s :
          (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
      (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
    (0 : (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
have a : Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ((Iso.commRingCatIsoToRingEquiv (appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens))) :
        (a : (↑Γ(X, 𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.presheaf.map (homOfLE sorry).op) :
            (a : (↑(X.presheaf.obj (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) →
              (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
          ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
              s :
            (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
        (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) :
    (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ((Iso.commRingCatIsoToRingEquiv (appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens))) :
        (a : (↑Γ(X, 𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      0 :
    (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
Tactic: apply ((𝒰.f i).appIso _).commRingCatIsoToRingEquiv.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U) s
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : Membership.mem (α := ↥X) (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) ((𝒰.f i) x : ↥X)
⊢ Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((Iso.commRingCatIsoToRingEquiv (appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens))) :
          (a : (↑Γ(X, 𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
            (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑(X.presheaf.obj (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) →
                (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
            ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
                  (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
                s :
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
          (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((Iso.commRingCatIsoToRingEquiv (appIso (𝒰.f i) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens))) :
          (a : (↑Γ(X, 𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
            (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        0 :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
have a : Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ((CommRingCat.Hom.hom (appLE (𝒰.f i) (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) sorry) :
        (a : (↑Γ(X, 𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
          (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.presheaf.map (homOfLE sorry).op) :
            (a : (↑(X.presheaf.obj (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) →
              (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
          ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
              s :
            (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
        (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) :
    (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
Tactic: rw [map_zero, ← RingEquiv.coe_toRingHom, Iso.commRingCatIsoToRingEquiv_toRingHom,
    Scheme.Hom.appIso_hom']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U) s
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : Membership.mem (α := ↥X) (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) ((𝒰.f i) x : ↥X)
⊢ Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((CommRingCat.Hom.hom
            (appLE (𝒰.f i) (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) :
          (a : (↑Γ(X, 𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →
            (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
              (a : (↑(X.presheaf.obj (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) →
                (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
            ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
                  (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
                s :
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
          (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) :
      (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
have a : Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ((CommRingCat.Hom.hom (appLE (𝒰.f i ≫ f) (↑U : Y.Opens) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) sorry) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      s :
    (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  (0 : (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
Tactic: simp only [homOfLE_leOfHom, Scheme.Hom.app_eq_appLE, ← RingHom.comp_apply,
    ← CommRingCat.hom_comp, Scheme.Hom.appLE_map, Scheme.Hom.appLE_comp_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
⊢ ⨅ (i : 𝒰.I₀), ker (𝒰.f i ≫ f) = ker f
have refine : ⨅ (i : 𝒰.I₀), ker (𝒰.f i ≫ f) ≤ ker f
Tactic: refine le_antisymm ?_ (le_iInf fun i ↦ (𝒰.f i).le_ker_comp f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
⊢ ⨅ (i : 𝒰.I₀), ker (𝒰.f i ≫ f) ≤ ker f
have refine : ∀ (I : Y.IdealSheafData) (hI : ∀ (i : 𝒰.I₀), I ≤ ker (𝒰.f i ≫ f)) (U : (↑Y.affineOpens : Type u)),
  I.ideal U ≤ (ker f).ideal U
Tactic: refine iInf_le_iff.mpr fun I hI U ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
I : Y.IdealSheafData
hI : ∀ (i : 𝒰.I₀), I ≤ ker (𝒰.f i ≫ f)
U : (↑Y.affineOpens : Type u)
⊢ I.ideal U ≤ (ker f).ideal U
have rw : ∀ (i : 𝒰.I₀), I.ideal U ≤ (ker (𝒰.f i ≫ f)).ideal U
Tactic: rw [← f.iInf_ker_openCover_map_comp_apply 𝒰, le_iInf_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
inst_1 : Finite.{u_1 + 1} 𝒰.I₀
⊢ ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : Set ↥Y)
have inl : IsEmpty.{u_1 + 1} 𝒰.I₀ → ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : Set ↥Y)
Tactic: cases isEmpty_or_nonempty 𝒰.I₀
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
inst_1 : Finite.{u_1 + 1} 𝒰.I₀
inl : IsEmpty.{u_1 + 1} 𝒰.I₀ → ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : Set ↥Y)
⊢ ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : Set ↥Y)
have inr : Nonempty.{u_1 + 1} 𝒰.I₀ → ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : Set ↥Y)
Tactic: cases isEmpty_or_nonempty 𝒰.I₀
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
inst_1 : Finite.{u_1 + 1} 𝒰.I₀
h : IsEmpty.{u_1 + 1} 𝒰.I₀
⊢ ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : Set ↥Y)
have this : IsEmpty.{u + 1} ↥X
Tactic: have : IsEmpty X := Function.isEmpty 𝒰.idx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
inst_1 : Finite.{u_1 + 1} 𝒰.I₀
h : Nonempty.{u_1 + 1} 𝒰.I₀
this :
  ∀ (U : (↑Y.affineOpens : Type u)),
    (⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y)) ∩ (↑(↑U : Y.Opens) : Set ↥Y) =
      (↑f.ker.support : Set ↥Y) ∩ (↑(↑U : Y.Opens) : Set ↥Y)
⊢ ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : Set ↥Y)
have h : ∀ (x : ↥Y),
  Membership.mem (γ := Set ↥Y) (⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y)) x ↔ x ∈ (↑f.ker.support : Set ↥Y)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
inst_1 : Finite.{u_1 + 1} 𝒰.I₀
h : Nonempty.{u_1 + 1} 𝒰.I₀
this :
  ∀ (U : (↑Y.affineOpens : Type u)),
    (⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y)) ∩ (↑(↑U : Y.Opens) : Set ↥Y) =
      (↑f.ker.support : Set ↥Y) ∩ (↑(↑U : Y.Opens) : Set ↥Y)
x : ↥Y
⊢ Membership.mem (γ := Set ↥Y) (⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y)) x ↔ x ∈ (↑f.ker.support : Set ↥Y)
have h : ∀ (U : TopologicalSpace.Opens ↥Y) (hU : U ∈ Y.affineOpens) (hxU : x ∈ (↑U : Set ↥Y)),
  Membership.mem (γ := Set ↥Y) (⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y)) x ↔ x ∈ (↑f.ker.support : Set ↥Y)
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
inst_1 : Finite.{u_1 + 1} 𝒰.I₀
h : Nonempty.{u_1 + 1} 𝒰.I₀
⊢ ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : Set ↥Y)
have inr : ∀ (U : (↑Y.affineOpens : Type u)),
  (⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y)) ∩ (↑(↑U : Y.Opens) : Set ↥Y) =
    (↑f.ker.support : Set ↥Y) ∩ (↑(↑U : Y.Opens) : Set ↥Y)
Tactic: suffices ∀ U : Y.affineOpens,
      (⋃ i, (𝒰.f i ≫ f).ker.support) ∩ U = (f.ker.support ∩ U : Set Y) by
    ext x
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
    simpa [hxU] using congr(x ∈ $(this ⟨U, hU⟩))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U : Y.Opens
V : (↑(↑U : Scheme).affineOpens : Type u)
⊢ (Hom.ker (f ∣_ U)).ideal V =
    f.ker.ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U.ι ''ᵁ (↑V : (↑U : Scheme).Opens)) ⋯)
have h : ∀ (x : (↑Γ((↑U : Scheme), (↑V : (↑U : Scheme).Opens)) : Type u)),
  x ∈ (Hom.ker (f ∣_ U)).ideal V ↔
    Membership.mem (γ := Ideal (↑Γ((↑U : Scheme), (↑V : (↑U : Scheme).Opens)) : Type u))
      (f.ker.ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U.ι ''ᵁ (↑V : (↑U : Scheme).Opens)) sorry) :
        Ideal
          (↑Γ(Y,
                (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U.ι ''ᵁ (↑V : (↑U : Scheme).Opens)) sorry) :
                  Y.Opens)) :
            Type u))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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)
⊢ (Hom.ker f').ideal W =
    Ideal.comap (S :=
      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯) : Y.Opens)) :
        Type u))
      (F := (↑Γ(V, (↑W : V.Opens)) : Type u) →+* (↑Γ(Y, iV ''ᵁ (↑W : V.Opens)) : Type u))
      (CommRingCat.Hom.hom (Iso.inv (Hom.appIso iV (↑W : V.Opens))))
      ((Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯))
have this : QuasiCompact f'
Tactic: have : QuasiCompact f' := MorphismProperty.of_isPullback H.flip inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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 : QuasiCompact f'
⊢ (Hom.ker f').ideal W =
    Ideal.comap (S :=
      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯) : Y.Opens)) :
        Type u))
      (F := (↑Γ(V, (↑W : V.Opens)) : Type u) →+* (↑Γ(Y, iV ''ᵁ (↑W : V.Opens)) : Type u))
      (CommRingCat.Hom.hom (Iso.inv (Hom.appIso iV (↑W : V.Opens))))
      ((Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯))
have this₁ : IsOpenImmersion iU
Tactic: have : IsOpenImmersion iU := MorphismProperty.of_isPullback H inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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 : IsOpenImmersion iU
⊢ (Hom.ker f').ideal W =
    Ideal.comap (S :=
      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯) : Y.Opens)) :
        Type u))
      (F := (↑Γ(V, (↑W : V.Opens)) : Type u) →+* (↑Γ(Y, iV ''ᵁ (↑W : V.Opens)) : Type u))
      (CommRingCat.Hom.hom (Iso.inv (Hom.appIso iV (↑W : V.Opens))))
      ((Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯))
have h : ∀ (x : (↑Γ(V, (↑W : V.Opens)) : Type u)),
  x ∈ (Hom.ker f').ideal W ↔
    Membership.mem (γ := Ideal (↑Γ(V, (↑W : V.Opens)) : Type u))
      (Ideal.comap (S :=
        (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) sorry) : Y.Opens)) :
          Type u))
        (F := (↑Γ(V, (↑W : V.Opens)) : Type u) →+* (↑Γ(Y, iV ''ᵁ (↑W : V.Opens)) : Type u))
        (CommRingCat.Hom.hom (Iso.inv (Hom.appIso iV (↑W : V.Opens))))
        ((Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) sorry)))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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 : IsOpenImmersion iU
x : (↑Γ(V, (↑W : V.Opens)) : Type u)
⊢ x ∈ (Hom.ker f').ideal W ↔
    Membership.mem (γ := Ideal (↑Γ(V, (↑W : V.Opens)) : Type u))
      (Ideal.comap (S :=
        (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯) : Y.Opens)) :
          Type u))
        (F := (↑Γ(V, (↑W : V.Opens)) : Type u) →+* (↑Γ(Y, iV ''ᵁ (↑W : V.Opens)) : Type u))
        (CommRingCat.Hom.hom (Iso.inv (Hom.appIso iV (↑W : V.Opens))))
        ((Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯)))
      x
have this₁ : iU ''ᵁ f' ⁻¹ᵁ (↑W : V.Opens) = f ⁻¹ᵁ iV ''ᵁ (↑W : V.Opens)
Tactic: have : iU ''ᵁ f' ⁻¹ᵁ W = f ⁻¹ᵁ iV ''ᵁ W :=
    IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback H W
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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 : 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)) ≪≫ Hom.appIso iU (f' ⁻¹ᵁ (↑W : V.Opens))
⊢ Iso.inv (Hom.appIso iV (↑W : V.Opens)) ≫ Hom.app f (iV ''ᵁ (↑W : V.Opens)) = Hom.app f' (↑W : V.Opens) ≫ e.inv
have rw : Hom.app f (iV ''ᵁ (↑W : V.Opens)) ≫ e.hom = Iso.hom (Hom.appIso iV (↑W : V.Opens)) ≫ Hom.app f' (↑W : V.Opens)
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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 : 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)) ≪≫ Hom.appIso iU (f' ⁻¹ᵁ (↑W : V.Opens))
⊢ x ∈ (Hom.ker f').ideal W ↔
    Membership.mem (γ := Ideal (↑Γ(V, (↑W : V.Opens)) : Type u))
      (Ideal.comap (S :=
        (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯) : Y.Opens)) :
          Type u))
        (F := (↑Γ(V, (↑W : V.Opens)) : Type u) →+* (↑Γ(Y, iV ''ᵁ (↑W : V.Opens)) : Type u))
        (CommRingCat.Hom.hom (Iso.inv (Hom.appIso iV (↑W : V.Opens))))
        ((Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯)))
      x
have this₁ : Iso.inv (Hom.appIso iV (↑W : V.Opens)) ≫ Hom.app f (iV ''ᵁ (↑W : V.Opens)) = Hom.app f' (↑W : V.Opens) ≫ e.inv
Tactic: have : (iV.appIso W).inv ≫ f.app _ = f'.app W ≫ e.inv := by
    rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]
    simp only [Scheme.Hom.app_eq_appLE, Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, eqToIso.hom,
      eqToHom_op, Scheme.Hom.appIso_hom', Scheme.Hom.map_appLE, e, Scheme.Hom.appLE_comp_appLE, H.w]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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
⊢ x ∈ (Hom.ker f').ideal W ↔
    Membership.mem (γ := Ideal (↑Γ(V, (↑W : V.Opens)) : Type u))
      (Ideal.comap (S :=
        (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯) : Y.Opens)) :
          Type u))
        (F := (↑Γ(V, (↑W : V.Opens)) : Type u) →+* (↑Γ(Y, iV ''ᵁ (↑W : V.Opens)) : Type u))
        (CommRingCat.Hom.hom (Iso.inv (Hom.appIso iV (↑W : V.Opens))))
        ((Hom.ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (iV ''ᵁ (↑W : V.Opens)) ⋯)))
      x
have h : 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: simp only [Scheme.Hom.ker_apply, RingHom.mem_ker, Ideal.mem_comap, ← RingHom.comp_apply,
    ← CommRingCat.hom_comp, this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
⊢ (↑(ker f).support : Set ↥Y) = closure (Set.range (ι := ↥X) ⇑f)
have a : (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
a : (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
⊢ (↑(ker f).support : Set ↥Y) = closure (Set.range (ι := ↥X) ⇑f)
have a₁ : closure (Set.range (ι := ↥X) ⇑f) ⊆ (↑(ker f).support : Set ↥Y)
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
⊢ (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
have 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)
Tactic: wlog hY : ∃ S, Y = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
⊢ (↑(ker f).support : Set ↥Y) ⊆ closure (Set.range (ι := ↥X) ⇑f)
have 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)
Tactic: wlog hY : ∃ S, Y = Spec S
Cleared hypotheses: f, inst