awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (z : (↑Γ(X, U) : Type u_1)),
    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))
            z :
          (↑Γ(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)) * z = 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 - y) = 0

Tactic:
generalize x - y = z
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : (↑Γ(X, U) : Type u_1)
H :
  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))
        z :
      (↑Γ(X, X.basicOpen f) : Type u_1))
    (0 : (↑Γ(X, X.basicOpen f) : Type u_1))
toIsLocalizationMap : ∀ (n : ℕ) (e : f ^ n * z = 0), ∃ (c : ↥(Submonoid.powers f)), (↑c : (↑Γ(X, U) : Type u_1)) * z = 0
⊢ ∃ (c : ↥(Submonoid.powers f)), (↑c : (↑Γ(X, U) : Type u_1)) * z = 0

Tactic:
obtain ⟨n, e⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact X hU _ _ H

Premises used: AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : (↑Γ(X, U) : Type u_1)
H :
  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))
        z :
      (↑Γ(X, X.basicOpen f) : Type u_1))
    (0 : (↑Γ(X, X.basicOpen f) : Type u_1))
n : ℕ
e : f ^ n * z = 0
⊢ ∃ (c : ↥(Submonoid.powers f)), (↑c : (↑Γ(X, U) : Type u_1)) * z = 0

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

Premises used: 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 y z : (↑Γ(X, U) : Type u_1)
H :
  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))
        z :
      (↑Γ(X, X.basicOpen f) : Type u_1))
    (0 : (↑Γ(X, X.basicOpen f) : Type u_1))
n : ℕ
e : f ^ n * z = 0
toIsLocalizationMap :
  (↑(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)) *
      z =
    0
⊢ ∃ (c : ↥(Submonoid.powers f)), (↑c : (↑Γ(X, U) : Type u_1)) * z = 0

Tactic:
refine ⟨⟨_, n, rfl⟩, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y z : (↑Γ(X, U) : Type u_1)
H :
  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))
        z :
      (↑Γ(X, X.basicOpen f) : Type u_1))
    (0 : (↑Γ(X, X.basicOpen f) : Type u_1))
n : ℕ
e : f ^ n * z = 0
⊢ (↑(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)) *
      z =
    0

Tactic:
simpa [mul_comm z] using e

Premises used: mul_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f g s : (↑Γ(X, U) : Type u)
hfg :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) f (X.basicOpen s) ⋯)
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) g (X.basicOpen s) ⋯)
obtain : ∀ (n : ℕ) (hc : s ^ n * f = s ^ n * g), ∃ (n : ℕ), s ^ n * f = s ^ n * g
⊢ ∃ (n : ℕ), s ^ n * f = s ^ n * g

Tactic:
obtain ⟨n, hc⟩ := (isLocalization_basicOpen_of_qcqs hU hU' s).exists_of_eq s hfg

Premises used: IsLocalization.Away.exists_of_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f g s : (↑Γ(X, U) : Type u)
hfg :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) f (X.basicOpen s) ⋯)
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) g (X.basicOpen s) ⋯)
n : ℕ
hc : s ^ n * f = s ^ n * g
w : ℕ
h : s ^ n * f = s ^ n * g
⊢ ∃ (n : ℕ), s ^ n * f = s ^ n * g

Tactic:
use n
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f g s : (↑Γ(X, ⊤) : Type u)
hfg :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) f (X.basicOpen s) ⋯)
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) g (X.basicOpen s) ⋯)
⊢ ∃ (n : ℕ), s ^ n * f = s ^ n * g

Tactic:
exists_of_res_eq_of_qcqs (U := ⊤) CompactSpace.isCompact_univ isQuasiSeparated_univ hfg

Premises used: CompactSpace.isCompact_univ, isQuasiSeparated_univ, AlgebraicGeometry.exists_of_res_eq_of_qcqs
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : (↑Γ(X, U) : Type u)
hf :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) f (X.basicOpen s) ⋯)
    0
h : ∃ (n : ℕ), s ^ n * f = s ^ n * 0
⊢ ∃ (n : ℕ), s ^ n * f = 0

Tactic:
simpa using h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : (↑Γ(X, U) : Type u)
hf :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) f (X.basicOpen s) ⋯)
    0
suffices : ∃ (n : ℕ), s ^ n * f = s ^ n * 0
⊢ ∃ (n : ℕ), s ^ n * f = 0

Tactic:
suffices h : ∃ n, s ^ n * f = s ^ n * 0 by
    simpa using h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : (↑Γ(X, U) : Type u)
hf :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) f (X.basicOpen s) ⋯)
    0
apply :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) f (X.basicOpen s) ⋯)
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) 0 (X.basicOpen s) ⋯)
⊢ ∃ (n : ℕ), s ^ n * f = s ^ n * 0

Tactic:
apply exists_of_res_eq_of_qcqs hU hU'

