awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u_1)
x : (↑Γ(X, X.basicOpen f) : Type u_1)
⊢ ∀ (z : (↑Γ(X, X.basicOpen f) : Type u_1)),
    ∃ (x : (↑Γ(X, U) : Type u_1) × ↥(Submonoid.powers f)),
      HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
          ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
                (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
              (↑x.2 : (↑Γ(X, U) : Type u_1)) :
            (↑Γ(X, X.basicOpen f) : Type u_1)) =
        (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          x.1

Tactic:
have := (hU.isLocalization_basicOpen f).1.2
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u_1)
x : (↑Γ(X, X.basicOpen f) : Type u_1)
this :
  ∀ (z : (↑Γ(X, X.basicOpen f) : Type u_1)),
    ∃ (x : (↑Γ(X, U) : Type u_1) × ↥(Submonoid.powers f)),
      HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
          ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
                (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
              (↑x.2 : (↑Γ(X, U) : Type u_1)) :
            (↑Γ(X, X.basicOpen f) : Type u_1)) =
        (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          x.1
obtain :
  ∀ (y : (↑Γ(X, U) : Type u_1)) (n : ℕ)
    (d :
      HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) x
          ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
                (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
              (↑(y,
                      Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
                        Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x)
                        ((fun (x : ℕ) ↦ f ^ x) n) ⋯).2 :
                (↑Γ(X, U) : Type u_1)) :
            (↑Γ(X, X.basicOpen f) : Type u_1)) =
        (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          (y,
              Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                ⋯).1),
    ∃ (n : ℕ) (y : (↑Γ(X, U) : Type u_1)),
      TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) y (X.basicOpen f) ⋯ =
        HPow.hPow (α :=
            ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.obj (op (X.basicOpen f))))
            (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
              (CC := CommRingCat.carrier) f (X.basicOpen f) ⋯)
            n *
          x
⊢ ∃ (n : ℕ) (y : (↑Γ(X, U) : Type u_1)),
    TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier) y (X.basicOpen f) ⋯ =
      HPow.hPow (α :=
          ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
            (X.presheaf.obj (op (X.basicOpen f))))
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
            (CC := CommRingCat.carrier) f (X.basicOpen f) ⋯)
          n *
        x

Tactic:
obtain ⟨⟨y, _, n, rfl⟩, d⟩ := this x

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u_1)
x : (↑Γ(X, X.basicOpen f) : Type u_1)
this :
  ∀ (z : (↑Γ(X, X.basicOpen f) : Type u_1)),
    ∃ (x : (↑Γ(X, U) : Type u_1) × ↥(Submonoid.powers f)),
      HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
          ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
                (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
              (↑x.2 : (↑Γ(X, U) : Type u_1)) :
            (↑Γ(X, X.basicOpen f) : Type u_1)) =
        (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          x.1
y : (↑Γ(X, U) : Type u_1)
n : ℕ
d :
  HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) x
      ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          (↑(y,
                  Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) n) ⋯).2 :
            (↑Γ(X, U) : Type u_1)) :
        (↑Γ(X, X.basicOpen f) : Type u_1)) =
    (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
        (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
      (y,
          Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
            Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n) ⋯).1
h :
  TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) y (X.basicOpen f) ⋯ =
    HPow.hPow (α :=
        ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
          (X.presheaf.obj (op (X.basicOpen f))))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f (X.basicOpen f) ⋯)
        n *
      x
⊢ ∃ (n : ℕ) (y : (↑Γ(X, U) : Type u_1)),
    TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier) y (X.basicOpen f) ⋯ =
      HPow.hPow (α :=
          ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
            (X.presheaf.obj (op (X.basicOpen f))))
          (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
            (CC := CommRingCat.carrier) f (X.basicOpen f) ⋯)
          n *
        x

Tactic:
use n, y
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u_1)
x : (↑Γ(X, X.basicOpen f) : Type u_1)
this :
  ∀ (z : (↑Γ(X, X.basicOpen f) : Type u_1)),
    ∃ (x : (↑Γ(X, U) : Type u_1) × ↥(Submonoid.powers f)),
      HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
          ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
                (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
              (↑x.2 : (↑Γ(X, U) : Type u_1)) :
            (↑Γ(X, X.basicOpen f) : Type u_1)) =
        (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          x.1
y : (↑Γ(X, U) : Type u_1)
n : ℕ
d :
  HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) x
      ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          (↑(y,
                  Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) n) ⋯).2 :
            (↑Γ(X, U) : Type u_1)) :
        (↑Γ(X, X.basicOpen f) : Type u_1)) =
    (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
        (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
      (y,
          Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
            Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n) ⋯).1
⊢ TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) y (X.basicOpen f) ⋯ =
    HPow.hPow (α :=
        ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
          (X.presheaf.obj (op (X.basicOpen f))))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f (X.basicOpen f) ⋯)
        n *
      x

Tactic:
simpa [mul_comm x] using d.symm

