awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
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 ⋯).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))
⊢ 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))

Tactic:
apply ((𝒰.f i).appIso _).commRingCatIsoToRingEquiv.injective

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CategoryTheory.PreZeroHypercover.f, RingEquiv.injective, AlgebraicGeometry.Scheme.Hom.appIso, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
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)) ⋯) :
          (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))
⊢ 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))

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]

Premises used: CommRingCat.hom_comp, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, RingHom.comp_apply, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, AlgebraicGeometry.Scheme.Hom.appLE_map
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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) (↑U : Y.Opens) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) :
          (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:
simpa [Scheme.Hom.appLE] using ideal_ker_le _ _ (Ideal.mem_iInf.mp hs i)

Premises used: AlgebraicGeometry.Scheme.Hom.ideal_ker_le, AlgebraicGeometry.Scheme.Hom.appLE, Ideal.mem_iInf, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
⊢ ⨅ (i : 𝒰.I₀), ker (𝒰.f i ≫ f) = ker f

Tactic:
le_antisymm ?_ (le_iInf fun i ↦ (𝒰.f i).le_ker_comp f)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.le_ker_comp, le_iInf, le_antisymm, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
refine : ⨅ (i : 𝒰.I₀), ker (𝒰.f i ≫ f) ≤ ker f
⊢ ⨅ (i : 𝒰.I₀), ker (𝒰.f i ≫ f) = ker f

Tactic:
refine le_antisymm ?_ (le_iInf fun i ↦ (𝒰.f i).le_ker_comp f)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.le_ker_comp, le_iInf, le_antisymm, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
⊢ ⨅ (i : 𝒰.I₀), ker (𝒰.f i ≫ f) ≤ ker f

Tactic:
iInf_le_iff.mpr fun I hI U ↦ ?_

Premises used: Iff.mpr, Set.Mem, iInf_le_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
refine :
  ∀ (I : Y.IdealSheafData) (hI : ∀ (i : 𝒰.I₀), I ≤ ker (𝒰.f i ≫ f)) (U : (↑Y.affineOpens : Type u)),
    I.ideal U ≤ (ker f).ideal U
⊢ ⨅ (i : 𝒰.I₀), ker (𝒰.f i ≫ f) ≤ ker f

Tactic:
refine iInf_le_iff.mpr fun I hI U ↦ ?_

Premises used: Iff.mpr, iInf_le_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
rw : ∀ (i : 𝒰.I₀), I.ideal U ≤ (ker (𝒰.f i ≫ f)).ideal U
⊢ I.ideal U ≤ (ker f).ideal U

Tactic:
rw [← f.iInf_ker_openCover_map_comp_apply 𝒰, le_iInf_iff]

Premises used: le_iInf_iff, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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 : 𝒰.I₀), I.ideal U ≤ (ker (𝒰.f i ≫ f)).ideal U

Tactic:
fun i ↦ hI i U

Premises used: Set.Mem
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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 : 𝒰.I₀), I.ideal U ≤ (ker (𝒰.f i ≫ f)).ideal U

Tactic:
exact fun i ↦ hI i U
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
inr : Nonempty.{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)

Tactic:
cases isEmpty_or_nonempty 𝒰.I₀

Premises used: isEmpty_or_nonempty, CategoryTheory.PreZeroHypercover.I₀, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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₀
⊢ IsEmpty.{u + 1} ↥X

Tactic:
have : IsEmpty X := Function.isEmpty 𝒰.idx
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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₀
this : IsEmpty.{u + 1} ↥X
⊢ ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : Set ↥Y)

Tactic:
simp [ker_eq_top_of_isEmpty]

Premises used: AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
inst_1 : Finite.{u_1 + 1} 𝒰.I₀
h_1 : 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)
h :
  ∀ (x : ↥Y),
    Membership.mem (γ := Set ↥Y) (⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y)) x ↔ x ∈ (↑f.ker.support : Set ↥Y)
