awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
⊢ Eq (α := Spec (CommRingCat.of (Localization.Away x')) ⟶ Proj 𝒜)
    ((basicOpenIsoSpecAway x').inv ≫
      (Spec Γ(X, ⊤)).homOfLE hx'x ≫
        (basicOpenIsoSpecAway x).hom ≫
          CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away t)))
            (Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x) f ⋯)))
            (Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t) (Localization.Away t))) ≫ awayι 𝒜 t hd h0d))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away (t * s))))
      (Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f ⋯)))
      (Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s)))) ≫
        awayι 𝒜 (t * s) hd' h0d'))
have e_a : Eq (α := Spec (CommRingCat.of (Localization.Away x')) ⟶ Proj 𝒜)
  (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away x)))
    (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away t)))
      (Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x) f sorry)))
      (Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t) (Localization.Away t))) ≫ awayι 𝒜 t hd h0d)))
  (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away (t * s))))
    (Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f sorry)))
    (Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s)))) ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 hs sorry)) ≫ awayι 𝒜 t hd h0d))
Tactic: rw [← SpecMap_awayMap_awayι (𝒜 := 𝒜) hd h0d
    hs rfl, basicOpenIsoSpecAway_inv_homOfLE_assoc (R := Γ(X, ⊤)) x (f s) x' (by simp [← H', H]),
    Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
⊢ Eq (α := Spec (CommRingCat.of (Localization.Away x')) ⟶ Proj 𝒜)
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away x)))
      (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))))
      (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away t)))
        (Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x) f ⋯)))
        (Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t) (Localization.Away t))) ≫ awayι 𝒜 t hd h0d)))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away (t * s))))
      (Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f ⋯)))
      (Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s)))) ≫
        Spec.map (CommRingCat.ofHom (awayMap 𝒜 hs ⋯)) ≫ awayι 𝒜 t hd h0d))
