awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑I.support : Set ↥X)) = (I.ideal U).radical
have h : PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑I.support : Set ↥X)) =
  PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
Tactic: rw [← vanishingIdeal_zeroLocus_eq_radical]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑I.support : Set ↥X)) =
    PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
have h : Eq (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑I.support : Set ↥X))
  (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑I.support : Set ↥X))
    (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
have h : Eq (α := Set ↥X)
  (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec sorry))
    (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑I.support : Set ↥X)))
  (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec sorry))
    (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))))
Tactic: apply U.2.fromSpec.isOpenEmbedding.injective.image_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ 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))))
have h : (↑I.support : Set ↥X) ∩ Set.range (ι := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(IsAffineOpen.fromSpec sorry) =
  Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec sorry))
    (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)))
⊢ 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))))
have h₁ : (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) =
  Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec sorry))
    (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)))
⊢ 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))))
have 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)
Tactic: rw [Set.image_preimage_eq_inter_range, IsAffineOpen.range_fromSpec,
    IsAffineOpen.fromSpec_image_zeroLocus, coe_support_inter]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
⊢ 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))))
have 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)
Tactic: rw [Set.image_preimage_eq_inter_range, IsAffineOpen.range_fromSpec,
    IsAffineOpen.fromSpec_image_zeroLocus, coe_support_inter]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
⊢ vanishingIdeal ⊤ = X.nilradical
have rw : vanishingIdeal (support ⊥) = X.nilradical
Tactic: rw [← support_bot, vanishingIdeal_support, nilradical]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
rw : vanishingIdeal (support ⊥) = X.nilradical
⊢ vanishingIdeal ⊤ = X.nilradical
have rw₁ : radical ⊥ = X.nilradical
Tactic: rw [← support_bot, vanishingIdeal_support, nilradical]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
rw : vanishingIdeal (support ⊥) = X.nilradical
rw₁ : radical ⊥ = X.nilradical
⊢ vanishingIdeal ⊤ = X.nilradical
have rw₂ : Eq.{u + 1} (α := X.IdealSheafData) (radical ⊥) (radical ⊥)
Tactic: rw [← support_bot, vanishingIdeal_support, nilradical]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
inst : IsReduced X
⊢ X.nilradical = ⊥
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
inst : IsReduced X
I : X.IdealSheafData
⊢ I.support = ⊤ ↔ I = ⊥
have rw : ⊤ ≤ I.support ↔ I = ⊥
Tactic: rw [← top_le_iff, le_support_iff_le_vanishingIdeal,
    vanishingIdeal_top, nilradical_eq_bot, le_bot_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
inst : IsReduced X
I : X.IdealSheafData
rw : ⊤ ≤ I.support ↔ I = ⊥
⊢ I.support = ⊤ ↔ I = ⊥
have rw₁ : I ≤ vanishingIdeal ⊤ ↔ I = ⊥
Tactic: rw [← top_le_iff, le_support_iff_le_vanishingIdeal,
    vanishingIdeal_top, nilradical_eq_bot, le_bot_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
inst : IsReduced X
I : X.IdealSheafData
rw : ⊤ ≤ I.support ↔ I = ⊥
rw₁ : I ≤ vanishingIdeal ⊤ ↔ I = ⊥
⊢ I.support = ⊤ ↔ I = ⊥
have rw₂ : I ≤ X.nilradical ↔ I = ⊥
Tactic: rw [← top_le_iff, le_support_iff_le_vanishingIdeal,
    vanishingIdeal_top, nilradical_eq_bot, le_bot_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
inst : IsReduced X
I : X.IdealSheafData
rw : ⊤ ≤ I.support ↔ I = ⊥
rw₁ : I ≤ vanishingIdeal ⊤ ↔ I = ⊥
rw₂ : I ≤ X.nilradical ↔ I = ⊥
⊢ I.support = ⊤ ↔ I = ⊥
have rw₃ : I ≤ ⊥ ↔ I = ⊥
Tactic: rw [← top_le_iff, le_support_iff_le_vanishingIdeal,
    vanishingIdeal_top, nilradical_eq_bot, le_bot_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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 = ⊥
⊢ I.support = ⊤ ↔ I = ⊥
have rw₄ : I = ⊥ ↔ I = ⊥
Tactic: rw [← top_le_iff, le_support_iff_le_vanishingIdeal,
    vanishingIdeal_top, nilradical_eq_bot, le_bot_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)))
⊢ 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)))
have 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 sorry).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))
Tactic: let I : IdealSheafData Y := ⟨fun U ↦ RingHom.ker (f.app U).hom, ?_, _, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
⊢ 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))
have 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 sorry).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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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))
⊢ 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))
have 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 sorry).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))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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))
have 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 sorry).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: refine Ideal.map_le_iff_le_comap.mpr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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 (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
have 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 sorry).op.unop).op))))
  x
Tactic: simp_rw [RingHom.comap_ker, ← CommRingCat.hom_comp, Scheme.affineBasicOpen_coe, f.naturality,
      CommRingCat.hom_comp, ← RingHom.comap_ker]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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
⊢ 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
have this : IsLocalization.Away s (↑Γ(Y, Y.basicOpen s) : Type u)
Tactic: have := U.2.isLocalization_basicOpen s
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
⊢ 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
have 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) sorry))),
  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 sorry).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) sorry))
Tactic: obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) x
Cleared hypotheses: x, hx