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 𝒜
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
intro intro₁ :
  ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z),
    Membership.mem (γ := Submodule A A)
      (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) z
⊢ LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
have intro₂ : ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z),
  Membership.mem (γ := Submodule A A)
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
    (∑
      i ∈
        DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z),
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            i) :
        A))
Tactic: classical
  intro z hz
  rw [← DirectSum.sum_support_decompose 𝒜 z]
  refine Ideal.sum_mem _ fun c hc ↦ if hc0 : c = 0 then ?_ else
    Ideal.subset_span ⟨⟨⟨c, Nat.pos_iff_ne_zero.mpr hc0⟩, _⟩, rfl⟩
  convert! Ideal.zero_mem _
  subst hc0
  exact hz
-- 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 𝒜
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
intro intro₁ :
  ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z),
    Membership.mem (γ := Submodule A A)
      (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) z
intro₂ :
  ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z),
    Membership.mem (γ := Submodule A A)
      (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
      (∑
        i ∈
          DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
            ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z),
        (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z :
                  DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              i) :
          A))
⊢ LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
have intro₃ : ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z)
  (c : ℕ)
  (hc :
    Membership.mem (γ := Finset ℕ)
      (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
      c)
  (hc0 : c = 0),
  Membership.mem (γ := Ideal A)
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
    (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          c) :
      A)
Tactic: classical
  intro z hz
  rw [← DirectSum.sum_support_decompose 𝒜 z]
  refine Ideal.sum_mem _ fun c hc ↦ if hc0 : c = 0 then ?_ else
    Ideal.subset_span ⟨⟨⟨c, Nat.pos_iff_ne_zero.mpr hc0⟩, _⟩, rfl⟩
  convert! Ideal.zero_mem _
  subst hc0
  exact hz
-- 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 𝒜
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
intro intro₁ :
  ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z),
    Membership.mem (γ := Submodule A A)
      (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) z
intro₂ :
  ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z),
    Membership.mem (γ := Submodule A A)
      (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
      (∑
        i ∈
          DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
            ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z),
        (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z :
                  DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              i) :
          A))
intro₃ :
  ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z)
    (c : ℕ)
    (hc :
      Membership.mem (γ := Finset ℕ)
        (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
          ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
        c)
    (hc0 : c = 0),
    Membership.mem (γ := Ideal A)
      (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
      (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            c) :
        A)
⊢ LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))
    (Ideal.span (Set.range fun (i : (i : ℕ+) × ↥(𝒜 (↑i : ℕ))) ↦ (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
have h : ∀ ⦃z : A⦄ (hz : Membership.mem (γ := Submodule A A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) z)
  (c : ℕ)
  (hc :
    Membership.mem (γ := Finset ℕ)
      (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
      c)
  (hc0 : c = 0),
  (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          c) :
      A) =
    0
Tactic: classical
  intro z hz
  rw [← DirectSum.sum_support_decompose 𝒜 z]
  refine Ideal.sum_mem _ fun c hc ↦ if hc0 : c = 0 then ?_ else
    Ideal.subset_span ⟨⟨⟨c, Nat.pos_iff_ne_zero.mpr hc0⟩, _⟩, rfl⟩
  convert! Ideal.zero_mem _
  subst hc0
  exact hz
-- 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 t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ (↑(X.basicOpen x) : Scheme) ⟶ (↑(basicOpen 𝒜 t) : Scheme)
have refine : (↑(X.basicOpen x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 t))
Tactic: refine ?_ ≫ (basicOpenIsoSpec _ _ hd h0d).inv
-- 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 t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ (↑(X.basicOpen x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 t))
have refine : (↑(PrimeSpectrum.basicOpen x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 t))
Tactic: refine (X.isoOfEq (X.toSpecΓ_preimage_basicOpen x)).inv ≫ X.toSpecΓ ∣_ _ ≫ ?_
-- 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 t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ (↑(PrimeSpectrum.basicOpen x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 t))
have refine : Localization.Away t →+* Localization.Away x
Tactic: refine (basicOpenIsoSpecAway _).hom ≫
    Spec.map (CommRingCat.ofHom (RingHom.comp ?_ (algebraMap _ (Localization.Away 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 t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ Localization.Away t →+* Localization.Away x
have refine : LE.le (α := Submonoid A) (Submonoid.powers t) (Submonoid.comap f (Submonoid.powers x))
Tactic: refine IsLocalization.map (M := .powers t) (T := .powers x) _ f ?_
-- 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 t' : A
d d' : ℕ
H : (f : (a : A) → (↑Γ(X, ⊤) : Type u)) t = x
h0d : 0 < d
hd : t ∈ 𝒜 d
⊢ LE.le (α := Submonoid A) (Submonoid.powers t) (Submonoid.comap f (Submonoid.powers x))
have 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))
Tactic: rw [← Submonoid.map_le_iff_le_comap, Submonoid.map_powers]
-- 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 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
⊢ 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'))
have simp : Eq (α := (↑(X.basicOpen x') : Scheme) ⟶ Proj 𝒜)
  (Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x) (X.basicOpen x') sorry ≫
    (basicOpenIsoSpecAway x).hom ≫
      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))
  (Scheme.Hom.resLE X.toSpecΓ (PrimeSpectrum.basicOpen x') (X.basicOpen x') sorry ≫
    (basicOpenIsoSpecAway x').hom ≫
      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'))
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_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (hypothesis)
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
⊢ 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'))
have hx'x : 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)
-- 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 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)
⊢ 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'))
have 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') sorry)
    ((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 sorry)))
          (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') sorry ≫
    (basicOpenIsoSpecAway x').hom ≫
      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'))
Tactic: rw [← Scheme.Hom.resLE_map_assoc _ (by simp [X.toSpecΓ_preimage_basicOpen]) hx'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 : 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)
⊢ 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'))
have 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 sorry)))
        (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 sorry)))
      (Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t') (Localization.Away t'))) ≫ awayι 𝒜 t' hd' h0d'))
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 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)
⊢ 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'))
have 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 sorry)))
          (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 sorry)))
    (Spec.map (CommRingCat.ofHom (algebraMap (Away 𝒜 t') (Localization.Away t'))) ≫ awayι 𝒜 t' hd' h0d'))
Tactic: simp only [← Iso.inv_comp_eq]
-- 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 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)
⊢ 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'))
have 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 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)))) ≫
        awayι 𝒜 (t * s) hd' h0d'))
Tactic: subst hts hn
Cleared hypotheses: t', d', H', h0d', hd', hts, hn