awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace.{u} ↥X
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
⊢ IsCompact.{u} (X := ↥X) (⋃ i ∈ s', (↑(X.basicOpen i) : Set ↥X))
have apply : ∀ i ∈ s', IsCompact (↑(X.basicOpen i) : Set ↥X)
Tactic: apply s'.isCompact_biUnion
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (hypothesis)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace.{u} ↥X
⊢ IsAffine X
have this₁ : CompactSpace.{u} ↥X
Tactic: have : CompactSpace X := by
    obtain ⟨s', hs', e⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
    rw [← isCompact_univ_iff, ← Opens.coe_top, ← iSup_basicOpen_of_span_eq_top _ _ e]
    simp only [Finset.mem_coe, Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk]
    apply s'.isCompact_biUnion
    exact fun i hi ↦ (hs₂ _ (hs' hi)).isCompact
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
⊢ IsAffine X
have affine : IsIso X.toSpecΓ
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
⊢ IsIso X.toSpecΓ
have affine : ∀ (i : (↑s : Type u)),
  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens
    (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)))
Tactic: refine HasAffineProperty.of_iSup_eq_top (P := MorphismProperty.isomorphisms Scheme)
    (fun i : s ↦ ⟨PrimeSpectrum.basicOpen i.1, ?_⟩) ?_ (fun i ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
affine :
  ∀ (i : (↑s : Type u)),
    Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens
      (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)))
