awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
h :
  (↑I.support : Set ↥X) ∩ Set.range (ι := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(IsAffineOpen.fromSpec ⋯) =
    Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
h₁ :
  (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
h₂ :
  (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
h₃ h₄ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
      (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑I.support : Set ↥X)))
    (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))))

Tactic:
rw [Set.image_preimage_eq_inter_range, IsAffineOpen.range_fromSpec,
    IsAffineOpen.fromSpec_image_zeroLocus, coe_support_inter]

Premises used: Set.image_preimage_eq_inter_range, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ Eq.{u + 1} (α := X.IdealSheafData) (vanishingIdeal ⊥) ⊤

Tactic:
gc.u_top

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.gc, GaloisConnection.u_top
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
rw : vanishingIdeal (support ⊥) = X.nilradical
rw₁ : radical ⊥ = X.nilradical
rw₂ rw₃ : Eq.{u + 1} (α := X.IdealSheafData) (radical ⊥) (radical ⊥)
⊢ vanishingIdeal ⊤ = X.nilradical

Tactic:
rw [← support_bot, vanishingIdeal_support, nilradical]

Premises used: AlgebraicGeometry.Scheme.nilradical, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_support, AlgebraicGeometry.Scheme.IdealSheafData.support_bot
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
ι : Sort u_1
Z : ι → Closeds ↥X
⊢ vanishingIdeal (iSup Z) = ⨅ (i : ι), vanishingIdeal (Z i)

Tactic:
gc.u_iInf

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.gc, Set.Mem, iSup, setOf, GaloisConnection.u_iInf, OrderDual
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
Z : Set (Closeds ↥X)
⊢ vanishingIdeal (sSup Z) = ⨅ z ∈ Z, vanishingIdeal z

Tactic:
gc.u_sInf

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.gc, Set.Mem, OrderDual, GaloisConnection.u_sInf
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
Z Z' : Closeds ↥X
⊢ vanishingIdeal (Z ⊔ Z') = vanishingIdeal Z ⊓ vanishingIdeal Z'

Tactic:
gc.u_inf

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.gc, GaloisConnection.u_inf
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
⊢ (I ⊔ J).support = I.support ⊓ J.support

Tactic:
gc.l_sup

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.gc, OrderDual, GaloisConnection.l_sup
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
ι : Sort u_1
I : ι → X.IdealSheafData
⊢ (iSup I).support = ⨅ (i : ι), (I i).support

Tactic:
gc.l_iSup

Premises used: iInf, AlgebraicGeometry.Scheme.IdealSheafData.gc, Set.Mem, GaloisConnection.l_iSup, OrderDual
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : Set X.IdealSheafData
⊢ (sSup I).support = ⨅ i ∈ I, i.support

Tactic:
gc.l_sSup

Premises used: iInf, AlgebraicGeometry.Scheme.IdealSheafData.gc, Set.Mem, GaloisConnection.l_sSup, OrderDual
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : IsReduced X
h :
  ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)),
    x_1 ∈ X.nilradical.ideal x ↔ x_1 ∈ IdealSheafData.ideal ⊥ x
⊢ X.nilradical = ⊥

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : IsReduced X
x : (↑X.affineOpens : Type u)
x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)
⊢ x_1 ∈ X.nilradical.ideal x ↔ x_1 ∈ IdealSheafData.ideal ⊥ x

Tactic:
simp [nilradical, Ideal.radical_eq_iff.mpr (Ideal.isRadical_bot)]

Premises used: Iff.mpr, Ideal.isRadical_bot, AlgebraicGeometry.Scheme.nilradical, Ideal.radical_eq_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
inst : IsReduced X
I : X.IdealSheafData
rw : ⊤ ≤ I.support ↔ I = ⊥
rw₁ : I ≤ vanishingIdeal ⊤ ↔ I = ⊥
rw₂ : I ≤ X.nilradical ↔ I = ⊥
rw₃ : I ≤ ⊥ ↔ I = ⊥
rw₄ rw₅ : I = ⊥ ↔ I = ⊥
⊢ I.support = ⊤ ↔ I = ⊥

Tactic:
rw [← top_le_iff, le_support_iff_le_vanishingIdeal,
    vanishingIdeal_top, nilradical_eq_bot, le_bot_iff]

Premises used: le_bot_iff, AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal, AlgebraicGeometry.Scheme.nilradical_eq_bot, top_le_iff, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
U : (↑Y.affineOpens : Type u)
⊢ f.ker.ideal 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)))

Tactic:
ideal_ofIdeals_le _ _

Premises used: Set.Mem, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U : (↑Y.affineOpens : Type u)
refine_2 :
  f.ker.ideal 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)))
refine_1 :
  ∀ (U : (↑Y.affineOpens : Type u)) (f_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(Y, Y.basicOpen f_1) : Type u))
      (Ideal.map (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
        ((fun (U : (↑Y.affineOpens : 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))) :
              Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
          U))
      ((fun (U : (↑Y.affineOpens : 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))) :
            Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
        (Y.affineBasicOpen f_1))
⊢ f.ker.ideal 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)))

Tactic:
let I : IdealSheafData Y := ⟨fun U ↦ RingHom.ker (f.app U).hom, ?_, _, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U : (↑Y.affineOpens : Type u)
I : Y.IdealSheafData :=
  {
    ideal := fun (U : (↑Y.affineOpens : 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))),
    map_ideal_basicOpen := ⋯, supportSet_eq_iInter_zeroLocus := ⋯ }
⊢ f.ker.ideal 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)))

Tactic:
congr($(ofIdeals_ideal I).ideal U)

Premises used: congrArg, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_ideal, id, AlgebraicGeometry.Scheme.IdealSheafData.ideal
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U : (↑Y.affineOpens : Type u)
I : Y.IdealSheafData :=
  {
    ideal := fun (U : (↑Y.affineOpens : 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))),
    map_ideal_basicOpen := ⋯, supportSet_eq_iInter_zeroLocus := ⋯ }
⊢ f.ker.ideal 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)))

Tactic:
exact congr($(ofIdeals_ideal I).ideal U)
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U_1 U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
refine_1 :
  LE.le (α := Ideal (↑Γ(Y, Y.basicOpen s) : Type u))
    (Ideal.map (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑Y.affineOpens : 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))) :
            Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
        U))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      (Y.affineBasicOpen s))
refine_1₁ :
  LE.le (α := Ideal (↑Γ(Y, Y.basicOpen s) : Type u))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      (Y.affineBasicOpen s))
    (Ideal.map (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑Y.affineOpens : 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))) :
            Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
        U))
⊢ Eq (α := Ideal (↑Γ(Y, Y.basicOpen s) : Type u))
    (Ideal.map (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑Y.affineOpens : 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))) :
            Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
        U))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      (Y.affineBasicOpen s))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U_1 U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
⊢ LE.le (α := Ideal (↑Γ(Y, Y.basicOpen s) : Type u))
    (Ideal.map (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑Y.affineOpens : 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))) :
            Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
        U))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      (Y.affineBasicOpen s))

Tactic:
Ideal.map_le_iff_le_comap.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, Ideal.map_le_iff_le_comap
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U_1 U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
refine_1 :
  ∀ (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (hx :
      Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
        ((fun (U : (↑Y.affineOpens : 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))) :
              Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
          U)
        x),
    Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
      (Ideal.comap (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
        ((fun (U : (↑Y.affineOpens : 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))) :
              Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
          (Y.affineBasicOpen s)))
      x
⊢ LE.le (α := Ideal (↑Γ(Y, Y.basicOpen s) : Type u))
    (Ideal.map (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑Y.affineOpens : 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))) :
            Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
        U))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      (Y.affineBasicOpen s))

Tactic:
refine Ideal.map_le_iff_le_comap.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, Ideal.map_le_iff_le_comap
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U_1 U : (↑Y.affineOpens : Type u)
s x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      U)
    x
refine_1 :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (Ideal.comap (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (CommRingCat.Hom.hom (f.app (↑U : Y.Opens)))
      (RingHom.ker (CommRingCat.Hom.hom (X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op))))
    x
⊢ Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (Ideal.comap (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑Y.affineOpens : 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))) :
            Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
        (Y.affineBasicOpen s)))
    x

