awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
simp : 𝟙 Γ((↑U : Scheme), ⊤) = 𝟙 (X.presheaf.obj (op (⋯.functor.obj ⊤)))
⊢ 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:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ 𝟙 Γ((↑U : Scheme), ⊤) = 𝟙 (X.presheaf.obj (op (⋯.functor.obj ⊤)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ IsOpenImmersion (hU.isoSpec.inv ≫ U.ι)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.isoSpec.inv ≫ U.ι = hU.fromSpec

Tactic:
rfl

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpec, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ U.toSpecΓ ≫ hU.fromSpec = U.ι

Tactic:
toSpecΓ_isoSpec_inv_assoc _ _

Premises used: AlgebraicGeometry.IsAffineOpen.toSpecΓ_isoSpec_inv_assoc
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
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 ⋯)))).base) :
            (a : ↥(Spec Γ(X, U))) → ↥(Spec Γ((↑U : Scheme), ⊤))))) =
    (↑U : Set ↥X)
⊢ Set.range (ι := ↥(Spec Γ(X, U))) ⇑(hU.isoSpec.inv ≫ U.ι) = (↑U : Set ↥X)

Tactic:
dsimp [IsAffineOpen.isoSpec_inv]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec_inv
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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)
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 ⋯)))).base) :
        (a : ↥(Spec Γ(X, U))) → ↥(Spec Γ((↑U : Scheme), ⊤))))
⊢ 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)

Tactic:
rw [Set.range_comp, Set.range_eq_univ.mpr, Set.image_univ]

Premises used: Iff.mpr, Set.range_eq_univ, Set.range_comp, Set.image_univ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range (ι := ↥(↑U : Scheme)) (⇑(TopCat.Hom.hom U.ι.base) : (a : ↥(↑U : Scheme)) → ↥X) = (↑U : Set ↥X)

Tactic:
Subtype.range_coe

Premises used: Subtype.range_coe
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range (ι := ↥(↑U : Scheme)) (⇑(TopCat.Hom.hom U.ι.base) : (a : ↥(↑U : Scheme)) → ↥X) = (↑U : Set ↥X)

Tactic:
exact Subtype.range_coe

Premises used: Subtype.range_coe
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
rw :
  Epi (Y := (↑(↑U : Scheme).toPresheafedSpace : TopCat))
    ((Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))).base ≫
      PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (Iso.inv (↑U : Scheme).isoSpec))))
⊢ 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), ⊤))))

Tactic:
rw [← TopCat.coe_comp, ← TopCat.epi_iff_surjective]

Premises used: TopCat.epi_iff_surjective, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Epi (Y := (↑(↑U : Scheme).toPresheafedSpace : TopCat))
    ((Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))).base ≫
      PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' (Iso.inv (↑U : Scheme).isoSpec))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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 ⋯)))
rw₃ rw₄ :
  Eq (α := Spec Γ(X, U) ⟶ Spec Γ(X, ⊤)) (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 ⋯)))

Tactic:
rw [fromSpec, Category.assoc, ← Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top,
    isoSpec_inv_toSpecΓ_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top, AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_toSpecΓ_assoc
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.opensRange hU.fromSpec = U

Tactic:
Opens.ext (range_fromSpec hU)

Premises used: TopologicalSpace.Opens.ext, AlgebraicGeometry.IsAffineOpen.range_fromSpec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
⊢ IsAffine.{u} (↑U : Scheme)

Tactic:
have : IsAffine U := hU
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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)
⊢ IsAffine.{u} (↑V : Scheme)

Tactic:
haveI : IsAffine _ := hV
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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)
rw :
  Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯))) ≫
    Iso.inv (↑U : Scheme).isoSpec ≫ U.ι
| hV.fromSpec

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]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.le, AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, Quiver.Hom.unop, AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.Spec.map_comp_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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)
conv_rhs :
  Spec.map (X.presheaf.map f) ≫ hU.fromSpec =
    Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯))) ≫
      Iso.inv (↑U : Scheme).isoSpec ≫ U.ι
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec

Tactic:
conv_rhs =>
    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]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.le, AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, Quiver.Hom.unop, AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.Scheme.homOfLE_appTop, AlgebraicGeometry.Scheme.isoSpec_inv_naturality_assoc, AlgebraicGeometry.Spec.map_comp_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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)
rw :
  Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯) ≫ f)) ≫ Iso.inv (↑U : Scheme).isoSpec ≫ U.ι =
    Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯))) ≫
      Iso.inv (↑U : Scheme).isoSpec ≫ U.ι
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec =
    Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯))) ≫
      Iso.inv (↑U : Scheme).isoSpec ≫ U.ι

Tactic:
rw [fromSpec, isoSpec_inv, Category.assoc, ← Spec.map_comp_assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.Spec.map_comp_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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)
⊢ Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯) ≫ f)) ≫ Iso.inv (↑U : Scheme).isoSpec ≫ U.ι =
    Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯))) ≫
      Iso.inv (↑U : Scheme).isoSpec ≫ U.ι

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
⊢ IsAffine.{u} (↑U : Scheme)

