awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : (↑Γ(X, U) : Type u)
hj : j ∈ s
hs₃ :
  IsAffineOpen
    (X.basicOpen (U := U.ι ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ((↑U : Scheme), ⊤)) (Y := Γ(X, U.ι ''ᵁ ⊤)) (Iso.inv (Scheme.Hom.appIso U.ι ⊤)) :
          (a : (↑Γ((↑U : Scheme), ⊤) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) U.topIso.inv :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
            j :
          (↑Γ((↑U : Scheme), ⊤) : Type u))))
⊢ IsAffineOpen.{u} (X := (↑U : Scheme))
    ((↑U : Scheme).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) U.topIso.inv :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        j))

Tactic:
rw [← (Scheme.Opens.ι _).isAffineOpen_iff_of_isOpenImmersion, Scheme.image_basicOpen]

Premises used: AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
j : (↑Γ(X, U) : Type u)
hj : j ∈ s
⊢ IsAffineOpen
    (X.basicOpen (U := U.ι ''ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ((↑U : Scheme), ⊤)) (Y := Γ(X, U.ι ''ᵁ ⊤)) (Iso.inv (Scheme.Hom.appIso U.ι ⊤)) :
          (a : (↑Γ((↑U : Scheme), ⊤) : Type u)) → (↑Γ(X, U.ι ''ᵁ ⊤) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) U.topIso.inv :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
            j :
          (↑Γ((↑U : Scheme), ⊤) : Type u))))

Tactic:
simpa [Scheme.Opens.toScheme_presheaf_obj] using hs₂ j hj

Premises used: AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
respectsIso :
  (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
      IsAffine X).RespectsIso
to_basicOpen :
  ∀ {X Y : Scheme.{u_1}} [IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u_1)),
    IsAffine X → IsAffine.{u_1} (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)
of_basicOpenCover :
  ∀ {X Y : Scheme.{u_1}} [IsAffine Y] (f : X ⟶ Y) (s : Finset (↑Γ(Y, ⊤) : Type u_1)),
    Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤ →
      (∀ (r : ↥s), IsAffine.{u_1} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)) → IsAffine X
⊢ AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
respectsIso : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [IsAffine Z], IsAffine Y → IsAffine X
respectsIso₁ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [IsAffine Y], IsAffine X → IsAffine X
⊢ (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
      IsAffine X).RespectsIso

Tactic:
apply AffineTargetMorphismProperty.respectsIso_mk

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z_1 : Scheme
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z_1
X Y Z : Scheme
e : X ≅ Y
f_1 : Y ⟶ Z
inst : IsAffine Z
H : IsAffine Y
⊢ IsAffine Y

Tactic:
have : IsAffine _ := H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z_1 : Scheme
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z_1
X Y Z : Scheme
e : X ≅ Y
f_1 : Y ⟶ Z
inst : IsAffine Z
H this : IsAffine Y
⊢ IsAffine X

Tactic:
.of_isIso e.hom

Premises used: AlgebraicGeometry.IsAffine.of_isIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z_1 : Scheme
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z_1
X Y Z : Scheme
e : X ≅ Y
f_1 : Y ⟶ Z
inst : IsAffine Z
H this : IsAffine Y
⊢ IsAffine X

Tactic:
exact .of_isIso e.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
X_1 Y_1 Z_1 : Scheme
⊢ ∀ (e : Y_1 ≅ Z_1) (f : X_1 ⟶ Y_1) [IsAffine Y_1], IsAffine X_1 → IsAffine X_1

Tactic:
fun _ _ _ ↦ id

Premises used: id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [IsAffine Y], IsAffine X → IsAffine X

Tactic:
exact fun _ _ _ ↦ id

Premises used: id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
to_basicOpen :
  ∀ [IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u_1)), IsAffine X → IsAffine.{u_1} (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)
⊢ ∀ [IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u_1)), IsAffine X → IsAffine.{u_1} (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u_1)
H : IsAffine X
⊢ IsAffine X

Tactic:
have : IsAffine X := H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u_1)
H this : IsAffine X
to_basicOpen :
  IsAffineOpen
    (X.basicOpen (U := f ⁻¹ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
          (a : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u_1))
        r))
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r)

Tactic:
rw [Scheme.preimage_basicOpen]

Premises used: AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u_1)
H this : IsAffine X
⊢ IsAffineOpen
    (X.basicOpen (U := f ⁻¹ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
          (a : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u_1))
        r))

