awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this : IsIso α
⊢ PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp
have have : ∀ (this : CreatesLimitsOfSize.{v, w, u, u, u + 1, u + 1} Scheme.Spec),
  PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp
Tactic: have := monadicCreatesLimits.{v, w} Scheme.Spec.{u}
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Scheme
inst_1 : ∀ (i : I), IsAffine.{u} (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this_1 : ∀ (i : I), IsIso (α.app i)
this_2 : IsIso α
this : CreatesLimitsOfSize.{v, w, u, u, u + 1, u + 1} Scheme.Spec
⊢ PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp
have suffices : PreservesLimit (D ⋙ Scheme.Γ.rightOp) (Scheme.Spec ⋙ Scheme.Γ.rightOp)
Tactic: suffices PreservesLimit (D ⋙ Scheme.Γ.rightOp) (Scheme.Spec ⋙ Scheme.Γ.rightOp) from
    preservesLimit_comp_of_createsLimit _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
I : Type w
inst : Category.{v, w} I
D : CategoryTheory.Functor.{v, u, w, u + 1} I Schemeᵒᵖ
inst_1 : ∀ (i : I), IsAffine.{u} (unop (D.obj i))
⊢ PreservesColimit D Scheme.Γ
have this : ∀ (i : Iᵒᵖ), IsAffine.{u} (D.leftOp.obj i)
Tactic: have (i : _) : IsAffine (D.leftOp.obj i) := Functor.leftOp_obj D _ ▸ inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
⊢ HasLimits AffineScheme
have this : HasColimitsOfSize.{u, u, u, u + 1} AffineSchemeᵒᵖ
Tactic: haveI := Adjunction.has_colimits_of_equivalence Γ.{u}
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
this : HasColimitsOfSize.{u, u, u, u + 1} AffineSchemeᵒᵖ
⊢ HasLimits AffineScheme
have this₁ : HasLimits.{u, u + 1} AffineSchemeᵒᵖᵒᵖ
Tactic: haveI : HasLimits AffineScheme.{u}ᵒᵖᵒᵖ := Limits.hasLimits_op_of_hasColimits
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
⊢ PreservesLimits forgetToScheme
have apply : PreservesLimitsOfSize.{u_1, u_1, u_1, u_1, u_1 + 1, u_1 + 1}
  ((equivCommRingCat.functor ⋙ equivCommRingCat.inverse) ⋙ forgetToScheme)
Tactic: apply +allowSynthFailures @preservesLimits_of_natIso _ _ _ _ _ _
    (Functor.isoWhiskerRight equivCommRingCat.unitIso forgetToScheme).symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
inst : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen (Scheme.Hom.opensRange f)
have refine : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥(Y.restrict sorry)) ⇑(Y.ofRestrict sorry))
Tactic: refine .of_isIso (IsOpenImmersion.isoOfRangeEq f (Y.ofRestrict _) ?_).inv
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
⊢ IsAffineOpen.{u_1} (X := X) ⊤
have h : ⊤ = Scheme.Hom.opensRange (𝟙 X)
Tactic: convert! isAffineOpen_opensRange (𝟙 X)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
⊢ ⊤ = Scheme.Hom.opensRange (𝟙 X)
have h : (↑⊤ : Set ↥X) = (↑(Scheme.Hom.opensRange (𝟙 X)) : Set ↥X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
x : ↥X
U : X.Opens
hxU : x ∈ U
⊢ ∃ (W : X.Opens), IsAffineOpen W ∧ x ∈ W ∧ W.carrier ⊆ (↑U : Set ↥X)
have obtain : ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ X)
  (hf :
    IsOpenImmersion f ∧
      Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) x ∧ Set.range (ι := ↥(Spec R)) ⇑f ⊆ (↑U : Set ↥X)),
  ∃ (W : X.Opens), IsAffineOpen W ∧ x ∈ W ∧ W.carrier ⊆ (↑U : Set ↥X)
