awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X.Hom Y
⊢ f.copyBase ⇑f ⋯ = f
have obtain : ∀ (f₁ : ↥X → ↥Y) (f₂ : Continuous f₁)
  (f₃ :
    Y.presheaf ⟶
      Functor.obj
        (Presheaf.pushforward CommRingCat
          { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
            (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) })
        X.presheaf)
  (f₄ :
    ∀ (x : ↥X),
      IsLocalHom (R :=
        (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier)
                    {
                        base :=
                          { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                            (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                        c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                  (a : ↥X) → ↥Y)
                x)) :
          Type u_1))
        (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
        (↑(Y.presheaf.stalk
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier)
                      {
                          base :=
                            { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                              (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                          c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                    (a : ↥X) → ↥Y)
                  x)) :
            Type u_1) →+*
          (↑(X.presheaf.stalk x) : Type u_1))
        (CommRingCat.Hom.hom ({ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃ }.stalkMap x))),
  {
          base :=
            { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
              (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
          c := f₃, prop := f₄ : X.Hom Y }.copyBase
      ⇑{
          base :=
            { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
              (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
          c := f₃, prop := f₄ : X.Hom Y }
      sorry =
    { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }
Tactic: obtain ⟨⟨⟨f₁, f₂⟩, f₃⟩, f₄⟩ := f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f₁ : ↥X → ↥Y
f₂ : Continuous f₁
f₃ :
  Y.presheaf ⟶
    Functor.obj
      (Presheaf.pushforward CommRingCat
        { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
          (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) })
      X.presheaf
f₄ :
  ∀ (x : ↥X),
    IsLocalHom (R :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier)
                  {
                      base :=
                        { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                          (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                      c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                (a : ↥X) → ↥Y)
              x)) :
        Type u_1))
      (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
      (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier)
                    {
                        base :=
                          { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                            (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                        c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                  (a : ↥X) → ↥Y)
                x)) :
          Type u_1) →+*
        (↑(X.presheaf.stalk x) : Type u_1))
      (CommRingCat.Hom.hom ({ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃ }.stalkMap x))
⊢ {
          base :=
            { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
              (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
          c := f₃, prop := f₄ : X.Hom Y }.copyBase
      ⇑{
          base :=
            { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
              (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
          c := f₃, prop := f₄ : X.Hom Y }
      ⋯ =
    { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }
have simp : {
    base :=
      ofHom
        {
          toFun :=
            (⇑(@ConcreteCategory.hom _ TopCat.instCategory
                  (fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) carrier _ _
                  (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)
                  { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                    (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) }) :
              (a : ↥X) → ↥Y),
          continuous_toFun := sorry : C((↑X.toPresheafedSpace.1 : Type u_1), (↑Y.toPresheafedSpace.1 : Type u_1)) },
    c := f₃ ≫ (Presheaf.pushforwardEq sorry X.presheaf).hom, prop := sorry : X.Hom Y } =
  { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }
Tactic: simp only [Hom.copyBase]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f₁ : ↥X → ↥Y
f₂ : Continuous f₁
f₃ :
  Y.presheaf ⟶
    Functor.obj
      (Presheaf.pushforward CommRingCat
        { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
          (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) })
      X.presheaf
f₄ :
  ∀ (x : ↥X),
    IsLocalHom (R :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier)
                  {
                      base :=
                        { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                          (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                      c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                (a : ↥X) → ↥Y)
              x)) :
        Type u_1))
      (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
      (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier)
                    {
                        base :=
                          { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                            (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) },
                        c := f₃ : X.Hom Y.toPresheafedSpace }.base :
                  (a : ↥X) → ↥Y)
                x)) :
          Type u_1) →+*
        (↑(X.presheaf.stalk x) : Type u_1))
      (CommRingCat.Hom.hom ({ base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃ }.stalkMap x))