Premises used: AlgebraicGeometry.exists_of_res_eq_of_qcqs
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : (↑Γ(X, U) : Type u)
hf :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) f (X.basicOpen s) ⋯)
    0
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) f (X.basicOpen s) ⋯)
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier) 0 (X.basicOpen s) ⋯)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
inst : CompactSpace.{u_1} ↥X
inst_1 : QuasiSeparatedSpace.{u_1} ↥X
f s : (↑Γ(X, ⊤) : Type u_1)
hf :
  Eq (α :=
    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 s))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) f (X.basicOpen s) ⋯)
    0
⊢ ∃ (n : ℕ), s ^ n * f = 0

Tactic:
exists_of_res_zero_of_qcqs (U := ⊤) CompactSpace.isCompact_univ isQuasiSeparated_univ hf

Premises used: CompactSpace.isCompact_univ, AlgebraicGeometry.exists_of_res_zero_of_qcqs, isQuasiSeparated_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsIso (X := Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f)) (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f))

Tactic:
@IsIso.of_isIso_comp_right _ _ _ _ _ _ (X.presheaf.map
    (eqToHom (Scheme.toSpecΓ_preimage_basicOpen _ _).symm).op) _ ?_

Premises used: Quiver.Hom.op, CategoryTheory.eqToHom, CategoryTheory.IsIso.of_isIso_comp_right, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
refine : IsIso (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ IsIso (X := Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f)) (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f))

Tactic:
refine @IsIso.of_isIso_comp_right _ _ _ _ _ _ (X.presheaf.map
    (eqToHom (Scheme.toSpecΓ_preimage_basicOpen _ _).symm).op) _ ?_

