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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
refine : (↑(PrimeSpectrum.basicOpen x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 t))
⊢ (↑(X.basicOpen x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 t))

Tactic:
refine (X.isoOfEq (X.toSpecΓ_preimage_basicOpen x)).inv ≫ X.toSpecΓ ∣_ _ ≫ ?_

Premises used: AlgebraicGeometry.Scheme.toSpecΓ, AlgebraicGeometry.Scheme.isoOfEq, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, CategoryTheory.Iso.inv
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
refine : Localization.Away t →+* Localization.Away x
⊢ (↑(PrimeSpectrum.basicOpen x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 t))

Tactic:
refine (basicOpenIsoSpecAway _).hom ≫
    Spec.map (CommRingCat.ofHom (RingHom.comp ?_ (algebraMap _ (Localization.Away t))))

Premises used: AlgebraicGeometry.basicOpenIsoSpecAway, Algebra.algebraMap, Localization.Away, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, RingHom.comp, CategoryTheory.Iso.hom
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
refine : LE.le (α := Submonoid A) (Submonoid.powers t) (Submonoid.comap f (Submonoid.powers x))
⊢ Localization.Away t →+* Localization.Away x

Tactic:
refine IsLocalization.map (M := .powers t) (T := .powers x) _ f ?_

Premises used: IsLocalization.map
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
rw :
  LE.le (α := Submonoid (↑Γ(X, ⊤) : Type u))
    (Submonoid.powers ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) t) : Submonoid (↑Γ(X, ⊤) : Type u))
    (Submonoid.powers x : Submonoid (↑Γ(X, ⊤) : Type u))
⊢ LE.le (α := Submonoid A) (Submonoid.powers t) (Submonoid.comap f (Submonoid.powers x))

Tactic:
rw [← Submonoid.map_le_iff_le_comap, Submonoid.map_powers]

Premises used: Submonoid.map_le_iff_le_comap, Submonoid.map_powers
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ LE.le (α := Submonoid (↑Γ(X, ⊤) : Type u))
    (Submonoid.powers ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) t) : Submonoid (↑Γ(X, ⊤) : Type u))
    (Submonoid.powers x : Submonoid (↑Γ(X, ⊤) : Type u))

Tactic:
simp [H]
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
⊢ X.basicOpen x' ≤ X.basicOpen x

Tactic:
aesop
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
simp :
  Eq (α := (↑(X.basicOpen x') : Scheme) ⟶ Proj 𝒜)
    (Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x) (X.basicOpen 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))
    (Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x') (X.basicOpen 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'))
⊢ Eq (α := (↑(X.basicOpen x') : Scheme) ⟶ Proj 𝒜)
    (X.homOfLE ⋯ ≫ toBasicOpenOfGlobalSections 𝒜 f H h0d hd ≫ Scheme.Opens.ι (basicOpen 𝒜 t))
    (toBasicOpenOfGlobalSections 𝒜 f H' h0d' hd' ≫ Scheme.Opens.ι (basicOpen 𝒜 t'))

Tactic:
simp only [toBasicOpenOfGlobalSections, Scheme.isoOfEq_inv,
    ← Scheme.Hom.resLE_eq_morphismRestrict, CommRingCat.ofHom_comp, Spec.map_comp,
    Scheme.Hom.map_resLE_assoc, Category.assoc, basicOpenIsoSpec_inv_ι]

Premises used: AlgebraicGeometry.Scheme.isoOfEq_inv, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict, AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι, AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Scheme.Hom.map_resLE_assoc, CommRingCat.ofHom_comp
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)

Tactic:
aesop (add simp PrimeSpectrum.basicOpen_mul)

Premises used: PrimeSpectrum.basicOpen_mul
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
⊢ LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)

Tactic:
have hx'x : PrimeSpectrum.basicOpen x' ≤ PrimeSpectrum.basicOpen x := by
    aesop (add simp PrimeSpectrum.basicOpen_mul)
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
⊢ X.basicOpen x' ≤ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen x'

Tactic:
simp [X.toSpecΓ_preimage_basicOpen]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
rw :
  Eq (α := (↑(X.basicOpen x') : Scheme) ⟶ Proj 𝒜)
    (CategoryStruct.comp (Y := (↑(PrimeSpectrum.basicOpen x') : Scheme))
      (Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x') (X.basicOpen x') ⋯)
      ((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)))
    (Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x') (X.basicOpen 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'))
⊢ Eq (α := (↑(X.basicOpen x') : Scheme) ⟶ Proj 𝒜)
    (Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x) (X.basicOpen 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))
    (Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x') (X.basicOpen 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'))

Tactic:
rw [← Scheme.Hom.resLE_map_assoc _ (by simp [X.toSpecΓ_preimage_basicOpen]) hx'x]

Premises used: AlgebraicGeometry.Scheme.Hom.resLE_map_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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
e_a :
  Eq (α := (↑(PrimeSpectrum.basicOpen x') : Scheme) ⟶ Proj 𝒜)
    ((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))
    ((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'))
⊢ Eq (α := (↑(X.basicOpen x') : Scheme) ⟶ Proj 𝒜)
    (CategoryStruct.comp (Y := (↑(PrimeSpectrum.basicOpen x') : Scheme))
      (Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x') (X.basicOpen x') ⋯)
      ((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)))
    (Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x') (X.basicOpen 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'))

Tactic:
congr 1
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
e_a :
  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')))
      (Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f ⋯)))
      (Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t') (Localization.Away t'))) ≫ awayι 𝒜 t' hd' h0d'))
⊢ Eq (α := (↑(PrimeSpectrum.basicOpen x') : Scheme) ⟶ Proj 𝒜)
    ((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))
    ((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'))

Tactic:
simp only [← Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- 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 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
x x' : (↑Γ(X, ⊤) : Type u)
t t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
H' : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t' = x'
h0d' : 0 < d'
hd' : t' ∈ 𝒜 d'
s : A
hts : t * s = t'
n : ℕ
hn : d + n = d'
hs : s ∈ 𝒜 n
hx'x :
  LE.le (α := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) (PrimeSpectrum.basicOpen x')
    (PrimeSpectrum.basicOpen x)
e_a :
  ∀ {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'))
⊢ 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')))
      (Spec.map (CommRingCat.ofHom (IsLocalization.map (Localization.Away x') f ⋯)))
      (Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t') (Localization.Away t'))) ≫ awayι 𝒜 t' hd' h0d'))

Tactic:
subst hts hn
-- 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 𝒜
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' = HMul.hMul (β := (↑Γ(X, ⊤) : Type u)) x ((f : (a : A) → (↑Γ(X, ⊤) : Type u)) s : (↑Γ(X, ⊤) : Type u))

Tactic:
simp [← H', H]
-- 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 𝒜
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)
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 ⋯)))
        (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))
⊢ 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'))

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]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc, DFunLike.coe, 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 𝒜
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)
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 ⋯) (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)
⊢ 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))

Tactic:
simp only [← Category.assoc, ← Spec.map_comp, ← CommRingCat.ofHom_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Spec.map_comp, CommRingCat.ofHom_comp