awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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)
⊢ ∃ (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
have 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) sorry =
      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) sorry)
          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: obtain ⟨n, y, e⟩ := exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated X U hU hU' f z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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
have 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) sorry).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) sorry).1
Tactic: refine ⟨⟨y, _, n, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f 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
have toIsLocalizationMap : Eq (α := (↑Γ(X, X.basicOpen f) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).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: rw [← sub_eq_zero, ← map_sub, RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : (↑Γ(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))
          (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
have toIsLocalizationMap : Eq (α := (↑Γ(X, X.basicOpen f) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).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: simp_rw [← @sub_eq_zero _ _ (_ * x) (_ * y), ← mul_sub]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : (↑Γ(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))
          (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
have toIsLocalizationMap : ∀ (z : (↑Γ(X, U) : Type u_1)),
  Eq (α := (↑Γ(X, X.basicOpen f) : Type u_1))
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).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
Tactic: generalize x - y = z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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))
⊢ ∃ (c : ↥(Submonoid.powers f)), (↑c : (↑Γ(X, U) : Type u_1)) * z = 0
have toIsLocalizationMap : ∀ (n : ℕ) (e : f ^ n * 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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
have 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) sorry) :
      (↑Γ(X, U) : Type u_1)) *
    z =
  0
Tactic: refine ⟨⟨_, n, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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 : ℕ), s ^ n * f = s ^ n * g
have obtain : ∀ (n : ℕ) (hc : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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
⊢ ∃ (n : ℕ), s ^ n * f = 0
have suffices : ∃ (n : ℕ), s ^ n * f = s ^ n * 0
Tactic: suffices h : ∃ n, s ^ n * f = s ^ n * 0 by
    simpa using h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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
⊢ ∃ (n : ℕ), s ^ n * f = s ^ n * 0
have 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) sorry)
  (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
    CommRingCat.carrier) 0 (X.basicOpen s) sorry)
Tactic: apply exists_of_res_eq_of_qcqs hU hU'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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))
have refine : IsIso (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: refine @IsIso.of_isIso_comp_right _ _ _ _ _ _ (X.presheaf.map
    (eqToHom (Scheme.toSpecΓ_preimage_basicOpen _ _).symm).op) _ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : Type u)
⊢ IsIso (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have 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 sorry)))) :
    (a : (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
Tactic: rw [ConcreteCategory.isIso_iff_bijective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥X
f : (↑Γ(X, ⊤) : 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))
have inst : IsLocalization (Submonoid.powers f) (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)
Tactic: apply +allowSynthFailures IsLocalization.bijective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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)
⊢ 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))
have inst₁ : IsLocalization (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)
Tactic: apply +allowSynthFailures IsLocalization.bijective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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)
⊢ 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))
have 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 sorry)))).comp
    (algebraMap (↑Γ(X, ⊤) : Type u) (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)))
  (algebraMap (↑Γ(X, ⊤) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
Tactic: apply +allowSynthFailures IsLocalization.bijective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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))
⊢ 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))
have R : Type u
Tactic: apply +allowSynthFailures IsLocalization.bijective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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
⊢ 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))
have inst₂ : CommSemiring (↑Γ(X, ⊤) : Type u)
Tactic: apply +allowSynthFailures IsLocalization.bijective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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)
⊢ 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))
have M : Submonoid (↑Γ(X, ⊤) : Type u)
Tactic: apply +allowSynthFailures IsLocalization.bijective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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)
⊢ 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))
have inst₃ : Algebra (↑Γ(X, ⊤) : Type u) (↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f) : Type u)
Tactic: apply +allowSynthFailures IsLocalization.bijective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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)
⊢ 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))
have inst₄ : Algebra (↑Γ(X, ⊤) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
Tactic: apply +allowSynthFailures IsLocalization.bijective