awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥(U ⨿ V)
hx : Membership.mem (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W) x
h :
  ∀ (x : ↥U)
    (hx :
      Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W)
        ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inl x) : ↥(U ⨿ V))),
    Membership.mem (α := ↥(U ⨿ V)) (Scheme.Hom.opensRange i)
      ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inl x) : ↥(U ⨿ V))
h₁ :
  ∀ (x : ↥V)
    (hx :
      Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W)
        ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inr x) : ↥(U ⨿ V))),
    Membership.mem (α := ↥(U ⨿ V)) (Scheme.Hom.opensRange i)
      ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inr x) : ↥(U ⨿ V))
⊢ x ∈ Scheme.Hom.opensRange i

Tactic:
obtain ⟨(x | x), rfl⟩ := (coprodMk U V).surjective x

Premises used: AlgebraicGeometry.coprodMk, Homeomorph.surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx :
  Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W)
    ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inl x) : ↥(U ⨿ V))
⊢ Membership.mem (α := ↥X) W (f x : ↥X)

Tactic:
simpa [← Scheme.Hom.comp_apply] using hx

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx :
  Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W)
    ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inl x) : ↥(U ⨿ V))
⊢ Membership.mem (α := ↥X) W (f x : ↥X)

Tactic:
replace hx : f x ∈ W := by simpa [← Scheme.Hom.comp_apply] using hx
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx : Membership.mem (α := ↥X) W (f x : ↥X)
⊢ Eq (α := ↥(U ⨿ V))
    (i
        ((coprodMk (↑(f ⁻¹ᵁ W) : Scheme) (↑(g ⁻¹ᵁ W) : Scheme) :
              (a : ↥(↑(f ⁻¹ᵁ W) : Scheme) ⊕ ↥(↑(g ⁻¹ᵁ W) : Scheme)) → ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme)))
            (Sum.inl (Subtype.mk (p := fun (x : ↥U) ↦ x ∈ f ⁻¹ᵁ W) x hx)) :
          ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme))) :
      ↥(U ⨿ V))
    ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inl x) : ↥(U ⨿ V))

Tactic:
simp [i, ← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx : Membership.mem (α := ↥X) W (f x : ↥X)
⊢ Membership.mem (α := ↥(U ⨿ V)) (Scheme.Hom.opensRange i)
    ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inl x) : ↥(U ⨿ V))

Tactic:
exact ⟨coprodMk _ _ (.inl ⟨x, hx⟩), by simp [i, ← Scheme.Hom.comp_apply]⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx :
  Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W)
    ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inr x) : ↥(U ⨿ V))
⊢ Membership.mem (α := ↥X) W (g x : ↥X)

Tactic:
simpa [← Scheme.Hom.comp_apply] using hx

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx :
  Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W)
    ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inr x) : ↥(U ⨿ V))
⊢ Membership.mem (α := ↥X) W (g x : ↥X)

Tactic:
replace hx : g x ∈ W := by simpa [← Scheme.Hom.comp_apply] using hx
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx : Membership.mem (α := ↥X) W (g x : ↥X)
⊢ Eq (α := ↥(U ⨿ V))
    (i
        ((coprodMk (↑(f ⁻¹ᵁ W) : Scheme) (↑(g ⁻¹ᵁ W) : Scheme) :
              (a : ↥(↑(f ⁻¹ᵁ W) : Scheme) ⊕ ↥(↑(g ⁻¹ᵁ W) : Scheme)) → ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme)))
            (Sum.inr (Subtype.mk (p := fun (x : ↥V) ↦ x ∈ g ⁻¹ᵁ W) x hx)) :
          ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme))) :
      ↥(U ⨿ V))
    ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inr x) : ↥(U ⨿ V))

Tactic:
simp [i, ← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx : Membership.mem (α := ↥X) W (g x : ↥X)
⊢ Membership.mem (α := ↥(U ⨿ V)) (Scheme.Hom.opensRange i)
    ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inr x) : ↥(U ⨿ V))

Tactic:
exact ⟨coprodMk _ _ (.inr ⟨x, hx⟩), by simp [i, ← Scheme.Hom.comp_apply]⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme))
h :
  ∀ (x : ↥U) (hx : x ∈ f ⁻¹ᵁ W),
    Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W)
      (i
          ((coprodMk (↑(f ⁻¹ᵁ W) : Scheme) (↑(g ⁻¹ᵁ W) : Scheme) :
                (a : ↥(↑(f ⁻¹ᵁ W) : Scheme) ⊕ ↥(↑(g ⁻¹ᵁ W) : Scheme)) →
                  ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme)))
              (Sum.inl (Subtype.mk (p := fun (x : ↥U) ↦ x ∈ f ⁻¹ᵁ W) x hx)) :
            ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme))) :
        ↥(U ⨿ V))
