awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ⋯))
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)
⊢ 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:
refine (IsLocalization.mk'_mem_map_algebraMap_iff _ _ _ _ _).mpr ?_

Premises used: Iff.mpr, IsLocalization.mk'_mem_map_algebraMap_iff
-- 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_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
⊢ 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))
      ⋯)
    0

Tactic:
obtain ⟨_, rfl, H⟩ := this

Premises used: rfl
-- 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_1 : ℕ
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_1) ⋯))
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))
      ⋯)
    0
n : ℕ
hn :
  HMul.hMul (β := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      (HPow.hPow (α := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (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))
        n)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (f.app (↑U : Y.Opens)) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
          x :
        (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) =
    0
⊢ 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)
    ((fun (x : ℕ) ↦ s ^ x) n * x)

Tactic:
simpa using hn
-- 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) ⋯))
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 ⋯)
      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)

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⟩
-- 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) ⋯))
⊢ f ⁻¹ᵁ Y.basicOpen s =
    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)

Tactic:
simp
-- 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) ⋯))
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) ⋯)
    0
⊢ ∃ (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

Tactic:
refine ⟨f ⁻¹ᵁ Y.basicOpen s, by simp, ?_⟩
-- 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) ⋯))
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))
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))
⊢ 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))

Tactic:
trans (f.app (Y.basicOpen s)).hom (algebraMap Γ(Y, U) _ x)

Premises used: CommRingCat.Hom.hom, CommRingCat.carrier, Algebra.algebraMap, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.Hom.app, Opposite.op, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, DFunLike.coe, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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) ⋯))
⊢ 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))

Tactic:
simp [-NatTrans.naturality, RingHom.algebraMap_toAlgebra]

Premises used: CategoryTheory.NatTrans.naturality, RingHom.algebraMap_toAlgebra
-- 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) ⋯))
⊢ 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))

Tactic:
simp only [Scheme.affineBasicOpen_coe, RingHom.mem_ker] at hx

Premises used: RingHom.mem_ker, AlgebraicGeometry.Scheme.affineBasicOpen_coe
-- 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) ⋯))
⊢ 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))

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]
-- 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 :
  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))
refine_1 refine_1₁ refine_1₂ 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 ⋯).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) ⋯)
      0
⊢ 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

Tactic:
rwa [f.naturality] at hx

Premises used: AlgebraicGeometry.Scheme.Hom.naturality