awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
s : Set (↑M : Type u)
hs : Eq (α := Submodule (↑R : Type u) (↑M : Type u)) (Submodule.span (↑R : Type u) s) ⊤
t : Set ((↑s : Type u) →₀ (↑R : Type u))
ht :
  Submodule.span (↑R : Type u) t =
    LinearMap.ker (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)))
H₁ :
  Function.Exact (M := (↑(ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) : Type u)) (N :=
    (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u)) (P :=
    (↑(ModuleCat.of (↑R : Type u) (↑M : Type u)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
          LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) (Y :=
          ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u)))
          (ModuleCat.ofHom
            (Finsupp.linearCombination (↑R : Type u)
              (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t))))) :
      (a : (↑(ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) : Type u)) →
        (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
          LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) (Y :=
          ModuleCat.of (↑R : Type u) (↑M : Type u))
          (ModuleCat.ofHom
            (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s))))) :
      (a : (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u)) →
        (↑(ModuleCat.of (↑R : Type u) (↑M : Type u)) : Type u))
⊢ Eq.{u + 1} (α := tilde (ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) ⟶ tilde M)
    (CategoryStruct.comp (Y := tilde (ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))))
      (tilde.map
        (ModuleCat.ofHom
          (Finsupp.linearCombination (↑R : Type u)
            (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t)))))
      (tilde.map
        (ModuleCat.ofHom
          (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s))))))
    0
have rw : Eq (α := tilde (ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) ⟶ tilde M)
  (tilde.map
    (ModuleCat.ofHom
      (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)) ∘ₗ
        Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t)))))
  0
Tactic: rw [← tilde.map_comp, ← ModuleCat.ofHom_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
s : Set (↑M : Type u)
hs : Eq (α := Submodule (↑R : Type u) (↑M : Type u)) (Submodule.span (↑R : Type u) s) ⊤
t : Set ((↑s : Type u) →₀ (↑R : Type u))
ht :
  Submodule.span (↑R : Type u) t =
    LinearMap.ker (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)))
H₁ :
  Function.Exact (M := (↑(ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) : Type u)) (N :=
    (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u)) (P :=
    (↑(ModuleCat.of (↑R : Type u) (↑M : Type u)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
          LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) (Y :=
          ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u)))
          (ModuleCat.ofHom
            (Finsupp.linearCombination (↑R : Type u)
              (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t))))) :
      (a : (↑(ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) : Type u)) →
        (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
          LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) (Y :=
          ModuleCat.of (↑R : Type u) (↑M : Type u))
          (ModuleCat.ofHom
            (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s))))) :
      (a : (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u)) →
        (↑(ModuleCat.of (↑R : Type u) (↑M : Type u)) : Type u))
⊢ Eq (α := tilde (ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) ⟶ tilde M)
    (tilde.map
      (ModuleCat.ofHom
        (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)) ∘ₗ
          Finsupp.linearCombination (↑R : Type u)
            (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t)))))
    0
have h : Eq (α := ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u)) ⟶ M)
  (ModuleCat.ofHom
    (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)) ∘ₗ
      Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t))))
  0
Tactic: convert! tilde.map_zero
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
s : Set (↑M : Type u)
hs : Eq (α := Submodule (↑R : Type u) (↑M : Type u)) (Submodule.span (↑R : Type u) s) ⊤
t : Set ((↑s : Type u) →₀ (↑R : Type u))
ht :
  Submodule.span (↑R : Type u) t =
    LinearMap.ker (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)))
H₁ :
  Function.Exact (M := (↑(ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) : Type u)) (N :=
    (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u)) (P :=
    (↑(ModuleCat.of (↑R : Type u) (↑M : Type u)) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
          LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) (Y :=
          ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u)))
          (ModuleCat.ofHom
            (Finsupp.linearCombination (↑R : Type u)
              (Subtype.val (p := fun (x : (↑s : Type u) →₀ (↑R : Type u)) ↦ x ∈ t))))) :
      (a : (↑(ModuleCat.of (↑R : Type u) ((↑t : Type u) →₀ (↑R : Type u))) : Type u)) →
        (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
          LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X := ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) (Y :=
          ModuleCat.of (↑R : Type u) (↑M : Type u))
          (ModuleCat.ofHom
            (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s))))) :
      (a : (↑(ModuleCat.of (↑R : Type u) ((↑s : Type u) →₀ (↑R : Type u))) : Type u)) →
        (↑(ModuleCat.of (↑R : Type u) (↑M : Type u)) : Type u))
⊢ SheafOfModules.Presentation (tilde M)
have refine : IsColimit
  (CokernelCofork.ofπ
    (Iso.inv (tildeFinsupp (↑s : Type u)) ≫
      tilde.map
        (ModuleCat.ofHom
          (Finsupp.linearCombination (↑R : Type u) (Subtype.val (p := fun (x : (↑M : Type u)) ↦ x ∈ s)))))
    sorry)
Tactic: refine SheafOfModules.presentationOfIsCokernelFree.{u}
      ((tildeFinsupp t).inv ≫ tilde.map (ModuleCat.ofHom (Finsupp.linearCombination R (↑))) ≫
        (tildeFinsupp s).hom) ((tildeFinsupp s).inv ≫
          tilde.map (ModuleCat.ofHom (Finsupp.linearCombination R (↑)))) (by
    simp only [Category.assoc, Iso.hom_inv_id_assoc, Preadditive.IsIso.comp_left_eq_zero]
    rw [← tilde.map_comp, ← ModuleCat.ofHom_comp]
    convert! tilde.map_zero
    exact congr(ModuleCat.ofHom $(H₁.linearMap_comp_eq_zero))) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
⊢ IsIso M.fromTildeΓ
have rw : (tilde.functor R).essImage M
Tactic: rw [isIso_fromTildeΓ_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
g : Quiver.Hom (V := ModuleCat (↑R : Type u)) (ModuleCat.of (↑R : Type u) (P.relations.I →₀ (↑R : Type u)))
  (ModuleCat.of (↑R : Type u) (P.generators.I →₀ (↑R : Type u))) :=
  (tilde.functor R).preimage
    (Iso.hom (tildeFinsupp P.relations.I) ≫
      P.relations.π ≫ kernel.ι P.generators.π ≫ Iso.inv (tildeFinsupp P.generators.I))
⊢ cokernel ((tilde.functor R).map g) ≅ cokernel (P.relations.π ≫ kernel.ι P.generators.π)
have refine : (tilde.functor R).map g ≫ Iso.hom (tildeFinsupp P.generators.I) =
  Iso.hom (tildeFinsupp P.relations.I) ≫ P.relations.π ≫ kernel.ι P.generators.π
Tactic: refine cokernel.mapIso _ _ (tildeFinsupp _) (tildeFinsupp _) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Modules.Tilde (goal)
Goal:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
g : Quiver.Hom (V := ModuleCat (↑R : Type u)) (ModuleCat.of (↑R : Type u) (P.relations.I →₀ (↑R : Type u)))
  (ModuleCat.of (↑R : Type u) (P.generators.I →₀ (↑R : Type u))) :=
  (tilde.functor R).preimage
    (Iso.hom (tildeFinsupp P.relations.I) ≫
      P.relations.π ≫ kernel.ι P.generators.π ≫ Iso.inv (tildeFinsupp P.generators.I))
⊢ (tilde.functor R).map g ≫ Iso.hom (tildeFinsupp P.generators.I) =
    Iso.hom (tildeFinsupp P.relations.I) ≫ P.relations.π ≫ kernel.ι P.generators.π
have simp : (Iso.hom (tildeFinsupp P.relations.I) ≫
      P.relations.π ≫ kernel.ι P.generators.π ≫ Iso.inv (tildeFinsupp P.generators.I)) ≫
    Iso.hom (tildeFinsupp P.generators.I) =
  Iso.hom (tildeFinsupp P.relations.I) ≫ P.relations.π ≫ kernel.ι P.generators.π
Tactic: simp only [g, (tilde.functor R).map_preimage]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom f
inst_1 : IsAffineHom g
⊢ IsAffineHom (f ≫ g)
have isAffine_preimage : ∀ (U : Z.Opens), IsAffineOpen U → IsAffineOpen ((f ≫ g) ⁻¹ᵁ U)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom f
inst_1 : IsAffineHom g
U : Z.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen ((f ≫ g) ⁻¹ᵁ U)
have isAffine_preimage : IsAffineOpen ((Opens.map f.base).obj ((Opens.map g.base).obj U))
Tactic: rw [Scheme.Hom.comp_base, Opens.map_comp_obj]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom f
inst_1 : IsAffineHom g
U : Z.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen ((Opens.map f.base).obj ((Opens.map g.base).obj U))
have isAffine_preimage : IsAffineOpen ((Opens.map g.base).obj U)
Tactic: apply IsAffineHom.isAffine_preimage
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
⊢ IsAffineHom (X.basicOpen r).ι
have isAffine_preimage : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)
have isAffine_preimage : IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)
Tactic: fapply (Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion (X.basicOpen r).ι).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)
have h : (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U =
  X.basicOpen (U := U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X := X.presheaf.obj (op ⊤)) (Y := X.presheaf.obj (op U))
          (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : (↑(X.presheaf.obj (op ⊤)) : Type u_1)) → (↑(X.presheaf.obj (op U)) : Type u_1))
      r)
Tactic: convert! hU.basicOpen (X.presheaf.map (homOfLE le_top).op r)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
⊢ (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U =
    X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op ⊤)) (Y := X.presheaf.obj (op U))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(X.presheaf.obj (op ⊤)) : Type u_1)) → (↑(X.presheaf.obj (op U)) : Type u_1))
        r)