h₁ :
  ∀ (x : ↥V) (hx : x ∈ g ⁻¹ᵁ W),
    Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W)
      (i
          ((coprodMk (↑(f ⁻¹ᵁ W) : Scheme) (↑(g ⁻¹ᵁ W) : Scheme) :
                (a : ↥(↑(f ⁻¹ᵁ W) : Scheme) ⊕ ↥(↑(g ⁻¹ᵁ W) : Scheme)) →
                  ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme)))
              (Sum.inr (Subtype.mk (p := fun (x : ↥V) ↦ x ∈ g ⁻¹ᵁ W) x hx)) :
            ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme))) :
        ↥(U ⨿ V))
⊢ Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W) (i x : ↥(U ⨿ V))

Tactic:
obtain ⟨(⟨x, hx⟩ | ⟨x, hx⟩), rfl⟩ := (coprodMk _ _).surjective x

Premises used: AlgebraicGeometry.coprodMk, Homeomorph.surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥U
hx : x ∈ f ⁻¹ᵁ W
⊢ Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W)
    (i
        ((coprodMk (↑(f ⁻¹ᵁ W) : Scheme) (↑(g ⁻¹ᵁ W) : Scheme) :
              (a : ↥(↑(f ⁻¹ᵁ W) : Scheme) ⊕ ↥(↑(g ⁻¹ᵁ W) : Scheme)) → ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme)))
            (Sum.inl (Subtype.mk (p := fun (x : ↥U) ↦ x ∈ f ⁻¹ᵁ W) x hx)) :
          ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme))) :
      ↥(U ⨿ V))

Tactic:
simpa [← Scheme.Hom.comp_apply, i] using hx

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f_1 : X_1 ⟶ Y
g_1 : Y ⟶ Z
U V X : Scheme
f : U ⟶ X
g : V ⟶ X
inst : IsAffineHom f
inst_1 : IsAffineHom g
W : X.Opens
hW : IsAffineOpen W
this_1 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
this : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
i : (↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme) ⟶ U ⨿ V := coprod.map (f ⁻¹ᵁ W).ι (g ⁻¹ᵁ W).ι
x : ↥V
hx : x ∈ g ⁻¹ᵁ W
⊢ Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W)
    (i
        ((coprodMk (↑(f ⁻¹ᵁ W) : Scheme) (↑(g ⁻¹ᵁ W) : Scheme) :
              (a : ↥(↑(f ⁻¹ᵁ W) : Scheme) ⊕ ↥(↑(g ⁻¹ᵁ W) : Scheme)) → ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme)))
            (Sum.inr (Subtype.mk (p := fun (x : ↥V) ↦ x ∈ g ⁻¹ᵁ W) x hx)) :
          ↥((↑(f ⁻¹ᵁ W) : Scheme) ⨿ (↑(g ⁻¹ᵁ W) : Scheme))) :
      ↥(U ⨿ V))

Tactic:
simpa [← Scheme.Hom.comp_apply, i] using hx

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
H : ∀ (x : ↥Y), ∃ (U : Y.Opens), x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ IsAffineHom f

Tactic:
apply isAffineHom_of_forall_exists_isAffineOpen

Premises used: AlgebraicGeometry.isAffineHom_of_forall_exists_isAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
y : ↥Y
pos :
  ∀ (hy : Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥X) ⇑f) y),
    ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
neg : ∀ (hy : y ∉ Set.range (ι := ↥X) ⇑f), ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
by_cases hy : y ∈ Set.range f

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Set.range, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
y : ↥Y
hy : Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥X) ⇑f) y
pos : ∀ (x : ↥X), ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨x, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
x : ↥X
pos :
  ∀ (U : Opens ↥Y) (hU : U ∈ Y.affineOpens) (hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)),
    ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
