awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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
⊢ (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
      IsAffine X).RespectsIso
have respectsIso₁ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [IsAffine Y], IsAffine X → IsAffine X
Tactic: apply AffineTargetMorphismProperty.respectsIso_mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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 (f ⁻¹ᵁ Y.basicOpen r)
have 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))
Tactic: rw [Scheme.preimage_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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)
⊢ IsAffine X
have 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)) ⊤)
Tactic: apply_fun Ideal.map (f.appTop).hom at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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)) ⊤)
⊢ IsAffine X
have 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))))
  ⊤
Tactic: rw [Ideal.map_span, Ideal.map_top] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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))))
    ⊤
⊢ IsAffine X
have 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)
Tactic: apply isAffine_of_isAffineOpen_basicOpen _ hS
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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 : (↑Γ(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)
have this : ∀ (i : ↥S), IsAffineOpen (f ⁻¹ᵁ Y.basicOpen (↑i : (↑Γ(Y, ⊤) : Type u_1)))
Tactic: have : ∀ i : S, IsAffineOpen (f ⁻¹ᵁ Y.basicOpen i.1) := hS'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ @IsAffineHom = targetAffineLocally fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X
have 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
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
⊢ IsAffineHom f ↔ targetAffineLocally (fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X) f
have h : (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ↔
  ∀ (a : Y.Opens) (b : IsAffineOpen a), IsAffine.{u_1} (↑(f ⁻¹ᵁ a) : Scheme)
Tactic: simp only [targetAffineLocally, Scheme.affineOpens, Set.coe_setOf, Set.mem_setOf_eq,
      Subtype.forall, isAffineHom_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @IsAffineHom
have hP' : AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  IsAffine X
Tactic: apply HasAffineProperty.isStableUnderBaseChange
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    IsAffine X
have 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)
Tactic: apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥Y), ∃ (U : Y.Opens), x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ IsAffineHom f
have 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
Tactic: choose U hxU hU hfU using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
⊢ IsAffineHom f
have rw : ∀ (i : ↥Y),
  IsAffine.{u} (↑(f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U i) sorry) : Y.Opens)) : Scheme)
Tactic: rw [HasAffineProperty.iff_of_iSup_eq_top (P := @IsAffineHom) fun i ↦ ⟨U i, hU i⟩]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
⊢ IsAffineHom f
have rw₁ : Eq.{u + 1} (α := Y.Opens) (⨆ (i : ↥Y), (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) (U i) sorry) : Y.Opens)) ⊤
Tactic: rw [HasAffineProperty.iff_of_iSup_eq_top (P := @IsAffineHom) fun i ↦ ⟨U i, hU i⟩]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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
⊢ IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop fst) (Scheme.Hom.appTop snd)
have this : IsAffine P
Tactic: have : IsAffine P := .of_isPullback h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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
⊢ IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop fst) (Scheme.Hom.appTop snd)
have 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)
Tactic: have : IsPullback (AffineScheme.ofHom fst) (AffineScheme.ofHom snd) (AffineScheme.ofHom f)
      (AffineScheme.ofHom g) :=
    IsPullback.of_map_of_faithful AffineScheme.forgetToScheme.{u} h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