Tactic:
(isAffineOpen_top X).basicOpen _

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.basicOpen, Set.Mem, Set.univ, setOf, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u_1)
H this : IsAffine X
⊢ IsAffineOpen
    (X.basicOpen (U := f ⁻¹ᵁ ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
          (a : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u_1))
        r))

Tactic:
exact (isAffineOpen_top X).basicOpen _

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
of_basicOpenCover :
  ∀ [IsAffine Y] (f : X ⟶ Y) (s : Finset (↑Γ(Y, ⊤) : Type u_1)),
    Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤ →
      (∀ (r : ↥s), IsAffine.{u_1} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)) → IsAffine X
⊢ ∀ [IsAffine Y] (f : X ⟶ Y) (s : Finset (↑Γ(Y, ⊤) : Type u_1)),
    Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤ →
      (∀ (r : ↥s), IsAffine.{u_1} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)) → IsAffine X

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑S : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hS' : ∀ (r : ↥S), IsAffine.{u_1} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
⊢ Eq (α := Ideal (↑Γ(X, ⊤) : Type u_1))
    (Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (Ideal.span (↑S : Set (↑Γ(Y, ⊤) : Type u_1))))
    (Ideal.map (R := (↑Γ(Y, ⊤) : Type u_1)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤)

Tactic:
apply_fun Ideal.map (f.appTop).hom at hS

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.appTop, Ideal.map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS' : ∀ (r : ↥S), IsAffine.{u_1} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
hS :
  Eq (α := Ideal (↑Γ(X, ⊤) : Type u_1))
    (Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (Ideal.span (↑S : Set (↑Γ(Y, ⊤) : Type u_1))))
    (Ideal.map (R := (↑Γ(Y, ⊤) : Type u_1)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤)
⊢ Eq (α := Ideal (↑Γ(X, ⊤) : Type u_1))
    (Ideal.span
      ((⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) : (a : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1)) ''
        (↑S : Set (↑Γ(Y, ⊤) : Type u_1))))
    ⊤

Tactic:
rw [Ideal.map_span, Ideal.map_top] at hS

Premises used: Ideal.map_span, Ideal.map_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS' : ∀ (r : ↥S), IsAffine.{u_1} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
hS :
  Eq (α := Ideal (↑Γ(X, ⊤) : Type u_1))
    (Ideal.span
      ((⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) : (a : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1)) ''
        (↑S : Set (↑Γ(Y, ⊤) : Type u_1))))
    ⊤
of_basicOpenCover :
  ∀ (i : (↑Γ(X, ⊤) : Type u_1)),
    Membership.mem (γ := Set (↑Γ(X, ⊤) : Type u_1))
        ((⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) : (a : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1)) ''
          (↑S : Set (↑Γ(Y, ⊤) : Type u_1)))
        i →
      IsAffineOpen (X.basicOpen i)
⊢ IsAffine X

Tactic:
apply isAffine_of_isAffineOpen_basicOpen _ hS

Premises used: AlgebraicGeometry.isAffine_of_isAffineOpen_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS' : ∀ (r : ↥S), IsAffine.{u_1} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
hS :
  Eq (α := Ideal (↑Γ(X, ⊤) : Type u_1))
    (Ideal.span
      ((⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) : (a : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, ⊤) : Type u_1)) ''
        (↑S : Set (↑Γ(Y, ⊤) : Type u_1))))
    ⊤
⊢ ∀ (i : ↥S), IsAffineOpen (f ⁻¹ᵁ Y.basicOpen (↑i : (↑Γ(Y, ⊤) : Type u_1)))

Tactic:
have : ∀ i : S, IsAffineOpen (f ⁻¹ᵁ Y.basicOpen i.1) := hS'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
    IsAffineHom f ↔ targetAffineLocally (fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X) f
