awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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))
        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 ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE hU'U).op.unop).op) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U') : Type u))
        r)
⊢ 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)))

Tactic:
simp only [Scheme.preimage_basicOpen, ← CommRingCat.comp_apply, f.naturality]

Premises used: CommRingCat.comp_apply, AlgebraicGeometry.Scheme.Hom.naturality, AlgebraicGeometry.Scheme.preimage_basicOpen
-- 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)
⊢ 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))
        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 ≫ X.presheaf.map ((Opens.map f.base).map (homOfLE hU'U).op.unop).op) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U') : Type u))
        r)

Tactic:
simpa using ((Opens.map f.base).map (homOfLE hrU')).le

Premises used: Quiver.Hom.le, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map
-- 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 : y ∉ Set.range (ι := ↥X) ⇑f
neg :
  ∀ (U : Opens ↥Y) (hU : U ∈ Y.affineOpens) (hyU : y ∈ (↑U : Set ↥Y)) (hU' : (↑U : Set ↥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:
obtain ⟨_, ⟨U, hU, rfl⟩, hyU, hU'⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open hy hf₂.isOpen_compl

Premises used: IsClosed.isOpen_compl, AlgebraicGeometry.Scheme.isBasis_affineOpens, 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)
y : ↥Y
hy : y ∉ Set.range (ι := ↥X) ⇑f
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hyU : y ∈ (↑U : Set ↥Y)
hU' : (↑U : Set ↥Y) ⊆ (Set.range (ι := ↥X) ⇑f)ᶜ
⊢ Eq (α := Set ↥X) (⇑f ⁻¹' (↑U : Set ↥Y)) ∅

Tactic:
rw [Set.subset_compl_iff_disjoint_right, ← Set.preimage_eq_empty_iff] at hU'

Premises used: Set.subset_compl_iff_disjoint_right, Set.preimage_eq_empty_iff
-- 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 : y ∉ Set.range (ι := ↥X) ⇑f
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hyU : y ∈ (↑U : Set ↥Y)
hU' : Eq (α := Set ↥X) (⇑f ⁻¹' (↑U : Set ↥Y)) ∅
⊢ ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
⟨U, hyU, hU, ?_⟩

Premises used: 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)
y : ↥Y
hy : y ∉ Set.range (ι := ↥X) ⇑f
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hyU : y ∈ (↑U : Set ↥Y)
hU' : Eq (α := Set ↥X) (⇑f ⁻¹' (↑U : Set ↥Y)) ∅
neg : IsAffineOpen (f ⁻¹ᵁ U)
⊢ ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
refine ⟨U, hyU, hU, ?_⟩
-- 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 : y ∉ Set.range (ι := ↥X) ⇑f
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hyU : y ∈ (↑U : Set ↥Y)
hU' : Eq (α := Set ↥X) (⇑f ⁻¹' (↑U : Set ↥Y)) ∅
⊢ IsAffineOpen.{u} (X := X) ⊥

Tactic:
isAffineOpen_bot _

Premises used: AlgebraicGeometry.isAffineOpen_bot
-- 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 : y ∉ Set.range (ι := ↥X) ⇑f
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hyU : y ∈ (↑U : Set ↥Y)
hU' : Eq (α := Set ↥X) (⇑f ⁻¹' (↑U : Set ↥Y)) ∅
h : f ⁻¹ᵁ U = ⊥
⊢ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
convert! isAffineOpen_bot _

Premises used: AlgebraicGeometry.isAffineOpen_bot
-- 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 : y ∉ Set.range (ι := ↥X) ⇑f
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hyU : y ∈ (↑U : Set ↥Y)
hU' : Eq (α := Set ↥X) (⇑f ⁻¹' (↑U : Set ↥Y)) ∅
⊢ f ⁻¹ᵁ U = ⊥

Tactic:
Opens.ext hU'

Premises used: TopologicalSpace.Opens.ext
-- 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 : y ∉ Set.range (ι := ↥X) ⇑f
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hyU : y ∈ (↑U : Set ↥Y)
hU' : Eq (α := Set ↥X) (⇑f ⁻¹' (↑U : Set ↥Y)) ∅
⊢ f ⁻¹ᵁ U = ⊥

Tactic:
exact Opens.ext hU'

Premises used: TopologicalSpace.Opens.ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact (↑V : Set ↥Y)
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
⊢ IsAffine.{u} (↑U : Scheme)