Premises used: mul_comm, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : (↑Γ(X, U) : Type u_1)
toIsLocalizationMap :
  Submonoid.IsLocalizationMap (N := (↑Γ(X, X.basicOpen f) : Type u_1)) (Submonoid.powers f)
    (⇑(algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1)) :
      (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u_1)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : (↑Γ(X, U) : Type u_1)
toIsLocalizationMap :
  ∀ (y : ↥(Submonoid.powers f)),
    IsUnit (M := (↑Γ(X, X.basicOpen f) : Type u_1))
      ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          (↑y : (↑Γ(X, U) : Type u_1)) :
        (↑Γ(X, X.basicOpen f) : Type u_1))
toIsLocalizationMap₁ :
  ∀ (z : (↑Γ(X, X.basicOpen f) : Type u_1)),
    ∃ (x : (↑Γ(X, U) : Type u_1) × ↥(Submonoid.powers f)),
      HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
          ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
                (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
              (↑x.2 : (↑Γ(X, U) : Type u_1)) :
            (↑Γ(X, X.basicOpen f) : Type u_1)) =
        (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          x.1
toIsLocalizationMap₂ :
  ∀ {x y : (↑Γ(X, U) : Type u_1)},
    Eq (α := (↑Γ(X, X.basicOpen f) : Type u_1))
        ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
              (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
            x :
          (↑Γ(X, X.basicOpen f) : Type u_1))
        ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
              (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
            y :
          (↑Γ(X, X.basicOpen f) : Type u_1)) →
      ∃ (c : ↥(Submonoid.powers f)), (↑c : (↑Γ(X, U) : Type u_1)) * x = (↑c : (↑Γ(X, U) : Type u_1)) * y
⊢ Submonoid.IsLocalizationMap (N := (↑Γ(X, X.basicOpen f) : Type u_1)) (Submonoid.powers f)
    (⇑(algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1)) :
      (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : (↑Γ(X, U) : Type u_1)
n : ℕ
toIsLocalizationMap :
  IsUnit
    (HPow.hPow (α := (↑Γ(X, X.basicOpen f) : Type u_1))
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          f :
        (↑Γ(X, X.basicOpen f) : Type u_1))
      n)
⊢ IsUnit (M := (↑Γ(X, X.basicOpen f) : Type u_1))
    ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
          (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
        (↑(Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
              Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
              ⋯) :
          (↑Γ(X, U) : Type u_1)) :
      (↑Γ(X, X.basicOpen f) : Type u_1))

Tactic:
simp only [map_pow, RingHom.algebraMap_toAlgebra]

Premises used: map_pow, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : (↑Γ(X, U) : Type u_1)
n : ℕ
⊢ IsUnit
    (HPow.hPow (α := (↑Γ(X, X.basicOpen f) : Type u_1))
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          f :
        (↑Γ(X, X.basicOpen f) : Type u_1))
      n)

Tactic:
IsUnit.pow _ (RingedSpace.isUnit_res_basicOpen _ f)

Premises used: IsUnit.pow, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : (↑Γ(X, U) : Type u_1)
n : ℕ
⊢ IsUnit
    (HPow.hPow (α := (↑Γ(X, X.basicOpen f) : Type u_1))
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          f :
        (↑Γ(X, X.basicOpen f) : Type u_1))
      n)

Tactic:
exact IsUnit.pow _ (RingedSpace.isUnit_res_basicOpen _ f)