Tactic:
have : IsAffine U := hU
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine.{u} (↑U : Scheme)
simp :
  Spec.map (Scheme.Hom.appLE f U V i) ≫
      Spec.map (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫ Iso.inv (↑U : Scheme).isoSpec ≫ U.ι =
    Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫ Iso.inv (↑V : Scheme).isoSpec ≫ V.ι ≫ f
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f

Tactic:
simp only [IsAffineOpen.fromSpec, Category.assoc, isoSpec_inv]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_inv, AlgebraicGeometry.IsAffineOpen.fromSpec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine.{u} (↑U : Scheme)
simp_rw :
  Spec.map (Scheme.Hom.appLE f U V i) ≫
      Spec.map (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫ Iso.inv (↑U : Scheme).isoSpec ≫ U.ι =
    Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫
      Iso.inv (↑V : Scheme).isoSpec ≫ (X.homOfLE i ≫ (f ⁻¹ᵁ U).ι) ≫ f
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫
      Spec.map (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫ Iso.inv (↑U : Scheme).isoSpec ≫ U.ι =
    Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫ Iso.inv (↑V : Scheme).isoSpec ≫ V.ι ≫ f

Tactic:
simp_rw [← Scheme.homOfLE_ι _ i]

Premises used: AlgebraicGeometry.Scheme.homOfLE_ι
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
rw : Scheme.Opens.ι ⊤ = ⋯.isoSpec.hom ≫ X.isoSpec.inv
⊢ ⋯.fromSpec = X.isoSpec.inv

Tactic:
rw [fromSpec, Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq, AlgebraicGeometry.IsAffineOpen.fromSpec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
⊢ Scheme.Opens.ι ⊤ = ⋯.isoSpec.hom ≫ X.isoSpec.inv

Tactic:
simp [isoSpec_hom]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
⊢ U.ι ⁻¹ᵁ V = ⊤

Tactic:
have : U.ι ⁻¹ᵁ V = ⊤ := eq_top_iff.mpr fun x _ ↦ h x.2
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
rw :
  Eq (α := Γ(X, V) ⟶ Γ(Spec Γ(X, U), (hU.isoSpec.inv ≫ U.ι) ⁻¹ᵁ V))
    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
      (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫
        (U.topIso.hom ≫ Iso.inv (Scheme.ΓSpecIso Γ(X, U))) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (homOfLE h).op ≫
      Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫
      Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
rw [IsAffineOpen.fromSpec, Scheme.Hom.comp_app, Scheme.Opens.ι_app, Scheme.Hom.app_eq _ this,
    ← Scheme.Hom.appTop, IsAffineOpen.isoSpec_inv_appTop]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.Hom.appTop, AlgebraicGeometry.Scheme.Hom.app_eq, AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.Scheme.Opens.ι_app
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
simp :
  Eq (α := Γ(X, V) ⟶ Γ(Spec Γ(X, U), (hU.isoSpec.inv ≫ U.ι) ⁻¹ᵁ V))
    (X.presheaf.map
        (Quiver.Hom.op (homOfLE ⋯) ≫
          ((Scheme.Hom.opensFunctor U.ι).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))).op ≫
            Quiver.Hom.op (eqToHom ⋯)) ≫
      Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (homOfLE h).op ≫
      Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ Eq (α := Γ(X, V) ⟶ Γ(Spec Γ(X, U), (hU.isoSpec.inv ≫ U.ι) ⁻¹ᵁ V))
    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
      (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫
        (U.topIso.hom ≫ Iso.inv (Scheme.ΓSpecIso Γ(X, U))) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (homOfLE h).op ≫
      Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp only [Scheme.Opens.toScheme_presheaf_map, Scheme.Opens.topIso_hom,
    Category.assoc, ← X.presheaf.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.Functor.map_comp_assoc, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.Opens.topIso_hom, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ Eq (α := Γ(X, V) ⟶ Γ(Spec Γ(X, U), (hU.isoSpec.inv ≫ U.ι) ⁻¹ᵁ V))
    (X.presheaf.map
        (Quiver.Hom.op (homOfLE ⋯) ≫
          ((Scheme.Hom.opensFunctor U.ι).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom ⋯)))).op ≫
            Quiver.Hom.op (eqToHom ⋯)) ≫
      Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (homOfLE h).op ≫
      Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Continuous (X := ↥(Spec Γ(X, U))) (Y := ↥X) ⇑hU.fromSpec

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
h : (↑U : Set ↥X) = Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) Set.univ
⊢ IsCompact (↑U : Set ↥X)

Tactic:
convert! @IsCompact.image _ _ _ _ Set.univ hU.fromSpec PrimeSpectrum.compactSpace.1 (by fun_prop)

Premises used: CompactSpace.isCompact_univ, IsCompact.image
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ (↑U : Set ↥X) = Set.range (ι := ↥(Spec Γ(X, U))) ⇑hU.fromSpec

Tactic:
hU.range_fromSpec.symm

Premises used: AlgebraicGeometry.IsAffineOpen.range_fromSpec, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
h :
  Eq (α := Set ↥X) (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) Set.univ)
    (Set.range (ι := ↥(Spec Γ(X, U))) ⇑hU.fromSpec)
⊢ (↑U : Set ↥X) = Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) Set.univ

Tactic:
convert! hU.range_fromSpec.symm

Premises used: AlgebraicGeometry.IsAffineOpen.range_fromSpec, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Eq (α := Set ↥X) (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) Set.univ)
    (Set.range (ι := ↥(Spec Γ(X, U))) ⇑hU.fromSpec)

