awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
s : Set A
⊢ Eq (α := Set (ProjectiveSpectrum ℬ))
    (Set.preimage (β := ProjectiveSpectrum 𝒜) (comapFun f hf : (p : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
        (zeroLocus 𝒜 s : Set (ProjectiveSpectrum 𝒜)) :
      Set (ProjectiveSpectrum ℬ))
    (zeroLocus ℬ ((⇑f : (a : A) → B) '' s) : Set (ProjectiveSpectrum ℬ))
have h : ∀ (x : ProjectiveSpectrum ℬ),
  Membership.mem (γ := Set (ProjectiveSpectrum ℬ))
      (Set.preimage (β := ProjectiveSpectrum 𝒜) (comapFun f hf : (p : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
          (zeroLocus 𝒜 s : Set (ProjectiveSpectrum 𝒜)) :
        Set (ProjectiveSpectrum ℬ))
      x ↔
    Membership.mem (γ := Set (ProjectiveSpectrum ℬ)) (zeroLocus ℬ ((⇑f : (a : A) → B) '' s)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [← Iso.eq_inv_comp, Iso.comp_inv_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext x : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
x :
  AtPrime 𝒜
    (toIdeal (σ := σ) (𝒜 := 𝒜)
      (asHomogeneousIdeal
        (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
            (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
          p)))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: obtain ⟨c, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
c :
  NumDenSameDeg 𝒜
    (Ideal.primeCompl
      (toIdeal (σ := σ) (𝒜 := 𝒜)
        (asHomogeneousIdeal
          (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
              (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            p))))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [val_localRingHom, val_mk, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
c :
  NumDenSameDeg 𝒜
    (Ideal.primeCompl
      (toIdeal (σ := σ) (𝒜 := 𝒜)
        (asHomogeneousIdeal
          (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
              (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            p))))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [GradedRingHom.toRingHom_eq_toRingHom, Localization.localRingHom_mk,
    GradedRingHom.coe_toRingHom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
c :
  NumDenSameDeg 𝒜
    (Ideal.primeCompl
      (toIdeal (σ := σ) (𝒜 := 𝒜)
        (asHomogeneousIdeal
          (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
              (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            p))))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: erw [stalkIso'_symm_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (hypothesis)
Goal:
A B C σ τ ψ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
p : ↥(Proj ℬ)
x :
  (↑((Proj 𝒜).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(Proj ℬ).toPresheafedSpace : TopCat)) (Y := (↑(Proj 𝒜).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (sheafedSpaceMap f hf))) :
            (a : ↥(Proj ℬ)) → ↥(Proj 𝒜))
          p)) :
    Type u)
hx :
  IsUnit (M := (↑((Proj ℬ).presheaf.stalk p) : Type u))
    ((CommRingCat.Hom.hom (stalkIso ℬ p).inv :
          (a : AtPrime ℬ p.asHomogeneousIdeal.toIdeal) → (↑((Proj ℬ).presheaf.stalk p) : Type u))
        ((localRingHom f
                (toIdeal (σ := σ) (𝒜 := 𝒜)
                  (asHomogeneousIdeal
                    (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                        (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                      p)))
                p.asHomogeneousIdeal.toIdeal ⋯ :
              (a :
                  AtPrime 𝒜
                    ((ProjectiveSpectrum.comap f hf : (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                          p).asHomogeneousIdeal.toIdeal) →
                AtPrime ℬ p.asHomogeneousIdeal.toIdeal)
            ((CommRingCat.Hom.hom
                  (Iso.hom
                    (stalkIso 𝒜
                      (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                          (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                        p))) :
                (a :
                    (↑((Proj 𝒜).presheaf.stalk
                          ((ConcreteCategory.hom (sheafedSpaceMap f hf).hom.base : (a : ↥(Proj ℬ)) → ↥(Proj 𝒜)) p)) :
                      Type u)) →
                  AtPrime 𝒜
                    ((ProjectiveSpectrum.comap f hf : (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                          p).asHomogeneousIdeal.toIdeal)
              x) :
          AtPrime ℬ p.asHomogeneousIdeal.toIdeal) :
      (↑((Proj ℬ).presheaf.stalk p) : Type u))
⊢ IsUnit x
have this : IsLocalHom (R := (↑(CommRingCat.of (AtPrime ℬ p.asHomogeneousIdeal.toIdeal)) : Type u)) (S :=
  (↑((Proj ℬ).presheaf.stalk p) : Type u)) (CommRingCat.Hom.hom (stalkIso ℬ p).inv)
Tactic: have : IsLocalHom (stalkIso ℬ p).inv.hom := isLocalHom_of_isIso _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
i : ℕ
s : A
hs : s ∈ 𝒜 i
⊢ Eq (α := CommRingCat.of (Away 𝒜 s) ⟶ Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)))
    (awayToSection 𝒜 s ≫ Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ ((f : (a : A) → B) s)) ⋯)
    (CommRingCat.ofHom (Away.map f s) ≫ awayToSection ℬ ((f : (a : A) → B) s))
have hf₁ : ∀ (x : (↑(CommRingCat.of (Away 𝒜 s)) : Type u)),
  Eq (α := (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
    ((CommRingCat.Hom.hom
            (awayToSection 𝒜 s ≫ Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ ((f : (a : A) → B) s)) sorry) :
          (a : (↑(CommRingCat.of (Away 𝒜 s)) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
        x :
      (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
    ((CommRingCat.Hom.hom (CommRingCat.ofHom (Away.map f s) ≫ awayToSection ℬ ((f : (a : A) → B) s)) :
          (a : (↑(CommRingCat.of (Away 𝒜 s)) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
        x :
      (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
i : ℕ
s : A
hs : s ∈ 𝒜 i
x : (↑(CommRingCat.of (Away 𝒜 s)) : Type u)
⊢ Eq (α := (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
    ((CommRingCat.Hom.hom
            (awayToSection 𝒜 s ≫ Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ ((f : (a : A) → B) s)) ⋯) :
          (a : (↑(CommRingCat.of (Away 𝒜 s)) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
        x :
      (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
    ((CommRingCat.Hom.hom (CommRingCat.ofHom (Away.map f s) ≫ awayToSection ℬ ((f : (a : A) → B) s)) :
          (a : (↑(CommRingCat.of (Away 𝒜 s)) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
        x :
      (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
have hf₁ : ∀ (n : ℕ) (x : A) (hx : x ∈ 𝒜 (n • i)),
  Eq (α := (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
    ((CommRingCat.Hom.hom
            (awayToSection 𝒜 s ≫ Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ ((f : (a : A) → B) s)) sorry) :
          (a : (↑(CommRingCat.of (Away 𝒜 s)) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
        (Away.mk 𝒜 hs n x hx) :
      (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
    ((CommRingCat.Hom.hom (CommRingCat.ofHom (Away.map f s) ≫ awayToSection ℬ ((f : (a : A) → B) s)) :
          (a : (↑(CommRingCat.of (Away 𝒜 s)) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
        (Away.mk 𝒜 hs n x hx) :
      (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
Tactic: obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective _ hs
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
i : ℕ
s : A
hs : s ∈ 𝒜 i
n : ℕ
x : A
hx : x ∈ 𝒜 (n • i)
⊢ Eq (α := (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
    ((CommRingCat.Hom.hom
            (awayToSection 𝒜 s ≫ Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ ((f : (a : A) → B) s)) ⋯) :
          (a : (↑(CommRingCat.of (Away 𝒜 s)) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
        (Away.mk 𝒜 hs n x hx) :
      (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
    ((CommRingCat.Hom.hom (CommRingCat.ofHom (Away.map f s) ≫ awayToSection ℬ ((f : (a : A) → B) s)) :
          (a : (↑(CommRingCat.of (Away 𝒜 s)) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
        (Away.mk 𝒜 hs n x hx) :
      (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
have hf₁ : Eq (α := (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
  ((CommRingCat.Hom.hom (Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ ((f : (a : A) → B) s)) sorry) :
        (a : (↑Γ(Proj 𝒜, basicOpen 𝒜 s) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
      ((CommRingCat.Hom.hom (awayToSection 𝒜 s) : (a : Away 𝒜 s) → (↑Γ(Proj 𝒜, basicOpen 𝒜 s) : Type u))
        (Away.mk 𝒜 hs n x hx)) :
    (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
  ((CommRingCat.Hom.hom (awayToSection ℬ ((f : (a : A) → B) s)) :
        (a : Away ℬ ((f : (a : A) → B) s)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
      (Away.mk ℬ sorry n ((f : (a : A) → B) x) sorry) :
    (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
Tactic: simp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply, CommRingCat.hom_ofHom,
    Away.map_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
i : ℕ
s : A
hs : s ∈ 𝒜 i
n : ℕ
x : A
hx : x ∈ 𝒜 (n • i)
⊢ Eq (α := (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
    ((CommRingCat.Hom.hom (Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ ((f : (a : A) → B) s)) ⋯) :
          (a : (↑Γ(Proj 𝒜, basicOpen 𝒜 s) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
        ((CommRingCat.Hom.hom (awayToSection 𝒜 s) : (a : Away 𝒜 s) → (↑Γ(Proj 𝒜, basicOpen 𝒜 s) : Type u))
          (Away.mk 𝒜 hs n x hx)) :
      (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
    ((CommRingCat.Hom.hom (awayToSection ℬ ((f : (a : A) → B) s)) :
          (a : Away ℬ ((f : (a : A) → B) s)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
        (Away.mk ℬ ⋯ n ((f : (a : A) → B) x) ⋯) :
      (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
have hf₁ : ∀ (p : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))) : Opens (↑(top ℬ) : Type u))),
  Eq.{u + 1} (α := (fun (x : (↑(top ℬ) : Type u)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑p : (↑(top ℬ) : Type u)))
    ((↑((CommRingCat.Hom.hom (Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ ((f : (a : A) → B) s)) sorry) :
              (a : (↑Γ(Proj 𝒜, basicOpen 𝒜 s) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
            ((CommRingCat.Hom.hom (awayToSection 𝒜 s) : (a : Away 𝒜 s) → (↑Γ(Proj 𝒜, basicOpen 𝒜 s) : Type u))
              (Away.mk 𝒜 hs n x hx))) :
        (x : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
          (fun (x : (↑(top ℬ) : Type u)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u)))
      p)
    ((↑((CommRingCat.Hom.hom (awayToSection ℬ ((f : (a : A) → B) s)) :
              (a : Away ℬ ((f : (a : A) → B) s)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
            (Away.mk ℬ sorry n ((f : (a : A) → B) x) sorry)) :
        (x : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
          (fun (x : (↑(top ℬ) : Type u)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u)))
      p)
Tactic: refine Subtype.ext <| funext fun p ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ Eq (α := Spec (CommRingCat.of (Away (A := B) ℬ ((f : (a : A) → B) s : B))) ⟶ Proj 𝒜)
    (awayι ℬ ((f : (a : A) → B) s) ⋯ hi ≫ map f hf) (Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ awayι 𝒜 s hs hi)
have rw : Eq (α := Spec (CommRingCat.of (Away (A := B) ℬ ((f : (a : A) → B) s : B))) ⟶ Proj 𝒜)
  (CategoryStruct.comp (Y := (↑(basicOpen 𝒜 s) : Scheme))
    (Iso.inv (basicOpenIsoSpec ℬ ((f : (a : A) → B) s) sorry hi) ≫
      Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) sorry)
    (Scheme.Opens.ι (basicOpen 𝒜 s)))
  ((Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ Iso.inv (basicOpenIsoSpec 𝒜 s hs hi)) ≫
    Scheme.Opens.ι (basicOpen 𝒜 s))
Tactic: rw [awayι, awayι, Category.assoc, ι_comp_map, ← Category.assoc, ← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ Eq (α := Spec (CommRingCat.of (Away (A := B) ℬ ((f : (a : A) → B) s : B))) ⟶ Proj 𝒜)
    (CategoryStruct.comp (Y := (↑(basicOpen 𝒜 s) : Scheme))
      (Iso.inv (basicOpenIsoSpec ℬ ((f : (a : A) → B) s) ⋯ hi) ≫
        Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯)
      (Scheme.Opens.ι (basicOpen 𝒜 s)))
    ((Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ Iso.inv (basicOpenIsoSpec 𝒜 s hs hi)) ≫
      Scheme.Opens.ι (basicOpen 𝒜 s))
have e_a : Eq (α := Spec (CommRingCat.of (Away (A := B) ℬ ((f : (a : A) → B) s : B))) ⟶ (↑(basicOpen 𝒜 s) : Scheme))
  (Iso.inv (basicOpenIsoSpec ℬ ((f : (a : A) → B) s) sorry hi) ≫
    Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) sorry)
  (Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ Iso.inv (basicOpenIsoSpec 𝒜 s hs hi))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ Eq (α := Spec (CommRingCat.of (Away (A := B) ℬ ((f : (a : A) → B) s : B))) ⟶ (↑(basicOpen 𝒜 s) : Scheme))
    (Iso.inv (basicOpenIsoSpec ℬ ((f : (a : A) → B) s) ⋯ hi) ≫
      Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯)
    (Spec.map (CommRingCat.ofHom (Away.map f s)) ≫ Iso.inv (basicOpenIsoSpec 𝒜 s hs hi))
have e_a : Eq (α := (↑(map f hf ⁻¹ᵁ basicOpen 𝒜 s) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 s)))
  (Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) sorry ≫ Iso.hom (basicOpenIsoSpec 𝒜 s hs hi))
  (Iso.hom (basicOpenIsoSpec ℬ ((f : (a : A) → B) s) sorry hi) ≫ Spec.map (CommRingCat.ofHom (Away.map f s)))
Tactic: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
i : ℕ
hi : 0 < i
s : A
hs : s ∈ 𝒜 i
⊢ Eq (α := (↑(map f hf ⁻¹ᵁ basicOpen 𝒜 s) : Scheme) ⟶ Spec (CommRingCat.of (Away 𝒜 s)))
    (Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯ ≫ Iso.hom (basicOpenIsoSpec 𝒜 s hs hi))
    (Iso.hom (basicOpenIsoSpec ℬ ((f : (a : A) → B) s) ⋯ hi) ≫ Spec.map (CommRingCat.ofHom (Away.map f s)))
have e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine ext_to_Spec <| (cancel_mono (basicOpen ℬ (f s)).topIso.hom).mp ?_