Tactic: obtain ⟨R, f, hf⟩ := AlgebraicGeometry.Scheme.exists_affine_mem_range_and_range_subset hxU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
⊢ Opens.IsBasis X.affineOpens
have rw : ∀ {U : TopologicalSpace.Opens ↥X} {x : ↥X}, x ∈ U → ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
Tactic: rw [Opens.isBasis_iff_nbhd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ (↑U : Set ↥X)
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
have obtain : ∀ (S : Set ↥X)
  (hS :
    Membership.mem (γ := Set (Set ↥X))
      {x : Set ↥X |
        ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
      S)
  (hxS : x ∈ S) (hSU : S ⊆ (↑U : Set ↥X)), ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
Tactic: obtain ⟨S, hS, hxS, hSU⟩ := X.affineBasisCover_is_basis.exists_subset_of_mem_open hU U.isOpen
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ (↑U : Set ↥X)
S : Set ↥X
hS :
  Membership.mem (γ := Set (Set ↥X))
    {x : Set ↥X |
      ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
    S
hxS : x ∈ S
hSU : S ⊆ (↑U : Set ↥X)
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
have refine : { carrier := S, is_open' := sorry : TopologicalSpace.Opens ↥X } ∈ X.affineOpens
Tactic: refine ⟨⟨S, X.affineBasisCover_is_basis.isOpen hS⟩, ?_, hxS, hSU⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ (↑U : Set ↥X)
S : Set ↥X
hS :
  Membership.mem (γ := Set (Set ↥X))
    {x : Set ↥X |
      ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
    S
hxS : x ∈ S
hSU : S ⊆ (↑U : Set ↥X)
⊢ { carrier := S, is_open' := ⋯ : TopologicalSpace.Opens ↥X } ∈ X.affineOpens
have rcases : ∀ (i : X.affineBasisCover.I₀)
  (hxS : Membership.mem (γ := Set ↥X) (Set.range (ι := ↥(X.affineBasisCover.X i)) ⇑(X.affineBasisCover.f i)) x)
  (hSU : Set.range (ι := ↥(X.affineBasisCover.X i)) ⇑(X.affineBasisCover.f i) ⊆ (↑U : Set ↥X)),
  { carrier := Set.range (ι := ↥(X.affineBasisCover.X i)) ⇑(X.affineBasisCover.f i), is_open' := sorry :
      TopologicalSpace.Opens ↥X } ∈
    X.affineOpens
Tactic: rcases hS with ⟨i, rfl⟩
Cleared hypotheses: S, hS, hxS, hSU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
⊢ Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : (↑X.affineOpens : Type u_1)), (↑i : X.Opens)) ⊤
have h : (↑(⨆ (i : (↑X.affineOpens : Type u_1)), (↑i : X.Opens)) : Set ↥X) = (↑⊤ : Set ↥X)
Tactic: apply Opens.ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
⊢ (↑(⨆ (i : (↑X.affineOpens : Type u_1)), (↑i : X.Opens)) : Set ↥X) = (↑⊤ : Set ↥X)
have h : ⋃ (i : (↑X.affineOpens : Type u_1)), (↑(↑i : X.Opens) : Set ↥X) = (↑⊤ : Set ↥X)
Tactic: rw [Opens.coe_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
⊢ ⋃ (i : (↑X.affineOpens : Type u_1)), (↑(↑i : X.Opens) : Set ↥X) = (↑⊤ : Set ↥X)
have h : IsTopologicalBasis.{u_1} (α := ↥X) (Set.range fun (i : (↑X.affineOpens : Type u_1)) ↦ (↑(↑i : X.Opens) : Set ↥X))
Tactic: apply IsTopologicalBasis.sUnion_eq
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
⊢ IsTopologicalBasis.{u_1} (α := ↥X) (Set.range fun (i : (↑X.affineOpens : Type u_1)) ↦ (↑(↑i : X.Opens) : Set ↥X))
have h : IsTopologicalBasis (SetLike.coe '' X.affineOpens)
Tactic: rw [← Set.image_eq_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
⊢ Opens.IsBasis (Set.range (ι := (↑Γ(X, ⊤) : Type u_1)) X.basicOpen)
have h : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str →
  Set.range (ι := (↑Γ(X, ⊤) : Type u_1)) X.basicOpen =
    {x : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) |
      ∃ (U : Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1))),
        Membership.mem (γ := Set (Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1)))) (Set.range PrimeSpectrum.basicOpen) U ∧
          {
              carrier :=
                (⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) :
                    (a : (↑(Scheme.forgetToTop.obj X) : Type u_1)) →
                      (↑(Scheme.forgetToTop.obj (Spec Γ(X, ⊤))) : Type u_1)) ⁻¹'
                  (↑U : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1))),
              is_open' := sorry : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) } =
            x}
