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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
this : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hf₁ :
  ∀ (x : A) (hx : x ∈ Set.range f),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
have hf₂ : ∀ (r : ↥(𝒜 0)),
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (α := A) (β := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
      ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A))
Tactic: induction this using Algebra.adjoin_induction with
  | mem x hx =>
    obtain ⟨i, rfl⟩ := hx
    obtain ⟨n, hn⟩ := hfn i
    rw [GradedRing.projZeroRingHom_apply]
    by_cases hn' : n = 0
    · rw [DirectSum.decompose_of_mem_same 𝒜 (hn' ▸ hn), sub_self]
      exact zero_mem _
    · rw [DirectSum.decompose_of_mem_ne 𝒜 hn hn', sub_zero]
      exact Ideal.subset_span ⟨_, rfl⟩
  | algebraMap r =>
    convert! zero_mem (Ideal.span _)
    rw [sub_eq_zero]
    exact (DirectSum.decompose_of_mem_same 𝒜 r.2).symm
  | add x y hx hy _ _ =>
    rw [map_add, add_sub_add_comm]
    exact add_mem ‹_› ‹_›
  | mul x y hx hy hx' hy' =>
    convert!
      add_mem (Ideal.mul_mem_left _ x hy')
        (Ideal.mul_mem_right (GradedRing.projZeroRingHom 𝒜 y) _ hx') using 1
    rw [map_mul]
    ring
Cleared hypotheses: this
-- 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 𝒜
ι : Type u_2
f : ι → A
hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n
hf : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) ⊤
x : A
this : Membership.mem (γ := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin (↥(𝒜 0)) (Set.range f)) x
hf₁ :
  ∀ (x : A) (hx : x ∈ Set.range f),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
hf₂ :
  ∀ (r : ↥(𝒜 0)),
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (HSub.hSub (α := A) (β := A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A)
        ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) ((algebraMap (↥(𝒜 0)) A : (a : ↥(𝒜 0)) → A) r : A) : A))
⊢ Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
    (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A))
have hf₃ : ∀ (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),
  Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
      (HSub.hSub (β := A) x ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) x : A)) →
    Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
        (HSub.hSub (β := A) y ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) y : A)) →
      Membership.mem (γ := Submodule A A) (Ideal.span (Set.range f))
        (HSub.hSub (β := A) (x + y) ((GradedRing.projZeroRingHom 𝒜 : (a : A) → A) (x + y) : A))
Tactic: induction this using Algebra.adjoin_induction with
  | mem x hx =>
    obtain ⟨i, rfl⟩ := hx
    obtain ⟨n, hn⟩ := hfn i
    rw [GradedRing.projZeroRingHom_apply]
    by_cases hn' : n = 0
    · rw [DirectSum.decompose_of_mem_same 𝒜 (hn' ▸ hn), sub_self]
      exact zero_mem _
    · rw [DirectSum.decompose_of_mem_ne 𝒜 hn hn', sub_zero]
      exact Ideal.subset_span ⟨_, rfl⟩
  | algebraMap r =>
    convert! zero_mem (Ideal.span _)
    rw [sub_eq_zero]
    exact (DirectSum.decompose_of_mem_same 𝒜 r.2).symm
  | add x y hx hy _ _ =>
    rw [map_add, add_sub_add_comm]
    exact add_mem ‹_› ‹_›
  | mul x y hx hy hx' hy' =>
    convert!
      add_mem (Ideal.mul_mem_left _ x hy')
        (Ideal.mul_mem_right (GradedRing.projZeroRingHom 𝒜 y) _ hx') using 1
    rw [map_mul]
    ring
Cleared hypotheses: this
-- 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
⊢ 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)))
have 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 sorry)
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]
-- 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
⊢ 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 ⋯)
have 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 sorry)
Tactic: erw [Scheme.Hom.comp_app]
-- 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 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsIso (X := (↑(basicOpen 𝒜 f) : Scheme)) (basicOpenToSpec 𝒜 f)
have apply : IsIso (X := Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme))
  (Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f))
Tactic: apply (isIso_iff_of_reflects_iso _ Scheme.forgetToLocallyRingedSpace).mp ?_
-- 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 : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsIso (X := Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme))
    (Scheme.forgetToLocallyRingedSpace.map (basicOpenToSpec 𝒜 f))
have 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))
      sorry →
  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: convert! ProjectiveSpectrum.Proj.isIso_toSpec 𝒜 f f_deg hm using 1
-- 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 : 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)
have 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)))
Tactic: refine Eq.trans ?_ (ΓSpec.locallyRingedSpaceAdjunction.homEquiv_apply _ _ _).symm
-- 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 : 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))
    (ΓSpec.locallyRingedSpaceAdjunction.unit.app (Scheme.forgetToLocallyRingedSpace.obj (↑(basicOpen 𝒜 f) : Scheme)) ≫
      Spec.toLocallyRingedSpace.map (Quiver.Hom.op (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f)))
have 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 sorry)))) ≫
      Spec.map (awayToSection 𝒜 f)))
  (identityToΓSpec.app (↑(basicOpen 𝒜 f) : Scheme).toLocallyRingedSpace ≫
    Spec.locallyRingedSpaceMap (Quiver.Hom.unop (Quiver.Hom.op (ProjectiveSpectrum.Proj.awayToΓ 𝒜 f))))
Tactic: dsimp [basicOpenToSpec, Scheme.Opens.toSpecΓ]
-- 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 : 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 (α := (↑(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))))
have h : Scheme.Hom.toLRSHom
    ((↑(basicOpen 𝒜 f) : Scheme).toSpecΓ ≫ Spec.map (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (eqToHom sorry))) =
  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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (hypothesis)
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 := CommRingCat.of (Away 𝒜 f)) (awayToSection 𝒜 f)
have 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)))
Tactic: have := basicOpenToSpec_app_top 𝒜 f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (hypothesis)
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)))
⊢ IsIso (X := CommRingCat.of (Away 𝒜 f)) (awayToSection 𝒜 f)
have 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)
Tactic: rw [← Iso.inv_comp_eq, Iso.eq_comp_inv] at this
Cleared hypotheses: this
-- 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 : 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)) (awayToSection 𝒜 f)
have 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)))
Tactic: rw [← this, ← basicOpenIsoSpec_hom 𝒜 f f_deg hm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsAffineOpen (X := Proj 𝒜) (basicOpen 𝒜 f)
have rw : IsAffineOpen (X := Proj 𝒜) (Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm))
Tactic: rw [← opensRange_awayι 𝒜 f f_deg hm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ 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))))
have simp : Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
  (Scheme.Opens.ι (basicOpen 𝒜 f) ≫
    Iso.inv (Proj 𝒜).topIso ≫
      Iso.inv ((Proj 𝒜).isoOfEq sorry) ≫
        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))))
Tactic: simp only [Category.assoc, Iso.inv_comp_eq, basicOpenIsoSpec_hom]
-- 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
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 ⋯)
have simp : Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ Proj 𝒜) (Scheme.Opens.ι (basicOpen 𝒜 f))
  (((Proj 𝒜).homOfLE sorry ≫ ((Proj 𝒜).isoOfEq e).hom) ≫ Iso.hom (Proj 𝒜).topIso)
Tactic: simp only [← Category.assoc, Iso.comp_inv_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (hypothesis)
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 (α := (↑(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))))
have this : ∀ (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 sorry)
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_ι]
-- 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
this :
  ∀ (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 ⋯)
⊢ 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))))
have rw : Eq (α := (↑(basicOpen 𝒜 f) : Scheme) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
  (Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫
    Spec.map
      ((CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers 1)) ≫ awayToSection 𝒜 1) ≫
        (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE sorry))))
  (Scheme.Opens.toSpecΓ (basicOpen 𝒜 f) ≫
    Spec.map (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers f)) ≫ awayToSection 𝒜 f))
Tactic: rw [reassoc_of% this, ← Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, basicOpenToSpec,
    Category.assoc, ← Spec.map_comp, ← Spec.map_comp, ← Spec.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x =
    awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))
have hf : ∀ (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)),
  Eq (α := (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
    ((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x) :
          (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
        a :
      (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
    ((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
          (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
        a :
      (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
Tactic: ext a
-- 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
a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)
⊢ Eq (α := (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
    ((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x) :
          (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
        a :
      (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
    ((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
        a :
      (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
have hf : Eq.{u + 1} (α :=
  (x_1 :
      ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)) : TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))) →
    (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
      (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
  (↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x) :
          (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
        a) :
    (x_1 : ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)))) →
      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
        (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
  (↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
          (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
        a) :
    (x_1 : ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)))) →
      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
        (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
Tactic: apply Subtype.ext