⊢ @IsAffineHom = targetAffineLocally fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
h :
  (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ↔
    ∀ (a : Y.Opens) (b : IsAffineOpen a), IsAffine.{u_1} (↑(f ⁻¹ᵁ a) : Scheme)
⊢ IsAffineHom f ↔ targetAffineLocally (fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X) f

Tactic:
simp only [targetAffineLocally, Scheme.affineOpens, Set.coe_setOf, Set.mem_setOf_eq,
      Subtype.forall, isAffineHom_iff]

Premises used: Subtype.forall, Set.mem_setOf_eq, AlgebraicGeometry.isAffineHom_iff, AlgebraicGeometry.targetAffineLocally, AlgebraicGeometry.Scheme.affineOpens, Set.coe_setOf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ↔
    ∀ (a : Y.Opens) (b : IsAffineOpen a), IsAffine.{u_1} (↑(f ⁻¹ᵁ a) : Scheme)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hP' :
  AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    IsAffine X
⊢ MorphismProperty.IsStableUnderBaseChange @IsAffineHom

Tactic:
apply HasAffineProperty.isStableUnderBaseChange

Premises used: AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : ∀ (P : MorphismProperty Scheme) {Q : outParam AffineTargetMorphismProperty} [self : HasAffineProperty P Q],
  Q.IsLocal :=
  HasAffineProperty.isLocal_affineProperty
hP' :
  ∀ ⦃X Y S : Scheme.{u_1}⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), IsAffine Y → IsAffine.{u_1} (pullback f g)
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    IsAffine X

Tactic:
apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
this : ∀ (P : MorphismProperty Scheme) {Q : outParam AffineTargetMorphismProperty} [self : HasAffineProperty P Q],
  Q.IsLocal :=
  HasAffineProperty.isLocal_affineProperty
X_2 Y S : Scheme
X : IsAffine S
hX : IsAffine X_2
f : X_2 ⟶ S
g : Y ⟶ S
H : IsAffine Y
⊢ IsAffine.{u_1} (pullback f g)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffine X
inst_1 : IsAffine Y
⊢ IsAffineHom f

Tactic:
(HasAffineProperty.iff_of_isAffine (P := @IsAffineHom)).mpr inferInstance

Premises used: Iff.mpr, inferInstance, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : IsAffine Y
⊢ IsAffine X

Tactic:
(HasAffineProperty.iff_of_isAffine (P := @IsAffineHom) (f := f)).mp inferInstance

Premises used: inferInstance, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥Y), ∃ (U : Y.Opens), x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
choose :
  ∀ (U : (x : ↥Y) → Y.Opens) (hxU : ∀ (x : ↥Y), x ∈ U x) (hU : ∀ (x : ↥Y), IsAffineOpen (U x))
    (hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)), IsAffineHom f
⊢ IsAffineHom f

Tactic:
choose U hxU hU hfU using H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
U : (x : ↥Y) → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
rw :
  ∀ (i : ↥Y),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U i) ⋯) : Y.Opens)) : Scheme)
rw₁ :
  Eq.{u + 1} (α := Y.Opens) (⨆ (i : ↥Y), (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U i) ⋯) : Y.Opens))
    ⊤
⊢ IsAffineHom f

Tactic:
rw [HasAffineProperty.iff_of_iSup_eq_top (P := @IsAffineHom) fun i ↦ ⟨U i, hU i⟩]

Premises used: Subtype.mk, AlgebraicGeometry.HasAffineProperty.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
U : (x : ↥Y) → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ∀ (i : ↥Y),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U i) ⋯) : Y.Opens)) : Scheme)

Tactic:
hfU

Premises used: AlgebraicGeometry.IsAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
U : (x : ↥Y) → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ∀ (i : ↥Y),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U i) ⋯) : Y.Opens)) : Scheme)

Tactic:
exact hfU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
U : (x : ↥Y) → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
x : ↥Y
h : Membership.mem (γ := Opens ↥Y) ⊤ x
⊢ Membership.mem (γ := Opens ↥Y)
    (⨆ (i : ↥Y), (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U i) ⋯) : Y.Opens)) x

Tactic:
simpa using ⟨x, hxU x⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
U : (x : ↥Y) → Y.Opens
hxU : ∀ (x : ↥Y), x ∈ U x
hU : ∀ (x : ↥Y), IsAffineOpen (U x)
hfU : ∀ (x : ↥Y), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ Eq.{u + 1} (α := Y.Opens) (⨆ (i : ↥Y), (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U i) ⋯) : Y.Opens))
    ⊤

Tactic:
exact top_le_iff.mp (fun x _ ↦ by simpa using ⟨x, hxU x⟩)

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsAffineHom f
inst_1 : IsAffine Y
⊢ IsAffine.{u_1} (pullback f g)

