awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
⊢ autoParam
      (QuasiCompact (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
        (pullback.diagonal (terminal.from X)))
      QuasiSeparated.quasiCompact_diagonal._autoParam ↔
    QuasiCompact (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
have a : Eq (α := X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
  (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
  (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
    X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
Tactic: congr!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
⊢ Eq (α := X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
have a : CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X)) =
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.fst (terminal.from X) (terminal.from X) :
      pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
a :
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X)) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.fst (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)
⊢ Eq (α := X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
have a₁ : CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.diagonal (terminal.from X)) (pullback.snd (terminal.from X) (terminal.from X)) =
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
    (pullback.snd (terminal.from X) (terminal.from X) :
      pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)
Tactic: ext : 1
-- 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} ↥Y
f g : X ⟶ Y
⊢ CompactSpace.{u} ↥(equalizer f g)
have isCompact_univ : IsCompact.{u} (X := ↥(equalizer f g)) Set.univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
i : 𝒰.I₀
⊢ IsAffine.{u} (𝒰.X i)
have dsimp : IsAffine.{u}
  (PreZeroHypercover.X
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (pullback (Y :=
          Z.affineCover.X
            (i.fst (β := fun (i : Z.affineCover.I₀) ↦
              PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
                (Precoverage.ZeroHypercover.toPreZeroHypercover (pullback g (Z.affineCover.f i)).affineCover))))
          g
          (Z.affineCover.f
            (i.fst (β := fun (i : Z.affineCover.I₀) ↦
              PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
                (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (pullback g (Z.affineCover.f i)).affineCover))))).affineCover)
    (i.snd (β := fun (i : Z.affineCover.I₀) ↦
      PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
        (Precoverage.ZeroHypercover.toPreZeroHypercover (pullback g (Z.affineCover.f i)).affineCover))))
Tactic: dsimp [𝒰]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
⊢ QuasiSeparated f
have this : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
Tactic: have (i : _) : IsAffine (𝒰.X i) := by dsimp [𝒰]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
⊢ QuasiSeparated f
have apply : ∀
  (i :
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
          fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover).toPreZeroHypercover.1),
  QuasiSeparatedSpace.{u}
    ↥((Precoverage.ZeroHypercover.pullback₁ f
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
              fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
        i)
Tactic: apply HasAffineProperty.of_openCover
    ((Z.affineCover.pullback₁ g).bind fun x => Scheme.affineCover _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
i : Z.affineCover.I₀
j :
  PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover (pullback g (Z.affineCover.f i)).affineCover)
⊢ QuasiSeparatedSpace.{u}
    ↥((Precoverage.ZeroHypercover.pullback₁ f
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
              fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
        (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
            ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                        (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                      i) :
                  PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
              i))
          i j))
have refine_1 : (Precoverage.ZeroHypercover.pullback₁ f
        ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
          fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
    (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
      PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
        ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
            (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                    (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                      ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                  i) :
              PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
          i))
      i j) ⟶
  pullback (f ≫ g) (Z.affineCover.f i)
Tactic: refine @quasiSeparatedSpace_of_quasiSeparated _ _ ?_
    (HasAffineProperty.of_isPullback (.of_hasPullback _ (Z.affineCover.f i)) ‹_›) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ @QuasiSeparated ≤ MorphismProperty.diagonal @QuasiCompact
have rw : MorphismProperty.diagonal @QuasiCompact ≤ MorphismProperty.diagonal @QuasiCompact
Tactic: rw [quasiSeparated_eq_diagonal_is_quasiCompact]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u_1)
x : (↑Γ(X, X.basicOpen f) : Type u_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
have 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
Tactic: have := (hU.isLocalization_basicOpen f).1.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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
⊢ ∃ (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
have 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) 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),
  ∃ (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) 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 *
        x
Tactic: obtain ⟨⟨y, _, n, rfl⟩, d⟩ := this x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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
⊢ ∃ (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
have 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) 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 *
    x
Tactic: use n, y
-- 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)
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u_1)
have 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))
Tactic: constructor
-- 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)
⊢ 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))
have 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))
Tactic: constructor
-- 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)
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))
⊢ 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))
have 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
Tactic: constructor
-- 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)
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
⊢ 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))
have 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
Tactic: constructor
-- 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)
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))
have toIsLocalizationMap : IsUnit
  (HPow.hPow (α := (↑Γ(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))
        f :
      (↑Γ(X, X.basicOpen f) : Type u_1))
    n)
Tactic: simp only [map_pow, RingHom.algebraMap_toAlgebra]