awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
i :
  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
      (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 X))).I₀
dsimp : IsAffine X
⊢ IsAffine.{u_1}
    ((Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
          (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 X))).X
      i)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
i :
  (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
      (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 X))).I₀
⊢ IsAffine X

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
rw : ∀ {U : TopologicalSpace.Opens ↥X} {x : ↥X}, x ∈ U → ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
⊢ Opens.IsBasis X.affineOpens

Tactic:
rw [Opens.isBasis_iff_nbhd]

Premises used: TopologicalSpace.Opens.isBasis_iff_nbhd
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ (↑U : Set ↥X)
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
⊢ ∃ 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

Premises used: AlgebraicGeometry.Scheme.affineBasisCover_is_basis, TopologicalSpace.Opens.isOpen, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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

Tactic:
⟨⟨S, X.affineBasisCover_is_basis.isOpen hS⟩, ?_, hxS, hSU⟩

Premises used: AlgebraicGeometry.Scheme.affineBasisCover_is_basis, TopologicalSpace.IsTopologicalBasis.isOpen, TopologicalSpace.Opens.mk, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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)
refine : { carrier := S, is_open' := ⋯ : TopologicalSpace.Opens ↥X } ∈ X.affineOpens
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U

Tactic:
refine ⟨⟨S, X.affineBasisCover_is_basis.isOpen hS⟩, ?_, hxS, hSU⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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)
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' := ⋯ :
        TopologicalSpace.Opens ↥X } ∈
      X.affineOpens
⊢ { carrier := S, is_open' := ⋯ : TopologicalSpace.Opens ↥X } ∈ X.affineOpens

Tactic:
rcases hS with ⟨i, rfl⟩

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ (↑U : Set ↥X)
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' := ⋯ :
      TopologicalSpace.Opens ↥X } ∈
    X.affineOpens

Tactic:
isAffineOpen_opensRange _

Premises used: Set.Mem, AlgebraicGeometry.Scheme.Hom.opensRange, AlgebraicGeometry.isAffineOpen_opensRange, setOf, AlgebraicGeometry.IsAffineOpen, AlgebraicGeometry.Scheme.affineOpens
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ (↑U : Set ↥X)
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' := ⋯ :
      TopologicalSpace.Opens ↥X } ∈
    X.affineOpens

Tactic:
exact isAffineOpen_opensRange _

Premises used: AlgebraicGeometry.isAffineOpen_opensRange
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
h : (↑(⨆ (i : (↑X.affineOpens : Type u_1)), (↑i : X.Opens)) : Set ↥X) = (↑⊤ : Set ↥X)
⊢ Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : (↑X.affineOpens : Type u_1)), (↑i : X.Opens)) ⊤

Tactic:
apply Opens.ext

Premises used: TopologicalSpace.Opens.ext
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
h : ⋃ (i : (↑X.affineOpens : Type u_1)), (↑(↑i : X.Opens) : Set ↥X) = (↑⊤ : Set ↥X)
⊢ (↑(⨆ (i : (↑X.affineOpens : Type u_1)), (↑i : X.Opens)) : Set ↥X) = (↑⊤ : Set ↥X)

Tactic:
rw [Opens.coe_iSup]

Premises used: TopologicalSpace.Opens.coe_iSup
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
h : IsTopologicalBasis.{u_1} (α := ↥X) (Set.range fun (i : (↑X.affineOpens : Type u_1)) ↦ (↑(↑i : X.Opens) : Set ↥X))
⊢ ⋃ (i : (↑X.affineOpens : Type u_1)), (↑(↑i : X.Opens) : Set ↥X) = (↑⊤ : Set ↥X)

Tactic:
apply IsTopologicalBasis.sUnion_eq

Premises used: TopologicalSpace.IsTopologicalBasis.sUnion_eq
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
h : IsTopologicalBasis (SetLike.coe '' X.affineOpens)
⊢ IsTopologicalBasis.{u_1} (α := ↥X) (Set.range fun (i : (↑X.affineOpens : Type u_1)) ↦ (↑(↑i : X.Opens) : Set ↥X))

