awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
⊢ g.ker ≤ ker (f ≫ g)

Tactic:
ofIdeals_mono fun U ↦ ?_

Premises used: Set.Mem, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
refine :
  ∀ (U : (↑Z.affineOpens : Type u)),
    LE.le (α := (fun (U : (↑Z.affineOpens : Type u)) ↦ Ideal.{u} (↑Γ(Z, (↑U : Z.Opens)) : Type u)) U)
      (RingHom.ker (F := (↑Γ(Z, (↑U : Z.Opens)) : Type u) →+* (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
        (CommRingCat.Hom.hom (g.app (↑U : Z.Opens))))
      (RingHom.ker (F := (↑Γ(Z, (↑U : Z.Opens)) : Type u) →+* (↑Γ(X, (f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
        (CommRingCat.Hom.hom (app (f ≫ g) (↑U : Z.Opens))))
⊢ g.ker ≤ ker (f ≫ g)

Tactic:
refine ofIdeals_mono fun U ↦ ?_

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
U : (↑Z.affineOpens : Type u)
rw :
  LE.le (α := (fun (U : (↑Z.affineOpens : Type u)) ↦ Ideal.{u} (↑Γ(Z, (↑U : Z.Opens)) : Type u)) U)
    (RingHom.ker (F := (↑Γ(Z, (↑U : Z.Opens)) : Type u) →+* (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
      (CommRingCat.Hom.hom (g.app (↑U : Z.Opens))))
    (Ideal.comap (F := (↑Γ(Z, (↑U : Z.Opens)) : Type u) →+* (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
      (CommRingCat.Hom.hom (g.app (↑U : Z.Opens)))
      (RingHom.ker (F := (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u) →+* (↑Γ(X, (f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
        (CommRingCat.Hom.hom (app f (g ⁻¹ᵁ (↑U : Z.Opens))))))
⊢ LE.le (α := (fun (U : (↑Z.affineOpens : Type u)) ↦ Ideal.{u} (↑Γ(Z, (↑U : Z.Opens)) : Type u)) U)
    (RingHom.ker (F := (↑Γ(Z, (↑U : Z.Opens)) : Type u) →+* (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
      (CommRingCat.Hom.hom (g.app (↑U : Z.Opens))))
    (RingHom.ker (F := (↑Γ(Z, (↑U : Z.Opens)) : Type u) →+* (↑Γ(X, (f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
      (CommRingCat.Hom.hom (app (f ≫ g) (↑U : Z.Opens))))

Tactic:
rw [Scheme.Hom.comp_app f g U, CommRingCat.hom_comp, ← RingHom.comap_ker]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_app, RingHom.comap_ker, CommRingCat.hom_comp, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
U : (↑Z.affineOpens : Type u)
⊢ LE.le (α := (fun (U : (↑Z.affineOpens : Type u)) ↦ Ideal.{u} (↑Γ(Z, (↑U : Z.Opens)) : Type u)) U)
    (RingHom.ker (F := (↑Γ(Z, (↑U : Z.Opens)) : Type u) →+* (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
      (CommRingCat.Hom.hom (g.app (↑U : Z.Opens))))
    (Ideal.comap (F := (↑Γ(Z, (↑U : Z.Opens)) : Type u) →+* (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
      (CommRingCat.Hom.hom (g.app (↑U : Z.Opens)))
      (RingHom.ker (F := (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u) →+* (↑Γ(X, (f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
        (CommRingCat.Hom.hom (app f (g ⁻¹ᵁ (↑U : Z.Opens))))))

Tactic:
Ideal.ker_le_comap _

Premises used: Set.Mem, Ideal.ker_le_comap
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
U : (↑Z.affineOpens : Type u)
⊢ LE.le (α := (fun (U : (↑Z.affineOpens : Type u)) ↦ Ideal.{u} (↑Γ(Z, (↑U : Z.Opens)) : Type u)) U)
    (RingHom.ker (F := (↑Γ(Z, (↑U : Z.Opens)) : Type u) →+* (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
      (CommRingCat.Hom.hom (g.app (↑U : Z.Opens))))
    (Ideal.comap (F := (↑Γ(Z, (↑U : Z.Opens)) : Type u) →+* (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
      (CommRingCat.Hom.hom (g.app (↑U : Z.Opens)))
      (RingHom.ker (F := (↑Γ(Y, g ⁻¹ᵁ (↑U : Z.Opens)) : Type u) →+* (↑Γ(X, (f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Type u))
        (CommRingCat.Hom.hom (app f (g ⁻¹ᵁ (↑U : Z.Opens))))))

Tactic:
exact Ideal.ker_le_comap _

Premises used: Ideal.ker_le_comap
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : IsEmpty.{u + 1} ↥X
U : (↑Y.affineOpens : Type u)
x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
h : x ∈ ideal ⊤ U
⊢ Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (RingHom.ker (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (CommRingCat.Hom.hom (f.app (↑U : Y.Opens))))
    x

Tactic:
simpa using Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
h : ∀ (U : (↑Y.affineOpens : Type u)) (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)), x ∈ (ker f).ideal U ↔ x ∈ ideal ⊥ U
⊢ ker f = ⊥

Tactic:
ext U
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : (↑Y.affineOpens : Type u)
x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
⊢ x ∈ (ker f).ideal U ↔ x ∈ ideal ⊥ U

Tactic:
simp [map_eq_zero_iff _ (ConcreteCategory.bijective_of_isIso (f.app U)).1]

Premises used: AlgebraicGeometry.Scheme.Hom.app, And.left, map_eq_zero_iff, Subtype.val, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
⊢ ker (inv f ≫ f ≫ g) ≤ ker g

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine Y
⊢ RingHom.ker (F :=
      (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u_1) →+*
        (↑Γ(X, f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens)) : Type u_1))
      (CommRingCat.Hom.hom (Hom.app f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯) : Y.Opens))) ≤
    (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal
      (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) ⊤ ⋯)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine Y
refine :
  ∀ (U : (↑Y.affineOpens : Type u_1)),
    (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal U ≤
      RingHom.ker (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u_1) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u_1))
        (CommRingCat.Hom.hom (Hom.app f (↑U : Y.Opens)))
⊢ Hom.ker f = ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))

Tactic:
refine (le_of_isAffine ((f.ideal_ker_le _).trans (by simp))).antisymm
    (le_ofIdeals_iff.mpr fun U ↦ ?_)

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.IdealSheafData.le_of_isAffine, LE.le.antisymm, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine Y
U : (↑Y.affineOpens : Type u_1)
simp :
  LE.le (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))
    (RingHom.ker (CommRingCat.Hom.hom (Hom.app f ⊤ ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op)))
⊢ (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal U ≤
    RingHom.ker (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u_1) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u_1))
      (CommRingCat.Hom.hom (Hom.app f (↑U : Y.Opens)))

Tactic:
simp only [ofIdealTop_ideal, homOfLE_leOfHom, Ideal.map_le_iff_le_comap, RingHom.comap_ker,
    ← CommRingCat.hom_comp, f.naturality]

Premises used: RingHom.comap_ker, CommRingCat.hom_comp, CategoryTheory.homOfLE_leOfHom, Ideal.map_le_iff_le_comap, AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal, AlgebraicGeometry.Scheme.Hom.naturality
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine Y
U : (↑Y.affineOpens : Type u_1)
x : (↑Γ(Y, ⊤) : Type u_1)
⊢ Membership.mem (γ := Submodule (↑Γ(Y, ⊤) : Type u_1) (↑Γ(Y, ⊤) : Type u_1))
      (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f))) x →
    Membership.mem (γ := Submodule (↑Γ(Y, ⊤) : Type u_1) (↑Γ(Y, ⊤) : Type u_1))
      (RingHom.ker (CommRingCat.Hom.hom (Hom.app f ⊤ ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op)))
      x

Tactic:
simp +contextual
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
obtain :
  ∀ (U : TopologicalSpace.Opens ↥Y) (hU : U ∈ Y.affineOpens) (hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)),
    Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) (f x : ↥Y)
⊢ Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) (f x : ↥Y)

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

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
⊢ Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) (f x : ↥Y)

Tactic:
((coe_support_inter f.ker ⟨U, hU⟩).ge ⟨?_, hxU⟩).1

Premises used: Eq.ge, AlgebraicGeometry.Scheme.Hom.ker, Subtype.mk, And.left, And.intro, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
refine :
  Membership.mem (α := ↥Y)
    (Y.zeroLocus
      (↑((ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU)) :
        Set (↑Γ(Y, (↑⟨U, hU⟩ : Y.Opens)) : Type u)))
    (f x : ↥Y)
⊢ Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) (f x : ↥Y)

Tactic:
refine ((coe_support_inter f.ker ⟨U, hU⟩).ge ⟨?_, hxU⟩).1

Premises used: Eq.ge, AlgebraicGeometry.Scheme.Hom.ker, Subtype.mk, And.left, And.intro, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
simp :
  ∀ (f_1 : (↑Γ(Y, U) : Type u)),
    Membership.mem (γ := Ideal (↑Γ(Y, U) : Type u))
        ((ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) :
          Ideal (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Type u))
        f_1 →
      (f x : ↥Y) ∉ Y.basicOpen f_1
⊢ Membership.mem (α := ↥Y)
    (Y.zeroLocus
      (↑((ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU)) :
        Set (↑Γ(Y, (↑⟨U, hU⟩ : Y.Opens)) : Type u)))
    (f x : ↥Y)

Tactic:
simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]

Premises used: SetLike.mem_coe, AlgebraicGeometry.Scheme.mem_zeroLocus_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
s : (↑Γ(Y, U) : Type u)
hs :
  Membership.mem (γ := Ideal (↑Γ(Y, U) : Type u))
    ((ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) :
      Ideal (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Type u))
    s
hxs : Membership.mem (α := ↥Y) (Y.basicOpen s) (f x : ↥Y)
⊢ x ∈ f ⁻¹ᵁ Y.basicOpen s

Tactic:
have : x ∈ f ⁻¹ᵁ Y.basicOpen s := hxs
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
s : (↑Γ(Y, U) : Type u)
hs :
  Membership.mem (γ := Ideal (↑Γ(Y, U) : Type u))
    ((ker f).ideal (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) :
      Ideal (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)) : Type u))
    s
hxs : Membership.mem (α := ↥Y) (Y.basicOpen s) (f x : ↥Y)
this : x ∈ f ⁻¹ᵁ Y.basicOpen s
rwa :
  ∀
    (this :
      x ∈
        X.basicOpen (U := f ⁻¹ᵁ U)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (app f U) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
            s)),
    False
rwa₁ : ∀ (this : x ∈ X.basicOpen (U := f ⁻¹ᵁ U) 0), False
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : Membership.mem (γ := X.Opens) ⊥ x), False
⊢ False

Tactic:
rwa [Scheme.preimage_basicOpen, RingHom.mem_ker.mp (f.ideal_ker_le _ hs),
    Scheme.basicOpen_zero] at this

Premises used: RingHom.mem_ker, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, Iff.mp, AlgebraicGeometry.Scheme.basicOpen_zero, AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
H : f.ker = ⊤
⊢ IsEmpty.{u + 1} ↥X

Tactic:
simpa [H] using f.range_subset_ker_support

Premises used: AlgebraicGeometry.Scheme.Hom.range_subset_ker_support
-- 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)
⊢ ⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U = f.ker.ideal U

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

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.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
refine : ⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U ≤ f.ker.ideal U
⊢ ⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U = f.ker.ideal U

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

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.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
simp :
  Eq (α := (↑Γ(X, 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))
    (0 : (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
⊢ s ∈ f.ker.ideal U

Tactic:
simp only [Hom.ker_apply, RingHom.mem_ker]

Premises used: RingHom.mem_ker, AlgebraicGeometry.Scheme.Hom.ker_apply
-- 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
apply :
  ∀ x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens))),
    ∃ (V : TopologicalSpace.Opens ↥X) (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))),
      x ∈ V ∧
        Eq (α := (↑(X.presheaf.obj (Opposite.op V)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE hV).op) :
                (a : (↑(X.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))))) : Type u)) →
                  (↑(X.presheaf.obj (Opposite.op V)) : 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 V)) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X.presheaf.map (homOfLE hV).op) :
                (a : (↑(X.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))))) : Type u)) →
                  (↑(X.presheaf.obj (Opposite.op V)) : Type u))
              0 :
            (↑(X.presheaf.obj (Opposite.op V)) : Type u))
⊢ Eq (α := (↑Γ(X, 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))
    (0 : (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))

Tactic:
apply X.IsSheaf.section_ext

Premises used: TopCat.Presheaf.IsSheaf.section_ext, AlgebraicGeometry.SheafedSpace.IsSheaf, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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)
simp :
  ∃ (V : TopologicalSpace.Opens ↥X),
    Membership.mem (α := ↥X) V ((𝒰.f i) x : ↥X) ∧
      ∃ (x : V ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Eq (α := (↑(X.presheaf.obj (Opposite.op V)) : 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 V)) : 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 V)) : Type u))
          (0 : (↑(X.presheaf.obj (Opposite.op V)) : Type u))
⊢ ∃ (V : TopologicalSpace.Opens ↥X) (hV : V ≤ Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))),
    Membership.mem (α := ↥X) V ((𝒰.f i) x : ↥X) ∧
      Eq (α := (↑(X.presheaf.obj (Opposite.op V)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE hV).op) :
              (a : (↑(X.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))))) : Type u)) →
                (↑(X.presheaf.obj (Opposite.op V)) : 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 V)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE hV).op) :
              (a : (↑(X.presheaf.obj (Opposite.op (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))))) : Type u)) →
                (↑(X.presheaf.obj (Opposite.op V)) : Type u))
            0 :
          (↑(X.presheaf.obj (Opposite.op V)) : Type u))