⊢ {
      base :=
        ofHom
          {
            toFun :=
              (⇑(@ConcreteCategory.hom _ TopCat.instCategory
                    (fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) carrier _ _
                    (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)
                    { hom' := { toFun := f₁, continuous_toFun := f₂ : C(↥X, ↥Y) } :
                      (↑X.toPresheafedSpace : TopCat).Hom (↑Y.toPresheafedSpace : TopCat) }) :
                (a : ↥X) → ↥Y),
            continuous_toFun := ⋯ : C((↑X.toPresheafedSpace.1 : Type u_1), (↑Y.toPresheafedSpace.1 : Type u_1)) },
      c := f₃ ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom, prop := ⋯ : X.Hom Y } =
    { base := { hom' := { toFun := f₁, continuous_toFun := f₂ } }, c := f₃, prop := f₄ }
have e_toLRSHom' : f₃ ≫ (Presheaf.pushforwardEq sorry X.presheaf).hom = f₃
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R S : CommRingCat
e : R = S
⊢ map (eqToHom e) = eqToHom ⋯
have subst : map (eqToHom sorry) = eqToHom sorry
Tactic: subst e
Cleared hypotheses: S, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
inst : IsIso f
⊢ map (inv f) = inv (map f)
have change : Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)
Tactic: change Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
inst : IsIso f
⊢ Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)
have rw : Scheme.Spec.map (inv f.op) = inv (Scheme.Spec.map f.op)
Tactic: rw [op_inv, ← Scheme.Spec.map_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
inst : IsIso f
rw : Scheme.Spec.map (inv f.op) = inv (Scheme.Spec.map f.op)
⊢ Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)
have rw₁ : Scheme.Spec.map (inv f.op) = Scheme.Spec.map (inv f.op)
Tactic: rw [op_inv, ← Scheme.Spec.map_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : (↑Γ(Y, V) : Type u)
⊢ X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appLE f V U e) :
          (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, U) : Type u))
        s) =
    U ⊓ f ⁻¹ᵁ Y.basicOpen s
have simp : X.basicOpen (U := U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X.presheaf.map (homOfLE e).op) :
        (a : (↑Γ(X, f ⁻¹ᵁ V) : Type u)) → (↑Γ(X, U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app f V) :
            (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
          s :
        (↑Γ(X, f ⁻¹ᵁ V) : Type u))) =
  U ⊓
    X.basicOpen (U := f ⁻¹ᵁ V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app f V) :
          (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
        s)
Tactic: simp only [preimage_basicOpen, Hom.appLE, CommRingCat.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : (↑Γ(Y, V) : Type u)
⊢ X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE e).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ V) : Type u)) → (↑Γ(X, U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.app f V) :
              (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
            s :
          (↑Γ(X, f ⁻¹ᵁ V) : Type u))) =
    U ⊓
      X.basicOpen (U := f ⁻¹ᵁ V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app f V) :
            (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
          s)
have rw : U ⊓
    X.basicOpen (U := f ⁻¹ᵁ V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app f V) :
          (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
        s) =
  U ⊓
    X.basicOpen (U := f ⁻¹ᵁ V)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.app f V) :
          (a : (↑Γ(Y, V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ V) : Type u))
        s)