Tactic: convert!
    PrimeSpectrum.isBasis_basic_opens.of_isInducing
      (TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)).isInducing using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
e_2 : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str
⊢ Set.range (ι := (↑Γ(X, ⊤) : Type u_1)) X.basicOpen =
    {x : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) |
      ∃ (U : Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1))),
        Membership.mem (γ := Set (Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1)))) (Set.range PrimeSpectrum.basicOpen) U ∧
          {
              carrier :=
                (⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) :
                    (a : (↑(Scheme.forgetToTop.obj X) : Type u_1)) →
                      (↑(Scheme.forgetToTop.obj (Spec Γ(X, ⊤))) : Type u_1)) ⁻¹'
                  (↑U : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1))),
              is_open' := ⋯ : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) } =
            x}
have h : ∀ (V : Opens ↥X),
  V ∈ Set.range (ι := (↑Γ(X, ⊤) : Type u_1)) X.basicOpen ↔
    Membership.mem (γ := Set (Opens ↥X))
      {x : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) |
        ∃ (U : Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1))),
          Membership.mem (γ := Set (Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1)))) (Set.range PrimeSpectrum.basicOpen)
              U ∧
            {
                carrier :=
                  (⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) :
                      (a : (↑(Scheme.forgetToTop.obj X) : Type u_1)) →
                        (↑(Scheme.forgetToTop.obj (Spec Γ(X, ⊤))) : Type u_1)) ⁻¹'
                    (↑U : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1))),
                is_open' := sorry : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) } =
              x}
      V
Tactic: ext V
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
e_2 : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str
V : Opens ↥X
⊢ V ∈ Set.range (ι := (↑Γ(X, ⊤) : Type u_1)) X.basicOpen ↔
    Membership.mem (γ := Set (Opens ↥X))
      {x : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) |
        ∃ (U : Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1))),
          Membership.mem (γ := Set (Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1)))) (Set.range PrimeSpectrum.basicOpen)
              U ∧
            {
                carrier :=
                  (⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) :
                      (a : (↑(Scheme.forgetToTop.obj X) : Type u_1)) →
                        (↑(Scheme.forgetToTop.obj (Spec Γ(X, ⊤))) : Type u_1)) ⁻¹'
                    (↑U : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1))),
                is_open' := ⋯ : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) } =
              x}
      V
have h : (∃ (y : (↑Γ(X, ⊤) : Type u_1)), (↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen y) : Set ↥X) = (↑V : Set ↥X)) ↔
  ∃ (a : (↑Γ(X, ⊤) : Type u_1)),
    (↑{
            carrier :=
              (⇑(TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)) :
                  (a : (↑(Scheme.forgetToTop.obj X) : Type u_1)) →
                    (↑(Scheme.forgetToTop.obj (Spec Γ(X, ⊤))) : Type u_1)) ⁻¹'
                (↑(PrimeSpectrum.basicOpen a) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u_1))),
            is_open' := sorry : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) } :
        Set ↥X) =
      (↑V : Set ↥X)
Tactic: simp only [Set.mem_range, exists_exists_eq_and, Set.mem_setOf,
    ← Opens.coe_inj (V := V), ← Scheme.toSpecΓ_preimage_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
⊢ toSpecΓ ⊤ = ι ⊤ ≫ X.toSpecΓ
have simp : Eq (α := (↑⊤ : Scheme) ⟶ Spec Γ(X, ⊤))
  ((↑⊤ : Scheme).toSpecΓ ≫ Spec.map (X.presheaf.map (eqToHom sorry)) : (↑⊤ : Scheme) ⟶ Spec Γ(X, ⊤))
  ((↑⊤ : Scheme).toSpecΓ ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) : (↑⊤ : Scheme) ⟶ Spec Γ(X, ⊤))
