awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x_1 x y : A
hx : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hy : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) y
hx' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
hy' :
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A))
⊢ x * y -
      HMul.hMul (α := A) (β := A) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)
        ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) =
    x * HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A) +
      HMul.hMul (β := A) (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
        ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A)

Tactic:
ring
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
simp :
  CategoryStruct.comp (Y := Γ(Spec Γ(Proj 𝒜, basicOpen 𝒜 f), ⊤))
      (Scheme.Hom.app (Spec.map (awayToSection 𝒜 f)) ⊤ :
        Γ(Spec (CommRingCat.of (Away 𝒜 f)), ⊤) ⟶ Γ(Spec Γ(Proj 𝒜, basicOpen 𝒜 f), Spec.map (awayToSection 𝒜 f) ⁻¹ᵁ ⊤))
      (Scheme.Hom.app (Scheme.Opens.toSpecΓ (basicOpen 𝒜 f)) ⊤) =
    Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫ awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom ⋯)
⊢ Eq (α :=
    Γ(Spec (CommRingCat.of (Away 𝒜 f)), ⊤) ⟶
      Γ((↑(basicOpen 𝒜 f) : Scheme), (Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫ Spec.map (awayToSection 𝒜 f)) ⁻¹ᵁ ⊤))
    (Scheme.Hom.app (Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫ Spec.map (awayToSection 𝒜 f)) ⊤)
    (Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫
      awayToSection 𝒜 f ≫ Iso.inv (Scheme.Opens.topIso (basicOpen 𝒜 f)))

Tactic:
simp only [Scheme.Hom.comp_base, TopologicalSpace.Opens.map_comp_obj,
    TopologicalSpace.Opens.map_top, Scheme.Hom.comp_app, Scheme.Opens.topIso_inv, eqToHom_op]

Premises used: AlgebraicGeometry.Scheme.Opens.topIso_inv, AlgebraicGeometry.Scheme.Hom.comp_app, CategoryTheory.eqToHom_op, TopologicalSpace.Opens.map_comp_obj, TopologicalSpace.Opens.map_top, AlgebraicGeometry.Scheme.Hom.comp_base
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
erw :
  CategoryStruct.comp (Y := Γ(Spec Γ(Proj 𝒜, basicOpen 𝒜 f), ⊤))
      (Scheme.Hom.app (Spec.map (awayToSection 𝒜 f)) ⊤ :
        Γ(Spec (CommRingCat.of (Away 𝒜 f)), ⊤) ⟶ Γ(Spec Γ(Proj 𝒜, basicOpen 𝒜 f), Spec.map (awayToSection 𝒜 f) ⁻¹ᵁ ⊤))
      (Scheme.Hom.app (Spec.map (Iso.inv (Scheme.Opens.topIso (basicOpen 𝒜 f)))) ⊤ ≫
        Scheme.Hom.app (↑(basicOpen 𝒜 f) : Scheme).toSpecΓ
          (Spec.map (Iso.inv (Scheme.Opens.topIso (basicOpen 𝒜 f))) ⁻¹ᵁ ⊤)) =
    Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫ awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom ⋯)
⊢ CategoryStruct.comp (Y := Γ(Spec Γ(Proj 𝒜, basicOpen 𝒜 f), ⊤))
      (Scheme.Hom.app (Spec.map (awayToSection 𝒜 f)) ⊤ :
        Γ(Spec (CommRingCat.of (Away 𝒜 f)), ⊤) ⟶ Γ(Spec Γ(Proj 𝒜, basicOpen 𝒜 f), Spec.map (awayToSection 𝒜 f) ⁻¹ᵁ ⊤))
      (Scheme.Hom.app (Scheme.Opens.toSpecΓ (basicOpen 𝒜 f)) ⊤) =
    Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫ awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom ⋯)

Tactic:
erw [Scheme.Hom.comp_app]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_app
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
⊢ CategoryStruct.comp (Y := Γ(Spec Γ(Proj 𝒜, basicOpen 𝒜 f), ⊤))
      (Scheme.Hom.app (Spec.map (awayToSection 𝒜 f)) ⊤ :
        Γ(Spec (CommRingCat.of (Away 𝒜 f)), ⊤) ⟶ Γ(Spec Γ(Proj 𝒜, basicOpen 𝒜 f), Spec.map (awayToSection 𝒜 f) ⁻¹ᵁ ⊤))
      (Scheme.Hom.app (Spec.map (Iso.inv (Scheme.Opens.topIso (basicOpen 𝒜 f)))) ⊤ ≫
        Scheme.Hom.app (↑(basicOpen 𝒜 f) : Scheme).toSpecΓ
          (Spec.map (Iso.inv (Scheme.Opens.topIso (basicOpen 𝒜 f))) ⁻¹ᵁ ⊤)) =
    Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫ awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
apply :
  IsIso (X := Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme))
    (Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f))
⊢ IsIso (X := (↑(basicOpen 𝒜 f) : Scheme)) (basicOpenToSpec 𝒜 f)

Tactic:
apply (isIso_iff_of_reflects_iso _ Scheme.forgetToLocallyRingedSpace).mp ?_

Premises used: CategoryTheory.isIso_iff_of_reflects_iso, Iff.mp, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsIso (X :=
    (toLocallyRingedSpace 𝒜).restrict (U :=
      Functor.obj (C := TopologicalSpace.Opens (↑(↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))
        (TopologicalSpace.Opens.toTopCat (↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat))
        (ProjectiveSpectrum.basicOpen 𝒜 f))
      ⋯)
    (ProjectiveSpectrum.Proj.toSpec 𝒜 f)

Tactic:
ProjectiveSpectrum.Proj.isIso_toSpec 𝒜 f f_deg hm

Premises used: AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
h :
  Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) =
      (toLocallyRingedSpace 𝒜).restrict (U :=
        Functor.obj (C := TopologicalSpace.Opens (↑(↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))
          (TopologicalSpace.Opens.toTopCat (↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat))
          (ProjectiveSpectrum.basicOpen 𝒜 f))
        ⋯ →
    Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
        Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f)) →
      Eq (α :=
        Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) ⟶
          Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))))
        (Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f)) (ProjectiveSpectrum.Proj.toSpec 𝒜 f)
⊢ IsIso (X := Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme))
    (Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f))

Tactic:
convert! ProjectiveSpectrum.Proj.isIso_toSpec 𝒜 f f_deg hm using 1

Premises used: AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
e_3 :
  Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) =
    (toLocallyRingedSpace 𝒜).restrict (U :=
      Functor.obj (C := TopologicalSpace.Opens (↑(↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))
        (TopologicalSpace.Opens.toTopCat (↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat))
        (ProjectiveSpectrum.basicOpen 𝒜 f))
      ⋯
e_4 :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
⊢ Eq (α :=
    Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) ⟶
      Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))))
    (Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f)) (ProjectiveSpectrum.Proj.toSpec 𝒜 f)

Tactic:
Eq.trans ?_ (ΓSpec.locallyRingedSpaceAdjunction.homEquiv_apply _ _ _).symm

Premises used: AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction, CategoryTheory.Adjunction.homEquiv_apply, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
e_3 :
  Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) =
    (toLocallyRingedSpace 𝒜).restrict (U :=
      Functor.obj (C := TopologicalSpace.Opens (↑(↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))
        (TopologicalSpace.Opens.toTopCat (↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat))
        (ProjectiveSpectrum.basicOpen 𝒜 f))
      ⋯
e_4 :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
h :
  Eq (α :=
    Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) ⟶
      Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))))
    (Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f))
    (ΓSpec.locallyRingedSpaceAdjunction.unit.app (Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme)) ≫
      Spec.toLocallyRingedSpace.map (Quiver.Hom.op (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f)))
⊢ Eq (α :=
    Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) ⟶
      Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))))
    (Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f)) (ProjectiveSpectrum.Proj.toSpec 𝒜 f)

Tactic:
refine Eq.trans ?_ (ΓSpec.locallyRingedSpaceAdjunction.homEquiv_apply _ _ _).symm

Premises used: AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction, CategoryTheory.Adjunction.homEquiv_apply, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
e_3 :
  Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) =
    (toLocallyRingedSpace 𝒜).restrict (U :=
      Functor.obj (C := TopologicalSpace.Opens (↑(↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))
        (TopologicalSpace.Opens.toTopCat (↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat))
        (ProjectiveSpectrum.basicOpen 𝒜 f))
      ⋯
e_4 :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
h :
  Eq (α := (↑(basicOpen 𝒜 f) : Scheme).toLocallyRingedSpace ⟶ (Spec (CommRingCat.of (Away 𝒜 f))).toLocallyRingedSpace)
    (Scheme.Hom.toLRSHom
      (((↑(basicOpen 𝒜 f) : Scheme).toSpecΓ ≫ Spec.map ((Proj 𝒜).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) ≫
        Spec.map (awayToSection 𝒜 f)))
    (identityToΓSpec.app (↑(basicOpen 𝒜 f) : Scheme).toLocallyRingedSpace ≫
      Spec.locallyRingedSpaceMap (Quiver.Hom.unop (Quiver.Hom.op (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f))))
⊢ Eq (α :=
    Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) ⟶
      Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))))
    (Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f))
    (ΓSpec.locallyRingedSpaceAdjunction.unit.app (Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme)) ≫
      Spec.toLocallyRingedSpace.map (Quiver.Hom.op (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f)))

Tactic:
dsimp [basicOpenToSpec, Scheme.Opens.toSpecΓ]

Premises used: AlgebraicGeometry.Scheme.Opens.toSpecΓ, AlgebraicGeometry.Proj.basicOpenToSpec
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
e_3 :
  Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) =
    (toLocallyRingedSpace 𝒜).restrict (U :=
      Functor.obj (C := TopologicalSpace.Opens (↑(↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))
        (TopologicalSpace.Opens.toTopCat (↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat))
        (ProjectiveSpectrum.basicOpen 𝒜 f))
      ⋯
e_4 :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
h :
  Scheme.Hom.toLRSHom
      ((↑(basicOpen 𝒜 f) : Scheme).toSpecΓ ≫ Spec.map (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom ⋯))) =
    identityToΓSpec.app (↑(basicOpen 𝒜 f) : Scheme).toLocallyRingedSpace ≫
      Spec.locallyRingedSpaceMap (Quiver.Hom.unop (Quiver.Hom.op (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f)))