Tactic: rw [basicOpen_res]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u_1)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
⊢ x ∈ X.basicOpen f ⊔ X.basicOpen g
have hxU : x ∈ U
Tactic: have hxU : x ∈ U := X.basicOpen_le _ hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u_1)
x : ↥X
hx : x ∈ X.basicOpen (f + g)
hxU : x ∈ U
⊢ x ∈ X.basicOpen f ∨ x ∈ X.basicOpen g
have simp : ∀
  (hx :
    IsUnit
      (HAdd.hAdd (α := (↑(X.presheaf.stalk x) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
            f :
          (↑(X.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
            g :
          (↑(X.presheaf.stalk x) : Type u_1)))),
  IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          f :
        (↑(X.presheaf.stalk x) : Type u_1)) ∨
    IsUnit (M := (↑(X.presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
            (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
          g :
        (↑(X.presheaf.stalk x) : Type u_1))
Tactic: simp only [Scheme.mem_basicOpen _ _ _ hxU, map_add] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
⊢ Codisjoint (X.zeroLocus s) (↑U : Set ↥X)
have this : ∀ (x : ↥X), ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U
Tactic: have (x : X) : ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U := fun _ _ h ↦ X.basicOpen_le _ h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
⊢ X.zeroLocus (↑(Ideal.span s) : Set (↑Γ(X, U) : Type u)) = X.zeroLocus s
have h : ∀ (x : ↥X), x ∈ X.zeroLocus (↑(Ideal.span s) : Set (↑Γ(X, U) : Type u)) ↔ x ∈ X.zeroLocus s
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
⊢ x ∈ X.zeroLocus (↑(Ideal.span s) : Set (↑Γ(X, U) : Type u)) ↔ x ∈ X.zeroLocus s
have h : (∀ (f : (↑Γ(X, U) : Type u)), Membership.mem (γ := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) f → x ∉ X.basicOpen f) ↔
  ∀ f ∈ s, x ∉ X.basicOpen f
Tactic: simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
⊢ (∀ (f : (↑Γ(X, U) : Type u)), Membership.mem (γ := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) f → x ∉ X.basicOpen f) ↔
    ∀ f ∈ s, x ∉ X.basicOpen f
have h : ∀ (H : ∀ f ∈ s, x ∉ X.basicOpen f) (f : (↑Γ(X, U) : Type u)), x ∉ X.basicOpen (U := U) 0
Tactic: refine ⟨fun H f hfs ↦ H f (Ideal.subset_span hfs), fun H f ↦ Submodule.span_induction H ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
h : ∀ (H : ∀ f ∈ s, x ∉ X.basicOpen f) (f : (↑Γ(X, U) : Type u)), x ∉ X.basicOpen (U := U) 0
⊢ (∀ (f : (↑Γ(X, U) : Type u)), Membership.mem (γ := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) f → x ∉ X.basicOpen f) ↔
    ∀ f ∈ s, x ∉ X.basicOpen f
have h₁ : ∀ (H : ∀ f ∈ s, x ∉ X.basicOpen f) (f x_1 y : (↑Γ(X, U) : Type u))
  (hx :
    Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s) x_1)
  (hy :
    Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s) y),
  x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)
Tactic: refine ⟨fun H f hfs ↦ H f (Ideal.subset_span hfs), fun H f ↦ Submodule.span_induction H ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
h : ∀ (H : ∀ f ∈ s, x ∉ X.basicOpen f) (f : (↑Γ(X, U) : Type u)), x ∉ X.basicOpen (U := U) 0
h₁ :
  ∀ (H : ∀ f ∈ s, x ∉ X.basicOpen f) (f x_1 y : (↑Γ(X, U) : Type u))
    (hx :
      Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s)
        x_1)
    (hy :
      Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s) y),
    x ∉ X.basicOpen x_1 → x ∉ X.basicOpen y → x ∉ X.basicOpen (x_1 + y)
⊢ (∀ (f : (↑Γ(X, U) : Type u)), Membership.mem (γ := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) f → x ∉ X.basicOpen f) ↔
    ∀ f ∈ s, x ∉ X.basicOpen f
have h₂ : ∀ (H : ∀ f ∈ s, x ∉ X.basicOpen f) (f a x_1 : (↑Γ(X, U) : Type u))
  (hx :
    Membership.mem (γ := Submodule (↑Γ(X, U) : Type u) (↑Γ(X, U) : Type u)) (Submodule.span (↑Γ(X, U) : Type u) s) x_1),
  x ∉ X.basicOpen x_1 → x ∉ X.basicOpen (a • x_1)