Tactic: simp [Scheme.Opens.toSpecΓ, toSpecΓ_naturality]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ Eq (α := ↥(Spec Γ(X, U))) (hU.isoSpec.hom x : ↥(Spec Γ(X, U)))
    ((Spec.map (X.presheaf.germ U (↑x : ↥X) ⋯)) (closedPoint (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) :
      ↥(Spec (X.presheaf.obj (op U))))
have dsimp : Eq (α := ↥(Spec Γ(X, U)))
  ((TopCat.Hom.hom (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))).base :
        (a : ↥(Spec Γ((↑U : Scheme), ⊤))) → ↥(Spec Γ(X, U)))
      ((Spec.map ((↑U : Scheme).presheaf.germ ⊤ x True.intro))
        (closedPoint (↑((↑U : Scheme).presheaf.stalk x) : Type u))) :
    ↥(Spec Γ(X, U)))
  ((Spec.map (X.presheaf.germ U (↑x : ↥X) sorry)) (closedPoint (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) :
    ↥(Spec (X.presheaf.obj (op U))))
Tactic: dsimp [IsAffineOpen.isoSpec_hom, Scheme.isoSpec_hom, Scheme.toSpecΓ_apply, Scheme.Opens.toSpecΓ,
    TopCat.Presheaf.Γgerm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ Eq (α := ↥(Spec Γ(X, U)))
    ((TopCat.Hom.hom (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))).base :
          (a : ↥(Spec Γ((↑U : Scheme), ⊤))) → ↥(Spec Γ(X, U)))
        ((Spec.map ((↑U : Scheme).presheaf.germ ⊤ x True.intro))
          (closedPoint (↑((↑U : Scheme).presheaf.stalk x) : Type u))) :
      ↥(Spec Γ(X, U)))
    ((Spec.map (X.presheaf.germ U (↑x : ↥X) ⋯)) (closedPoint (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) :
      ↥(Spec (X.presheaf.obj (op U))))
have rw : Eq (α := ↥(Spec Γ(X, U)))
  ((Spec.map (X.presheaf.germ U (↑x : ↥X) sorry))
      ((Spec.map (U.stalkIso x).inv) (closedPoint (↑((↑U : Scheme).presheaf.stalk x) : Type u))) :
    ↥(Spec Γ(X, U)))
  ((Spec.map (X.presheaf.germ U (↑x : ↥X) sorry)) (closedPoint (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) :
    ↥(Spec (X.presheaf.obj (op U))))
Tactic: rw [← Scheme.Hom.comp_apply, ← Spec.map_comp,
    (Iso.eq_comp_inv _).mpr (Scheme.Opens.germ_stalkIso_hom U (V := ⊤) x trivial),
    X.presheaf.germ_res_assoc, Spec.map_comp, Scheme.Hom.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ Eq (α := ↥(Spec Γ(X, U)))
    ((Spec.map (X.presheaf.germ U (↑x : ↥X) ⋯))
        ((Spec.map (U.stalkIso x).inv) (closedPoint (↑((↑U : Scheme).presheaf.stalk x) : Type u))) :
      ↥(Spec Γ(X, U)))
    ((Spec.map (X.presheaf.germ U (↑x : ↥X) ⋯)) (closedPoint (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) :
      ↥(Spec (X.presheaf.obj (op U))))
have h : Eq (α := ↥(Spec (X.presheaf.stalk (↑x : ↥X))))
  ((Spec.map (U.stalkIso x).inv) (closedPoint (↑((↑U : Scheme).presheaf.stalk x) : Type u)) :
    ↥(Spec (X.presheaf.stalk (↑x : ↥X))))
  (closedPoint (↑(X.presheaf.stalk (↑x : ↥X)) : Type u) : PrimeSpectrum (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop hU.isoSpec.inv = U.topIso.hom ≫ Iso.inv (Scheme.ΓSpecIso Γ(X, U))
have rw : Scheme.Hom.appTop (hU.isoSpec.hom ≫ hU.isoSpec.inv) =
  (U.topIso.hom ≫ Iso.inv (Scheme.ΓSpecIso Γ(X, U))) ≫ Iso.hom (Scheme.ΓSpecIso Γ(X, U)) ≫ U.topIso.inv
Tactic: rw [← cancel_mono hU.isoSpec.hom.appTop, ← Scheme.Hom.comp_appTop, isoSpec_hom_appTop]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop (hU.isoSpec.hom ≫ hU.isoSpec.inv) =
    (U.topIso.hom ≫ Iso.inv (Scheme.ΓSpecIso Γ(X, U))) ≫ Iso.hom (Scheme.ΓSpecIso Γ(X, U)) ≫ U.topIso.inv
have simp : 𝟙 Γ((↑U : Scheme), ⊤) = 𝟙 (X.presheaf.obj (op (sorry.functor.obj ⊤)))
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range (ι := ↥(Spec Γ(X, U))) ⇑(hU.isoSpec.inv ≫ U.ι) = (↑U : Set ↥X)
have dsimp : Set.range (ι := ↥(Spec Γ(X, U)))
    (Function.comp (β := ↥(↑U : Scheme)) (⇑(TopCat.Hom.hom U.ι.base) : (a : ↥(↑U : Scheme)) → ↥X)
      (Function.comp (β := ↥(Spec Γ((↑U : Scheme), ⊤)))
        (⇑(TopCat.Hom.hom
              (PresheafedSpace.Hom.base
                (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (Iso.inv (↑U : Scheme).isoSpec))))) :
          (a : ↥(Spec Γ((↑U : Scheme), ⊤))) → ↥(↑U : Scheme))
        (⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))).base) :
          (a : ↥(Spec Γ(X, U))) → ↥(Spec Γ((↑U : Scheme), ⊤))))) =
  (↑U : Set ↥X)
Tactic: dsimp [IsAffineOpen.isoSpec_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range (ι := ↥(Spec Γ(X, U)))
      (Function.comp (β := ↥(↑U : Scheme)) (⇑(TopCat.Hom.hom U.ι.base) : (a : ↥(↑U : Scheme)) → ↥X)
        (Function.comp (β := ↥(Spec Γ((↑U : Scheme), ⊤)))
          (⇑(TopCat.Hom.hom
                (PresheafedSpace.Hom.base
                  (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (Iso.inv (↑U : Scheme).isoSpec))))) :
            (a : ↥(Spec Γ((↑U : Scheme), ⊤))) → ↥(↑U : Scheme))
          (⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))).base) :
            (a : ↥(Spec Γ(X, U))) → ↥(Spec Γ((↑U : Scheme), ⊤))))) =
    (↑U : Set ↥X)
