awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  ∀ (U : (Proj 𝒜).Opens) (e : U = ⊤),
    Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ (↑U : Scheme))
      (Scheme.Opens.ι (basicOpen 𝒜 f) ≫ Iso.inv (Proj 𝒜).topIso ≫ ((Proj 𝒜).isoOfEq e).inv) ((Proj 𝒜).homOfLE ⋯)
rw :
  Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
    (Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫
      Spec.map
        ((CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1)) ≫ awayToSection 𝒜 1) ≫
          (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
    (Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫
      Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)) ≫ awayToSection 𝒜 f))
⊢ Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
    (Scheme.Opens.ι (basicOpen 𝒜 f) ≫
      Iso.inv (Proj 𝒜).topIso ≫
        Iso.inv ((Proj 𝒜).isoOfEq ⋯) ≫
          Scheme.Opens.toSpecΓ (basicOpen 𝒜 1) ≫
            Spec.map (awayToSection 𝒜 1) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))))
    (basicOpenToSpec 𝒜 f ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f))))

Tactic:
rw [reassoc_of% this, ← Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, basicOpenToSpec,
    Category.assoc, ← Spec.map_comp, ← Spec.map_comp, ← Spec.map_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Proj.basicOpenToSpec
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  ∀ (U : (Proj 𝒜).Opens) (e : U = ⊤),
    Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ (↑U : Scheme))
      (Scheme.Opens.ι (basicOpen 𝒜 f) ≫ Iso.inv (Proj 𝒜).topIso ≫ ((Proj 𝒜).isoOfEq e).inv) ((Proj 𝒜).homOfLE ⋯)
⊢ Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
    (Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫
      Spec.map
        ((CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1)) ≫ awayToSection 𝒜 1) ≫
          (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
    (Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫
      Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)) ≫ awayToSection 𝒜 f))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