Tactic:
simp only [homOfLE_leOfHom, map_zero, exists_and_left]

Premises used: map_zero, exists_and_left, CategoryTheory.homOfLE_leOfHom
-- 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)
⊢ ∃ (V : TopologicalSpace.Opens ↥X),
    Membership.mem (α := ↥X) V ((𝒰.f i) x : ↥X) ∧
      ∃ (x : V ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Eq (α := (↑(X.presheaf.obj (Opposite.op V)) : 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 V)) : 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 V)) : Type u))
          (0 : (↑(X.presheaf.obj (Opposite.op V)) : Type u))

Tactic:
⟨𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ U.1, ⟨_, hxU, rfl⟩,
    Set.image_preimage_subset (𝒰.f i) (f ⁻¹ᵁ U), ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, CategoryTheory.PreZeroHypercover.f, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', SetLike.coe, And.intro, Set.image_preimage_subset, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, Subtype.val, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.Functor.obj, rfl
-- 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)
refine :
  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))
⊢ ∃ (V : TopologicalSpace.Opens ↥X),
    Membership.mem (α := ↥X) V ((𝒰.f i) x : ↥X) ∧
      ∃ (x : V ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Eq (α := (↑(X.presheaf.obj (Opposite.op V)) : 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 V)) : 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 V)) : Type u))
          (0 : (↑(X.presheaf.obj (Opposite.op V)) : Type u))

Tactic:
refine ⟨𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ U.1, ⟨_, hxU, rfl⟩,
    Set.image_preimage_subset (𝒰.f i) (f ⁻¹ᵁ U), ?_⟩