pos :
  ∀ (V : Opens ↥X) (hV : V ∈ X.affineOpens) (hxV : x ∈ (↑V : Set ↥X)) (hVU : (↑V : Set ↥X) ⊆ (↑(f ⁻¹ᵁ U) : Set ↥X)),
    ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).isOpen

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.isOpen, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.isBasis_affineOpens, CategoryTheory.Functor.obj, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑(f ⁻¹ᵁ U) : Set ↥X)
obtain : ∀ (U' : Set ↥Y) (hU' : IsOpen U') (e : ⇑f ⁻¹' U' = V.carrier), ∃ U' ≤ U, f ⁻¹ᵁ U' = V
⊢ ∃ U' ≤ U, f ⁻¹ᵁ U' = V

Tactic:
obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2

Premises used: Topology.IsInducing.isOpen_iff, Iff.mp, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑(f ⁻¹ᵁ U) : Set ↥X)
U' : Set ↥Y
hU' : IsOpen U'
e : ⇑f ⁻¹' U' = V.carrier
⊢ (↑(f ⁻¹ᵁ ({ carrier := U', is_open' := hU' : Opens ↥Y } ⊓ U)) : Set ↥X) = (↑V : Set ↥X)

Tactic:
simpa [e] using hVU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑(f ⁻¹ᵁ U) : Set ↥X)
pos :
  ∀ (U' : Y.Opens) (hU'U : U' ≤ U) (hV : f ⁻¹ᵁ U' ∈ X.affineOpens) (hxV : x ∈ (↑(f ⁻¹ᵁ U') : Set ↥X))
    (hVU : (↑(f ⁻¹ᵁ U') : Set ↥X) ⊆ (↑(f ⁻¹ᵁ U) : Set ↥X)),
    ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨U', hU'U, rfl⟩ : ∃ U' : Y.Opens, U' ≤ U ∧ f ⁻¹ᵁ U' = V := by
      obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2
      exact ⟨⟨U', hU'⟩ ⊓ U, inf_le_right, Opens.ext (by simpa [e] using hVU)⟩

Premises used: AlgebraicGeometry.Scheme.Opens, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ (↑(f ⁻¹ᵁ U') : Set ↥X)
hVU : (↑(f ⁻¹ᵁ U') : Set ↥X) ⊆ (↑(f ⁻¹ᵁ U) : Set ↥X)
pos :
  ∀ (r : (↑Γ(Y, U) : Type u)) (hrU' : Y.basicOpen r ≤ U')
    (hxr : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U') (f x) hxV) : ↥Y) : ↥Y)),
    ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
obtain ⟨r, hrU', hxr⟩ := hU.exists_basicOpen_le ⟨f x, hxV⟩ hxU

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ (↑(f ⁻¹ᵁ U') : Set ↥X)
hVU : (↑(f ⁻¹ᵁ U') : Set ↥X) ⊆ (↑(f ⁻¹ᵁ U) : Set ↥X)
r : (↑Γ(Y, U) : Type u)
hrU' : Y.basicOpen r ≤ U'
hxr : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U') (f x) hxV) : ↥Y) : ↥Y)
⊢ ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
⟨_, hxr, hU.basicOpen r, ?_⟩

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ (↑(f ⁻¹ᵁ U') : Set ↥X)
hVU : (↑(f ⁻¹ᵁ U') : Set ↥X) ⊆ (↑(f ⁻¹ᵁ U) : Set ↥X)
r : (↑Γ(Y, U) : Type u)
hrU' : Y.basicOpen r ≤ U'
hxr : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U') (f x) hxV) : ↥Y) : ↥Y)
pos : IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r)
⊢ ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
refine ⟨_, hxr, hU.basicOpen r, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ (↑(f ⁻¹ᵁ U') : Set ↥X)
hVU : (↑(f ⁻¹ᵁ U') : Set ↥X) ⊆ (↑(f ⁻¹ᵁ U) : Set ↥X)
r : (↑Γ(Y, U) : Type u)
hrU' : Y.basicOpen r ≤ U'
hxr : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U') (f x) hxV) : ↥Y) : ↥Y)
⊢ IsAffineOpen
    (X.basicOpen (U := f ⁻¹ᵁ U')
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U') :
          (a : (↑Γ(Y, U') : Type u)) → (↑Γ(X, f ⁻¹ᵁ U') : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hU'U).op) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(Y, U') : Type u))
            r :
          (↑Γ(Y, U') : Type u))))

Tactic:
hV.basicOpen (f.app _ (Y.presheaf.map (homOfLE hU'U).op r))

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.Hom.app, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
U' : Y.Opens
hU'U : U' ≤ U
hV : f ⁻¹ᵁ U' ∈ X.affineOpens
hxV : x ∈ (↑(f ⁻¹ᵁ U') : Set ↥X)
hVU : (↑(f ⁻¹ᵁ U') : Set ↥X) ⊆ (↑(f ⁻¹ᵁ U) : Set ↥X)
r : (↑Γ(Y, U) : Type u)
hrU' : Y.basicOpen r ≤ U'
hxr : Membership.mem (α := ↥Y) (Y.basicOpen r) ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U') (f x) hxV) : ↥Y) : ↥Y)
h :
  f ⁻¹ᵁ Y.basicOpen r =
    X.basicOpen (U := f ⁻¹ᵁ U')
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U') :
          (a : (↑Γ(Y, U') : Type u)) → (↑Γ(X, f ⁻¹ᵁ U') : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y.presheaf.map (homOfLE hU'U).op) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(Y, U') : Type u))
            r :
          (↑Γ(Y, U') : Type u)))
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r)

Tactic:
convert! hV.basicOpen (f.app _ (Y.presheaf.map (homOfLE hU'U).op r)) using 1

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.Hom.app, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace