awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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 (𝒜₊))
s : A
⊢ Eq (α := (↑(basicOpen ℬ ((f : (a : A) → B) s)) : Scheme) ⟶ Proj 𝒜)
    (Scheme.Opens.ι (basicOpen ℬ ((f : (a : A) → B) s)) ≫ map f hf :
      (↑(basicOpen ℬ ((f : (a : A) → B) s)) : Scheme) ⟶ Proj 𝒜)
    (Scheme.Hom.resLE (map f hf) (basicOpen 𝒜 s) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) ⋯ ≫ Scheme.Opens.ι (basicOpen 𝒜 s) :
      (↑(map f hf ⁻¹ᵁ basicOpen 𝒜 s) : Scheme) ⟶ Proj 𝒜)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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 (ℬ₊))
i : ℕ
s : A
hs : s ∈ 𝒜 i
⊢ LE.le (α := (Proj ℬ).Opens) (basicOpen ℬ ((f : (a : A) → B) s)) (basicOpen ℬ ((f : (a : A) → B) s))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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
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)) ⋯) :
            (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))
⊢ 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))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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)
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)) ⋯) :
            (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))
⊢ 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))

Tactic:
obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective _ hs

Premises used: HomogeneousLocalization.Away.mk_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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)
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)) ⋯) :
          (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))
⊢ 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))

Tactic:
simp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply, CommRingCat.hom_ofHom,
    Away.map_mk]

Premises used: CommRingCat.hom_comp, CommRingCat.hom_ofHom, RingHom.coe_comp, Function.comp_apply, HomogeneousLocalization.Away.map_mk
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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))

Tactic:
Subtype.ext <| funext fun p ↦ ?_

Premises used: funext, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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)
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)) ⋯) :
                (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 ℬ ⋯ n ((f : (a : A) → B) x) ⋯)) :
          (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)
⊢ 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))

Tactic:
refine Subtype.ext <| funext fun p ↦ ?_

Premises used: funext, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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
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) ⋯ 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))
⊢ 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)

Tactic:
rw [awayι, awayι, Category.assoc, ι_comp_map, ← Category.assoc, ← Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Proj.ι_comp_map, AlgebraicGeometry.Proj.awayι
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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
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) ⋯ 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))
⊢ 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))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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
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) ⋯ ≫ Iso.hom (basicOpenIsoSpec 𝒜 s hs hi))
    (Iso.hom (basicOpenIsoSpec ℬ ((f : (a : A) → B) s) ⋯ hi) ≫ Spec.map (CommRingCat.ofHom (Away.map f s)))
⊢ 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))

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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)))

Tactic:
ext_to_Spec <| (cancel_mono (basicOpen ℬ (f s)).topIso.hom).mp ?_

Premises used: AlgebraicGeometry.Scheme.Opens.topIso, AlgebraicGeometry.ext_to_Spec, AlgebraicGeometry.Proj.basicOpen, CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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
e_a : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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)))

Tactic:
refine ext_to_Spec <| (cancel_mono (basicOpen ℬ (f s)).topIso.hom).mp ?_

Premises used: AlgebraicGeometry.Scheme.Opens.topIso, AlgebraicGeometry.ext_to_Spec, AlgebraicGeometry.Proj.basicOpen, CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [basicOpenIsoSpec_hom, basicOpenToSpec_app_top, awayToSection_comp_appLE _ _ hs]

Premises used: AlgebraicGeometry.Proj.basicOpenToSpec_app_top, AlgebraicGeometry.Proj.awayToSection_comp_appLE, AlgebraicGeometry.Proj.basicOpenIsoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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 (ℬ₊))
⊢ Eq (α := Proj 𝒞 ⟶ Proj 𝒜) (map (g.comp f) ⋯) (CategoryStruct.comp (Y := Proj ℬ) (map g hg) (map f hf))

Tactic:
(mapAffineOpenCover _ <| irrelevant_le_map_comp hf hg).openCover.hom_ext _ _ fun s ↦ ?_

Premises used: HomogeneousIdeal.irrelevant_le_map_comp, AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Proj.mapAffineOpenCover, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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 (ℬ₊))
refine :
  ∀
    (s :
      PreZeroHypercover.I₀ (S := Proj 𝒞)
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))),
    Eq (α :=
      PreZeroHypercover.X
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
          s ⟶
        Proj 𝒜)
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
          s ≫
        map (g.comp f) ⋯)
      (PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
          s ≫
        CategoryStruct.comp (Y := Proj ℬ) (map g hg) (map f hf))
⊢ Eq (α := Proj 𝒞 ⟶ Proj 𝒜) (map (g.comp f) ⋯) (CategoryStruct.comp (Y := Proj ℬ) (map g hg) (map f hf))

Tactic:
refine (mapAffineOpenCover _ <| irrelevant_le_map_comp hf hg).openCover.hom_ext _ _ fun s ↦ ?_

Premises used: HomogeneousIdeal.irrelevant_le_map_comp, AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Proj.mapAffineOpenCover, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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 (ℬ₊))
s :
  PreZeroHypercover.I₀ (S := Proj 𝒞)
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
simp :
  Eq (α := Spec (Scheme.AffineCover.X (P := IsOpenImmersion) (mapAffineOpenCover (g.comp f) ⋯) s) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (Away.map (g.comp f) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ≫
      awayι 𝒜 (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯)
    (awayι 𝒞 ((g.comp f : (a : A) → C) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)) ⋯ ⋯ ≫
      CategoryStruct.comp (Y := Proj ℬ) (map g hg) (map f hf))
⊢ Eq (α :=
    PreZeroHypercover.X
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
        s ⟶
      Proj 𝒜)
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
        s ≫
      map (g.comp f) ⋯)
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
        s ≫
      CategoryStruct.comp (Y := Proj ℬ) (map g hg) (map f hf))

Tactic:
simp only [Scheme.AffineOpenCover.openCover_X, Scheme.AffineOpenCover.openCover_f,
    mapAffineOpenCover_f, awayι_comp_map (g.comp f) _ s.1.2 _ s.2.2]

Premises used: AlgebraicGeometry.Scheme.AffineOpenCover.openCover_f, GradedRingHom.comp, Sigma.fst, AlgebraicGeometry.Proj.mapAffineOpenCover_f, Sigma.snd, AlgebraicGeometry.Scheme.AffineOpenCover.openCover_X, AlgebraicGeometry.Proj.awayι_comp_map, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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 (ℬ₊))
s :
  PreZeroHypercover.I₀ (S := Proj 𝒞)
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
⊢ Eq (α := Spec (Scheme.AffineCover.X (P := IsOpenImmersion) (mapAffineOpenCover (g.comp f) ⋯) s) ⟶ Proj 𝒜)
    (Spec.map (CommRingCat.ofHom (Away.map (g.comp f) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ≫
      awayι 𝒜 (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯)
    (awayι 𝒞 ((g.comp f : (a : A) → C) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)) ⋯ ⋯ ≫
      CategoryStruct.comp (Y := Proj ℬ) (map g hg) (map f hf))

Tactic:
simp [awayι_comp_map_assoc _ _ _ _ (map_mem f s.2.2), awayι_comp_map _ _ _ _ s.2.2]

Premises used: AlgebraicGeometry.Proj.awayι_comp_map_assoc, Graded.map_mem, Sigma.snd, AlgebraicGeometry.Proj.awayι_comp_map, Subtype.property