awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
have 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)
Tactic: obtain ⟨r, hrU', hxr⟩ := hU.exists_basicOpen_le ⟨f x, hxV⟩ hxU
-- 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
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)
have pos : IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r)
Tactic: refine ⟨_, hxr, hU.basicOpen r, ?_⟩
-- 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
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 (f ⁻¹ᵁ Y.basicOpen r)
have 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)))
Tactic: convert! hV.basicOpen (f.app _ (Y.presheaf.map (homOfLE hU'U).op r)) using 1
-- 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
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)
⊢ 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)))
have 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)
Tactic: simp only [Scheme.preimage_basicOpen, ← CommRingCat.comp_apply, f.naturality]
-- 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 : y ∉ Set.range (ι := ↥X) ⇑f
⊢ ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
have 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)
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hyU, hU'⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open hy hf₂.isOpen_compl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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)ᶜ
⊢ ∃ (U : Y.Opens), y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
have hU'₁ : Eq (α := Set ↥X) (⇑f ⁻¹' (↑U : Set ↥Y)) ∅
Tactic: rw [Set.subset_compl_iff_disjoint_right, ← Set.preimage_eq_empty_iff] at hU'
Cleared hypotheses: hU'
-- 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 : 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)
have neg : IsAffineOpen (f ⁻¹ᵁ U)
Tactic: refine ⟨U, hyU, hU, ?_⟩
-- 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 : 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 (f ⁻¹ᵁ U)
have h : f ⁻¹ᵁ U = ⊥
Tactic: convert! isAffineOpen_bot _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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
⊢ IsCompact ((↑(pullback.fst f g ⁻¹ᵁ U) : Set ↥(pullback f g)) ⊓ (↑(pullback.snd f g ⁻¹ᵁ V) : Set ↥(pullback f g)))
have this : IsAffine.{u} (↑U : Scheme)
Tactic: have : IsAffine U.toScheme := hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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)
⊢ IsCompact ((↑(pullback.fst f g ⁻¹ᵁ U) : Set ↥(pullback f g)) ⊓ (↑(pullback.snd f g ⁻¹ᵁ V) : Set ↥(pullback f g)))
have this₁ : IsAffine.{u} (↑W : Scheme)
Tactic: have : IsAffine W.toScheme := hW
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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)
⊢ IsCompact ((↑(pullback.fst f g ⁻¹ᵁ U) : Set ↥(pullback f g)) ⊓ (↑(pullback.snd f g ⁻¹ᵁ V) : Set ↥(pullback f g)))
have this₁ : CompactSpace.{u} ↥(↑V : Scheme)
Tactic: have : CompactSpace V := isCompact_iff_compactSpace.mp hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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 ((↑(pullback.fst f g ⁻¹ᵁ U) : Set ↥(pullback f g)) ⊓ (↑(pullback.snd f g ⁻¹ᵁ V) : Set ↥(pullback f g)))
have 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
Tactic: convert! isCompact_range p.continuous
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
⊢ IsIso (f ∣_ U) ↔ IsIso (Scheme.Hom.app f U)
have this : IsAffine.{u} (↑U : Scheme)
Tactic: have : IsAffine U := hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
have refine : IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.app f U)
Tactic: refine (HasAffineProperty.iff_of_isAffine (P := .isomorphisms _)).trans <|
    (and_iff_right (hU.preimage f)).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
⊢ IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.app f U)
have rw : IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry)
Tactic: rw [Scheme.Hom.app_eq_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
⊢ IsIso (Scheme.Hom.appTop (f ∣_ U)) ↔ IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)
have simp : IsIso (X := Γ((↑U : Scheme), ⊤)) (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ⊤) sorry) ↔
  IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) sorry)
Tactic: simp only [morphismRestrict_app', TopologicalSpace.Opens.map_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
U : Y.Opens
hU : IsAffineOpen U
this : IsAffine.{u} (↑U : Scheme)
⊢ IsIso (X := Γ((↑U : Scheme), ⊤)) (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ⊤) ⋯) ↔
    IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)
have a : Γ((↑U : Scheme), ⊤) = Γ(Y, U)
Tactic: congr!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
⊢ IsIso (X := Γ((↑U : Scheme), ⊤)) (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ⊤) ⋯) ↔
    IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)
have a₁ : Γ((↑(f ⁻¹ᵁ U) : Scheme), ⊤) = Γ(X, f ⁻¹ᵁ U)
Tactic: congr!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
⊢ IsIso (X := Γ((↑U : Scheme), ⊤)) (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ⊤) ⋯) ↔
    IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)
have a₂ : Γ((↑U : Scheme), ⊤) = Γ(Y, U) → Γ((↑(f ⁻¹ᵁ U) : Scheme), ⊤) = Γ(X, f ⁻¹ᵁ U) → U.ι ''ᵁ ⊤ = U
Tactic: congr!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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
⊢ IsIso (X := Γ((↑U : Scheme), ⊤)) (Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) ((f ⁻¹ᵁ U).ι ''ᵁ ⊤) ⋯) ↔
    IsIso (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯)
have a₃ : Γ((↑U : Scheme), ⊤) = Γ(Y, U) → Γ((↑(f ⁻¹ᵁ U) : Scheme), ⊤) = Γ(X, f ⁻¹ᵁ U) → (f ⁻¹ᵁ U).ι ''ᵁ ⊤ = f ⁻¹ᵁ U
Tactic: congr!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃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)
have 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) sorry) →
  ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
