awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
e :
  f ⁻¹ᵁ
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r) =
    X.basicOpen (U := f ⁻¹ᵁ f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, f ''ᵁ U)) (Hom.app f (f ''ᵁ U)) :
          (a : (↑Γ(Y, f ''ᵁ U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
            r :
          (↑Γ(Y, f ''ᵁ U) : Type u)))
⊢ f ''ᵁ X.basicOpen r =
    Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r)
have rw : ∀
  (e :
    f ⁻¹ᵁ
        Y.basicOpen (U := f ''ᵁ U)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
            r) =
      X.basicOpen r),
  f ''ᵁ X.basicOpen r =
    Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r)
Tactic: rw [Scheme.Hom.appIso_inv_app_apply, Scheme.basicOpen_res, inf_eq_right.mpr _] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
e :
  f ⁻¹ᵁ
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r) =
    X.basicOpen (U := f ⁻¹ᵁ f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, f ''ᵁ U)) (Hom.app f (f ''ᵁ U)) :
          (a : (↑Γ(Y, f ''ᵁ U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ f ''ᵁ U) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
            r :
          (↑Γ(Y, f ''ᵁ U) : Type u)))
rw :
  ∀
    (e :
      f ⁻¹ᵁ
          Y.basicOpen (U := f ''ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
              r) =
        X.basicOpen r),
    f ''ᵁ X.basicOpen r =
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r)
⊢ f ''ᵁ X.basicOpen r =
    Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r)
have rw₁ : ∀
  (e :
    f ⁻¹ᵁ
        Y.basicOpen (U := f ''ᵁ U)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
            r) =
      f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r),
  X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U
Tactic: rw [Scheme.Hom.appIso_inv_app_apply, Scheme.basicOpen_res, inf_eq_right.mpr _] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : (↑Γ(X, U) : Type u)
e :
  f ⁻¹ᵁ
      Y.basicOpen (U := f ''ᵁ U)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
          r) =
    X.basicOpen r
⊢ f ''ᵁ X.basicOpen r =
    Y.basicOpen (U := f ''ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
        r)
have rw : Y.basicOpen (U := f ''ᵁ U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (Hom.appIso f U)) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u))
      r) ≤
  Hom.opensRange f
Tactic: rw [← e, f.image_preimage_eq_opensRange_inf, inf_eq_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
⊢ ⇑f '' X.zeroLocus s =
    Y.zeroLocus (U := f ''ᵁ U)
        ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) : (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
          s) ∩
      Set.range (ι := ↥X) ⇑f
have h : ∀ (x : ↥Y),
  Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
    x ∈
      Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥Y
⊢ Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
    x ∈
      Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f
have pos : ∀ (hx : Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥X) ⇑f) x),
  Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
    x ∈
      Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f
Tactic: by_cases hx : x ∈ Set.range f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥Y
pos :
  ∀ (hx : Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥X) ⇑f) x),
    Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
      x ∈
        Y.zeroLocus (U := f ''ᵁ U)
            ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
                (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
              s) ∩
          Set.range (ι := ↥X) ⇑f
⊢ Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
    x ∈
      Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f
have neg : ∀ (hx : x ∉ Set.range (ι := ↥X) ⇑f),
  Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
    x ∈
      Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f
Tactic: by_cases hx : x ∈ Set.range f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥Y
hx : Membership.mem (γ := Set ↥Y) (Set.range (ι := ↥X) ⇑f) x
⊢ Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
    x ∈
      Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f
have pos : ∀ (x : ↥X),
  Membership.mem (α := ↥Y) (γ := Set ↥Y) (⇑f '' X.zeroLocus s) (f x : ↥Y) ↔
    Membership.mem (α := ↥Y)
      (Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f)
      (f x : ↥Y)
Tactic: obtain ⟨x, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥Y
hx : x ∉ Set.range (ι := ↥X) ⇑f
⊢ Membership.mem (γ := Set ↥Y) (⇑f '' X.zeroLocus s) x ↔
    x ∈
      Y.zeroLocus (U := f ''ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Iso.inv (Hom.appIso f U))) :
              (a : (↑Γ(X, U) : Type u)) → (↑Γ(Y, f ''ᵁ U) : Type u)) ''
            s) ∩
        Set.range (ι := ↥X) ⇑f
have neg : x ∉ (fun (a : ↥X) ↦ f a) '' X.zeroLocus s
Tactic: simp only [Set.mem_inter_iff, hx, and_false, iff_false]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ Eq (α := ↥Z) (f x : ↥Z) (g (snd p : ↥Y) : ↥Z)
have rw : Eq (α := ↥Z) ((snd ≫ g) p : ↥Z) (g (snd p : ↥Y) : ↥Z)
Tactic: rw [← hx, ← Scheme.Hom.comp_apply, h.w]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ x = fst p
have rw : x = x
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst_1 : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ (Z.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap g (snd p))).hom ≫ Hom.stalkMap snd p =
    Hom.stalkMap f x ≫ (X.presheaf.stalkCongr ⋯ ≪≫ asIso (Hom.stalkMap fst p)).hom