Tactic:
simp_rw [RingHom.comap_ker, ← CommRingCat.hom_comp, Scheme.affineBasicOpen_coe, f.naturality,
      CommRingCat.hom_comp, ← RingHom.comap_ker]

Premises used: RingHom.comap_ker, CommRingCat.hom_comp, AlgebraicGeometry.Scheme.affineBasicOpen_coe, AlgebraicGeometry.Scheme.Hom.naturality
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U_1 U : (↑Y.affineOpens : Type u)
s x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      U)
    x
⊢ Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (Ideal.comap (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (CommRingCat.Hom.hom (f.app (↑U : Y.Opens)))
      (RingHom.ker (CommRingCat.Hom.hom (X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op))))
    x

Tactic:
Ideal.ker_le_comap _ hx

Premises used: Ideal.ker_le_comap
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U_1 U : (↑Y.affineOpens : Type u)
s x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      U)
    x
⊢ Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (Ideal.comap (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (CommRingCat.Hom.hom (f.app (↑U : Y.Opens)))
      (RingHom.ker (CommRingCat.Hom.hom (X.presheaf.map ((Opens.map f.base).map (homOfLE ⋯).op.unop).op))))
    x

Tactic:
exact Ideal.ker_le_comap _ hx

Premises used: Ideal.ker_le_comap
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U_1 U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
x : (↑Γ(Y, Y.basicOpen s) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, Y.basicOpen s) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      (Y.affineBasicOpen s))
    x
⊢ IsLocalization.Away s (↑Γ(Y, Y.basicOpen s) : Type u)

Tactic:
have := U.2.isLocalization_basicOpen s
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U_1 U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
x : (↑Γ(Y, Y.basicOpen s) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, Y.basicOpen s) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      (Y.affineBasicOpen s))
    x
this : IsLocalization.Away s (↑Γ(Y, Y.basicOpen s) : Type u)
refine_1 :
  ∀ (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (n : ℕ)
    (hx :
      Membership.mem (γ := Submodule (↑Γ(Y, Y.basicOpen s) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u))
        ((fun (U : (↑Y.affineOpens : 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))) :
              Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
          (Y.affineBasicOpen s))
        (IsLocalization.mk' (↑Γ(Y, Y.basicOpen s) : Type u) x
          (Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
            Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x)
            ((fun (x : ℕ) ↦ s ^ x) n) ⋯))),
    Membership.mem (γ := Submodule (↑Γ(Y, Y.basicOpen s) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u))
      (Ideal.map (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
        ((fun (U : (↑Y.affineOpens : 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))) :
              Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
          U))
      (IsLocalization.mk' (↑Γ(Y, Y.basicOpen s) : Type u) x
        (Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
          Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x)
          ((fun (x : ℕ) ↦ s ^ x) n) ⋯))
⊢ Membership.mem (γ := Submodule (↑Γ(Y, Y.basicOpen s) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u))
    (Ideal.map (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑Y.affineOpens : 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))) :
            Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
        U))
    x

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) x

Premises used: Submonoid.powers, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U_1 U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
this : IsLocalization.Away s (↑Γ(Y, Y.basicOpen s) : Type u)
x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
n : ℕ
hx :
  Membership.mem (γ := Submodule (↑Γ(Y, Y.basicOpen s) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u))
    ((fun (U : (↑Y.affineOpens : 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))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      (Y.affineBasicOpen s))
    (IsLocalization.mk' (↑Γ(Y, Y.basicOpen s) : Type u) x
      (Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
        Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x)
        ((fun (x : ℕ) ↦ s ^ x) n) ⋯))
⊢ Membership.mem (γ := Submodule (↑Γ(Y, Y.basicOpen s) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u))
    (Ideal.map (R := (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑Y.affineOpens : 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))) :
            Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
        U))
    (IsLocalization.mk' (↑Γ(Y, Y.basicOpen s) : Type u) x
      (Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
        Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x)
        ((fun (x : ℕ) ↦ s ^ x) n) ⋯))

Tactic:
(IsLocalization.mk'_mem_map_algebraMap_iff _ _ _ _ _).mpr ?_

Premises used: Iff.mpr, Set.Mem, setOf, IsLocalization.mk'_mem_map_algebraMap_iff