Tactic:
Set.image_univ

Premises used: Set.image_univ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Eq (α := Set ↥X) (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) Set.univ)
    (Set.range (ι := ↥(Spec Γ(X, U))) ⇑hU.fromSpec)

Tactic:
exact Set.image_univ

Premises used: Set.image_univ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥(↑U : Scheme)) ⇑(U.ι ≫ f)) (Set.range (ι := ↥(↑(f ''ᵁ U) : Scheme)) ⇑(f ''ᵁ U).ι)

Tactic:
simp [Scheme.Hom.comp_base, Set.range_comp]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Hom.comp_base
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : X ⟶ Y
H : IsOpenImmersion f
rwa rwa₁ rwa₂ rwa₃ : IsAffineOpen U
⊢ IsAffineOpen (f ''ᵁ U)

Tactic:
rwa [f.isAffineOpen_iff_of_isOpenImmersion]

Premises used: AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst : IsIso f
⊢ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
haveI : IsAffine _ := hU
  .of_isIso (f ∣_ U)

Premises used: AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.IsAffineOpen, AlgebraicGeometry.morphismRestrict
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst : IsOpenImmersion f
hU' : U ≤ Scheme.Hom.opensRange f
rwa : IsAffineOpen (f ''ᵁ f ⁻¹ᵁ U)
rwa₁ : IsAffineOpen (Scheme.Hom.opensRange f ⊓ U)
rwa₂ rwa₃ rwa₄ rwa₅ : IsAffineOpen U
⊢ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
rwa [← f.isAffineOpen_iff_of_isOpenImmersion, f.image_preimage_eq_opensRange_inf,
    inf_eq_right.mpr hU']

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, inf_eq_right
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X_1 Y : Scheme
U_1 : X_1.Opens
hU : IsAffineOpen U_1
f : (↑Γ(X_1, U_1) : Type u)
X : Scheme
U : X.Opens
⊢ Eq.{max 1 (u + 1)} (α := (↑X.affineOpens : Type u) → Prop)
    (fun (U_2 : (↑X.affineOpens : Type u)) ↦ (↑U_2 : X.Opens) ≤ Scheme.Hom.opensRange U.ι)
    fun (V : (↑X.affineOpens : Type u)) ↦ (↑V : X.Opens) ≤ U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
V : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ U }
⊢ (↑(((affineOpensRestrict U).symm :
            (a : { V : (↑X.affineOpens : Type u) // (↑V : X.Opens) ≤ U }) → (↑(↑U : Scheme).affineOpens : Type u))
          V) :
      (↑U : Scheme).Opens) =
    U.ι ⁻¹ᵁ (↑(↑V : (↑X.affineOpens : Type u)) : X.Opens)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X_1 Y : Scheme
U : X_1.Opens
hU : IsAffineOpen U
f : (↑Γ(X_1, U) : Type u)
X : Scheme
inst : IsAffine X
⊢ CompactSpace.{u_1} ↥X

Tactic:
⟨(isAffineOpen_top X).isCompact⟩

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.isCompact, CompactSpace.mk
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
simp_rw : hU.fromSpec ⁻¹ᵁ Scheme.Hom.opensRange hU.fromSpec = ⊤
⊢ hU.fromSpec ⁻¹ᵁ U = ⊤

Tactic:
simp_rw [← hU.opensRange_fromSpec, Scheme.Hom.preimage_opensRange]

Premises used: AlgebraicGeometry.IsAffineOpen.opensRange_fromSpec, AlgebraicGeometry.Scheme.Hom.preimage_opensRange
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Iso.hom (Scheme.ΓSpecIso Γ(X, U)) ≫ Scheme.Hom.app hU.fromSpec U =
    (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
simp [IsAffineOpen.fromSpec_app_of_le]

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpec_app_of_le
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
rw :
  Scheme.Hom.app hU.fromSpec U =
    Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ Iso.hom (Scheme.ΓSpecIso Γ(X, U)) ≫ Scheme.Hom.app hU.fromSpec U
rw₁ rw₂ : Scheme.Hom.app hU.fromSpec U = Scheme.Hom.app hU.fromSpec U
⊢ Scheme.Hom.app hU.fromSpec U =
    Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
rw [← hU.ΓSpecIso_hom_fromSpec_app, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
rw :
  Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
    ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier)
            (Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
        f))
    ((Spec Γ(X, U)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
        f))
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f =
    (Spec Γ(X, U)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
        f)

Tactic:
rw [Scheme.preimage_basicOpen, hU.fromSpec_app_self]

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpec_app_self, AlgebraicGeometry.Scheme.preimage_basicOpen