⊢ ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : Set ↥Y)

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
inst_1 : Finite.{u_1 + 1} 𝒰.I₀
h_1 : 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
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)
⊢ 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

Premises used: isOpen_univ, Set.mem_univ, AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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
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:
simpa [hxU] using congr(x ∈ $(this ⟨U, hU⟩))

Premises used: Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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₀
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)
⊢ ⋃ (i : 𝒰.I₀), (↑(ker (𝒰.f i ≫ f)).support : Set ↥Y) = (↑f.ker.support : 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⟩))
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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₀
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:
simp only [Set.iUnion_inter, coe_support_inter, ← f.iInf_ker_openCover_map_comp_apply 𝒰,
    Scheme.zeroLocus_iInf_of_nonempty]

Premises used: AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, Set.iUnion_inter, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U : Y.Opens
V : (↑(↑U : Scheme).affineOpens : Type u)
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)) ⋯) :
          Ideal
            (↑Γ(Y,
                  (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U.ι ''ᵁ (↑V : (↑U : Scheme).Opens)) ⋯) :
                    Y.Opens)) :
              Type u))
        x
⊢ (Hom.ker (f ∣_ U)).ideal V =
    f.ker.ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U.ι ''ᵁ (↑V : (↑U : Scheme).Opens)) ⋯)

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U : Y.Opens
V : (↑(↑U : Scheme).affineOpens : Type u)
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)) ⋯) :
        Ideal
          (↑Γ(Y,
                (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U.ι ''ᵁ (↑V : (↑U : Scheme).Opens)) ⋯) :
                  Y.Opens)) :
            Type u))
      x

Tactic:
simpa [Scheme.Hom.appLE] using map_eq_zero_iff _
    (ConcreteCategory.bijective_of_isIso
      (X.presheaf.map (eqToHom (image_morphismRestrict_preimage f U V)).op)).1

Premises used: AlgebraicGeometry.image_morphismRestrict_preimage, Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, And.left, map_eq_zero_iff, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, AlgebraicGeometry.Scheme.toLocallyRingedSpace, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- 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)
⊢ QuasiCompact f'

Tactic:
have : QuasiCompact f' := MorphismProperty.of_isPullback H.flip inferInstance
-- 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 : QuasiCompact f'
⊢ IsOpenImmersion iU

Tactic:
have : IsOpenImmersion iU := MorphismProperty.of_isPullback H inferInstance
-- 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 : IsOpenImmersion iU
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)) ⋯) : 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
⊢ (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)) ⋯))

Tactic:
ext x
-- 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 : IsOpenImmersion iU
x : (↑Γ(V, (↑W : V.Opens)) : Type u)
⊢ 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
-- 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 : 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))
rw : Hom.app f (iV ''ᵁ (↑W : V.Opens)) ≫ e.hom = Iso.hom (Hom.appIso iV (↑W : V.Opens)) ≫ Hom.app 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

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Iso.inv_comp_eq
-- 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 : 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))
⊢ Hom.app f (iV ''ᵁ (↑W : V.Opens)) ≫ e.hom = Iso.hom (Hom.appIso iV (↑W : V.Opens)) ≫ Hom.app f' (↑W : V.Opens)

Tactic:
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]

Premises used: CategoryTheory.eqToIso.hom, CategoryTheory.Iso.op_hom, AlgebraicGeometry.Scheme.Hom.appIso_hom', CategoryTheory.eqToHom_op, CategoryTheory.Iso.trans_hom, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, AlgebraicGeometry.Scheme.Hom.map_appLE, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, CategoryTheory.Functor.mapIso_hom
-- 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 : 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

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]
-- 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
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))
⊢ 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

Tactic:
simp only [Scheme.Hom.ker_apply, RingHom.mem_ker, Ideal.mem_comap, ← RingHom.comp_apply,
    ← CommRingCat.hom_comp, this]

Premises used: RingHom.mem_ker, AlgebraicGeometry.Scheme.Hom.ker_apply, CommRingCat.hom_comp, RingHom.comp_apply, Ideal.mem_comap