have refine : ∀ (W : X.Opens) (hW : IsAffineOpen W), IsAffineOpen (X := U ⨿ V) (coprod.desc f g ⁻¹ᵁ W)
Tactic: refine ⟨fun W hW ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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
⊢ IsAffineOpen (X := U ⨿ V) (coprod.desc f g ⁻¹ᵁ W)
have this : IsAffine.{u} (↑(f ⁻¹ᵁ W) : Scheme)
Tactic: have : IsAffine (f ⁻¹ᵁ W).toScheme := hW.preimage f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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)
⊢ IsAffineOpen (X := U ⨿ V) (coprod.desc f g ⁻¹ᵁ W)
have this₁ : IsAffine.{u} (↑(g ⁻¹ᵁ W) : Scheme)
Tactic: have : IsAffine (g ⁻¹ᵁ W).toScheme := hW.preimage g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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 (X := U ⨿ V) (coprod.desc f g ⁻¹ᵁ W)
have h : coprod.desc f g ⁻¹ᵁ W = Scheme.Hom.opensRange i
Tactic: convert! isAffineOpen_opensRange i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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).ι
⊢ coprod.desc f g ⁻¹ᵁ W = Scheme.Hom.opensRange i
have h : coprod.desc f g ⁻¹ᵁ W ≤ Scheme.Hom.opensRange i
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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
⊢ coprod.desc f g ⁻¹ᵁ W = Scheme.Hom.opensRange i
have h₁ : Scheme.Hom.opensRange i ≤ coprod.desc f g ⁻¹ᵁ W
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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
⊢ x ∈ Scheme.Hom.opensRange i
have 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))
Tactic: obtain ⟨(x | x), rfl⟩ := (coprodMk U V).surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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))
⊢ x ∈ Scheme.Hom.opensRange i
have 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))
Tactic: obtain ⟨(x | x), rfl⟩ := (coprodMk U V).surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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 (α := ↥(U ⨿ V)) (Scheme.Hom.opensRange i)
    ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inl x) : ↥(U ⨿ V))
have hx₁ : Membership.mem (α := ↥X) W (f x : ↥X)
Tactic: replace hx : f x ∈ W := by simpa [← Scheme.Hom.comp_apply] using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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 (α := ↥(U ⨿ V)) (Scheme.Hom.opensRange i)
    ((coprodMk U V : (a : ↥U ⊕ ↥V) → ↥(U ⨿ V)) (Sum.inr x) : ↥(U ⨿ V))
have hx₁ : Membership.mem (α := ↥X) W (g x : ↥X)
Tactic: replace hx : g x ∈ W := by simpa [← Scheme.Hom.comp_apply] using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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))
⊢ Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W) (i x : ↥(U ⨿ V))
have 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))
Tactic: obtain ⟨(⟨x, hx⟩ | ⟨x, hx⟩), rfl⟩ := (coprodMk _ _).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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))
⊢ Membership.mem (α := ↥(U ⨿ V)) (γ := Opens ↥(U ⨿ V)) (coprod.desc f g ⁻¹ᵁ W) (i x : ↥(U ⨿ V))
have 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))
Tactic: obtain ⟨(⟨x, hx⟩ | ⟨x, hx⟩), rfl⟩ := (coprodMk _ _).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing (X := ↥X) (Y := ↥Y) ⇑f
hf₂ : IsClosed (X := ↥Y) (Set.range (ι := ↥X) ⇑f)
⊢ IsAffineHom f
have H : ∀ (x : ↥Y), ∃ (U : Y.Opens), x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
Tactic: apply isAffineHom_of_forall_exists_isAffineOpen
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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
⊢ ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
have pos : ∀ (hy : Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥X) ⇑f) y),
  ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
Tactic: by_cases hy : y ∈ Set.range f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
⊢ ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
have neg : ∀ (hy : y ∉ Set.range (ι := ↥X) ⇑f), ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
Tactic: by_cases hy : y ∈ Set.range f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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
⊢ ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
have pos : ∀ (x : ↥X), ∃ (U : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
Tactic: obtain ⟨x, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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 : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
have 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)
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
have 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)
Tactic: obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).isOpen
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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' ≤ U, f ⁻¹ᵁ U' = V
have obtain : ∀ (U' : Set ↥Y) (hU' : IsOpen U') (e : ⇑f ⁻¹' U' = V.carrier), ∃ U' ≤ U, f ⁻¹ᵁ U' = V
Tactic: obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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 : Y.Opens), Membership.mem (α := ↥Y) U (f x : ↥Y) ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
have 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)
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)⟩
Cleared hypotheses: V, hV, hxV, hVU