Premises used: IsUnit.pow, AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : (↑Γ(X, U) : Type u_1)
z : (↑Γ(X, X.basicOpen f) : Type u_1)
toIsLocalizationMap :
  ∀ (n : ℕ) (y : (↑Γ(X, U) : Type u_1))
    (e :
      TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) y (X.basicOpen f) ⋯ =
        HPow.hPow (α :=
            ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X.presheaf.obj (op (X.basicOpen f))))
            (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1))
              (CC := CommRingCat.carrier) f (X.basicOpen f) ⋯)
            n *
          z),
    ∃ (x : (↑Γ(X, U) : Type u_1) × ↥(Submonoid.powers f)),
      HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
          ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
                (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
              (↑x.2 : (↑Γ(X, U) : Type u_1)) :
            (↑Γ(X, X.basicOpen f) : Type u_1)) =
        (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          x.1
⊢ ∃ (x : (↑Γ(X, U) : Type u_1) × ↥(Submonoid.powers f)),
    HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
        ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
              (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
            (↑x.2 : (↑Γ(X, U) : Type u_1)) :
          (↑Γ(X, X.basicOpen f) : Type u_1)) =
      (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
          (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
        x.1

Tactic:
obtain ⟨n, y, e⟩ := exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated X U hU hU' f z

Premises used: AlgebraicGeometry.exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : (↑Γ(X, U) : Type u_1)
z : (↑Γ(X, X.basicOpen f) : Type u_1)
n : ℕ
y : (↑Γ(X, U) : Type u_1)
e :
  TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) y (X.basicOpen f) ⋯ =
    HPow.hPow (α :=
        ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
          (X.presheaf.obj (op (X.basicOpen f))))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f (X.basicOpen f) ⋯)
        n *
      z
⊢ ∃ (x : (↑Γ(X, U) : Type u_1) × ↥(Submonoid.powers f)),
    HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
        ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
              (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
            (↑x.2 : (↑Γ(X, U) : Type u_1)) :
          (↑Γ(X, X.basicOpen f) : Type u_1)) =
      (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
          (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
        x.1

Tactic:
⟨⟨y, _, n, rfl⟩, ?_⟩

Premises used: Prod.mk, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : (↑Γ(X, U) : Type u_1)
z : (↑Γ(X, X.basicOpen f) : Type u_1)
n : ℕ
y : (↑Γ(X, U) : Type u_1)
e :
  TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) y (X.basicOpen f) ⋯ =
    HPow.hPow (α :=
        ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
          (X.presheaf.obj (op (X.basicOpen f))))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f (X.basicOpen f) ⋯)
        n *
      z
toIsLocalizationMap :
  HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
      ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          (↑(y,
                  Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) n) ⋯).2 :
            (↑Γ(X, U) : Type u_1)) :
        (↑Γ(X, X.basicOpen f) : Type u_1)) =
    (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
        (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
      (y,
          Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
            Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n) ⋯).1
⊢ ∃ (x : (↑Γ(X, U) : Type u_1) × ↥(Submonoid.powers f)),
    HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
        ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
              (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
            (↑x.2 : (↑Γ(X, U) : Type u_1)) :
          (↑Γ(X, X.basicOpen f) : Type u_1)) =
      (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
          (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
        x.1

Tactic:
refine ⟨⟨y, _, n, rfl⟩, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : (↑Γ(X, U) : Type u_1)
z : (↑Γ(X, X.basicOpen f) : Type u_1)
n : ℕ
y : (↑Γ(X, U) : Type u_1)
e :
  TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) y (X.basicOpen f) ⋯ =
    HPow.hPow (α :=
        ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
          (X.presheaf.obj (op (X.basicOpen f))))
        (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) f (X.basicOpen f) ⋯)
        n *
      z
⊢ HMul.hMul (β := (↑Γ(X, X.basicOpen f) : Type u_1)) z
      ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          (↑(y,
                  Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) n) ⋯).2 :
            (↑Γ(X, U) : Type u_1)) :
        (↑Γ(X, X.basicOpen f) : Type u_1)) =
    (algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
        (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
      (y,
          Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u_1)) ↦
            Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u_1)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n) ⋯).1

Tactic:
simpa only [map_pow, Subtype.coe_mk, RingHom.algebraMap_toAlgebra, mul_comm z] using e.symm

Premises used: Subtype.coe_mk, map_pow, mul_comm, RingHom.algebraMap_toAlgebra, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : (↑Γ(X, U) : Type u_1)
toIsLocalizationMap :
  Eq (α := (↑Γ(X, X.basicOpen f) : Type u_1))
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          (x - y) :
        (↑Γ(X, X.basicOpen f) : Type u_1))
      (0 : (↑Γ(X, X.basicOpen f) : Type u_1)) →
    ∃ (c : ↥(Submonoid.powers f)), (↑c : (↑Γ(X, U) : Type u_1)) * x = (↑c : (↑Γ(X, U) : Type u_1)) * y
⊢ Eq (α := (↑Γ(X, X.basicOpen f) : Type u_1))
      ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          x :
        (↑Γ(X, X.basicOpen f) : Type u_1))
      ((algebraMap (↑Γ(X, U) : Type u_1) (↑Γ(X, X.basicOpen f) : Type u_1) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          y :
        (↑Γ(X, X.basicOpen f) : Type u_1)) →
    ∃ (c : ↥(Submonoid.powers f)), (↑c : (↑Γ(X, U) : Type u_1)) * x = (↑c : (↑Γ(X, U) : Type u_1)) * y

Tactic:
rw [← sub_eq_zero, ← map_sub, RingHom.algebraMap_toAlgebra]

Premises used: map_sub, sub_eq_zero, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : (↑Γ(X, U) : Type u_1)
toIsLocalizationMap :
  Eq (α := (↑Γ(X, X.basicOpen f) : Type u_1))
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          (x - y) :
        (↑Γ(X, X.basicOpen f) : Type u_1))
      (0 : (↑Γ(X, X.basicOpen f) : Type u_1)) →
    ∃ (c : ↥(Submonoid.powers f)), (↑c : (↑Γ(X, U) : Type u_1)) * (x - y) = 0
⊢ Eq (α := (↑Γ(X, X.basicOpen f) : Type u_1))
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
          (x - y) :
        (↑Γ(X, X.basicOpen f) : Type u_1))
      (0 : (↑Γ(X, X.basicOpen f) : Type u_1)) →
    ∃ (c : ↥(Submonoid.powers f)), (↑c : (↑Γ(X, U) : Type u_1)) * x = (↑c : (↑Γ(X, U) : Type u_1)) * y

Tactic:
simp_rw [← @sub_eq_zero _ _ (_ * x) (_ * y), ← mul_sub]

Premises used: mul_sub, sub_eq_zero