awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
⊢ Iso.hom (IsAffineOpen.isoSpec ⋯) ≫
      Spec.map (f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) =
    Spec.map f ∣_ basicOpen r ≫
      ⋯.isoSpec.hom ≫ Spec.map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have refine_3 : Scheme.Opens.ι (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) ≫
    (Spec S).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso S).inv ≫ Spec.map f =
  (Spec.map f ⁻¹ᵁ basicOpen r).ι ≫ Spec.map f ≫ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv
Tactic: simp only [IsAffineOpen.isoSpec_hom, homOfLE_leOfHom, Spec.map_comp, Category.assoc,
      Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, Scheme.Opens.toSpecΓ_top,
      Scheme.homOfLE_ι_assoc, morphismRestrict_ι_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
⊢ Scheme.Opens.ι (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) ≫
      (Spec S).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso S).inv ≫ Spec.map f =
    (Spec.map f ⁻¹ᵁ basicOpen r).ι ≫ Spec.map f ≫ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv
have refine_3 : Scheme.Opens.ι (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) ≫ Spec.map f =
  (Spec.map f ⁻¹ᵁ basicOpen r).ι ≫ Spec.map f
Tactic: simp only [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Category.assoc, Iso.inv_hom_id,
      Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
⊢ ⨆ i ∈ s, X.basicOpen i = U
have a : ⨆ i ∈ s, X.basicOpen i ≤ U
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
a : ⨆ i ∈ s, X.basicOpen i ≤ U
⊢ ⨆ i ∈ s, X.basicOpen i = U
have a₁ : U ≤ ⨆ i ∈ s, X.basicOpen i
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
⊢ ⨆ i ∈ s, X.basicOpen i ≤ U
have a : ∀ (i : (↑Γ(X, U) : Type u_1)) (j : i ∈ s), X.basicOpen i ≤ U
Tactic: rw [iSup₂_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
⊢ Membership.mem (γ := Opens ↥X) (⨆ i ∈ s, X.basicOpen i) x
have a : ∀ (V : Opens ↥X) (hV : V ∈ X.affineOpens) (hxV : x ∈ (↑V : Set ↥X)) (hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)),
  Membership.mem (γ := Opens ↥X) (⨆ i ∈ s, X.basicOpen i) x
Tactic: obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open hx U.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ Membership.mem (γ := Opens ↥X) (⨆ i ∈ s, X.basicOpen i) x
have a : (↑V : Set ↥X) ⊆ (↑(⨆ i ∈ s, X.basicOpen i) : Set ↥X)
Tactic: refine SetLike.mem_of_subset ?_ hxV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ Eq (α := Ideal (↑Γ(X, V) : Type u_1))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier)
              (X.presheaf.map
                ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y :=
                  (↑U : Set ↥X))))) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1)) ''
        s))
    ⊤
have rw : Eq (α := Ideal (↑Γ(X, V) : Type u_1))
  (Ideal.map
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier)
      (X.presheaf.map
        ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y := (↑U : Set ↥X)))))
    (Ideal.span s))
  ⊤
Tactic: rw [← Ideal.map_span, hs, Ideal.map_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
rw :
  Eq (α := Ideal (↑Γ(X, V) : Type u_1))
    (Ideal.map
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier)
        (X.presheaf.map
          ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y := (↑U : Set ↥X)))))
      (Ideal.span s))
    ⊤
⊢ Eq (α := Ideal (↑Γ(X, V) : Type u_1))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier)
              (X.presheaf.map
                ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y :=
                  (↑U : Set ↥X))))) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1)) ''
        s))
    ⊤
have rw₁ : Eq (α := Ideal (↑Γ(X, V) : Type u_1))
  (Ideal.map (R := (↑(X.presheaf.obj (op U)) : Type u_1))
    (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier)
      (X.presheaf.map
        ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y := (↑U : Set ↥X)))))
    ⊤)
  ⊤
Tactic: rw [← Ideal.map_span, hs, Ideal.map_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
rw :
  Eq (α := Ideal (↑Γ(X, V) : Type u_1))
    (Ideal.map
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier)
        (X.presheaf.map
          ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y := (↑U : Set ↥X)))))
      (Ideal.span s))
    ⊤
rw₁ :
  Eq (α := Ideal (↑Γ(X, V) : Type u_1))
    (Ideal.map (R := (↑(X.presheaf.obj (op U)) : Type u_1))
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier)
        (X.presheaf.map
          ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y := (↑U : Set ↥X)))))
      ⊤)
    ⊤
⊢ Eq (α := Ideal (↑Γ(X, V) : Type u_1))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier)
              (X.presheaf.map
                ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y :=
                  (↑U : Set ↥X))))) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1)) ''
        s))
    ⊤