Tactic:
rw [← Set.image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
⊢ IsTopologicalBasis (SetLike.coe '' X.affineOpens)

Tactic:
X.isBasis_affineOpens

Premises used: TopologicalSpace.Opens.IsBasis, AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
⊢ IsTopologicalBasis (SetLike.coe '' X.affineOpens)

Tactic:
exact X.isBasis_affineOpens

Premises used: AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
f : (↑Γ(X, ⊤) : Type u_1)
⊢ X.isoSpec.hom ⁻¹ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f

Tactic:
Scheme.toSpecΓ_preimage_basicOpen _ _

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
⊢ Opens.IsBasis.{u_1} (α := (↑(Scheme.forgetToTop.obj X) : Type u_1))
    {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}

Tactic:
PrimeSpectrum.isBasis_basic_opens.of_isInducing
      (TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)).isInducing

Premises used: Homeomorph.isInducing, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Scheme.forgetToTop, TopologicalSpace.Opens.IsBasis.of_isInducing, TopCat.homeoOfIso, CategoryTheory.Functor.mapIso, PrimeSpectrum.isBasis_basic_opens
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
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' := ⋯ : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) } =
              x}
⊢ Opens.IsBasis (Set.range (ι := (↑Γ(X, ⊤) : Type u_1)) X.basicOpen)

Tactic:
convert!
    PrimeSpectrum.isBasis_basic_opens.of_isInducing
      (TopCat.homeoOfIso (Scheme.forgetToTop.mapIso X.isoSpec)).isInducing using 1

Premises used: Homeomorph.isInducing, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Scheme.forgetToTop, TopologicalSpace.Opens.IsBasis.of_isInducing, TopCat.homeoOfIso, CategoryTheory.Functor.mapIso, PrimeSpectrum.isBasis_basic_opens
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
e_2 : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str
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' := ⋯ : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) } =
                x}
        V
⊢ 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}

Tactic:
ext V
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
e_2 : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str
V : Opens ↥X
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' := ⋯ : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) } :
          Set ↥X) =
        (↑V : Set ↥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

Tactic:
simp only [Set.mem_range, exists_exists_eq_and, Set.mem_setOf,
    ← Opens.coe_inj (V := V), ← Scheme.toSpecΓ_preimage_basicOpen]

Premises used: Set.mem_range, Set.mem_setOf, exists_exists_eq_and, TopologicalSpace.Opens.coe_inj, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
e_2 : X.instTopologicalSpaceCarrierCarrier = (Scheme.forgetToTop.obj X).str
V : Opens ↥X
⊢ (∃ (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' := ⋯ : Opens (↑(Scheme.forgetToTop.obj X) : Type u_1) } :
          Set ↥X) =
        (↑V : Set ↥X)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U V : X.Opens
h : U ≤ V
⊢ ((↑U : Scheme).toSpecΓ ≫ Spec.map U.topIso.inv) ≫ Spec.map (X.presheaf.map (homOfLE h).op) =
    X.homOfLE h ≫ (↑V : Scheme).toSpecΓ ≫ Spec.map V.topIso.inv

Tactic:
simp [← Spec.map_comp, ← X.presheaf.map_comp, toSpecΓ_naturality_assoc]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality_assoc, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
⊢ ((↑U : Scheme).toSpecΓ ≫ Spec.map U.topIso.inv) ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) =
    U.ι ≫ X.toSpecΓ

Tactic:
simp [← Spec.map_comp, ← X.presheaf.map_comp, toSpecΓ_naturality]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
simp :
  Eq (α := (↑⊤ : Scheme) ⟶ Spec Γ(X, ⊤))
    ((↑⊤ : Scheme).toSpecΓ ≫ Spec.map (X.presheaf.map (eqToHom ⋯)) : (↑⊤ : Scheme) ⟶ Spec Γ(X, ⊤))
    ((↑⊤ : Scheme).toSpecΓ ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) : (↑⊤ : Scheme) ⟶ Spec Γ(X, ⊤))
⊢ toSpecΓ ⊤ = ι ⊤ ≫ X.toSpecΓ

Tactic:
simp [Scheme.Opens.toSpecΓ, toSpecΓ_naturality]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.Opens.toSpecΓ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
⊢ Eq (α := (↑⊤ : Scheme) ⟶ Spec Γ(X, ⊤))
    ((↑⊤ : Scheme).toSpecΓ ≫ Spec.map (X.presheaf.map (eqToHom ⋯)) : (↑⊤ : Scheme) ⟶ Spec Γ(X, ⊤))
    ((↑⊤ : Scheme).toSpecΓ ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) : (↑⊤ : Scheme) ⟶ Spec Γ(X, ⊤))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
⊢ Hom.appTop U.toSpecΓ = Iso.hom (ΓSpecIso Γ(X, U)) ≫ U.topIso.inv