Premises used: Quiver.Hom.op, CategoryTheory.eqToHom, CategoryTheory.IsIso.of_isIso_comp_right, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
rw :
  Function.Bijective (α := (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)) (β :=
    (↑Γ(X, X.basicOpen f) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier)
          (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) :
      (a : (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
⊢ IsIso (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
rw [ConcreteCategory.isIso_iff_bijective]

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
inst_2 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
inst : IsLocalization (Submonoid.powers f) (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)
inst₁ : IsLocalization (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)
hf :
  Eq (α := (↑Γ(X, ⊤) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier)
          (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))).comp
      (algebraMap (↑Γ(X, ⊤) : Type u) (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)))
    (algebraMap (↑Γ(X, ⊤) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
R : Type u
inst₂ : CommSemiring (↑Γ(X, ⊤) : Type u)
M : Submonoid (↑Γ(X, ⊤) : Type u)
inst₃ : Algebra (↑Γ(X, ⊤) : Type u) (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)
inst₄ : Algebra (↑Γ(X, ⊤) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
⊢ Function.Bijective (α := (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)) (β :=
    (↑Γ(X, X.basicOpen f) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier)
          (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) :
      (a : (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))

Tactic:
apply +allowSynthFailures IsLocalization.bijective

Premises used: IsLocalization.bijective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsLocalization (Submonoid.powers f) (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)

Tactic:
StructureSheaf.IsLocalization.to_basicOpen _ _

Premises used: Set.Mem, AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsLocalization (Submonoid.powers f) (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)

Tactic:
exact StructureSheaf.IsLocalization.to_basicOpen _ _

Premises used: AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsLocalization (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
isLocalization_basicOpen_of_qcqs ?_ ?_ _

Premises used: AlgebraicGeometry.isLocalization_basicOpen_of_qcqs
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst_1 : CompactSpace.{u} ↥X
inst_2 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
inst : IsCompact.{u} (X := ↥X) (Opens.carrier ⊤)
inst₁ : IsQuasiSeparated.{u} (α := ↥X) (Opens.carrier ⊤)
⊢ IsLocalization (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
refine isLocalization_basicOpen_of_qcqs ?_ ?_ _

Premises used: AlgebraicGeometry.isLocalization_basicOpen_of_qcqs
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsCompact.{u} (X := ↥X) (Opens.carrier ⊤)

Tactic:
isCompact_univ

Premises used: Set.univ, setOf, isCompact_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsCompact.{u} (X := ↥X) (Opens.carrier ⊤)

Tactic:
exact isCompact_univ

Premises used: isCompact_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsQuasiSeparated.{u} (α := ↥X) (Opens.carrier ⊤)

Tactic:
isQuasiSeparated_univ

Premises used: Set.univ, setOf, isQuasiSeparated_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsQuasiSeparated.{u} (α := ↥X) (Opens.carrier ⊤)

Tactic:
exact isQuasiSeparated_univ

Premises used: isQuasiSeparated_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ Eq (α := (↑Γ(X, ⊤) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier)
          (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))).comp
      (algebraMap (↑Γ(X, ⊤) : Type u) (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)))
    (algebraMap (↑Γ(X, ⊤) : Type u) (↑Γ(X, X.basicOpen f) : Type u))

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, RingHom.algebraMap_toAlgebra,
      ← Functor.map_comp]

Premises used: CommRingCat.hom_comp, CategoryTheory.Functor.map_comp, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
erw :
  P (R := (↑Γ(X, ⊤) : Type u)) (S := (↑Γ(pullback f g, ⊤) : Type u))
    (CommRingCat.Hom.hom
        (Scheme.Hom.appTop
          (CategoryStruct.comp (Y :=
            AffineScheme.forgetToScheme.obj
              (pullback (X := AffineScheme.of X) (Y := AffineScheme.of Y) (Z := AffineScheme.of S)
                (AffineScheme.ofHom f) (AffineScheme.ofHom g)))
            (Iso.inv (PreservesPullback.iso AffineScheme.forgetToScheme (AffineScheme.ofHom f) (AffineScheme.ofHom g)))
            (AffineScheme.forgetToScheme.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))) :
      (↑Γ(X, ⊤) : Type u) →+* (↑Γ(pullback f g, ⊤) : Type u))
⊢ P (S := (↑Γ(pullback f g, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))

Tactic:
erw [← PreservesPullback.iso_inv_fst AffineScheme.forgetToScheme (AffineScheme.ofHom f)
      (AffineScheme.ofHom g)]

Premises used: CategoryTheory.Limits.PreservesPullback.iso_inv_fst, AlgebraicGeometry.AffineScheme.ofHom, AlgebraicGeometry.AffineScheme.forgetToScheme
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
rw :
  P (R := (↑Γ(X, ⊤) : Type u)) (S :=
    (↑Γ(AffineScheme.forgetToScheme.obj (pullback (AffineScheme.ofHom f) (AffineScheme.ofHom g)), ⊤) : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.appTop (InducedCategory.Hom.hom (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)))))
⊢ P (R := (↑Γ(X, ⊤) : Type u)) (S := (↑Γ(pullback f g, ⊤) : Type u))
    (CommRingCat.Hom.hom
        (Scheme.Hom.appTop
          (CategoryStruct.comp (Y :=
            AffineScheme.forgetToScheme.obj
              (pullback (X := AffineScheme.of X) (Y := AffineScheme.of Y) (Z := AffineScheme.of S)
                (AffineScheme.ofHom f) (AffineScheme.ofHom g)))
            (Iso.inv (PreservesPullback.iso AffineScheme.forgetToScheme (AffineScheme.ofHom f) (AffineScheme.ofHom g)))
            (AffineScheme.forgetToScheme.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))) :
      (↑Γ(X, ⊤) : Type u) →+* (↑Γ(pullback f g, ⊤) : Type u))

Tactic:
rw [Scheme.Hom.comp_appTop, CommRingCat.hom_comp, hP'.cancel_right_isIso,
    AffineScheme.forgetToScheme_map]

Premises used: RingHom.RespectsIso.cancel_right_isIso, CommRingCat.hom_comp, AlgebraicGeometry.AffineScheme.forgetToScheme_map, AlgebraicGeometry.Scheme.Hom.comp_appTop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hP' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y S : Scheme
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : IsAffine S
f : X ⟶ S
g : Y ⟶ S
H : P (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
have :
  ∀
    (this :
      Eq (α :=
        Opposite.unop (AffineScheme.Γ.rightOp.obj (AffineScheme.of X)) ⟶
          Opposite.unop
            (AffineScheme.Γ.rightOp.obj
              (pullback (X := AffineScheme.of X) (Y := AffineScheme.of Y) (Z := AffineScheme.of S)
                (AffineScheme.ofHom f) (AffineScheme.ofHom g))))
        (Quiver.Hom.unop
          (CategoryStruct.comp (Y :=
            pullback (X := AffineScheme.Γ.rightOp.obj (AffineScheme.of X)) (Y :=
              AffineScheme.Γ.rightOp.obj (AffineScheme.of Y)) (Z := AffineScheme.Γ.rightOp.obj (AffineScheme.of S))
              (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom f)) (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom g)))
            (Iso.hom (PreservesPullback.iso AffineScheme.Γ.rightOp (AffineScheme.ofHom f) (AffineScheme.ofHom g)))
            (pullback.fst (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom f))
              (AffineScheme.Γ.rightOp.map (AffineScheme.ofHom g)))))
        (Quiver.Hom.unop (AffineScheme.Γ.rightOp.map (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g))))),
    P (R := (↑Γ(X, ⊤) : Type u)) (S :=
      (↑Γ(AffineScheme.forgetToScheme.obj (pullback (AffineScheme.ofHom f) (AffineScheme.ofHom g)), ⊤) : Type u))
      (CommRingCat.Hom.hom
        (Scheme.Hom.appTop (InducedCategory.Hom.hom (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)))))
⊢ P (R := (↑Γ(X, ⊤) : Type u)) (S :=
    (↑Γ(AffineScheme.forgetToScheme.obj (pullback (AffineScheme.ofHom f) (AffineScheme.ofHom g)), ⊤) : Type u))
    (CommRingCat.Hom.hom
      (Scheme.Hom.appTop (InducedCategory.Hom.hom (pullback.fst (AffineScheme.ofHom f) (AffineScheme.ofHom g)))))

Tactic:
have := congr_arg Quiver.Hom.unop
      (PreservesPullback.iso_hom_fst AffineScheme.Γ.rightOp (AffineScheme.ofHom f)
        (AffineScheme.ofHom g))