have rw : Set.range (ι := ↥(↑U : Scheme)) (⇑(TopCat.Hom.hom U.ι.base) : (a : ↥(↑U : Scheme)) → ↥X) = (↑U : Set ↥X)
Tactic: rw [Set.range_comp, Set.range_eq_univ.mpr, Set.image_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
rw : Set.range (ι := ↥(↑U : Scheme)) (⇑(TopCat.Hom.hom U.ι.base) : (a : ↥(↑U : Scheme)) → ↥X) = (↑U : Set ↥X)
⊢ Set.range (ι := ↥(Spec Γ(X, U)))
      (Function.comp (β := ↥(↑U : Scheme)) (⇑(TopCat.Hom.hom U.ι.base) : (a : ↥(↑U : Scheme)) → ↥X)
        (Function.comp (β := ↥(Spec Γ((↑U : Scheme), ⊤)))
          (⇑(TopCat.Hom.hom
                (PresheafedSpace.Hom.base
                  (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (Iso.inv (↑U : Scheme).isoSpec))))) :
            (a : ↥(Spec Γ((↑U : Scheme), ⊤))) → ↥(↑U : Scheme))
          (⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))).base) :
            (a : ↥(Spec Γ(X, U))) → ↥(Spec Γ((↑U : Scheme), ⊤))))) =
    (↑U : Set ↥X)