have subst : Eq (α := Z.presheaf.stalk (f (fst p : ↥X)) ⟶ P.presheaf.stalk p)
  (Iso.hom (Z.presheaf.stalkCongr sorry ≪≫ asIso (Hom.stalkMap g (snd p))) ≫ Hom.stalkMap snd p)
  (Hom.stalkMap f (fst p) ≫ Iso.hom (X.presheaf.stalkCongr sorry ≪≫ asIso (Hom.stalkMap fst p)))
Tactic: subst hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := Ideal (R i))
      (Ideal.span ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) '' s)) ⊤
⊢ Eq (α := Ideal ((i : ι) → R i)) (Ideal.span s) ⊤
have simp : ∀
  (hs' :
    ∀ (i : ι),
      ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ R i),
        Eq (α := R i)
          (c.sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
            a *
              ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
                  Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
                i_1)
          1),
  ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
    Eq (α := (i : ι) → R i)
      (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1
Tactic: simp only [Ideal.eq_top_iff_one, ← Subtype.range_val (s := s), ← Set.range_comp,
    Finsupp.mem_ideal_span_range_iff_exists_finsupp] at hs' ⊢
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
hs' :
  ∀ (i : ι),
    ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ R i),
      Eq (α := R i)
        (c.sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
          a *
            ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
                Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
              i_1)
        1
⊢ ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
    Eq (α := (i : ι) → R i)
      (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1
have choose : ∀ (f : (i : ι) → { x : (i : ι) → R i // x ∈ s } →₀ R i)
  (hf :
    ∀ (i : ι),
      Eq (α := R i)
        ((f i).sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
          a *
            ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
                Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
              i_1)
        1),
  ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
    Eq (α := (i : ι) → R i)
      (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1
Tactic: choose f hf using hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x : (i : ι) → R i // x ∈ s } →₀ R i
hf :
  ∀ (i : ι),
    Eq (α := R i)
      ((f i).sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
        a *
          ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
              Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
            i_1)
      1
⊢ ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
    Eq (α := (i : ι) → R i)
      (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1
have have : ∀ (this : Fintype (↑s : Type (max u_1 u_2))),
  ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
    Eq (α := (i : ι) → R i)
      (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1
Tactic: have : Fintype s := hs.fintype
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x : (i : ι) → R i // x ∈ s } →₀ R i
hf :
  ∀ (i : ι),
    Eq (α := R i)
      ((f i).sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
        a *
          ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
              Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
            i_1)
      1
this : Fintype (↑s : Type (max u_1 u_2))
⊢ ∃ (c : { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i),
    Eq (α := (i : ι) → R i)
      (c.sum fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) 1
have refine : Eq (α := (i : ι) → R i)
  (Finsupp.sum
    ((Equiv.symm Finsupp.equivFunOnFinite :
        (a : { x : (i : ι) → R i // x ∈ s } → (i : ι) → R i) → { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i)
      fun (i : { x : (i : ι) → R i // x ∈ s }) (x : ι) ↦ (f x : (a : { x : (i : ι) → R i // x ∈ s }) → R x) i)
    fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i))
  1
Tactic: refine ⟨Finsupp.equivFunOnFinite.symm fun i x ↦ f x i, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u_2
R : ι → Type u_1
inst : (i : ι) → CommRing (R i)
s : Set ((i : ι) → R i)
hs : s.Finite
f : (i : ι) → { x : (i : ι) → R i // x ∈ s } →₀ R i
hf :
  ∀ (i : ι),
    Eq (α := R i)
      ((f i).sum fun (i_1 : { x : (i : ι) → R i // x ∈ s }) (a : R i) ↦
        a *
          ((⇑(Pi.evalRingHom (fun (x : ι) ↦ R x) i) : (a : (i : ι) → R i) → R i) ∘
              Subtype.val (p := fun (x : (i : ι) → R i) ↦ x ∈ s))
            i_1)
      1
this : Fintype (↑s : Type (max u_1 u_2))
⊢ Eq (α := (i : ι) → R i)
    (Finsupp.sum
      ((Equiv.symm Finsupp.equivFunOnFinite :
          (a : { x : (i : ι) → R i // x ∈ s } → (i : ι) → R i) → { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i)
        fun (i : { x : (i : ι) → R i // x ∈ s }) (x : ι) ↦ (f x : (a : { x : (i : ι) → R i // x ∈ s }) → R x) i)
      fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i))
    1
have h : ∀ (i : ι),
  Eq.{u_1 + 1} (α := R i)
    (Finsupp.sum
      ((Equiv.symm Finsupp.equivFunOnFinite :
          (a : { x : (i : ι) → R i // x ∈ s } → (i : ι) → R i) → { x : (i : ι) → R i // x ∈ s } →₀ (i : ι) → R i)
        fun (i : { x : (i : ι) → R i // x ∈ s }) (x : ι) ↦ (f x : (a : { x : (i : ι) → R i // x ∈ s }) → R x) i)
      (fun (i : { x : (i : ι) → R i // x ∈ s }) (a : (i : ι) → R i) ↦ a * (↑i : (i : ι) → R i)) i)
    (1 i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
⊢ U = ⊤
have obtain : ∀ (s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) (hs : U.carrierᶜ = zeroLocus s), U = ⊤
Tactic: obtain ⟨s, hs⟩ := (PrimeSpectrum.isOpen_iff _).mp U.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
⊢ ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, TopologicalSpace.Opens.carrier (basicOpen i)
have obtain : ∀ (t : Finset (↑s : Type u))
  (ht :
    V ⊆
      ⋃ i ∈ t,
        TopologicalSpace.Opens.carrier (basicOpen (↑i : (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)))),
  ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, TopologicalSpace.Opens.carrier (basicOpen i)
Tactic: obtain ⟨t, ht⟩ := hV'.elim_finite_subcover
      (fun i : s ↦ (basicOpen i.1).1) (fun _ ↦ (basicOpen _).2)
      (by simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ s)), ← hs])
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
⊢ U = ⊤
have obtain : ∀ (t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)) (hts : t ⊆ s) (ht : t.Finite)
  (ht' : V ⊆ ⋃ i ∈ t, TopologicalSpace.Opens.carrier (basicOpen i)), U = ⊤
Tactic: obtain ⟨t, hts, ht, ht'⟩ : ∃ t ⊆ s, t.Finite ∧ V ⊆ ⋃ i ∈ t, (basicOpen i).1 := by
    obtain ⟨t, ht⟩ := hV'.elim_finite_subcover
      (fun i : s ↦ (basicOpen i.1).1) (fun _ ↦ (basicOpen _).2)
      (by simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ s)), ← hs])
    exact ⟨t.map (Function.Embedding.subtype _), by simp, Finset.finite_toSet _, by simpa using ht⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (hypothesis)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ ⋃ i ∈ t, TopologicalSpace.Opens.carrier (basicOpen i)
⊢ U = ⊤
have ht'₁ : V ⊆ (zeroLocus t)ᶜ
Tactic: replace ht' : V ⊆ (zeroLocus t)ᶜ := by
    simpa [← Set.compl_iInter, ← zeroLocus_iUnion₂ (κ := (· ∈ t))] using ht'
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Eq (α := Ideal (↑(R i) : Type u))
    (Ideal.span
      ((⇑(Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i) :
          (a : (i : ι) → (↑(R i) : Type u)) → (↑(R i) : Type u)) ''
        t))
    ⊤
have rw : Subset (α := Set (PrimeSpectrum ((i : ι) → (↑(R i) : Type u))))
  (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))
  (zeroLocus t)ᶜ
Tactic: rw [← zeroLocus_empty_iff_eq_top, zeroLocus_span, ← preimage_comap_zeroLocus,
      ← Set.compl_univ_iff, ← Set.preimage_compl, Set.preimage_eq_univ_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.PointsPi (goal)
Goal:
ι : Type u
R : ι → CommRingCat
U : (Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))).Opens
V : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))
hV : (↑(Scheme.Hom.opensRange (sigmaSpec R)) : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u))))) ⊆ V
hV' : IsCompact V
hVU : V ⊆ (↑U : Set ↥(Spec (CommRingCat.of ((i : ι) → (↑(R i) : Type u)))))
s : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hs : U.carrierᶜ = zeroLocus s
t : Set (↑(CommRingCat.of ((i : ι) → (↑(R i) : Type u))) : Type u)
hts : t ⊆ s
ht : t.Finite
ht' : V ⊆ (zeroLocus t)ᶜ
i : ι
⊢ Subset (α := Set (PrimeSpectrum ((i : ι) → (↑(R i) : Type u))))
    (Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)))
    (zeroLocus t)ᶜ
have trans : Set.range (ι := PrimeSpectrum (↑(R i) : Type u)) (comap (Pi.evalRingHom (fun (x : ι) ↦ (↑(R x) : Type u)) i)) ⊆
  (Scheme.Hom.opensRange (Sigma.ι (C := Scheme) (fun (i : ι) ↦ Spec (R i)) i ≫ sigmaSpec R)).carrier
Tactic: trans (Sigma.ι _ i ≫ sigmaSpec R).opensRange.1