hf :
  ∀ (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)),
    Eq (α := (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
      ((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x) :
            (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
          a :
        (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
      ((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
            (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
          a :
        (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
⊢ CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x =
    awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
ext a
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)
hf :
  Eq.{u + 1} (α :=
    (x_1 :
        ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)) :
            TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))) →
      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
        (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
    (↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x) :
            (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
          a) :
      (x_1 : ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)))) →
        (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
          (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
    (↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
            (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
          a) :
      (x_1 : ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)))) →
        (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
          (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
⊢ Eq (α := (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
    ((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x) :
          (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
        a :
      (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
    ((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
        a :
      (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)
hi :
  Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
    (Opposite.unop (Opposite.op (basicOpen 𝒜 x)) : TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u)) i_1
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) i ∈ 𝒜 n
⊢ Eq (α := Localization (M := A) i_1.asHomogeneousIdeal.toIdeal.primeCompl)
    (Localization.mk ((RingHom.id A : (a : A) → A) ((↑a : A) * g ^ i))
        (Subtype.mk (p := fun (x_1 : A) ↦
          x_1 ∈
            (↑(Subtype.mk (p := fun (x_2 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                        Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                          (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_2)
                        i_1 hi) :
                    (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl)
          ((RingHom.id A : (a : A) → A)
            (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯) :
              A))
          ⋯) :
      Localization (M := A)
        (↑(Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                    Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                      (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_1)
                    i_1 hi) :
                (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl)
    (val.{0, u, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
        ((↑((CommRingCat.Hom.hom ((Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                  (a : (↑Γ(Proj 𝒜, basicOpen 𝒜 f) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
                ((CommRingCat.Hom.hom (awayToSection 𝒜 f) : (a : Away 𝒜 f) → (↑Γ(Proj 𝒜, basicOpen 𝒜 f) : Type u))
                  (mk
                    { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ i) hb',
                      den_mem := ⋯ }))) :
            (x_1 : ↥(basicOpen 𝒜 x)) →
              AtPrime 𝒜 (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal)
          (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
            Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
              (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_1)
            i_1 hi)) :
      Localization (M := A) i_1.asHomogeneousIdeal.toIdeal.primeCompl)

Tactic:
Localization.mk_eq_mk_iff.mpr ?_

Premises used: Iff.mpr, Localization.mk, Quotient.liftOn', Set.Mem, setOf, Quotient.mk', OreLocalization.oreDiv, Localization.mk_eq_mk_iff, HomogeneousLocalization.NumDenSameDeg.embedding, HomogeneousLocalization.val
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)
hi :
  Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
    (Opposite.unop (Opposite.op (basicOpen 𝒜 x)) : TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u)) i_1
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) i ∈ 𝒜 n
⊢ f ^ i * ((↑a : A) * g ^ i) = (f * g) ^ i * (↑a : A)

Tactic:
ring
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
rw :
  Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 f)))
    ((Proj 𝒜).homOfLE ⋯ ≫ Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫ Spec.map (awayToSection 𝒜 f))
    ((Proj 𝒜).homOfLE ⋯ ≫ basicOpenToSpec 𝒜 f)
⊢ Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 f)))
    (basicOpenToSpec 𝒜 x ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx))) ((Proj 𝒜).homOfLE ⋯ ≫ basicOpenToSpec 𝒜 f)

Tactic:
rw [basicOpenToSpec, Category.assoc, ← Spec.map_comp, awayMap_awayToSection,
    Spec.map_comp, Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Proj.awayMap_awayToSection, AlgebraicGeometry.Proj.basicOpenToSpec
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 f)))
    ((Proj 𝒜).homOfLE ⋯ ≫ Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫ Spec.map (awayToSection 𝒜 f))
    ((Proj 𝒜).homOfLE ⋯ ≫ basicOpenToSpec 𝒜 f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
rw :
  Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫
      Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
    (awayι 𝒜 x ⋯ ⋯)
rw₁ :
  Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫
      Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
    (Iso.inv (basicOpenIsoSpec 𝒜 x ⋯ ⋯) ≫ Scheme.Opens.ι (basicOpen 𝒜 x))
rw₂ :
  Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜)
    (Iso.hom (basicOpenIsoSpec 𝒜 x ⋯ ⋯) ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫
        Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
    (Scheme.Opens.ι (basicOpen 𝒜 x))
rw₃ :
  Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜)
    (basicOpenToSpec 𝒜 x ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫
        Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
    (Scheme.Opens.ι (basicOpen 𝒜 x))
rw₄ :
  Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜)
    ((Proj 𝒜).homOfLE ⋯ ≫
      basicOpenToSpec 𝒜 f ≫ Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
    (Scheme.Opens.ι (basicOpen 𝒜 x))
rw₅ :
  Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜)
    ((Proj 𝒜).homOfLE ⋯ ≫
      Iso.hom (basicOpenIsoSpec 𝒜 f f_deg hm) ≫
        Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
    (Scheme.Opens.ι (basicOpen 𝒜 x))
rw₆ :
  Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜) ((Proj 𝒜).homOfLE ⋯ ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
    (Scheme.Opens.ι (basicOpen 𝒜 x))
rw₇ rw₈ :
  Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜) (Scheme.Opens.ι (basicOpen 𝒜 x)) (Scheme.Opens.ι (basicOpen 𝒜 x))
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm) (awayι 𝒜 x ⋯ ⋯)

Tactic:
rw [awayι, awayι, Iso.eq_inv_comp, basicOpenIsoSpec_hom, basicOpenToSpec_SpecMap_awayMap_assoc,
  ← basicOpenIsoSpec_hom _ _ f_deg hm, Iso.hom_inv_id_assoc, Scheme.homOfLE_ι]

Premises used: AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc, CategoryTheory.Iso.hom_inv_id_assoc, AlgebraicGeometry.Proj.basicOpenIsoSpec_hom, CategoryTheory.Iso.eq_inv_comp, AlgebraicGeometry.Proj.awayι
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
rw :
  Eq (α := Set ↥(Proj 𝒜))
    (Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 f)))) ⇑(awayι 𝒜 f f_deg hm) ∩
      Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 g)))) ⇑(awayι 𝒜 g g_deg hm'))
    (Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 x)))) ⇑(awayι 𝒜 x ⋯ ⋯))
⊢ Eq (α := Set ↥(Proj 𝒜))
    (Set.range (ι :=
      ↥(Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))
      ⇑(Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ≫ awayι 𝒜 f f_deg hm))
    (Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 x)))) ⇑(awayι 𝒜 x ⋯ ⋯))

Tactic:
rw [IsOpenImmersion.range_pullback_to_base_of_left]

Premises used: AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g_1 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
rw :
  Eq (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 f ⊓ Scheme.Hom.opensRange (awayι 𝒜 g g_deg hm')))
    (TopologicalSpace.Opens.carrier (Scheme.Hom.opensRange (awayι 𝒜 x ⋯ ⋯)))
rw₁ :
  Eq (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g))
    (TopologicalSpace.Opens.carrier (Scheme.Hom.opensRange (awayι 𝒜 x ⋯ ⋯)))
rw₂ :
  Eq (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g))
    (TopologicalSpace.Opens.carrier (basicOpen 𝒜 x))
