awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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) ⋯))
have refine_1 : ∃ (s_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u)),
  Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) s_1 ∧
    Membership.mem (γ := Ideal (↑Γ(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)
      (s_1 * x)
Tactic: refine (IsLocalization.mk'_mem_map_algebraMap_iff _ _ _ _ _).mpr ?_
-- 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_1 : 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) ⋯))
this :
  ∃ (V : X.Opens) (hV :
    V =
      X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
        ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
          s)),
    Eq (α :=
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (X.presheaf.obj (Opposite.op V)))
      (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)
        V ⋯)
      0
⊢ ∃ (s_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u)),
    Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) s_1 ∧
      Membership.mem (γ := Ideal (↑Γ(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)
        (s_1 * x)
have H : Eq (α :=
  ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
    (X.presheaf.obj
      (Opposite.op
        (X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
          ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            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)
    (X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
      ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        s))
    sorry)
  0
Tactic: obtain ⟨_, rfl, H⟩ := 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
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) ⋯))
⊢ ∃ (s_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u)),
    Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) s_1 ∧
      Membership.mem (γ := Ideal (↑Γ(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)
        (s_1 * x)
have refine_1 : ∃ (V : X.Opens) (hV :
  V =
    X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
      ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        s)),
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op V)))
    (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)
      V sorry)
    0
Tactic: suffices ∃ (V : X.Opens) (hV : V = X.basicOpen ((f.app U).hom s)),
        letI := hV.trans_le (X.basicOpen_le _); ((f.app U).hom x |_ V) = 0 by
      obtain ⟨_, rfl, H⟩ := this
      obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact
        X (U := f ⁻¹ᵁ U) (QuasiCompact.isCompact_preimage (f := f) _ U.1.2 U.2.isCompact)
        (f.app U x) (f.app U s) H
      exact ⟨_, ⟨n, rfl⟩, by simpa using hn⟩
-- 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 :
  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) ⋯))
⊢ ∃ (V : X.Opens) (hV :
    V =
      X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
        ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
          s)),
    Eq (α :=
      ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
        (X.presheaf.obj (Opposite.op V)))
      (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)
        V ⋯)
      0
have refine_1 : 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: refine ⟨f ⁻¹ᵁ Y.basicOpen s, by simp, ?_⟩
-- 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 :
  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 (α := (↑Γ(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))
have trans : 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))
  ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
        (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
      ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
          x :
        (↑Γ(Y, Y.basicOpen s) : Type u)) :
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
Tactic: trans (f.app (Y.basicOpen s)).hom (algebraMap Γ(Y, U) _ x)
-- 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 :
  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) ⋯))
trans :
  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))
    ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
            x :
          (↑Γ(Y, Y.basicOpen s) : Type u)) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
⊢ 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))
have trans₁ : Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
  ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
        (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
      ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
          x :
        (↑Γ(Y, Y.basicOpen s) : Type u)) :
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
  (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
Tactic: trans (f.app (Y.basicOpen s)).hom (algebraMap Γ(Y, U) _ x)
-- 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 (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
            x :
          (↑Γ(Y, Y.basicOpen s) : Type u)) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
have hx₁ : Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
  ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
        (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
      (IsLocalization.mk' (M := Submonoid.powers s) (↑Γ(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) (s ^ n) sorry)) :
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
  (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
Tactic: simp only [Scheme.affineBasicOpen_coe, RingHom.mem_ker] at hx
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 (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        (IsLocalization.mk' (M := Submonoid.powers s) (↑Γ(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) (s ^ n) ⋯)) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
⊢ Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
            x :
          (↑Γ(Y, Y.basicOpen s) : Type u)) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
have rw : Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
  ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
        (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
      (HMul.hMul (α := (↑Γ(Y, Y.basicOpen s) : Type u)) (β := (↑Γ(Y, Y.basicOpen s) : Type u))
        ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
            (↑(Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
                  Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x) (s ^ n) sorry) :
              (↑Γ(Y, (↑U : Y.Opens)) : Type u)) :
          (↑Γ(Y, Y.basicOpen s) : Type u))
        (IsLocalization.mk' (M := Submonoid.powers s) (↑Γ(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) (s ^ n) sorry) :
          (↑Γ(Y, Y.basicOpen s) : Type u))) :
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
  (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
Tactic: rw [← IsLocalization.mk'_spec' (M := .powers s), map_mul, hx, mul_zero]
-- 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 (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        (IsLocalization.mk' (M := Submonoid.powers s) (↑Γ(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) (s ^ n) ⋯)) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
rw :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        (HMul.hMul (α := (↑Γ(Y, Y.basicOpen s) : Type u)) (β := (↑Γ(Y, Y.basicOpen s) : Type u))
          ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
              (↑(Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x) (s ^ n)
                    ⋯) :
                (↑Γ(Y, (↑U : Y.Opens)) : Type u)) :
            (↑Γ(Y, Y.basicOpen s) : Type u))
          (IsLocalization.mk' (M := Submonoid.powers s) (↑Γ(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) (s ^ n) ⋯) :
            (↑Γ(Y, Y.basicOpen s) : Type u))) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
⊢ Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
            x :
          (↑Γ(Y, Y.basicOpen s) : Type u)) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
have y : ↥(Submonoid.powers s)
Tactic: rw [← IsLocalization.mk'_spec' (M := .powers s), map_mul, hx, mul_zero]