awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : (↑Γ(X, U) : Type u)
I : Ideal (↑Γ(X, U) : Type u)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    Membership.mem (α := (↑(X.presheaf.stalk x) : Type u)) (γ := Ideal (↑(X.presheaf.stalk x) : Type u))
      (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          s :
        (↑(X.presheaf.stalk x) : Type u))
this_1 : (x : ↥(Spec Γ(X, U))) → Algebra (↑Γ(X, U) : Type u) (↑(X.presheaf.stalk (hU.fromSpec x)) : Type u) :=
  fun (x : ↥(Spec Γ(X, U))) ↦
    X.presheaf.algebra_section_stalk
      (((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' : (a : ↥(Spec Γ(X, U))) → ↥(↑U : Scheme)) x)
this :
  ∀ (P : Ideal (↑Γ(X, U) : Type u)) [hP : P.IsPrime],
    IsLocalization.AtPrime
      (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP : PrimeSpectrum (↑Γ(X, U) : Type u) })) : Type u) P
⊢ s ∈ I

Tactic:
Submodule.mem_of_localization_maximal
      (fun P hP ↦ X.presheaf.stalk (hU.fromSpec ⟨P, hP.isPrime⟩))
      (fun P hP ↦ Algebra.linearMap _ _) _ _ ?_

Premises used: PrimeSpectrum.mk, Submodule.mem_of_localization_maximal, CommRingCat.carrier, CategoryTheory.ConcreteCategory.hom, Set.Mem, AlgebraicGeometry.IsAffineOpen.fromSpec, Algebra.linearMap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Ideal.IsMaximal.isPrime, TopCat.Presheaf.stalk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal (↑Γ(X, U) : Type u)
⊢ I ≤ J ↔
    ∀ (x : ↥X) (h : x ∈ U),
      LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)

Tactic:
⟨fun h _ _ ↦ Ideal.map_mono h,
    fun H _ hs ↦ hU.mem_ideal_iff.mpr fun x hx ↦ H x hx (Ideal.mem_map_of_mem _ hs)⟩

Premises used: Iff.mpr, CommRingCat.Hom.hom, Ideal.mem_map_of_mem, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Iff.intro, AlgebraicGeometry.PresheafedSpace.presheaf, Ideal.map_mono, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal (↑Γ(X, U) : Type u)
simp_rw :
  I ≤ J ∧ J ≤ I ↔
    ∀ (x : ↥X) (h : x ∈ U),
      LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J) ∧
        LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
simp_rw₁ :
  ((∀ (x : ↥X) (h : x ∈ U),
        LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)) ∧
      ∀ (x : ↥X) (h : x ∈ U),
        LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)) ↔
    ∀ (x : ↥X) (h : x ∈ U),
      LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J) ∧
        LE.le (α := Ideal (↑(X.presheaf.stalk x) : Type u))
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)
          (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
⊢ I = J ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
        (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J)

Tactic:
simp_rw [le_antisymm_iff, hU.ideal_le_iff, forall_and]

Premises used: AlgebraicGeometry.IsAffineOpen.ideal_le_iff, le_antisymm_iff, forall_and
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U_1 : X.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X, U_1) : Type u)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)
⊢ IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal

Tactic:
have := hU.isLocalization_stalk ⟨f x, hVU hx⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U_1 : X.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X, U_1) : Type u)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this_1 : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)
this_2 :
  IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
this : Algebra (↑(X.presheaf.obj (op V)) : Type u)
  (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u) :=
  X.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal

Tactic:
have := hV.isLocalization_stalk ⟨x, hx⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U_1 : X.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X, U_1) : Type u)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this_1 : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)
this_2 :
  IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
this_3 : Algebra (↑(X.presheaf.obj (op V)) : Type u)
  (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u) :=
  X.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
⊢ Y.presheaf.stalk (f x) ≅
    CommRingCat.of (Localization.AtPrime (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal)

Tactic:
exact ((IsLocalization.algEquiv (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal.primeCompl
      (Y.presheaf.stalk (f x))
      (Localization.AtPrime (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal)).toCommRingCatIso:)

Premises used: CommRingCat.carrier, CategoryTheory.ConcreteCategory.hom, Localization.AtPrime, RingEquiv.toCommRingCatIso, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopCat.Presheaf.stalk, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, IsLocalization.algEquiv, AlgEquiv.toRingEquiv, AlgebraicGeometry.IsAffineOpen.primeIdealOf, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Ideal.primeCompl, DFunLike.coe, PrimeSpectrum.asIdeal, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U_1 : X.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X, U_1) : Type u)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this_1 : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)
this_2 :
  IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
this_3 : Algebra (↑(X.presheaf.obj (op V)) : Type u)
  (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u) :=
  X.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
⊢ X.presheaf.stalk x ≅
    CommRingCat.of (Localization.AtPrime (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal)

Tactic:
exact ((IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl
      (X.presheaf.stalk x)
      (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toCommRingCatIso:)

Premises used: CommRingCat.carrier, Localization.AtPrime, RingEquiv.toCommRingCatIso, TopCat.Presheaf.stalk, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, IsLocalization.algEquiv, AlgEquiv.toRingEquiv, AlgebraicGeometry.IsAffineOpen.primeIdealOf, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Ideal.primeCompl, PrimeSpectrum.asIdeal, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U_1 : X.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X, U_1) : Type u)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this_1 : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)
this_2 :
  IsLocalization.AtPrime (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y)) : Type u)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
