awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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) ⋯))
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (f ⁻¹ᵁ Y.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier)
      ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        x)
      (f ⁻¹ᵁ Y.basicOpen s) ⋯)
    0
have hx₁ : Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
  ((CommRingCat.Hom.hom (Y.presheaf.map (homOfLE sorry).op ≫ f.app (Y.basicOpen s)) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
      x :
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
  (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
Tactic: replace hx : (Y.presheaf.map (homOfLE (Y.basicOpen_le s)).op ≫ f.app _).hom x = 0 := by
      trans (f.app (Y.basicOpen s)).hom (algebraMap Γ(Y, U) _ x)
      · simp [-NatTrans.naturality, RingHom.algebraMap_toAlgebra]
      · simp only [Scheme.affineBasicOpen_coe, RingHom.mem_ker] at hx
        rw [← IsLocalization.mk'_spec' (M := .powers s), map_mul, hx, mul_zero]
Cleared hypotheses: 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 : (↑Γ(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 :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    ((CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (f ⁻¹ᵁ Y.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier)
      ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        x)
      (f ⁻¹ᵁ Y.basicOpen s) ⋯)
    0
have refine_1 : ∀
  (hx :
    Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
      ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens) ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE sorry).op.unop).op) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
          x :
        (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
      (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))),
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (f ⁻¹ᵁ Y.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier)
      ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        x)
      (f ⁻¹ᵁ Y.basicOpen s) sorry)
    0
Tactic: rwa [f.naturality] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
⊢ g.ker ≤ ker (f ≫ g)
have 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))))
Tactic: refine ofIdeals_mono fun U ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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))))
    (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))))
have 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))))))
Tactic: rw [Scheme.Hom.comp_app f g U, CommRingCat.hom_comp, ← RingHom.comap_ker]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
⊢ ker f = ⊥
have h : ∀ (U : (↑Y.affineOpens : Type u)) (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)), x ∈ (ker f).ideal U ↔ x ∈ ideal ⊥ U
Tactic: ext U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine Y
⊢ Hom.ker f = ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))
have 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)))
Tactic: refine (le_of_isAffine ((f.ideal_ker_le _).trans (by simp))).antisymm
    (le_ofIdeals_iff.mpr fun U ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine Y
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)))
have 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 sorry).op.unop).op)))
Tactic: simp only [ofIdealTop_ideal, homOfLE_leOfHom, Ideal.map_le_iff_le_comap, RingHom.comap_ker,
    ← CommRingCat.hom_comp, f.naturality]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Membership.mem (α := ↥Y) (↑(ker f).support : Set ↥Y) (f x : ↥Y)
have 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)
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
have 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)
Tactic: refine ((coe_support_inter f.ker ⟨U, hU⟩).ge ⟨?_, hxU⟩).1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
    (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)
have 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
Tactic: simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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)
⊢ False
have this : x ∈ f ⁻¹ᵁ Y.basicOpen s
Tactic: have : x ∈ f ⁻¹ᵁ Y.basicOpen s := hxs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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
⊢ False
have 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
Tactic: rwa [Scheme.preimage_basicOpen, RingHom.mem_ker.mp (f.ideal_ker_le _ hs),
    Scheme.basicOpen_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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
⊢ False
have rwa₁ : ∀ (this : x ∈ X.basicOpen (U := f ⁻¹ᵁ U) 0), False
Tactic: rwa [Scheme.preimage_basicOpen, RingHom.mem_ker.mp (f.ideal_ker_le _ hs),
    Scheme.basicOpen_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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
⊢ False
have rwa₂ : ∀ (this : Membership.mem (γ := X.Opens) ⊥ x), False
Tactic: rwa [Scheme.preimage_basicOpen, RingHom.mem_ker.mp (f.ideal_ker_le _ hs),
    Scheme.basicOpen_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
⊢ ⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U = f.ker.ideal U
have refine : ⨅ (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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U) s
⊢ s ∈ f.ker.ideal U
have 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))
Tactic: simp only [Hom.ker_apply, RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U) s
⊢ 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))
have 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))
Tactic: apply X.IsSheaf.section_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U) s
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : Membership.mem (α := ↥X) (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) ((𝒰.f i) x : ↥X)
⊢ ∃ (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))
have 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 sorry).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: simp only [homOfLE_leOfHom, map_zero, exists_and_left]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
𝒰 : OpenCover.{u_1, u} X
U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
hs :
  Membership.mem (γ := Submodule (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, (↑U : Y.Opens)) : Type u))
    (⨅ (i : 𝒰.I₀), (ker (𝒰.f i ≫ f)).ideal U) s
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : Membership.mem (α := ↥X) (Opposite.unop (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) ((𝒰.f i) x : ↥X)
⊢ ∃ (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))
have 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 sorry).op) :
        (a : (↑(X.presheaf.obj (Opposite.op (f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u)) →
          (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
      ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
          s :
        (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
    (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
  (0 : (↑(X.presheaf.obj (Opposite.op (𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ (↑U : Y.Opens)))) : Type u))
Tactic: refine ⟨𝒰.f i ''ᵁ 𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ U.1, ⟨_, hxU, rfl⟩,
    Set.image_preimage_subset (𝒰.f i) (f ⁻¹ᵁ U), ?_⟩