rw₃ :
  Eq (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (f * g)))
    (TopologicalSpace.Opens.carrier (basicOpen 𝒜 x))
rw₄ rw₅ :
  Eq (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (f * g)))
    (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (f * g)))
⊢ Eq (α := Set ↥(Proj 𝒜))
    (TopologicalSpace.Opens.carrier
      (Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm) ⊓ Scheme.Hom.opensRange (awayι 𝒜 g g_deg hm')))
    (TopologicalSpace.Opens.carrier (Scheme.Hom.opensRange (awayι 𝒜 x ⋯ ⋯)))

Tactic:
rw [opensRange_awayι, opensRange_awayι, opensRange_awayι, ← basicOpen_mul, hx]

Premises used: AlgebraicGeometry.Proj.basicOpen_mul, AlgebraicGeometry.Proj.opensRange_awayι
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ Eq (α := Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ⟶ Proj 𝒜)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)
    (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ≫ awayι 𝒜 f f_deg hm)

Tactic:
IsOpenImmersion.isoOfRangeEq_hom_fac ..

Premises used: AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
rw :
  Eq (α := Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ⟶ Proj 𝒜)
    ((Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx))) ≫
      awayι 𝒜 f f_deg hm)
    (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ≫ awayι 𝒜 f f_deg hm)
rw₁ :
  Eq (α := Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ⟶ Proj 𝒜)
    ((Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx))) ≫
      awayι 𝒜 f f_deg hm)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)
x₁ : A
hx₁ : x = f * g
rw₂ :
  Eq (α := Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ⟶ Proj 𝒜)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫
      Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)
x₂ : A
hx₂ : x = f * g
rw₃ :
  Eq (α := Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ⟶ Proj 𝒜)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)
x₃ : A
hx₃ : x = f * g
rw₄ :
  Eq (α := Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ⟶ Proj 𝒜)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)
x₄ : A
hx₄ : x = f * g
⊢ Eq (α :=
    Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ⟶
      Spec (CommRingCat.of (Away 𝒜 f)))
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)))
    (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))

Tactic:
rw [← cancel_mono (awayι 𝒜 f f_deg hm), ← pullbackAwayιIso_hom_awayι,
    Category.assoc, SpecMap_awayMap_awayι]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι, CategoryTheory.cancel_mono, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι, AlgebraicGeometry.Proj.awayι
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
rw :
  Eq (α := Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ⟶ Proj 𝒜)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)
⊢ Eq (α :=
    Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ⟶
      Spec (CommRingCat.of (Away 𝒜 g)))
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯)))
    (Limits.pullback.snd (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))

Tactic:
rw [← cancel_mono (awayι 𝒜 g g_deg hm'), ← Limits.pullback.condition,
    ← pullbackAwayιIso_hom_awayι 𝒜 f_deg hm g_deg hm' hx,
    Category.assoc, SpecMap_awayMap_awayι]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι, CategoryTheory.cancel_mono, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Proj.awayι
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
⊢ Eq (α := Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ⟶ Proj 𝒜)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)
    (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x ⋯ ⋯)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
rw :
  Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Spec (CommRingCat.of (Away 𝒜 f)))
    (Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫
      Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)))
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)))
x₁ : A
hx₁ : x = f * g
rw₁ :
  Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Spec (CommRingCat.of (Away 𝒜 f)))
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx))) (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)))
hx₂ : x = f * g
rw₂ :
  Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Spec (CommRingCat.of (Away 𝒜 f)))
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx))) (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)))
hx₃ : x = f * g
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Spec (CommRingCat.of (Away 𝒜 f)))
    (Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫
      Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)))

Tactic:
rw [← pullbackAwayιIso_hom_SpecMap_awayMap_left, Iso.inv_hom_id_assoc]

Premises used: AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left, CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x : A
hx : x = f * g
rw :
  Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Spec (CommRingCat.of (Away 𝒜 g)))
    (Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫
      Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯)))
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯)))
rw₁ rw₂ :
  Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Spec (CommRingCat.of (Away 𝒜 g)))
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯))) (Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯)))
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Spec (CommRingCat.of (Away 𝒜 g)))
    (Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫
      Limits.pullback.snd (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg ⋯)))

Tactic:
rw [← pullbackAwayιIso_hom_SpecMap_awayMap_right (hx := hx) .., Iso.inv_hom_id_assoc]

Premises used: AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right, CategoryTheory.Iso.inv_hom_id_assoc