have rw₂ : Eq.{u_1 + 1} (α := Ideal (↑Γ(X, V) : Type u_1)) ⊤ ⊤
Tactic: rw [← Ideal.map_span, hs, Ideal.map_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ (↑V : Set ↥X) ⊆ (↑(⨆ i ∈ s, X.basicOpen i) : Set ↥X)
have a : (↑(⨆ (f :
        (↑((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier)
                    (X.presheaf.map
                      ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y :=
                        (↑U : Set ↥X))))) :
                (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1)) ''
              s) :
          Type u_1)),
        X.basicOpen (↑f : (↑Γ(X, V) : Type u_1))) :
    Set ↥X) ⊆
  (↑(⨆ i ∈ s, X.basicOpen i) : Set ↥X)
Tactic: rw [← (hV.iSup_basicOpen_eq_self_iff (s := X.presheaf.map (homOfLE hVU).op '' s)).mpr
      (by rw [← Ideal.map_span, hs, Ideal.map_top])]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ (↑(⨆ (f :
          (↑((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                      CommRingCat.carrier)
                      (X.presheaf.map
                        ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y :=
                          (↑U : Set ↥X))))) :
                  (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1)) ''
                s) :
            Type u_1)),
          X.basicOpen (↑f : (↑Γ(X, V) : Type u_1))) :
      Set ↥X) ⊆
    (↑(⨆ i ∈ s, X.basicOpen i) : Set ↥X)
have a : ∀ (i : (↑(X.presheaf.obj (op U)) : Type u_1)) (i_1 : i ∈ s),
  (↑V : Set ↥X) ∩ (↑(X.basicOpen i) : Set ↥X) ⊆ ⋃ i ∈ s, (↑(X.basicOpen i) : Set ↥X)
Tactic: simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Set.iUnion_coe_set, Set.mem_image,
      Set.iUnion_exists, Set.biUnion_and', Set.iUnion_iUnion_eq_right, Scheme.basicOpen_res,
      Opens.coe_inf, Opens.coe_mk, Set.iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
⊢ ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
have obtain : ∀ (i : ι) (hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)),
  ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
Tactic: obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
⊢ ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
have obtain : ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1))
  (e : X.basicOpen f = X.basicOpen g) (hf : (↑x : ↥X) ∈ X.basicOpen f),
  ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
Tactic: obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1)
e : X.basicOpen f = X.basicOpen g
hf : (↑x : ↥X) ∈ X.basicOpen f
⊢ ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
have refine : P (X.affineBasicOpen f)
Tactic: refine ⟨f, hf, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1)
e : X.basicOpen f = X.basicOpen g
hf : (↑x : ↥X) ∈ X.basicOpen f
⊢ P (X.affineBasicOpen f)
have h : X.affineBasicOpen f = X.affineBasicOpen g
Tactic: convert! basicOpen _ g (hU i) using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)
g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1)
e : X.basicOpen f = X.basicOpen g
hf : (↑x : ↥X) ∈ X.basicOpen f
⊢ X.affineBasicOpen f = X.affineBasicOpen g
have h : (↑(X.affineBasicOpen f) : X.Opens) = (↑(X.affineBasicOpen g) : X.Opens)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
⊢ P V
have have : ∀
  (this :
    ∀ (x : ↥(↑V : X.Opens)),
      ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)),
  P V
Tactic: have : ∀ (x : V.1), ∃ f : Γ(X, V), ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f) := by
    intro x
    obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))
    obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩
    refine ⟨f, hf, ?_⟩
    convert! basicOpen _ g (hU i) using 1
    ext1
    exact e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
this :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
⊢ P V
have choose : ∀ (f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1))
  (hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x))
  (hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))), P V
Tactic: choose f hf₁ hf₂ using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
⊢ P V
have obtain : ∀ (t : Finset (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (ht₁ : (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ⊆ Set.range f)
  (ht₂ :
    Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1))) ⊤),
  P V
Tactic: obtain ⟨t, ht₁, ht₂⟩ := (Ideal.span_eq_top_iff_finite _).mp this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
f : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u_1)
hf₁ : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥(↑V : X.Opens)), P (X.affineBasicOpen (f x))
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (Set.range f)) ⊤
t : Finset (↑Γ(X, (↑V : X.Opens)) : Type u_1)
ht₁ : (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1)) ⊆ Set.range f
ht₂ : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (Ideal.span (↑t : Set (↑Γ(X, (↑V : X.Opens)) : Type u_1))) ⊤
⊢ P V
have apply : ∀ (f : ↥t), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)))
Tactic: apply openCover V t ht₂