awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
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)
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 := ⋯ })),
    ∃ (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)
⊢ ∃ (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⟩

Premises used: Localization.r
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
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)

Tactic:
⟨V, m, i, j, ⟨-r, neg_mem r_mem⟩, ⟨s, s_mem⟩, nin, fun y => ?_⟩

Premises used: Subtype.mk, Exists.intro, Neg.neg, NegMemClass.neg_mem
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
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 := ⋯ })
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) ⋯,
          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)

Tactic:
refine ⟨V, m, i, j, ⟨-r, neg_mem r_mem⟩, ⟨s, s_mem⟩, nin, fun y => ?_⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
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
⊢ ∀ (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 ⋯))

Tactic:
simp only [ext_iff_val, val_mk] at hy

Premises used: HomogeneousLocalization.val_mk, HomogeneousLocalization.ext_iff_val
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
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
y : ↥V
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 ⋯))
⊢ 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 := ⋯ })

Tactic:
simp only [Pi.neg_apply, ext_iff_val, val_neg, hy, val_mk, neg_mk]

Premises used: HomogeneousLocalization.val_mk, HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_neg, Localization.neg_mk, Pi.neg_apply
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
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)
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 := ⋯ })),
    ∃ (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)
⊢ ∃ (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⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
V : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
s t :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
            (CategoryTheory.Presheaf.IsSheaf (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
        V) :
    Type u_1)
h :
  (↑s :
      (x : ↥(unop V)) →
        (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) =
    (↑t :
      (x : ↥(unop V)) →
        (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
⊢ s = t

Tactic:
Subtype.ext h

Premises used: Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
V : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
s t :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
            (CategoryTheory.Presheaf.IsSheaf (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
        V) :
    Type u_1)
x : ↥(unop V)
⊢ (↑(s + t) :
        (x : ↥(unop V)) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      x =
    (↑s :
          (x : ↥(unop V)) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x +
      (↑t :
          (x : ↥(unop V)) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
V : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
s t :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
            (CategoryTheory.Presheaf.IsSheaf (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
        V) :
    Type u_1)
x : ↥(unop V)
⊢ (↑(s * t) :
        (x : ↥(unop V)) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      x =
    (↑s :
          (x : ↥(unop V)) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x *
      (↑t :
          (x : ↥(unop V)) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
V : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
s t :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
            (CategoryTheory.Presheaf.IsSheaf (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
        V) :
    Type u_1)
x : ↥(unop V)
⊢ (↑(s - t) :
        (x : ↥(unop V)) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      x =
    (↑s :
          (x : ↥(unop V)) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x -
      (↑t :
          (x : ↥(unop V)) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
V : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
            (CategoryTheory.Presheaf.IsSheaf (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
        V) :
    Type u_1)
x : ↥(unop V)
n : ℕ
⊢ (↑(s ^ n) :
        (x : ↥(unop V)) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      x =
    (↑s :
          (x : ↥(unop V)) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x ^
      n

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
V : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
x : ↥(unop V)
⊢ Eq.{u_1 + 1} (α :=
    (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
    ((↑0 :
        (x : ↥(unop V)) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      x)
    0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
V : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ
x : ↥(unop V)
⊢ Eq.{u_1 + 1} (α :=
    (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
    ((↑1 :
        (x : ↥(unop V)) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      x)
    1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
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)
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hx : x ∈ U
⊢ Eq (α :=
    Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) (op U) ⟶
      CommRingCat.of (at x))
    (CategoryStruct.comp (Y := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
        (Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) U x hx :
          Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
              (op U) ⟶
            Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
        (stalkToFiberRingHom 𝒜 x : Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x ⟶ CommRingCat.of (at x)) :
      Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) (op U) ⟶
        CommRingCat.of (at x))
    (openToLocalization 𝒜 U x hx :
      Functor.obj
          (ObjectProperty.FullSubcategory.obj (P :=
              (CategoryTheory.Presheaf.IsSheaf (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
              (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
            (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
          (op U) ⟶
        CommRingCat.of (at x))

Tactic:
Limits.colimit.ι_desc _ _

Premises used: Set.Mem, setOf, CategoryTheory.Functor.comp, AlgebraicGeometry.openToLocalization, CategoryTheory.Limits.colimit.ι_desc