Tactic:
have : IsAffine U.toScheme := hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact (↑V : Set ↥Y)
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this : IsAffine.{u} (↑U : Scheme)
⊢ IsAffine.{u} (↑W : Scheme)

Tactic:
have : IsAffine W.toScheme := hW
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact (↑V : Set ↥Y)
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑W : Scheme)
⊢ CompactSpace.{u} ↥(↑V : Scheme)

Tactic:
have : CompactSpace V := isCompact_iff_compactSpace.mp hV
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact (↑V : Set ↥Y)
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this_1 : IsAffine.{u} (↑U : Scheme)
this_2 : IsAffine.{u} (↑W : Scheme)
this : CompactSpace.{u} ↥(↑V : Scheme)
f' : (↑U : Scheme) ⟶ (↑W : Scheme) := Scheme.Hom.resLE f W U hUW
⊢ Subset (α := Set ↥Z) (Set.range (ι := ↥(↑V : Scheme)) ⇑(V.ι ≫ g)) (Set.range (ι := ↥(↑W : Scheme)) ⇑W.ι)

Tactic:
simpa [Set.range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact (↑V : Set ↥Y)
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this_1 : IsAffine.{u} (↑U : Scheme)
this_2 : IsAffine.{u} (↑W : Scheme)
this : CompactSpace.{u} ↥(↑V : Scheme)
f' : (↑U : Scheme) ⟶ (↑W : Scheme) := Scheme.Hom.resLE f W U hUW
q : (↑V : Scheme) ⟶ (↑W : Scheme) := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
⊢ f' ≫ W.ι = U.ι ≫ f

Tactic:
simp [f']
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact (↑V : Set ↥Y)
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this_1 : IsAffine.{u} (↑U : Scheme)
this_2 : IsAffine.{u} (↑W : Scheme)
this : CompactSpace.{u} ↥(↑V : Scheme)
f' : (↑U : Scheme) ⟶ (↑W : Scheme) := Scheme.Hom.resLE f W U hUW
q : (↑V : Scheme) ⟶ (↑W : Scheme) := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
⊢ q ≫ W.ι = V.ι ≫ g

Tactic:
simp [q]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact (↑V : Set ↥Y)
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this_1 : IsAffine.{u} (↑U : Scheme)
this_2 : IsAffine.{u} (↑W : Scheme)
this : CompactSpace.{u} ↥(↑V : Scheme)
f' : (↑U : Scheme) ⟶ (↑W : Scheme) := Scheme.Hom.resLE f W U hUW
q : (↑V : Scheme) ⟶ (↑W : Scheme) := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
p : pullback f' q ⟶ pullback f g := pullback.map f' q f g U.ι V.ι W.ι ⋯ ⋯
⊢ IsCompact (X := ↥(pullback f g)) (Set.range (ι := ↥(pullback f' q)) ⇑p)

Tactic:
isCompact_range p.continuous

Premises used: isCompact_range, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact (↑V : Set ↥Y)
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this_1 : IsAffine.{u} (↑U : Scheme)
this_2 : IsAffine.{u} (↑W : Scheme)
this : CompactSpace.{u} ↥(↑V : Scheme)
f' : (↑U : Scheme) ⟶ (↑W : Scheme) := Scheme.Hom.resLE f W U hUW
q : (↑V : Scheme) ⟶ (↑W : Scheme) := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
p : pullback f' q ⟶ pullback f g := pullback.map f' q f g U.ι V.ι W.ι ⋯ ⋯
h :
  (↑(pullback.fst f g ⁻¹ᵁ U) : Set ↥(pullback f g)) ⊓ (↑(pullback.snd f g ⁻¹ᵁ V) : Set ↥(pullback f g)) =
    Set.range (ι := ↥(pullback f' q)) ⇑p
⊢ IsCompact ((↑(pullback.fst f g ⁻¹ᵁ U) : Set ↥(pullback f g)) ⊓ (↑(pullback.snd f g ⁻¹ᵁ V) : Set ↥(pullback f g)))

Tactic:
convert! isCompact_range p.continuous

Premises used: isCompact_range, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
U : X.Opens
hU : IsAffineOpen U
V : Y.Opens
hV : IsCompact (↑V : Set ↥Y)
W : Z.Opens
hW : IsAffineOpen W
hUW : U ≤ f ⁻¹ᵁ W
hVW : V ≤ g ⁻¹ᵁ W
this_1 : IsAffine.{u} (↑U : Scheme)
this_2 : IsAffine.{u} (↑W : Scheme)
this : CompactSpace.{u} ↥(↑V : Scheme)
f' : (↑U : Scheme) ⟶ (↑W : Scheme) := Scheme.Hom.resLE f W U hUW
q : (↑V : Scheme) ⟶ (↑W : Scheme) := IsOpenImmersion.lift W.ι (V.ι ≫ g) ⋯
p : pullback f' q ⟶ pullback f g := pullback.map f' q f g U.ι V.ι W.ι ⋯ ⋯
⊢ (↑(pullback.fst f g ⁻¹ᵁ U) : Set ↥(pullback f g)) ⊓ (↑(pullback.snd f g ⁻¹ᵁ V) : Set ↥(pullback f g)) =
    Set.range (ι := ↥(pullback f' q)) ⇑p

Tactic:
simp [p, Scheme.Pullback.range_map]

Premises used: AlgebraicGeometry.Scheme.Pullback.range_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
⊢ IsAffine.{u} (↑U : Scheme)

Tactic:
have : IsAffine U := hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
⊢ IsIso (f ∣_ U) ↔ IsIso (Scheme.Hom.app f U)

Tactic:
(HasAffineProperty.iff_of_isAffine (P := .isomorphisms _)).trans <|
    (and_iff_right (hU.preimage f)).trans ?_

Premises used: and_iff_right, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, Iff.trans, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
refine : IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.app f U)
⊢ IsIso (f ∣_ U) ↔ IsIso (Scheme.Hom.app f U)

Tactic:
refine (HasAffineProperty.iff_of_isAffine (P := .isomorphisms _)).trans <|
    (and_iff_right (hU.preimage f)).trans ?_

Premises used: and_iff_right, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, Iff.trans, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
rw : IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)
⊢ IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.app f U)

Tactic:
rw [Scheme.Hom.app_eq_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.app_eq_appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
simp :
  IsIso (X := Γ((↑U : Scheme), ⊤)) (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ⊤) ⋯) ↔
    IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)
⊢ IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)

Tactic:
simp only [morphismRestrict_app', TopologicalSpace.Opens.map_top]

Premises used: AlgebraicGeometry.morphismRestrict_app', TopologicalSpace.Opens.map_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
a : Γ((↑U : Scheme), ⊤) = Γ(Y, U)
a₁ : Γ((↑(f ⁻¹ᵁ U) : Scheme), ⊤) = Γ(X, f ⁻¹ᵁ U)
a₂ : Γ((↑U : Scheme), ⊤) = Γ(Y, U) → Γ((↑(f ⁻¹ᵁ U) : Scheme), ⊤) = Γ(X, f ⁻¹ᵁ U) → U.ι ''ᵁ ⊤ = U
a₃ : Γ((↑U : Scheme), ⊤) = Γ(Y, U) → Γ((↑(f ⁻¹ᵁ U) : Scheme), ⊤) = Γ(X, f ⁻¹ᵁ U) → (f ⁻¹ᵁ U).ι ''ᵁ ⊤ = f ⁻¹ᵁ U
⊢ IsIso (X := Γ((↑U : Scheme), ⊤)) (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ⊤) ⋯) ↔
    IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)

Tactic:
congr!
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
⊢ Γ((↑U : Scheme), ⊤) = Γ(Y, U)

Tactic:
simp [Scheme.Opens.toScheme_presheaf_obj]

Premises used: AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
⊢ Γ((↑(f ⁻¹ᵁ U) : Scheme), ⊤) = Γ(X, f ⁻¹ᵁ U)

Tactic:
simp [Scheme.Opens.toScheme_presheaf_obj]

Premises used: AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
e_3 : Γ((↑U : Scheme), ⊤) = Γ(Y, U)
e_4 : Γ((↑(f ⁻¹ᵁ U) : Scheme), ⊤) = Γ(X, f ⁻¹ᵁ U)
⊢ U.ι ''ᵁ ⊤ = U

Tactic:
simp [Scheme.Opens.toScheme_presheaf_obj]

Premises used: AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
e_3 : Γ((↑U : Scheme), ⊤) = Γ(Y, U)
e_4 : Γ((↑(f ⁻¹ᵁ U) : Scheme), ⊤) = Γ(X, f ⁻¹ᵁ U)
⊢ (f ⁻¹ᵁ U).ι ''ᵁ ⊤ = f ⁻¹ᵁ U

Tactic:
simp [Scheme.Opens.toScheme_presheaf_obj]

Premises used: AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
mp :
  (∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X) (pullback f₁ f₂)
        (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) →
    ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
mpr :
  (∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)) →
    ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
      [IsOpenImmersion f₁] [IsOpenImmersion f₂],
      (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X) (pullback f₁ f₂)
        (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
⊢ (∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X) (pullback f₁ f₂)
        (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) ↔
    ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], IsAffine.{u} (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
⊢ IsAffine.{u} (↑U : Scheme)

Tactic:
haveI : IsAffine _ := hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], IsAffine.{u} (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this : IsAffine.{u} (↑U : Scheme)
⊢ IsAffine.{u} (↑V : Scheme)

Tactic:
haveI : IsAffine _ := hV
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], IsAffine.{u} (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑V : Scheme)
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
⊢ X.homOfLE ⋯ ≫ V.ι = X.homOfLE ⋯ ≫ U.ι

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], IsAffine.{u} (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑V : Scheme)
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
h :
  ∀ (x : ↥(↑V : Scheme)),
    x ∈ (↑(V.ι ⁻¹ᵁ Scheme.Hom.opensRange U.ι) : Set ↥(↑V : Scheme)) ↔
      x ∈ (↑(Scheme.Hom.opensRange (X := (↑(U ⊓ V) : Scheme)) (X.homOfLE ⋯)) : Set ↥(↑V : Scheme))
⊢ V.ι ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (X := (↑(U ⊓ V) : Scheme)) (X.homOfLE ⋯)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], IsAffine.{u} (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑V : Scheme)
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
x : ↥(↑V : Scheme)
⊢ x ∈ (↑(V.ι ⁻¹ᵁ Scheme.Hom.opensRange U.ι) : Set ↥(↑V : Scheme)) ↔
    x ∈ (↑(Scheme.Hom.opensRange (X := (↑(U ⊓ V) : Scheme)) (X.homOfLE ⋯)) : Set ↥(↑V : Scheme))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], IsAffine.{u} (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑V : Scheme)
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
⊢ IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) U.ι V.ι