Tactic:
letI : IsAffineHom (pullback.snd f g) := MorphismProperty.pullback_snd _ _ ‹_›
  isAffine_of_isAffineHom (pullback.snd f g)

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.isAffine_of_isAffineHom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsAffineHom g
inst_1 : IsAffine X
⊢ IsAffine.{u_1} (pullback f g)

Tactic:
letI : IsAffineHom (pullback.fst f g) := MorphismProperty.pullback_fst _ _ ‹_›
  isAffine_of_isAffineHom (pullback.fst f g)

Premises used: AlgebraicGeometry.isAffine_of_isAffineHom, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z P : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst : IsAffine X
inst_1 : IsAffineHom g
h : IsPullback fst snd f g
⊢ IsAffine P

Tactic:
.of_isIso h.isoPullback.hom

Premises used: AlgebraicGeometry.IsAffine.of_isIso, CategoryTheory.IsPullback.isoPullback, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z P : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : IsAffine Z
h : IsPullback fst snd f g
⊢ IsAffine P

Tactic:
have : IsAffine P := .of_isPullback h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z P : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : IsAffine Z
h : IsPullback fst snd f g
this : IsAffine P
⊢ IsPullback (P := AffineScheme.of P) (X := AffineScheme.of X) (Y := AffineScheme.of Y) (Z := AffineScheme.of Z)
    (AffineScheme.ofHom fst) (AffineScheme.ofHom snd) (AffineScheme.ofHom f) (AffineScheme.ofHom g)

Tactic:
have : IsPullback (AffineScheme.ofHom fst) (AffineScheme.ofHom snd) (AffineScheme.ofHom f)
      (AffineScheme.ofHom g) :=
    IsPullback.of_map_of_faithful AffineScheme.forgetToScheme.{u} h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z P : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : IsAffine Z
h : IsPullback fst snd f g
this_1 : IsAffine P
this :
  IsPullback (P := AffineScheme.of P) (X := AffineScheme.of X) (Y := AffineScheme.of Y) (Z := AffineScheme.of Z)
    (AffineScheme.ofHom fst) (AffineScheme.ofHom snd) (AffineScheme.ofHom f) (AffineScheme.ofHom g)
⊢ IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop fst) (Scheme.Hom.appTop snd)

Tactic:
exact (IsPullback.map AffineScheme.Γ.rightOp this).unop.flip

Premises used: CategoryTheory.IsPushout.flip, AlgebraicGeometry.AffineScheme.Γ, CategoryTheory.IsPullback.unop, CategoryTheory.Functor.rightOp, CategoryTheory.IsPullback.map
-- 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
⊢ IsAffineHom (X := U ⨿ V) (coprod.desc f g)

Tactic:
⟨fun W hW ↦ ?_⟩

Premises used: AlgebraicGeometry.IsAffineHom.mk
-- 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
refine : ∀ (W : X.Opens) (hW : IsAffineOpen W), IsAffineOpen (X := U ⨿ V) (coprod.desc f g ⁻¹ᵁ W)
⊢ IsAffineHom (X := U ⨿ V) (coprod.desc f g)

Tactic:
refine ⟨fun W hW ↦ ?_⟩
-- 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
⊢ IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)

Tactic:
have : IsAffine (f ⁻¹ᵁ W).toScheme := hW.preimage f
-- 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 : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
⊢ IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)

Tactic:
have : IsAffine (g ⁻¹ᵁ W).toScheme := hW.preimage g
-- 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).ι
⊢ IsAffineOpen (Scheme.Hom.opensRange i)

Tactic:
isAffineOpen_opensRange i

Premises used: AlgebraicGeometry.isAffineOpen_opensRange
-- 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).ι
h : coprod.desc f g ⁻¹ᵁ W = Scheme.Hom.opensRange i
⊢ IsAffineOpen (X := U ⨿ V) (coprod.desc f g ⁻¹ᵁ W)

Tactic:
convert! isAffineOpen_opensRange i

Premises used: AlgebraicGeometry.isAffineOpen_opensRange
-- 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).ι
h : coprod.desc f g ⁻¹ᵁ W ≤ Scheme.Hom.opensRange i
h₁ : Scheme.Hom.opensRange i ≤ coprod.desc f g ⁻¹ᵁ W
⊢ coprod.desc f g ⁻¹ᵁ W = Scheme.Hom.opensRange i

Tactic:
apply le_antisymm

Premises used: le_antisymm