have rw₁ : Function.Surjective.{u + 1, u + 1} (α := ↥(Spec Γ(X, U))) (β := ↥(↑U : Scheme))
  (Function.comp (β := ↥(Spec Γ((↑U : Scheme), ⊤)))
    (⇑(TopCat.Hom.hom
          (PresheafedSpace.Hom.base
            (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (Iso.inv (↑U : Scheme).isoSpec))))) :
      (a : ↥(Spec Γ((↑U : Scheme), ⊤))) → ↥(↑U : Scheme))
    (⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))).base) :
      (a : ↥(Spec Γ(X, U))) → ↥(Spec Γ((↑U : Scheme), ⊤))))
Tactic: rw [Set.range_comp, Set.range_eq_univ.mpr, Set.image_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective.{u + 1, u + 1} (α := ↥(Spec Γ(X, U))) (β := ↥(↑U : Scheme))
    (Function.comp (β := ↥(Spec Γ((↑U : Scheme), ⊤)))
      (⇑(TopCat.Hom.hom
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (Iso.inv (↑U : Scheme).isoSpec))))) :
        (a : ↥(Spec Γ((↑U : Scheme), ⊤))) → ↥(↑U : Scheme))
      (⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))).base) :
        (a : ↥(Spec Γ(X, U))) → ↥(Spec Γ((↑U : Scheme), ⊤))))
have rw : Epi (Y := (↑(↑U : Scheme).toPresheafedSpace : TopCat))
  ((Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))).base ≫
    PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (Iso.inv (↑U : Scheme).isoSpec))))
Tactic: rw [← TopCat.coe_comp, ← TopCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.fromSpec ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have rw : (hU.isoSpec.inv ≫ U.ι) ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: rw [fromSpec, Category.assoc, ← Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top,
    isoSpec_inv_toSpecΓ_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
rw : (hU.isoSpec.inv ≫ U.ι) ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ hU.fromSpec ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have rw₁ : hU.isoSpec.inv ≫ U.ι ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: rw [fromSpec, Category.assoc, ← Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top,
    isoSpec_inv_toSpecΓ_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
rw : (hU.isoSpec.inv ≫ U.ι) ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
rw₁ : hU.isoSpec.inv ≫ U.ι ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ hU.fromSpec ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have rw₂ : hU.isoSpec.inv ≫ U.toSpecΓ ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) =
  Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: rw [fromSpec, Category.assoc, ← Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top,
    isoSpec_inv_toSpecΓ_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
rw : (hU.isoSpec.inv ≫ U.ι) ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
rw₁ : hU.isoSpec.inv ≫ U.ι ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
rw₂ :
  hU.isoSpec.inv ≫ U.toSpecΓ ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) =
    Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ hU.fromSpec ≫ X.toSpecΓ = Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have rw₃ : Eq (α := Spec Γ(X, U) ⟶ Spec Γ(X, ⊤)) (Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))))
  (Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))))
Tactic: rw [fromSpec, Category.assoc, ← Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top,
    isoSpec_inv_toSpecΓ_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec
have this : IsAffine.{u} (↑U : Scheme)
Tactic: have : IsAffine U := hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this : IsAffine.{u} (↑U : Scheme)
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec
have this₁ : IsAffine.{u} (↑V : Scheme)
Tactic: haveI : IsAffine _ := hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑V : Scheme)
| hV.fromSpec
have rw : Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (eqToHom sorry))) ≫ Iso.inv (↑U : Scheme).isoSpec ≫ U.ι
Tactic: rw [fromSpec, ← X.homOfLE_ι (V := U) f.unop.le, isoSpec_inv, Category.assoc,
      ← Scheme.isoSpec_inv_naturality_assoc,
      ← Spec.map_comp_assoc, Scheme.homOfLE_appTop, ← Functor.map_comp]