have e_a : Eq (α := Spec (CommRingCat.of (Localization.Away x')) ⟶ Proj 𝒜)
  (Spec.map
      (CommRingCat.ofHom
        (@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
          (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
          (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.map (Localization.Away x) f sorry) (algebraMap (Away 𝒜 t) (Localization.Away t))))) ≫
    awayι 𝒜 t hd h0d)
  (Spec.map
      (CommRingCat.ofHom
        (@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
          (IsLocalization.map (Localization.Away x') f sorry)
          (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs sorry)))) ≫
    awayι 𝒜 t hd h0d)
Tactic: simp only [← Category.assoc, ← Spec.map_comp, ← CommRingCat.ofHom_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
⊢ Eq (α := Spec (CommRingCat.of (Localization.Away x')) ⟶ Proj 𝒜)
    (Spec.map
        (CommRingCat.ofHom
          (@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
            (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
              (IsLocalization.map (Localization.Away x) f ⋯) (algebraMap (Away 𝒜 t) (Localization.Away t))))) ≫
      awayι 𝒜 t hd h0d)
    (Spec.map
        (CommRingCat.ofHom
          (@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.map (Localization.Away x') f ⋯)
            (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs ⋯)))) ≫
      awayι 𝒜 t hd h0d)
have e_a : Eq (α := Away 𝒜 t →+* Localization.Away x')
  (@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
    (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
    (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (Localization.Away x) f sorry) (algebraMap (Away 𝒜 t) (Localization.Away t))))
  (@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
    (IsLocalization.map (Localization.Away x') f sorry)
    (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs sorry)))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
⊢ Eq (α := Away 𝒜 t →+* Localization.Away x')
    (@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
      (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
        (IsLocalization.map (Localization.Away x) f ⋯) (algebraMap (Away 𝒜 t) (Localization.Away t))))
    (@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (Localization.Away x') f ⋯)
      (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs ⋯)))
have e_a : ∀ (x_1 : Away 𝒜 t),
  Eq (α := Localization.Away x')
    ((@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
            (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
              (IsLocalization.map (Localization.Away x) f sorry) (algebraMap (Away 𝒜 t) (Localization.Away t))) :
          (a : Away 𝒜 t) → Localization.Away x')
        x_1 :
      Localization.Away x')
    ((@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.map (Localization.Away x') f sorry)
            (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs sorry)) :
          (a : Away 𝒜 t) → Localization.Away x')
        x_1 :
      Localization.Away x')
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
⊢ Eq (α := Localization.Away x')
    ((@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
            (@RingHom.comp _ (Localization.Away t) _ _ Semiring.toNonAssocSemiring _
              (IsLocalization.map (Localization.Away x) f ⋯) (algebraMap (Away 𝒜 t) (Localization.Away t))) :
          (a : Away 𝒜 t) → Localization.Away x')
        x_1 :
      Localization.Away x')
    ((@RingHom.comp _ (Localization.Away (t * s)) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.map (Localization.Away x') f ⋯)
            (RingHom.comp (algebraMap (Away 𝒜 (t * s)) (Localization.Away (t * s))) (awayMap 𝒜 hs ⋯)) :
          (a : Away 𝒜 t) → Localization.Away x')
        x_1 :
      Localization.Away x')
have e_a : Eq (α := Localization.Away x')
  ((IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s) :
        (a : Localization.Away x) → Localization.Away x')
      ((IsLocalization.map (Localization.Away x) f sorry : (a : Localization.Away t) → Localization.Away x) (val x_1)) :
    Localization.Away x')
  ((IsLocalization.map (Localization.Away x') f sorry : (a : Localization.Away (t * s)) → Localization.Away x')
      ((Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t sorry :
          (a : Localization.Away t) → Localization (Submonoid.powers (t * s)))
        (val x_1)) :
    Localization.Away x')
Tactic: simp only [RingHom.coe_comp, Function.comp_apply,
    HomogeneousLocalization.algebraMap_apply, HomogeneousLocalization.val_awayMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
⊢ Eq (α := Localization.Away x')
    ((IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s) :
          (a : Localization.Away x) → Localization.Away x')
        ((IsLocalization.map (Localization.Away x) f ⋯ : (a : Localization.Away t) → Localization.Away x) (val x_1)) :
      Localization.Away x')
    ((IsLocalization.map (Localization.Away x') f ⋯ : (a : Localization.Away (t * s)) → Localization.Away x')
        ((Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t ⋯ :
            (a : Localization.Away t) → Localization (Submonoid.powers (t * s)))
          (val x_1)) :
      Localization.Away x')
have e_a : Eq (α := Localization.Away x')
  ((@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
          (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
          (IsLocalization.map (Localization.Away x) f sorry) :
        (a : Localization.Away t) → Localization.Away x')
      (val x_1) :
    Localization.Away x')
  ((RingHom.comp (IsLocalization.map (Localization.Away x') f sorry)
          (Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t sorry) :
        (a : Localization.Away t) → Localization.Away x')
      (val x_1) :
    Localization.Away x')
Tactic: simp only [← RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
⊢ Eq (α := Localization.Away x')
    ((@RingHom.comp _ (Localization.Away x) _ _ Semiring.toNonAssocSemiring _
            (IsLocalization.Away.awayToAwayRight x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s))
            (IsLocalization.map (Localization.Away x) f ⋯) :
          (a : Localization.Away t) → Localization.Away x')
        (val x_1) :
      Localization.Away x')
    ((RingHom.comp (IsLocalization.map (Localization.Away x') f ⋯)
            (Localization.awayLift (algebraMap A (Localization (Submonoid.powers (t * s)))) t ⋯) :
          (a : Localization.Away t) → Localization.Away x')
        (val x_1) :
      Localization.Away x')
have e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: apply IsLocalization.ringHom_ext (M := .powers t)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t : A
d : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
s : A
n : ℕ
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) (t * s) = x'
h0d' : 0 < d + n
hd' : t * s ∈ 𝒜 (d + n)
x_1 : Away 𝒜 t
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f_1 : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
⊢ Eq (α := Ideal A)
    (Ideal.span
      (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
        x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
          0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
            r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
    (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
have a : LE.le (α := Ideal A)
  (Ideal.span
    (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
      x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
        0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
          r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
  (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f_1 : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
a :
  LE.le (α := Ideal A)
    (Ideal.span
      (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
        x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
          0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
            r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
    (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
⊢ Eq (α := Ideal A)
    (Ideal.span
      (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
        x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
          0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
            r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
    (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
have a₁ : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
  (Ideal.span
    (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
      x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
        0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
          r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f_1 : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
⊢ LE.le (α := Ideal A)
    (Ideal.span
      (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
        x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
          0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
            r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
    (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
have a : ∀ (y : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i),
  y.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
      0 < y.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
        r ∈ 𝒜 (y.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i))) ∈
    (↑(HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) : Set A)
Tactic: rw [Ideal.span_le, Set.range_subset_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f_1 : A →+* (↑Γ(X, ⊤) : Type u)
x_1 x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
⊢ Membership.mem (γ := Submodule A A)
    (Ideal.span
      (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
        x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
          0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
            r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
    x
have a : Membership.mem (γ := Submodule A A)
  (Ideal.span
    (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
      x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
        0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
          r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
  (∑
    i ∈
      DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x),
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          i) :
      A))
Tactic: rw [← DirectSum.sum_support_decompose 𝒜 x]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f_1 : A →+* (↑Γ(X, ⊤) : Type u)
x_1 x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
x : A
hx : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) x
⊢ Membership.mem (γ := Submodule A A)
    (Ideal.span
      (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
        x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
          0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
            r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
    (∑
      i ∈
        DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x),
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            i) :
        A))
have a : ∀ (c : ℕ)
  (hc :
    Membership.mem (γ := Finset ℕ)
      (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x))
      c),
  Membership.mem (γ := Ideal A)
    (Ideal.span
      (Set.range fun (x : (i : ℕ) ×' (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ↦
        x.snd (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i).fst (β := fun (r : A) ↦
          0 < x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i) ∧
            r ∈ 𝒜 (x.fst (β := fun (i : ℕ) ↦ (r : A) ×' 0 < i ∧ r ∈ 𝒜 i)))))
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) x : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          c) :
      A)
Tactic: refine Ideal.sum_mem _ fun c hc ↦ ?_