this_3 : Algebra (↑(X.presheaf.obj (op V)) : Type u)
  (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u) :=
  X.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥X)) : Type u)
    (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
a : (↑Γ(Y, U) : Type u)
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((algebraMap (↑Γ(X, V) : Type u) (↑(X.presheaf.stalk x) : Type u) :
          (a : (↑Γ(X, V) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u)) a :
          (↑Γ(X, V) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x) :
          (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((algebraMap (↑Γ(Y, U) : Type u) (↑(Y.presheaf.stalk (f x)) : Type u) :
              (a : (↑Γ(Y, U) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
            a :
          (↑(Y.presheaf.stalk (f x)) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))

Tactic:
simp only [RingHom.algebraMap_toAlgebra, Scheme.Hom.germ_stalkMap_apply, Scheme.Hom.appLE,
      homOfLE_leOfHom, CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply,
      X.presheaf.germ_res_apply]

Premises used: TopCat.Presheaf.germ_res_apply, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_apply, CommRingCat.hom_comp, AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, RingHom.coe_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Function.comp_apply, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
trans :
  ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
trans₁ :
  Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤

Tactic:
trans ⋃ i : s, (PrimeSpectrum.basicOpen i.1).1 = Set.univ

Premises used: Set.univ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
trans :
  ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq (α := Set ↥(Spec Γ(X, U)))
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
      (⇑hU.fromSpec ⁻¹' U.carrier)
trans₁ :
  Eq (α := Set ↥(Spec Γ(X, U)))
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
      (⇑hU.fromSpec ⁻¹' U.carrier) ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ

Tactic:
trans hU.fromSpec ⁻¹' (⨆ f : s, X.basicOpen (f : Γ(X, U))).1 = hU.fromSpec ⁻¹' U.1

Premises used: iSup, AlgebraicGeometry.IsAffineOpen.fromSpec, TopologicalSpace.Opens.carrier, AlgebraicGeometry.Scheme.basicOpen, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U
rw rw₁ : Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' U.carrier) (⇑hU.fromSpec ⁻¹' U.carrier)
⊢ Eq (α := Set ↥(Spec Γ(X, U)))
    (Set.preimage (β := ↥X) (⇑hU.fromSpec)
      (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
    (⇑hU.fromSpec ⁻¹' U.carrier)

Tactic:
rw [h]
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
refine :
  Eq (α := Set ↥(Spec Γ(X, U)))
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
      (⇑hU.fromSpec ⁻¹' U.carrier) →
    ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U ↔
    Eq (α := Set ↥(Spec Γ(X, U)))
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
      (⇑hU.fromSpec ⁻¹' U.carrier)

Tactic:
refine ⟨fun h => by rw [h], ?_⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h :
  Eq (α := Set ↥(Spec Γ(X, U)))
    (Set.preimage (β := ↥X) (⇑hU.fromSpec)
      (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
    (⇑hU.fromSpec ⁻¹' U.carrier)
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec)
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))))))
    (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (⇑hU.fromSpec ⁻¹' U.carrier))

Tactic:
apply_fun Set.image hU.fromSpec at h

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Set.image, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h :
  Eq (α := Set ↥X)
    (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec)
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))))))
    (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (⇑hU.fromSpec ⁻¹' U.carrier))
⊢ Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) ∩ (↑U : Set ↥X) =
    U.carrier ∩ (↑U : Set ↥X)

Tactic:
rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.range_fromSpec]
        at h

Premises used: Set.image_preimage_eq_inter_range, AlgebraicGeometry.IsAffineOpen.range_fromSpec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h :
  Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) ∩ (↑U : Set ↥X) =
    U.carrier ∩ (↑U : Set ↥X)
⊢ (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)

Tactic:
simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h

Premises used: Set.inter_self, Set.inter_eq_right, TopologicalSpace.Opens.carrier_eq_coe
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
h₁ : (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X) = (↑U : Set ↥X)
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) = U

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
⊢ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X) = (↑U : Set ↥X)

Tactic:
Set.Subset.antisymm ?_ h

Premises used: Set.Subset.antisymm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
h₁ : (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X) = (↑U : Set ↥X)

Tactic:
refine Set.Subset.antisymm ?_ h

Premises used: Set.Subset.antisymm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
h₁ : ∀ (x : (↑Γ(X, U) : Type u)) (h : x ∈ s), (↑(X.basicOpen x) : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X) ⊆ (↑U : Set ↥X)

Tactic:
simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]

Premises used: TopologicalSpace.Opens.coe_iSup, Set.iUnion_subset_iff, SetCoe.forall
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
x : (↑Γ(X, U) : Type u)
h₁ : x ∈ s → (↑(X.basicOpen x) : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ ∀ (h : x ∈ s), (↑(X.basicOpen x) : Set ↥X) ⊆ (↑U : Set ↥X)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
x : (↑Γ(X, U) : Type u)
h_1 : x ∈ s
⊢ (↑(X.basicOpen x) : Set ↥X) ⊆ (↑U : Set ↥X)

Tactic:
X.basicOpen_le x

Premises used: AlgebraicGeometry.Scheme.basicOpen_le, Set.Subset
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : (↑U : Set ↥X) ⊆ (↑(⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))) : Set ↥X)
x : (↑Γ(X, U) : Type u)
h_1 : x ∈ s
⊢ (↑(X.basicOpen x) : Set ↥X) ⊆ (↑U : Set ↥X)

Tactic:
exact X.basicOpen_le x

Premises used: AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
simp :
  Eq (α := Set ↥(Spec Γ(X, U)))
      (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
      (⇑hU.fromSpec ⁻¹' U.carrier) ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ
⊢ Eq (α := Set ↥(Spec Γ(X, U)))
      (Set.preimage (β := ↥X) (⇑hU.fromSpec)
        (Opens.carrier (⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)))))
      (⇑hU.fromSpec ⁻¹' U.carrier) ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ

Tactic:
simp only [Opens.iSup_def, Set.preimage_iUnion]

Premises used: TopologicalSpace.Opens.iSup_def, Set.preimage_iUnion