Tactic:
simp [Scheme.Opens.toSpecΓ]

Premises used: AlgebraicGeometry.Scheme.Opens.toSpecΓ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (f ⁻¹ᵁ U).toSpecΓ ≫ Spec.map (Hom.app f U) = f ∣_ U ≫ U.toSpecΓ

Tactic:
simp only [toSpecΓ, topIso, Functor.op_obj, Functor.mapIso_inv, Iso.op_inv, eqToIso.inv,
    eqToHom_op, Hom.app_eq_appLE, Category.assoc, ← Spec.map_comp, Hom.appLE_map,
    toSpecΓ_naturality_assoc, TopologicalSpace.Opens.map_top, morphismRestrict_appLE, Hom.map_appLE]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.op_inv, AlgebraicGeometry.Scheme.Opens.topIso, AlgebraicGeometry.Scheme.Opens.toSpecΓ_naturality_assoc, AlgebraicGeometry.morphismRestrict_appLE, CategoryTheory.eqToHom_op, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Spec.map_comp, CategoryTheory.Functor.mapIso_inv, AlgebraicGeometry.Scheme.Opens.toSpecΓ, TopologicalSpace.Opens.map_top, AlgebraicGeometry.Scheme.Hom.map_appLE, AlgebraicGeometry.Scheme.Hom.appLE_map, CategoryTheory.Functor.op_obj, CategoryTheory.eqToIso.inv
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
hUV : V ≤ f ⁻¹ᵁ U
⊢ V.toSpecΓ ≫ Spec.map (Hom.appLE f U V hUV) = Hom.resLE f U V hUV ≫ U.toSpecΓ

Tactic:
simp [Hom.appLE, Hom.resLE]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.Hom.resLE
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.isoSpec.hom = U.toSpecΓ

Tactic:
rfl

Premises used: Quiver.Hom.unop, AlgebraicGeometry.Scheme.Opens.toSpecΓ, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ U.toSpecΓ ≫ hU.isoSpec.inv = 𝟙 (↑U : Scheme)

Tactic:
hU.isoSpec.hom_inv_id

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, Quiver.Hom.unop, CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.isoSpec.inv ≫ U.toSpecΓ = 𝟙 (Spec Γ(X, U))

Tactic:
hU.isoSpec.inv_hom_id

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, CategoryTheory.Iso.inv_hom_id, Quiver.Hom.unop
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
dsimp :
  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))))
⊢ 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))))

Tactic:
dsimp [IsAffineOpen.isoSpec_hom, Scheme.isoSpec_hom, Scheme.toSpecΓ_apply, Scheme.Opens.toSpecΓ,
    TopCat.Presheaf.Γgerm]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Scheme.isoSpec_hom, TopCat.Presheaf.Γgerm, AlgebraicGeometry.Scheme.Opens.toSpecΓ, AlgebraicGeometry.IsAffineOpen.isoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
rw :
  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))))
⊢ 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))))

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]

Premises used: Iff.mpr, trivial, CategoryTheory.Iso.eq_comp_inv, TopCat.Presheaf.germ_res_assoc, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
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))
⊢ 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))))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ 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:
IsLocalRing.comap_closedPoint (U.stalkIso x).inv.hom

Premises used: CommRingCat.Hom.hom, IsLocalRing.comap_closedPoint, AlgebraicGeometry.Scheme.Opens.stalkIso, PrimeSpectrum.comap, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ 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:
exact IsLocalRing.comap_closedPoint (U.stalkIso x).inv.hom

Premises used: CommRingCat.Hom.hom, IsLocalRing.comap_closedPoint, AlgebraicGeometry.Scheme.Opens.stalkIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop hU.isoSpec.hom = Iso.hom (Scheme.ΓSpecIso Γ(X, U)) ≫ U.topIso.inv

Tactic:
simp [isoSpec, Scheme.isoSpec]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, AlgebraicGeometry.Scheme.isoSpec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
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
⊢ Scheme.Hom.appTop hU.isoSpec.inv = U.topIso.hom ≫ Iso.inv (Scheme.ΓSpecIso Γ(X, U))

Tactic:
rw [← cancel_mono hU.isoSpec.hom.appTop, ← Scheme.Hom.comp_appTop, isoSpec_hom_appTop]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, AlgebraicGeometry.Scheme.Hom.appTop, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Hom.comp_appTop, CategoryTheory.Iso.hom, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop