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 : 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
⊢ 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'))
have 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 sorry sorry)
Tactic: rw [← cancel_mono (awayι 𝒜 f f_deg hm), ← pullbackAwayιIso_hom_awayι,
    Category.assoc, SpecMap_awayMap_awayι]
-- 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 : 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
⊢ 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'))
have 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 sorry sorry)
  (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x sorry sorry)
Tactic: rw [← cancel_mono (awayι 𝒜 f f_deg hm), ← pullbackAwayιIso_hom_awayι,
    Category.assoc, SpecMap_awayMap_awayι]
-- 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 : 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') ⟶
      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'))
have 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 sorry sorry)
  (Iso.hom (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx) ≫ awayι 𝒜 x sorry sorry)
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ι]
-- 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 : 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 (α := 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)))
have 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)))
Tactic: rw [← pullbackAwayιIso_hom_SpecMap_awayMap_left, 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 𝒜
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
⊢ 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)))
have 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)))
Tactic: rw [← pullbackAwayιIso_hom_SpecMap_awayMap_left, 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 𝒜
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 (α := 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 ⋯)))
have 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 sorry)))
  (Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg sorry)))
Tactic: rw [← pullbackAwayιIso_hom_SpecMap_awayMap_right (hx := hx) .., 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 𝒜
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 ⋯)))
⊢ 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 ⋯)))
have rw₁ : Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Spec (CommRingCat.of (Away 𝒜 g)))
  (Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg sorry))) (Spec.map (CommRingCat.ofHom (awayMap 𝒜 f_deg sorry)))
Tactic: rw [← pullbackAwayιIso_hom_SpecMap_awayMap_right (hx := hx) .., 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 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ Eq (α := (Spec (CommRingCat.of (Away 𝒜 f))).Opens) (awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g)
    (PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg))
have h : (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
  (↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))
Tactic: ext1
-- 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 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    (↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))
have trans : (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
  Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg sorry)))
Tactic: trans Set.range (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg rfl)))
-- 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 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
trans :
  (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯)))
⊢ (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    (↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))
have trans₁ : Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg sorry))) =
  (↑(PrimeSpectrum.basicOpen (Away.isLocalizationElem f_deg g_deg)) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))
Tactic: trans Set.range (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg rfl)))
-- 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 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) ⇑(Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg ⋯)))
have rw : (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
  Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g)))))
    ⇑(Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' sorry) ≫
        Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))
Tactic: rw [← pullbackAwayιIso_inv_fst 𝒜 f_deg hm g_deg hm' rfl]
-- 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 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ (↑(awayι 𝒜 f f_deg hm ⁻¹ᵁ basicOpen 𝒜 g) : Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) =
    Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g)))))
      ⇑(Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯) ≫
          Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))
have simp : Eq (α := Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) (⇑(awayι 𝒜 f f_deg hm) ⁻¹' (↑(basicOpen 𝒜 g) : Set ↥(Proj 𝒜)))
  (Set.image (α :=
    ↥(Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))
    (⇑(TopCat.Hom.hom
          (PresheafedSpace.Hom.base
            (LocallyRingedSpace.Hom.toHom
              (Scheme.Hom.toLRSHom' (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))) :
      (a : ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))) → ↥(Spec (CommRingCat.of (Away 𝒜 f))))
    (Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g)))))
      (⇑(TopCat.Hom.hom
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toHom
                (Scheme.Hom.toLRSHom' (Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' sorry)))))) :
        (a : ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) →
          ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))
Tactic: simp only [TopologicalSpace.Opens.map_coe, Scheme.Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.coe_comp, Set.range_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 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
⊢ Eq (α := Set ↥(Spec (CommRingCat.of (Away 𝒜 f)))) (⇑(awayι 𝒜 f f_deg hm) ⁻¹' (↑(basicOpen 𝒜 g) : Set ↥(Proj 𝒜)))
    (Set.image (α :=
      ↥(Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))
      (⇑(TopCat.Hom.hom
            (PresheafedSpace.Hom.base
              (LocallyRingedSpace.Hom.toHom
                (Scheme.Hom.toLRSHom' (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))) :
        (a : ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))) → ↥(Spec (CommRingCat.of (Away 𝒜 f))))
      (Set.range (ι := ↥(Spec (CommRingCat.of (Away 𝒜 (f * g)))))
        (⇑(TopCat.Hom.hom
              (PresheafedSpace.Hom.base
                (LocallyRingedSpace.Hom.toHom
                  (Scheme.Hom.toLRSHom' (Iso.inv (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' ⋯)))))) :
          (a : ↥(Spec (CommRingCat.of (Away 𝒜 (f * g))))) →
            ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))
have rw : Eq (α := Set ↥(Spec (CommRingCat.of (Away 𝒜 f))))
  (⇑(awayι 𝒜 f f_deg hm) ⁻¹' (↑(Scheme.Hom.opensRange (awayι 𝒜 g g_deg hm')) : Set ↥(Proj 𝒜)))
  (Set.image (α :=
    ↥(Limits.pullback (X := Spec (CommRingCat.of (Away 𝒜 f))) (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))
    (⇑(TopCat.Hom.hom
          (PresheafedSpace.Hom.base
            (LocallyRingedSpace.Hom.toHom
              (Scheme.Hom.toLRSHom' (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')))))) :
      (a : ↥(Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm'))) → ↥(Spec (CommRingCat.of (Away 𝒜 f))))
    Set.univ)
Tactic: rw [Set.range_eq_univ.mpr (by exact
      (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' rfl).inv.homeomorph.surjective),
      ← opensRange_awayι _ _ g_deg hm']
-- 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_1 g_1 : A
m_1 : ℕ
f_deg_1 : f_1 ∈ 𝒜 m_1
hm_1 : 0 < m_1
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
hm' : 0 < m'
x_1 : A
hx : x_1 = f_1 * g
ι : Type u_2
f : ι → A
m : ι → ℕ
f_deg : ∀ (i : ι), f i ∈ 𝒜 (m i)
hm : ∀ (i : ι), 0 < m i
hf : LE.le (α := Ideal A) (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜)) (Ideal.span (Set.range f))
x : ↥(Proj 𝒜)
⊢ Membership.mem (γ := (Proj 𝒜).Opens)
    (Scheme.Hom.opensRange (X :=
      Spec
        (CommRingCat.of
          (Away 𝒜
            (f
              (Exists.choose (p := fun (i : ι) ↦
                Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x) ⋯)))))
      (awayι 𝒜
        (f
          (Exists.choose (p := fun (i : ι) ↦
            Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x) ⋯))
        ⋯ ⋯))
    x
have rw : Membership.mem (γ := (Proj 𝒜).Opens)
  (basicOpen 𝒜
    (f
      (Exists.choose (p := fun (i : ι) ↦ Membership.mem (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (f i)) x)
        sorry)))
  x
Tactic: rw [opensRange_awayι]
-- 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
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
have rw : 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: rw [← DirectSum.sum_support_decompose 𝒜 z]
-- 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
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))
have refine : ∀ (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: 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⟩
-- 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
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)
have h : (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
          (a : ℕ) → ↥(𝒜 a))
        c) :
    A) =
  0
Tactic: convert! Ideal.zero_mem _
-- 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
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
have h : ∀
  (hc :
    Membership.mem (γ := Finset ℕ)
      (DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i))
        ((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z))
      0),
  (↑((((DirectSum.decompose 𝒜 : (a : A) → DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) z : DirectSum ℕ fun (i : ℕ) ↦ ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          0) :
      A) =
    0
Tactic: subst hc0
Cleared hypotheses: c, hc, hc0
-- 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
⊢ 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⦄,
  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
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