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' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 f)))
    (basicOpenToSpec 𝒜 x ≫ Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx))) ((Proj 𝒜).homOfLE ⋯ ≫ basicOpenToSpec 𝒜 f)
have rw : Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 f)))
  ((Proj 𝒜).homOfLE sorry ≫ Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫ Spec.map (awayToSection 𝒜 f))
  ((Proj 𝒜).homOfLE sorry ≫ basicOpenToSpec 𝒜 f)
Tactic: rw [basicOpenToSpec, Category.assoc, ← Spec.map_comp, awayMap_awayToSection,
    Spec.map_comp, Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_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'
x : A
hx : x = f * g
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm) (awayι 𝒜 x ⋯ ⋯)
have 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 sorry sorry)
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_ι]
-- 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'
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 ⋯ ⋯)
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm) (awayι 𝒜 x ⋯ ⋯)
have 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 sorry sorry) ≫ Scheme.Opens.ι (basicOpen 𝒜 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_ι]
-- 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'
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))
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm) (awayι 𝒜 x ⋯ ⋯)
have rw₂ : Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜)
  (Iso.hom (basicOpenIsoSpec 𝒜 x sorry sorry) ≫
    Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫
      Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
  (Scheme.Opens.ι (basicOpen 𝒜 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_ι]
-- 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'
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))
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm) (awayι 𝒜 x ⋯ ⋯)
have 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))
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_ι]
-- 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'
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))
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm) (awayι 𝒜 x ⋯ ⋯)
have rw₄ : Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜)
  ((Proj 𝒜).homOfLE sorry ≫ basicOpenToSpec 𝒜 f ≫ Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
  (Scheme.Opens.ι (basicOpen 𝒜 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_ι]
-- 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'
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))
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm) (awayι 𝒜 x ⋯ ⋯)
have rw₅ : Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜)
  ((Proj 𝒜).homOfLE sorry ≫
    Iso.hom (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
  (Scheme.Opens.ι (basicOpen 𝒜 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_ι]
-- 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'
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))
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm) (awayι 𝒜 x ⋯ ⋯)
have rw₆ : Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜) ((Proj 𝒜).homOfLE sorry ≫ Scheme.Opens.ι (basicOpen 𝒜 f))
  (Scheme.Opens.ι (basicOpen 𝒜 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_ι]
-- 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'
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))
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 x)) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)) ≫ awayι 𝒜 f f_deg hm) (awayι 𝒜 x ⋯ ⋯)
have rw₇ : Eq (α := (↑(basicOpen 𝒜 x) : Scheme) ⟶ Proj 𝒜) (Scheme.Opens.ι (basicOpen 𝒜 x)) (Scheme.Opens.ι (basicOpen 𝒜 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_ι]
-- 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
⊢ 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 ⋯ ⋯))
have 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 sorry sorry))
Tactic: rw [IsOpenImmersion.range_pullback_to_base_of_left]
-- 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
⊢ 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 ⋯ ⋯)))
have 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 sorry sorry)))
Tactic: rw [opensRange_awayι, opensRange_awayι, opensRange_awayι, ← basicOpen_mul, hx]
-- 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
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 ⋯ ⋯)))
⊢ 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 ⋯ ⋯)))
have rw₁ : Eq (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g))
  (TopologicalSpace.Opens.carrier (Scheme.Hom.opensRange (awayι 𝒜 x sorry sorry)))
Tactic: rw [opensRange_awayι, opensRange_awayι, opensRange_awayι, ← basicOpen_mul, hx]
-- 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
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 ⋯ ⋯)))
⊢ 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 ⋯ ⋯)))
have rw₂ : Eq (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 f ⊓ basicOpen 𝒜 g))
  (TopologicalSpace.Opens.carrier (basicOpen 𝒜 x))
Tactic: rw [opensRange_awayι, opensRange_awayι, opensRange_awayι, ← basicOpen_mul, hx]
-- 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
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))
⊢ 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 ⋯ ⋯)))
have rw₃ : Eq (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (f * g)))
  (TopologicalSpace.Opens.carrier (basicOpen 𝒜 x))
Tactic: rw [opensRange_awayι, opensRange_awayι, opensRange_awayι, ← basicOpen_mul, hx]
-- 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
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))
⊢ 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 ⋯ ⋯)))
have rw₄ : Eq (α := Set ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (f * g)))
  (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (f * g)))
Tactic: rw [opensRange_awayι, opensRange_awayι, opensRange_awayι, ← basicOpen_mul, hx]
-- 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 𝒜 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)
  (Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ≫ awayι 𝒜 f f_deg hm)
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)
⊢ 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ι]