Tactic:
have := IsOpenImmersion.isPullback (X.homOfLE inf_le_left) (X.homOfLE inf_le_right)
      U.ι V.ι (by simp) (by ext; simp)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], IsAffine.{u} (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this_1 : IsAffine.{u} (↑U : Scheme)
this_2 : IsAffine.{u} (↑V : Scheme)
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
this : IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) U.ι V.ι
⊢ IsAffineOpen (U ⊓ V)

Tactic:
.of_isIso this.isoPullback.hom

Premises used: AlgebraicGeometry.IsAffine.of_isIso, AlgebraicGeometry.IsAffineOpen, CategoryTheory.IsPullback.isoPullback, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [IsAffine U₁] [IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂], IsAffine.{u} (pullback f₁ f₂)
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
this_1 : IsAffine.{u} (↑U : Scheme)
this_2 : IsAffine.{u} (↑V : Scheme)
g : pullback U.ι V.ι ⟶ X := pullback.fst U.ι V.ι ≫ U.ι
this : IsPullback (X.homOfLE ⋯) (X.homOfLE ⋯) U.ι V.ι
⊢ IsAffineOpen (U ⊓ V)

Tactic:
exact .of_isIso this.isoPullback.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
⊢ IsAffineOpen (Scheme.Hom.opensRange f₁ ⊓ Scheme.Hom.opensRange f₂)

Tactic:
H _ _ (isAffineOpen_opensRange f₁) (isAffineOpen_opensRange f₂)

Premises used: AlgebraicGeometry.isAffineOpen_opensRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
h :
  Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁) =
    Scheme.Hom.opensRange f₁ ⊓ Scheme.Hom.opensRange f₂
⊢ IsAffineOpen (Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁))

Tactic:
convert! H _ _ (isAffineOpen_opensRange f₁) (isAffineOpen_opensRange f₂) using 1

Premises used: AlgebraicGeometry.isAffineOpen_opensRange