⊢ IsIso X.toSpecΓ
have affine₁ : Eq.{u + 1} (α := (Spec Γ(X, ⊤)).Opens)
  (⨆ (i : (↑s : Type u)),
    (↑((fun (i : (↑s : Type u)) ↦
            (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) sorry :
              { x : (Spec Γ(X, ⊤)).Opens //
                Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
          i) :
      (Spec Γ(X, ⊤)).Opens))
  ⊤
Tactic: refine HasAffineProperty.of_iSup_eq_top (P := MorphismProperty.isomorphisms Scheme)
    (fun i : s ↦ ⟨PrimeSpectrum.basicOpen i.1, ?_⟩) ?_ (fun i ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
affine :
  ∀ (i : (↑s : Type u)),
    Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens
      (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)))
affine₁ :
  Eq.{u + 1} (α := (Spec Γ(X, ⊤)).Opens)
    (⨆ (i : (↑s : Type u)),
      (↑((fun (i : (↑s : Type u)) ↦
              (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                  (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                { x : (Spec Γ(X, ⊤)).Opens //
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
            i) :
        (Spec Γ(X, ⊤)).Opens))
    ⊤
⊢ IsIso X.toSpecΓ
have affine₂ : ∀ (i : (↑s : Type u)),
  IsAffine.{u}
    (↑(X.toSpecΓ ⁻¹ᵁ
          (↑((fun (i : (↑s : Type u)) ↦
                  (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                      Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                      (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) sorry :
                    { x : (Spec Γ(X, ⊤)).Opens //
                      Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
                i) :
            (Spec Γ(X, ⊤)).Opens)) :
      Scheme)
Tactic: refine HasAffineProperty.of_iSup_eq_top (P := MorphismProperty.isomorphisms Scheme)
    (fun i : s ↦ ⟨PrimeSpectrum.basicOpen i.1, ?_⟩) ?_ (fun i ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
affine :
  ∀ (i : (↑s : Type u)),
    Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens
      (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)))
affine₁ :
  Eq.{u + 1} (α := (Spec Γ(X, ⊤)).Opens)
    (⨆ (i : (↑s : Type u)),
      (↑((fun (i : (↑s : Type u)) ↦
              (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                  (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                { x : (Spec Γ(X, ⊤)).Opens //
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
            i) :
        (Spec Γ(X, ⊤)).Opens))
    ⊤
affine₂ :
  ∀ (i : (↑s : Type u)),
    IsAffine.{u}
      (↑(X.toSpecΓ ⁻¹ᵁ
            (↑((fun (i : (↑s : Type u)) ↦
                    (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                        Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                        (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                      { x : (Spec Γ(X, ⊤)).Opens //
                        Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
                  i) :
              (Spec Γ(X, ⊤)).Opens)) :
        Scheme)
⊢ IsIso X.toSpecΓ
have affine₃ : ∀ (i : (↑s : Type u)),
  IsIso (X :=
    Γ((↑(↑((fun (i : (↑s : Type u)) ↦ ⟨PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)), sorry⟩) i) :
            (Spec Γ(X, ⊤)).Opens) :
        Scheme),
      ⊤))
    (Scheme.Hom.appTop
      (X.toSpecΓ ∣_
        (↑((fun (i : (↑s : Type u)) ↦
                (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                    Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                    (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) sorry :
                  { x : (Spec Γ(X, ⊤)).Opens //
                    Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
              i) :
          (Spec Γ(X, ⊤)).Opens)))
Tactic: refine HasAffineProperty.of_iSup_eq_top (P := MorphismProperty.isomorphisms Scheme)
    (fun i : s ↦ ⟨PrimeSpectrum.basicOpen i.1, ?_⟩) ?_ (fun i ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsAffineOpen.{u} (X := Spec Γ(X, ⊤)) (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)))
have affine : IsAffineOpen.{u} (X := Spec Γ(X, ⊤))
  ((Spec Γ(X, ⊤)).basicOpen (U := ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (Scheme.ΓSpecIso Γ(X, ⊤))) :
        (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
      (↑i : (↑Γ(X, ⊤) : Type u))))
Tactic: simp only [← basicOpen_eq_of_affine]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
⊢ Eq.{u + 1} (α := (Spec Γ(X, ⊤)).Opens)
    (⨆ (i : (↑s : Type u)),
      (↑((fun (i : (↑s : Type u)) ↦
              (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                  (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                { x : (Spec Γ(X, ⊤)).Opens //
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
            i) :
        (Spec Γ(X, ⊤)).Opens))
    ⊤
have affine : Eq.{u + 1} (α := Ideal (↑Γ(X, ⊤) : Type u))
  (Ideal.span (Set.range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : (↑Γ(X, ⊤) : Type u)) ↦ x ∈ s)))) ⊤
Tactic: rw [PrimeSpectrum.iSup_basicOpen_eq_top_iff, Subtype.range_coe_subtype, Set.setOf_mem_eq, hs]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
affine :
  Eq.{u + 1} (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span (Set.range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : (↑Γ(X, ⊤) : Type u)) ↦ x ∈ s)))) ⊤
⊢ Eq.{u + 1} (α := (Spec Γ(X, ⊤)).Opens)
    (⨆ (i : (↑s : Type u)),
      (↑((fun (i : (↑s : Type u)) ↦
              (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                  (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                { x : (Spec Γ(X, ⊤)).Opens //
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
            i) :
        (Spec Γ(X, ⊤)).Opens))
    ⊤
have affine₁ : Eq.{u + 1} (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span {x : (↑Γ(X, ⊤) : Type u) | x ∈ s}) ⊤
Tactic: rw [PrimeSpectrum.iSup_basicOpen_eq_top_iff, Subtype.range_coe_subtype, Set.setOf_mem_eq, hs]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
affine :
  Eq.{u + 1} (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span (Set.range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : (↑Γ(X, ⊤) : Type u)) ↦ x ∈ s)))) ⊤
affine₁ : Eq.{u + 1} (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span {x : (↑Γ(X, ⊤) : Type u) | x ∈ s}) ⊤
affine₂ : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
⊢ Eq.{u + 1} (α := (Spec Γ(X, ⊤)).Opens)
    (⨆ (i : (↑s : Type u)),
      (↑((fun (i : (↑s : Type u)) ↦
              (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                  (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                { x : (Spec Γ(X, ⊤)).Opens //
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
            i) :
        (Spec Γ(X, ⊤)).Opens))
    ⊤
have affine₃ : Eq.{u + 1} (α := Ideal (↑Γ(X, ⊤) : Type u)) ⊤ ⊤
Tactic: rw [PrimeSpectrum.iSup_basicOpen_eq_top_iff, Subtype.range_coe_subtype, Set.setOf_mem_eq, hs]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsAffine.{u}
    (↑(X.toSpecΓ ⁻¹ᵁ
          (↑((fun (i : (↑s : Type u)) ↦
                  (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                      Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                      (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                    { x : (Spec Γ(X, ⊤)).Opens //
                      Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
                i) :
            (Spec Γ(X, ⊤)).Opens)) :
      Scheme)
have affine : IsAffine.{u} (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme)
Tactic: rw [Scheme.toSpecΓ_preimage_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsIso (X :=
    Γ((↑(↑((fun (i : (↑s : Type u)) ↦ ⟨PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)), ⋯⟩) i) :
            (Spec Γ(X, ⊤)).Opens) :
        Scheme),
      ⊤))
    (Scheme.Hom.appTop
      (X.toSpecΓ ∣_
        (↑((fun (i : (↑s : Type u)) ↦
                (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                    Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                    (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                  { x : (Spec Γ(X, ⊤)).Opens //
                    Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
              i) :
          (Spec Γ(X, ⊤)).Opens)))
have affine : IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
  (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤) ≫
    X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: simp only [Opens.map_top, morphismRestrict_app]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
    (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have affine : IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
  (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤))
Tactic: refine IsIso.comp_isIso' ?_ inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
    (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤))
have a : IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
    (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤)) ↔
  IsIso (X := Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))))
    (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))))
Tactic: convert! isIso_ΓSpec_adjunction_unit_app_basicOpen i.1 using 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
⊢ IsAffineOpen U
have hs₁ : Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u))
  (Ideal.span
    ((⇑(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)) ''
      s))
  ⊤
Tactic: apply isAffine_of_isAffineOpen_basicOpen (U.topIso.inv '' s)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
hs₁ :
  Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u))
    (Ideal.span
      ((⇑(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)) ''
        s))
    ⊤
⊢ IsAffineOpen U
have hs₃ : ∀ (i : (↑Γ((↑U : Scheme), ⊤) : Type u)),
  Membership.mem (γ := Set (↑Γ((↑U : Scheme), ⊤) : 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)) ''
        s)
      i →
    IsAffineOpen ((↑U : Scheme).basicOpen i)
Tactic: apply isAffine_of_isAffineOpen_basicOpen (U.topIso.inv '' s)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
⊢ Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u))
    (Ideal.span
      ((⇑(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)) ''
        s))
    ⊤
have hs₁ : Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u)) (Ideal.map (CommRingCat.Hom.hom U.topIso.inv) (Ideal.span s)) ⊤
Tactic: rw [← Ideal.map_span U.topIso.inv.hom, hs, Ideal.map_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
hs₁ : Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u)) (Ideal.map (CommRingCat.Hom.hom U.topIso.inv) (Ideal.span s)) ⊤
⊢ Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u))
    (Ideal.span
      ((⇑(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)) ''
        s))
    ⊤
have hs₃ : Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u))
  (Ideal.map (R := (↑Γ(X, U) : Type u)) (CommRingCat.Hom.hom U.topIso.inv) ⊤) ⊤
Tactic: rw [← Ideal.map_span U.topIso.inv.hom, hs, Ideal.map_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
hs₁ : Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u)) (Ideal.map (CommRingCat.Hom.hom U.topIso.inv) (Ideal.span s)) ⊤
hs₃ :
  Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u))
    (Ideal.map (R := (↑Γ(X, U) : Type u)) (CommRingCat.Hom.hom U.topIso.inv) ⊤) ⊤
⊢ Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u))
    (Ideal.span
      ((⇑(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)) ''
        s))
    ⊤
have hs₄ : Eq.{u + 1} (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u)) ⊤ ⊤
Tactic: rw [← Ideal.map_span U.topIso.inv.hom, hs, Ideal.map_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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.{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))
have 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))))
Tactic: rw [← (Scheme.Opens.ι _).isAffineOpen_iff_of_isOpenImmersion, Scheme.image_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X
have respectsIso : (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    IsAffine X).RespectsIso
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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
⊢ AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
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)
⊢ AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (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 : X ≅ Y) (f : Y ⟶ Z) [IsAffine Z], IsAffine Y → IsAffine X
Tactic: apply AffineTargetMorphismProperty.respectsIso_mk