have h : (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U = U ⊓ X.basicOpen r
Tactic: rw [X.basicOpen_res]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
⊢ (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U = U ⊓ X.basicOpen r
have h : (↑((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U) : Set ↥X) = (↑(U ⊓ X.basicOpen r) : Set ↥X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Affine (goal)
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
⊢ (↑((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U) : Set ↥X) = (↑(U ⊓ X.basicOpen r) : Set ↥X)
have h : U.1 ∩ Set.range (ι := ↥(↑(X.basicOpen r) : Scheme)) ⇑(X.basicOpen r).ι = (↑(U ⊓ X.basicOpen r) : Set ↥X)
Tactic: refine Set.image_preimage_eq_inter_range.trans ?_
-- 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)
⊢ QuasiSeparatedSpace.{u} ↥X
have rw : ∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: rw [quasiSeparatedSpace_iff_forall_affineOpens]
-- 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)
U V : (↑X.affineOpens : Type u)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have obtain : ∀ (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.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: obtain ⟨s', hs', e⟩ := (Ideal.span_eq_top_iff_finite _).mp 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)
U V : (↑X.affineOpens : Type u)
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.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have rw : IsCompact.{u} (X := ↥X)
  (⋃ (i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)),
    (↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
Tactic: rw [← Set.inter_univ (_ ∩ _), ← Opens.coe_top, ← iSup_basicOpen_of_span_eq_top _ _ e,
    ← iSup_subtype'', Opens.coe_iSup, Set.inter_iUnion]
-- 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)
U V : (↑X.affineOpens : Type u)
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' : Set (↑Γ(X, ⊤) : Type u)) : Type u)),
      (↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
have h : ∀ (i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)),
  IsCompact
    ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
Tactic: apply isCompact_iUnion
-- 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)
U V : (↑X.affineOpens : Type u)
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))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
⊢ IsCompact
    ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
have h : IsCompact
  ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X) ∩
    ((↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X)))
Tactic: rw [Set.inter_inter_distrib_right]
-- 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)
U V : (↑X.affineOpens : Type u)
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))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
⊢ IsCompact
    ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X) ∩
      ((↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X)))
have h : IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
Tactic: refine (hs₂ i (hs' i.2)).isQuasiSeparated _ _ Set.inter_subset_right
    (U.1.2.inter (X.basicOpen _).2) ?_ Set.inter_subset_right (V.1.2.inter (X.basicOpen _).2) ?_
-- 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)
U V : (↑X.affineOpens : Type u)
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))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
h : IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
⊢ IsCompact
    ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X) ∩
      ((↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X)))
have h₁ : IsCompact ((↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
Tactic: refine (hs₂ i (hs' i.2)).isQuasiSeparated _ _ Set.inter_subset_right
    (U.1.2.inter (X.basicOpen _).2) ?_ Set.inter_subset_right (V.1.2.inter (X.basicOpen _).2) ?_
-- 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)
U V : (↑X.affineOpens : Type u)
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))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
have h : IsCompact
  (↑(X.basicOpen (U := (↑U : X.Opens))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
              (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
            (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
          (↑i : (↑Γ(X, ⊤) : Type u)))) :
    Set ↥X)
Tactic: rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]
-- 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)
U V : (↑X.affineOpens : Type u)
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))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
⊢ IsCompact ((↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
have h : IsCompact
  (↑(X.basicOpen (U := (↑V : X.Opens))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑V : X.Opens)))
              (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
            (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u))
          (↑i : (↑Γ(X, ⊤) : Type u)))) :
    Set ↥X)
Tactic: rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]
-- 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)
⊢ IsAffine X
have this : QuasiSeparatedSpace.{u} ↥X
Tactic: have : QuasiSeparatedSpace X := isAffine_of_isAffineOpen_basicOpen_aux s hs 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 : QuasiSeparatedSpace.{u} ↥X
⊢ CompactSpace.{u} ↥X
have obtain : ∀ (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))) ⊤), CompactSpace.{u} ↥X
Tactic: obtain ⟨s', hs', e⟩ := (Ideal.span_eq_top_iff_finite _).mp 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 : 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))) ⊤
⊢ CompactSpace.{u} ↥X
have rw : IsCompact (↑(⨆ i ∈ (↑s' : Set (↑Γ(X, ⊤) : Type u)), X.basicOpen i) : Set ↥X)
Tactic: rw [← isCompact_univ_iff, ← Opens.coe_top, ← iSup_basicOpen_of_span_eq_top _ _ e]
-- 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 (↑(⨆ i ∈ (↑s' : Set (↑Γ(X, ⊤) : Type u)), X.basicOpen i) : Set ↥X)
have simp : IsCompact.{u} (X := ↥X) (⋃ i ∈ s', (↑(X.basicOpen i) : Set ↥X))
Tactic: simp only [Finset.mem_coe, Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk]