awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
obtain : ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.asHomogeneousIdeal
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
    Nonempty.{u_1 + 1} (Proj.restrict ⋯ ≅ «Spec».toLocallyRingedSpace.obj (op R))
have obtain₁ : ∀ (f : A) (m : ℕ) (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (hx : f ∉ x.asHomogeneousIdeal),
  ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
    Nonempty.{u_1 + 1} (Proj.restrict sorry ≅ «Spec».toLocallyRingedSpace.obj (op R))
Tactic: classical
    obtain ⟨f, m, f_deg, hm, hx⟩ : ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.1 := by
      by_contra!
      refine x.not_irrelevant_le fun z hz ↦ ?_
      rw [← DirectSum.sum_support_decompose 𝒜 z]
      exact x.1.toIdeal.sum_mem fun k hk ↦ this _ k (SetLike.coe_mem _) <| by_contra <| by aesop
    exact ⟨⟨pbo f, hx⟩, .of (A⁰_ f), ⟨projIsoSpec 𝒜 f f_deg hm⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
a b : (x : ↥(unop U)) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
ha :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    a
hb :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    b
x : ↥(unop U)
⊢ ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop U),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      at x)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
      (U := V) fun (x : ↥V) ↦ (a + b) ((i : (a : ↥V) → ↥(unop U)) x)
have rcases : ∀ (Va : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (ma : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ Va)
  (ia : Va ⟶ unop U) (ja : ℕ) (ra : A) (ra_mem : ra ∈ 𝒜 ja) (sa : A) (sa_mem : sa ∈ 𝒜 ja)
  (hwa :
    ∀ (x : ↥Va),
      (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) sa sa_mem) : A) ∉
        (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal)
  (wa :
    ∀ (x : ↥Va),
      Eq (α := at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥(unop U)) x) :
              at (↑((ia : (a : ↥Va) → ↥(unop U)) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))
          x)
        (HomogeneousLocalization.mk
          { deg := ja, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) ra ra_mem,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) sa sa_mem, den_mem := sorry })),
  ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop U),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      at x)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
      (U := V) fun (x : ↥V) ↦ (a + b) ((i : (a : ↥V) → ↥(unop U)) x)
Tactic: rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, hwa, wa⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
a : (x : ↥(unop U)) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
ha :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    a
x : ↥(unop U)
⊢ ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop U),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      at x)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
      (U := V) fun (x : ↥V) ↦ (-a) ((i : (a : ↥V) → ↥(unop U)) x)
have rcases : ∀ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (m : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V)
  (i : V ⟶ unop U) (j : ℕ) (r : A) (r_mem : r ∈ 𝒜 j) (s : A) (s_mem : s ∈ 𝒜 j)
  (nin :
    ∀ (x : ↥V),
      (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) s s_mem) : A) ∉
        (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal)
  (hy :
    ∀ (x : ↥V),
      Eq (α := at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        ((fun (x : ↥V) ↦
            (a ((i : (a : ↥V) → ↥(unop U)) x) :
              at (↑((i : (a : ↥V) → ↥(unop U)) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))
          x)
        (HomogeneousLocalization.mk
          { deg := j, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) r r_mem,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) s s_mem, den_mem := sorry })),
  ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop U),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      at x)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
      (U := V) fun (x : ↥V) ↦ (-a) ((i : (a : ↥V) → ↥(unop U)) x)
Tactic: rcases ha x with ⟨V, m, i, j, ⟨r, r_mem⟩, ⟨s, s_mem⟩, nin, hy⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
a : (x : ↥(unop U)) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
ha :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    a
x : ↥(unop U)
V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
m : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V
i : V ⟶ unop U
j : ℕ
r : A
r_mem : r ∈ 𝒜 j
s : A
s_mem : s ∈ 𝒜 j
nin :
  ∀ (x : ↥V),
    (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) s s_mem) : A) ∉
      (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal
hy :
  ∀ (x : ↥V),
    Eq (α := at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      ((fun (x : ↥V) ↦
          (a ((i : (a : ↥V) → ↥(unop U)) x) :
            at (↑((i : (a : ↥V) → ↥(unop U)) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))
        x)
      (HomogeneousLocalization.mk
        { deg := j, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) r r_mem,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) s s_mem, den_mem := ⋯ })
⊢ ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop U),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      at x)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
      (U := V) fun (x : ↥V) ↦ (-a) ((i : (a : ↥V) → ↥(unop U)) x)
have refine : ∀ (y : ↥V),
  Eq (α := at (↑y : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) ((fun (x : ↥V) ↦ (-a) ((i : (a : ↥V) → ↥(unop U)) x)) y)
    (HomogeneousLocalization.mk
      { deg := j, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) (-r) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) s s_mem, den_mem := sorry })
Tactic: refine ⟨V, m, i, j, ⟨-r, neg_mem r_mem⟩, ⟨s, s_mem⟩, nin, fun y => ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (hypothesis)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
a : (x : ↥(unop U)) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
ha :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    a
x : ↥(unop U)
V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
m : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V
i : V ⟶ unop U
j : ℕ
r : A
r_mem : r ∈ 𝒜 j
s : A
s_mem : s ∈ 𝒜 j
nin :
  ∀ (x : ↥V),
    (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) s s_mem) : A) ∉
      (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal
hy :
  ∀ (x : ↥V),
    Eq (α := at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      ((fun (x : ↥V) ↦
          (a ((i : (a : ↥V) → ↥(unop U)) x) :
            at (↑((i : (a : ↥V) → ↥(unop U)) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))
        x)
      (HomogeneousLocalization.mk
        { deg := j, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) r r_mem,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) s s_mem, den_mem := ⋯ })
y : ↥V
⊢ Eq (α := at (↑y : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) ((fun (x : ↥V) ↦ (-a) ((i : (a : ↥V) → ↥(unop U)) x)) y)
    (HomogeneousLocalization.mk
      { deg := j, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) (-r) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 j) s s_mem, den_mem := ⋯ })
have hy₁ : ∀ (x : ↥V),
  Eq (α :=
    Localization (M := A)
      (Ideal.primeCompl
        (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (σ := σ) (𝒜 := 𝒜)
          (ProjectiveSpectrum.asHomogeneousIdeal
            (↑((i : (a : ↥V) → ↥(unop U)) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))))
    (val (a ((i : (a : ↥V) → ↥(unop U)) x)))
    (Localization.mk r
      (Subtype.mk (p := fun (x_1 : A) ↦
        Membership.mem (γ := Submonoid A)
          (Ideal.primeCompl
            (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (σ := σ) (𝒜 := 𝒜)
              (ProjectiveSpectrum.asHomogeneousIdeal
                (↑((i : (a : ↥V) → ↥(unop U)) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))))
          x_1)
        s sorry))
Tactic: simp only [ext_iff_val, val_mk] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
a b : (x : ↥(unop U)) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))
ha :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    a
hb :
  PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
    at x)
    (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
        (isLocallyFraction 𝒜) :
      PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
    b
x : ↥(unop U)
⊢ ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop U),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      at x)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
      (U := V) fun (x : ↥V) ↦ (a * b) ((i : (a : ↥V) → ↥(unop U)) x)
have rcases : ∀ (Va : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (ma : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ Va)
  (ia : Va ⟶ unop U) (ja : ℕ) (ra : A) (ra_mem : ra ∈ 𝒜 ja) (sa : A) (sa_mem : sa ∈ 𝒜 ja)
  (hwa :
    ∀ (x : ↥Va),
      (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) sa sa_mem) : A) ∉
        (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal)
  (wa :
    ∀ (x : ↥Va),
      Eq (α := at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        ((fun (x : ↥Va) ↦
            (a ((ia : (a : ↥Va) → ↥(unop U)) x) :
              at (↑((ia : (a : ↥Va) → ↥(unop U)) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))
          x)
        (HomogeneousLocalization.mk
          { deg := ja, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) ra ra_mem,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 ja) sa sa_mem, den_mem := sorry })),
  ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop U),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      at x)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
      (U := V) fun (x : ↥V) ↦ (a * b) ((i : (a : ↥V) → ↥(unop U)) x)
Tactic: rcases ha x with ⟨Va, ma, ia, ja, ⟨ra, ra_mem⟩, ⟨sa, sa_mem⟩, hwa, wa⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
z : at x
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
          (stalkToFiberRingHom 𝒜 x) :
        (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → (↑(CommRingCat.of (at x)) : Type u_1))
      (homogeneousLocalizationToStalk 𝒜 x z) =
    z
have obtain : ∀ (z : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl),
  Eq (α := (↑(CommRingCat.of (at x)) : 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.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
            (stalkToFiberRingHom 𝒜 x) :
          (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → (↑(CommRingCat.of (at x)) : Type u_1))
        (homogeneousLocalizationToStalk 𝒜 x (Quotient.mk'' z)) :
      (↑(CommRingCat.of (at x)) : Type u_1))
    (Quotient.mk'' z :
      _root_.Quotient (α := HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)
        (Setoid.ker (HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)))
Tactic: obtain ⟨z, rfl⟩ := Quotient.mk''_surjective z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s : Set A
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(Ideal.span s) : Set A)) (zeroLocus 𝒜 s)
have h : ∀ (x : ProjectiveSpectrum 𝒜),
  Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(Ideal.span s) : Set A)) x ↔
    Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ (↑(vanishingIdeal t) : Set A) = {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}
have h : ∀ (f : A), f ∈ (↑(vanishingIdeal t) : Set A) ↔ Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f
Tactic: ext f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ (↑(vanishingIdeal t) : Set A) ↔ Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f
have h : (∀ (i : ProjectiveSpectrum 𝒜),
    Membership.mem (γ := Submodule A A)
      (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : i ∈ t), i.asHomogeneousIdeal)) f) ↔
  Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f
Tactic: rw [vanishingIdeal, SetLike.mem_coe, ← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_iInf,
    Submodule.mem_iInf]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ (∀ (i : ProjectiveSpectrum 𝒜),
      Membership.mem (γ := Submodule A A)
        (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : i ∈ t), i.asHomogeneousIdeal)) f) ↔
    Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f
have h : ∀ (x : ProjectiveSpectrum 𝒜),
  Membership.mem (γ := Submodule A A)
      (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : x ∈ t), x.asHomogeneousIdeal)) f ↔
    x ∈ t → f ∈ x.asHomogeneousIdeal
Tactic: refine forall_congr' fun x => ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
x : ProjectiveSpectrum 𝒜
⊢ Membership.mem (γ := Submodule A A)
      (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : x ∈ t), x.asHomogeneousIdeal)) f ↔
    x ∈ t → f ∈ x.asHomogeneousIdeal
have h : Membership.mem (γ := Submodule A A) (⨅ (_ : x ∈ t), x.asHomogeneousIdeal.toIdeal) f ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
Tactic: rw [HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf, HomogeneousIdeal.mem_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
x : ProjectiveSpectrum 𝒜
h :
  Membership.mem (γ := Submodule A A) (⨅ (_ : x ∈ t), x.asHomogeneousIdeal.toIdeal) f ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
⊢ Membership.mem (γ := Submodule A A)
      (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : x ∈ t), x.asHomogeneousIdeal)) f ↔
    x ∈ t → f ∈ x.asHomogeneousIdeal
have h₁ : (∀ (i : x ∈ t), f ∈ x.asHomogeneousIdeal.toIdeal) ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
Tactic: rw [HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf, HomogeneousIdeal.mem_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
x : ProjectiveSpectrum 𝒜
h :
  Membership.mem (γ := Submodule A A) (⨅ (_ : x ∈ t), x.asHomogeneousIdeal.toIdeal) f ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
h₁ : (∀ (i : x ∈ t), f ∈ x.asHomogeneousIdeal.toIdeal) ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
⊢ Membership.mem (γ := Submodule A A)
      (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : x ∈ t), x.asHomogeneousIdeal)) f ↔
    x ∈ t → f ∈ x.asHomogeneousIdeal
have h₂ : (∀ (i : x ∈ t), f ∈ x.asHomogeneousIdeal) ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
Tactic: rw [HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf, HomogeneousIdeal.mem_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
have rw : f ∈ (↑(vanishingIdeal t) : Set A) ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
Tactic: rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
rw : f ∈ (↑(vanishingIdeal t) : Set A) ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
have rw₁ : Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
Tactic: rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
rw : f ∈ (↑(vanishingIdeal t) : Set A) ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
rw₁ : Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
have rw₂ : (∀ x ∈ t, f ∈ x.asHomogeneousIdeal) ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
Tactic: rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (hypothesis)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ GaloisConnection (fun (s : Set A) ↦ zeroLocus 𝒜 s) fun (t : (Set (ProjectiveSpectrum 𝒜))ᵒᵈ) ↦
    (↑(vanishingIdeal t) : Set A)
have ideal_gc : GaloisConnection (β := Ideal A) Ideal.span SetLike.coe
Tactic: have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi A _).gc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t t' : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal (t ∪ t') = vanishingIdeal t ⊓ vanishingIdeal t'
have h : (vanishingIdeal (t ∪ t')).toIdeal = (vanishingIdeal t ⊓ vanishingIdeal t').toIdeal
Tactic: ext1