⊢ (∀ ⦃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)
have 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) sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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
⊢ IsAffineOpen (U ⊓ V)
have this : IsAffine.{u} (↑U : Scheme)
Tactic: haveI : IsAffine _ := hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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)
⊢ IsAffineOpen (U ⊓ V)
have this₁ : IsAffine.{u} (↑V : Scheme)
Tactic: haveI : IsAffine _ := hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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.ι
⊢ V.ι ⁻¹ᵁ Scheme.Hom.opensRange U.ι = Scheme.Hom.opensRange (X := (↑(U ⊓ V) : Scheme)) (X.homOfLE ⋯)
have h : ∀ (x : ↥(↑V : Scheme)),
  x ∈ (↑(V.ι ⁻¹ᵁ Scheme.Hom.opensRange U.ι) : Set ↥(↑V : Scheme)) ↔
    x ∈ (↑(Scheme.Hom.opensRange (X := (↑(U ⊓ V) : Scheme)) (X.homOfLE sorry)) : Set ↥(↑V : Scheme))
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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.ι
⊢ IsAffineOpen (U ⊓ V)
have this₁ : IsPullback (X.homOfLE sorry) (X.homOfLE sorry) U.ι V.ι
Tactic: have := IsOpenImmersion.isPullback (X.homOfLE inf_le_left) (X.homOfLE inf_le_right)
      U.ι V.ι (by simp) (by ext; simp)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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 (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁))
have h : Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁) =
  Scheme.Hom.opensRange f₁ ⊓ Scheme.Hom.opensRange f₂
Tactic: convert! H _ _ (isAffineOpen_opensRange f₁) (isAffineOpen_opensRange f₂) using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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₂
⊢ IsAffine.{u} (pullback f₁ f₂)
have this : IsAffineOpen (Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁))
Tactic: have : IsAffineOpen (pullback.fst f₁ f₂ ≫ f₁).opensRange := by
      convert! H _ _ (isAffineOpen_opensRange f₁) (isAffineOpen_opensRange f₂) using 1
      exact Opens.ext (IsOpenImmersion.range_pullback_to_base_of_left _ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
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₂
this : IsAffineOpen (Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁))
⊢ IsAffine.{u} (pullback f₁ f₂)
have this₁ : IsAffine.{u} (↑(Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁)) : Scheme)
Tactic: change IsAffine _ at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsAffineHom (Y := pullback.diagonalObj f) (pullback.diagonal f) ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
have refine : targetAffineLocally
    (AffineTargetMorphismProperty.diagonal fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X) f ↔
  ∀ (U : Y.Opens),
    IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
Tactic: refine congr($(HasAffineProperty.eq_targetAffineLocally
    (.diagonal @IsAffineHom)) f).to_iff.trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally
      (AffineTargetMorphismProperty.diagonal fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X) f ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
have simp : (∀ (a : Y.Opens) (b : IsAffineOpen a) (a_1 : X.Opens) (b : a_1 ≤ f ⁻¹ᵁ a) (a_2 : X.Opens) (b : a_2 ≤ f ⁻¹ᵁ a),
    IsAffineOpen (f ⁻¹ᵁ a ⊓ a_1) → IsAffineOpen (f ⁻¹ᵁ a ⊓ a_2) → IsAffineOpen (f ⁻¹ᵁ a ⊓ (a_1 ⊓ a_2))) ↔
  ∀ (U : Y.Opens),
    IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
Tactic: simp only [targetAffineLocally, diagonal_isAffine_iff_forall_isAffineOpen_inf,
    (IsOpenImmersion.opensEquiv (f ⁻¹ᵁ _).ι).forall_congr_left, Scheme.affineOpens,
    Subtype.forall, Set.mem_setOf_eq, Scheme.Opens.opensRange_ι, ← Scheme.Hom.preimage_inf,
    IsOpenImmersion.opensEquiv_symm_apply, Scheme.Hom.image_preimage_eq_opensRange_inf,
    ← Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion (Scheme.Opens.ι _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (a : Y.Opens) (b : IsAffineOpen a) (a_1 : X.Opens) (b : a_1 ≤ f ⁻¹ᵁ a) (a_2 : X.Opens) (b : a_2 ≤ f ⁻¹ᵁ a),
      IsAffineOpen (f ⁻¹ᵁ a ⊓ a_1) → IsAffineOpen (f ⁻¹ᵁ a ⊓ a_2) → IsAffineOpen (f ⁻¹ᵁ a ⊓ (a_1 ⊓ a_2))) ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
have a : ∀ (U : Y.Opens) (hU : IsAffineOpen U) (V₁ : X.Opens) (hV₁ : V₁ ≤ f ⁻¹ᵁ U) (V₂ : X.Opens) (hV₂ : V₂ ≤ f ⁻¹ᵁ U),
  IsAffineOpen (f ⁻¹ᵁ U ⊓ V₁) → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
Tactic: congr! with U hU V₁ hV₁ V₂ hV₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V₁ : X.Opens
hV₁ : V₁ ≤ f ⁻¹ᵁ U
V₂ : X.Opens
hV₂ : V₂ ≤ f ⁻¹ᵁ U
⊢ IsAffineOpen (f ⁻¹ᵁ U ⊓ V₁) → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
have a : IsAffineOpen V₁ → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
  IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
Tactic: rw [inf_eq_right.mpr hV₁, inf_eq_right.mpr hV₂, inf_eq_right.mpr (inf_le_left.trans hV₁)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V₁ : X.Opens
hV₁ : V₁ ≤ f ⁻¹ᵁ U
V₂ : X.Opens
hV₂ : V₂ ≤ f ⁻¹ᵁ U
a :
  IsAffineOpen V₁ → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
⊢ IsAffineOpen (f ⁻¹ᵁ U ⊓ V₁) → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
have a₁ : IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
  IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
Tactic: rw [inf_eq_right.mpr hV₁, inf_eq_right.mpr hV₂, inf_eq_right.mpr (inf_le_left.trans hV₁)]