⊢ Eq (α := (↑(basicOpen 𝒜 f) : Scheme).toLocallyRingedSpace ⟶ (Spec (CommRingCat.of (Away 𝒜 f))).toLocallyRingedSpace)
    (Scheme.Hom.toLRSHom
      (((↑(basicOpen 𝒜 f) : Scheme).toSpecΓ ≫ Spec.map ((Proj 𝒜).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) ≫
        Spec.map (awayToSection 𝒜 f)))
    (identityToΓSpec.app (↑(basicOpen 𝒜 f) : Scheme).toLocallyRingedSpace ≫
      Spec.locallyRingedSpaceMap (Quiver.Hom.unop (Quiver.Hom.op (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f))))

Tactic:
simp only [eqToHom_op, Category.assoc, ← Spec.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToHom_op, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
e_3 :
  Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme) =
    (toLocallyRingedSpace 𝒜).restrict (U :=
      Functor.obj (C := TopologicalSpace.Opens (↑(↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat) : Type u))
        (TopologicalSpace.Opens.toTopCat (↑(toLocallyRingedSpace 𝒜).toPresheafedSpace : TopCat))
        (ProjectiveSpectrum.basicOpen 𝒜 f))
      ⋯
e_4 :
  Scheme.forgetToLocallyRingedSpace.obj (Spec (CommRingCat.of (Away 𝒜 f))) =
    Spec.locallyRingedSpaceObj (CommRingCat.of (Away 𝒜 f))
⊢ Scheme.Hom.toLRSHom
      ((↑(basicOpen 𝒜 f) : Scheme).toSpecΓ ≫ Spec.map (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom ⋯))) =
    identityToΓSpec.app (↑(basicOpen 𝒜 f) : Scheme).toLocallyRingedSpace ≫
      Spec.locallyRingedSpaceMap (Quiver.Hom.unop (Quiver.Hom.op (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ Eq (α := Γ(Spec (CommRingCat.of (Away 𝒜 f)), ⊤) ⟶ Γ((↑(basicOpen 𝒜 f) : Scheme), basicOpenToSpec 𝒜 f ⁻¹ᵁ ⊤))
    (Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤)
    (Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫
      awayToSection 𝒜 f ≫ Iso.inv (Scheme.Opens.topIso (basicOpen 𝒜 f)))

Tactic:
have := basicOpenToSpec_app_top 𝒜 f
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  Eq (α := Γ(Spec (CommRingCat.of (Away 𝒜 f)), ⊤) ⟶ Γ((↑(basicOpen 𝒜 f) : Scheme), basicOpenToSpec 𝒜 f ⁻¹ᵁ ⊤))
    (Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤)
    (Iso.hom (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫
      awayToSection 𝒜 f ≫ Iso.inv (Scheme.Opens.topIso (basicOpen 𝒜 f)))
⊢ Eq (α := CommRingCat.of (Away 𝒜 f) ⟶ Γ(Proj 𝒜, basicOpen 𝒜 f))
    ((Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫ Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤) ≫
      Iso.hom (Scheme.Opens.topIso (basicOpen 𝒜 f)))
    (awayToSection 𝒜 f)

Tactic:
rw [← Iso.inv_comp_eq, Iso.eq_comp_inv] at this

Premises used: CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  Eq (α := CommRingCat.of (Away 𝒜 f) ⟶ Γ(Proj 𝒜, basicOpen 𝒜 f))
    ((Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫ Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤) ≫
      Iso.hom (Scheme.Opens.topIso (basicOpen 𝒜 f)))
    (awayToSection 𝒜 f)
rw :
  IsIso (X := CommRingCat.of (Away 𝒜 f))
    ((Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫
        Scheme.Hom.app (Iso.hom (basicOpenIsoSpec 𝒜 f f_deg hm)) ⊤) ≫
      Iso.hom (Scheme.Opens.topIso (basicOpen 𝒜 f)))
⊢ IsIso (X := CommRingCat.of (Away 𝒜 f)) (awayToSection 𝒜 f)

Tactic:
rw [← this, ← basicOpenIsoSpec_hom 𝒜 f f_deg hm]

Premises used: AlgebraicGeometry.Proj.basicOpenIsoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f g : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  Eq (α := CommRingCat.of (Away 𝒜 f) ⟶ Γ(Proj 𝒜, basicOpen 𝒜 f))
    ((Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫ Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤) ≫
      Iso.hom (Scheme.Opens.topIso (basicOpen 𝒜 f)))
    (awayToSection 𝒜 f)
⊢ IsIso (X := CommRingCat.of (Away 𝒜 f))
    ((Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (Away 𝒜 f))) ≫
        Scheme.Hom.app (Iso.hom (basicOpenIsoSpec 𝒜 f f_deg hm)) ⊤) ≫
      Iso.hom (Scheme.Opens.topIso (basicOpen 𝒜 f)))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
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
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 f)) ⟶ Proj 𝒜)
    (Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f)) (awayι 𝒜 f f_deg hm)

Tactic:
rfl

Premises used: AlgebraicGeometry.Proj.awayι, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
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
⊢ Eq (α := (Proj 𝒜).Opens) (Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm)) (basicOpen 𝒜 f)

Tactic:
(Scheme.Hom.opensRange_comp_of_isIso _ _).trans (basicOpen 𝒜 f).opensRange_ι

Premises used: AlgebraicGeometry.Scheme.Opens.opensRange_ι, AlgebraicGeometry.Proj.basicOpen, AlgebraicGeometry.Scheme.Hom.opensRange_comp_of_isIso, AlgebraicGeometry.Proj.awayι, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
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
rw : IsAffineOpen (X := Proj 𝒜) (Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm))
⊢ IsAffineOpen (X := Proj 𝒜) (basicOpen 𝒜 f)

Tactic:
rw [← opensRange_awayι 𝒜 f f_deg hm]

Premises used: AlgebraicGeometry.Proj.opensRange_awayι
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
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
⊢ IsAffineOpen (X := Proj 𝒜) (Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm))

Tactic:
isAffineOpen_opensRange (awayι _ _ _ _)

Premises used: AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.Proj.awayι
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
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
⊢ IsAffineOpen (X := Proj 𝒜) (Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm))

Tactic:
exact isAffineOpen_opensRange (awayι _ _ _ _)

Premises used: AlgebraicGeometry.isAffineOpen_opensRange, AlgebraicGeometry.Proj.awayι
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
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
simp :
  Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
    (Scheme.Opens.ι (basicOpen 𝒜 f) ≫
      Iso.inv (Proj 𝒜).topIso ≫
        Iso.inv ((Proj 𝒜).isoOfEq ⋯) ≫
          Scheme.Opens.toSpecΓ (basicOpen 𝒜 1) ≫
            Spec.map (awayToSection 𝒜 1) ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))))
    (basicOpenToSpec 𝒜 f ≫ Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f))))
⊢ Eq (α := Spec (CommRingCat.of (Away 𝒜 f)) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
    ((Iso.inv (basicOpenIsoSpec 𝒜 f f_deg hm) ≫ Scheme.Opens.ι (basicOpen 𝒜 f)) ≫
      Iso.inv (Proj 𝒜).topIso ≫
        Iso.inv ((Proj 𝒜).isoOfEq ⋯) ≫
          (Scheme.Opens.toSpecΓ (basicOpen 𝒜 1) ≫ Spec.map (awayToSection 𝒜 1)) ≫
            Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1))))
    (Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f))))

Tactic:
simp only [Category.assoc, Iso.inv_comp_eq, basicOpenIsoSpec_hom]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_comp_eq, AlgebraicGeometry.Proj.basicOpenIsoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
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
U : (Proj 𝒜).Opens
e : U = ⊤
simp :
  Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ Proj 𝒜) (Scheme.Opens.ι (basicOpen 𝒜 f))
    (((Proj 𝒜).homOfLE ⋯ ≫ ((Proj 𝒜).isoOfEq e).hom) ≫ Iso.hom (Proj 𝒜).topIso)
⊢ Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ (↑U : Scheme))
    (Scheme.Opens.ι (basicOpen 𝒜 f) ≫ Iso.inv (Proj 𝒜).topIso ≫ ((Proj 𝒜).isoOfEq e).inv) ((Proj 𝒜).homOfLE ⋯)

Tactic:
simp only [← Category.assoc, Iso.comp_inv_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
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
U : (Proj 𝒜).Opens
e : U = ⊤
⊢ Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ Proj 𝒜) (Scheme.Opens.ι (basicOpen 𝒜 f))
    (((Proj 𝒜).homOfLE ⋯ ≫ ((Proj 𝒜).isoOfEq e).hom) ≫ Iso.hom (Proj 𝒜).topIso)

Tactic:
simp only [Scheme.topIso_hom, Category.assoc, Scheme.isoOfEq_hom_ι, Scheme.homOfLE_ι]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.isoOfEq_hom_ι, AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.Scheme.topIso_hom
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
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
⊢ ∀ (U : (Proj 𝒜).Opens) (e : U = ⊤),
    Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ (↑U : Scheme))
      (Scheme.Opens.ι (basicOpen 𝒜 f) ≫ Iso.inv (Proj 𝒜).topIso ≫ ((Proj 𝒜).isoOfEq e).inv) ((Proj 𝒜).homOfLE ⋯)

Tactic:
have (U) (e : U = ⊤) : (basicOpen 𝒜 f).ι ≫ (Scheme.topIso _).inv ≫ (Scheme.isoOfEq _ e).inv =
      Scheme.homOfLE _ (le_top.trans_eq e.symm) := by
    simp only [← Category.assoc, Iso.comp_inv_eq]
    simp only [Scheme.topIso_hom, Category.assoc, Scheme.isoOfEq_hom_ι, Scheme.homOfLE_ι]