Tactic: refine ⟨fun H f hfs ↦ H f (Ideal.subset_span hfs), fun H f ↦ Submodule.span_induction H ?_ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ s, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
⊢ x ∉ X.basicOpen (U := U) 0
have h : x ∉ ⊥
Tactic: simp only [Scheme.basicOpen_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
s t : Set (↑Γ(X, U) : Type u)
⊢ X.zeroLocus (s * t) = X.zeroLocus s ∪ X.zeroLocus t
have simp : Eq.{u + 1} (α := Set ↥X) (⋂ a ∈ s, ⋂ b ∈ t, (X.basicOpen (a * b)).carrierᶜ)
  ((⋂ f ∈ s, (X.basicOpen f).carrierᶜ) ∪ ⋂ f ∈ t, (X.basicOpen f).carrierᶜ)
Tactic: simp only [← Set.image2_mul, zeroLocus_def, Set.biInter_image2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
I J : Ideal (↑Γ(X, U) : Type u)
⊢ X.zeroLocus (↑(I * J) : Set (↑Γ(X, U) : Type u)) =
    X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ∪ X.zeroLocus (↑J : Set (↑Γ(X, U) : Type u))
have rw : X.zeroLocus (↑(I * J) : Set (↑Γ(X, U) : Type u)) =
  X.zeroLocus
    (↑(HMul.hMul (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span (↑I : Set (↑Γ(X, U) : Type u)))
          (Ideal.span (↑J : Set (↑Γ(X, U) : Type u)))) :
      Set (↑Γ(X, U) : Type u))
Tactic: rw [← X.zeroLocus_setMul, ← X.zeroLocus_span (U := U) (↑I * ↑J), ← Ideal.span_mul_span]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set (↑Γ(X, V) : Type u)
⊢ X.zeroLocus (U := U)
      ((⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) : (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
        s) =
    X.zeroLocus s ∪ (↑U : Set ↥X)ᶜ
have h : ∀ (x : ↥X),
  x ∈
      X.zeroLocus (U := U)
        ((⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) : (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
          s) ↔
    x ∈ X.zeroLocus s ∪ (↑U : Set ↥X)ᶜ
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set (↑Γ(X, V) : Type u)
x : ↥X
⊢ x ∈
      X.zeroLocus (U := U)
        ((⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) : (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
          s) ↔
    x ∈ X.zeroLocus s ∪ (↑U : Set ↥X)ᶜ
have h : (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f
Tactic: suffices (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → (∀ f ∈ s, x ∉ X.basicOpen f) by
    simpa [or_iff_not_imp_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U V : X.Opens
i : U = V
s : Set (↑Γ(X, V) : Type u)
⊢ X.zeroLocus (U := U)
      ((⇑(CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom i)))) :
          (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
        s) =
    X.zeroLocus s
have h : ∀ (x : ↥X),
  x ∈
      X.zeroLocus (U := U)
        ((⇑(CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (eqToHom i)))) :
            (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u)) ''
          s) ↔
    x ∈ X.zeroLocus s
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
s t : Set (↑Γ(X, U) : Type u)
h : s ⊆ t
⊢ X.zeroLocus t ⊆ X.zeroLocus s
have simp : ∀ (x : ↥X), (∀ f ∈ t, x ∉ X.basicOpen f) → ∀ f ∈ s, x ∉ X.basicOpen f
Tactic: simp only [Set.subset_def, Scheme.mem_zeroLocus_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
s : Set (↑Γ(Y, U) : Type u)
⊢ ⇑f ⁻¹' Y.zeroLocus s =
    X.zeroLocus (U := f ⁻¹ᵁ U)
      ((⇑(CommRingCat.Hom.hom (Hom.app f U)) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u)) '' s)
have h : ∀ (x : ↥X),
  Membership.mem (γ := Set ↥X) (⇑f ⁻¹' Y.zeroLocus s) x ↔
    x ∈
      X.zeroLocus (U := f ⁻¹ᵁ U)
        ((⇑(CommRingCat.Hom.hom (Hom.app f U)) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u)) '' s)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
⊢ X.zeroLocus (U := U) Set.univ = (↑U : Set ↥X)ᶜ
have h : ∀ (x : ↥X), x ∈ X.zeroLocus (U := U) Set.univ ↔ x ∈ (↑U : Set ↥X)ᶜ
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
x : ↥X
⊢ x ∈ X.zeroLocus (U := U) Set.univ ↔ x ∈ (↑U : Set ↥X)ᶜ
have h : (∃ (x_1 : (↑Γ(X, U) : Type u)), x ∈ X.basicOpen x_1) ↔ x ∈ U
Tactic: simp only [Scheme.mem_zeroLocus_iff, Set.mem_univ, forall_const, Set.mem_compl_iff,
    SetLike.mem_coe, ← not_exists, not_iff_not]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
⊢ X.zeroLocus (↑I.radical : Set (↑Γ(X, U) : Type u)) = X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u))
have refine : X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ⊆ X.zeroLocus (↑I.radical : Set (↑Γ(X, U) : Type u))
Tactic: refine (X.zeroLocus_mono I.le_radical).antisymm ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
⊢ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ⊆ X.zeroLocus (↑I.radical : Set (↑Γ(X, U) : Type u))
have simp : ∀ (x : ↥X), (∀ f ∈ I, x ∉ X.basicOpen f) → ∀ f ∈ I.radical, x ∉ X.basicOpen f
Tactic: simp only [Set.subset_def, mem_zeroLocus_iff, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
n : ℕ
hn : f ^ n ∈ I
hx : x ∈ X.basicOpen f
⊢ False
have inl : ∀ (hn : HPow.hPow (β := ℕ) f 0 ∈ I), False
Tactic: rcases n.eq_zero_or_pos with rfl | hn'
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
n : ℕ
hn : f ^ n ∈ I
hx : x ∈ X.basicOpen f
inl : ∀ (hn : HPow.hPow (β := ℕ) f 0 ∈ I), False
⊢ False
have inr : ∀ (hn' : n > 0), False
Tactic: rcases n.eq_zero_or_pos with rfl | hn'