awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ IsSeparated (X := Proj 𝒜) (toSpecZero 𝒜)

Tactic:
⟨IsZariskiLocalAtTarget.of_openCover (Pullback.openCoverOfLeftRight
    (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover _ _) ?_⟩

Premises used: AlgebraicGeometry.Proj.affineOpenCover, AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight, AlgebraicGeometry.IsSeparated.mk, AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.IsZariskiLocalAtTarget.of_openCover
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
refine :
  ∀
    (i :
      (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
            (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))).1),
    IsClosedImmersion (X :=
      PreZeroHypercover.X (S := Proj 𝒜)
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Precoverage.ZeroHypercover.pullback₁ (T := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜))
            (diagonal (toSpecZero 𝒜))
            (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
              (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))))
        i)
      (Cover.pullbackHom (P := IsOpenImmersion)
          (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
            (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))
          (diagonal (toSpecZero 𝒜)) i :
        PreZeroHypercover.X (S := Proj 𝒜)
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (Precoverage.ZeroHypercover.pullback₁ (T := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜))
                (diagonal (toSpecZero 𝒜))
                (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
                  (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))))
            i ⟶
          PreZeroHypercover.X (S := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜))
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
                (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜)))
            i)
⊢ IsSeparated (X := Proj 𝒜) (toSpecZero 𝒜)

Tactic:
refine ⟨IsZariskiLocalAtTarget.of_openCover (Pullback.openCoverOfLeftRight
    (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover _ _) ?_⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
⊢ IsClosedImmersion (X :=
    pullback (Y :=
      pullback (X := Spec (AffineCover.X (P := IsOpenImmersion) (affineOpenCover 𝒜) i)) (Y :=
        Spec (AffineCover.X (P := IsOpenImmersion) (affineOpenCover 𝒜) j))
        (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜)
        (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜))
      (Z := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜)) (diagonal (toSpecZero 𝒜))
      (pullback.map (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜)
        (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜) (toSpecZero 𝒜) (toSpecZero 𝒜)
        (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯)
        (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯) (𝟙 (Spec (CommRingCat.of ↥(𝒜 0)))) ⋯ ⋯))
    (snd (diagonal (toSpecZero 𝒜))
      (pullback.map (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜)
        (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯ ≫ toSpecZero 𝒜) (toSpecZero 𝒜) (toSpecZero 𝒜)
        (awayι 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯)
        (awayι 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯) (𝟙 (Spec (CommRingCat.of ↥(𝒜 0)))) ⋯ ⋯))

Tactic:
(MorphismProperty.cancel_left_of_respectsIso (P := @IsClosedImmersion)
    (f := (pullbackDiagonalMapIdIso ..).inv) _).mp ?_

Premises used: Iff.mp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Limits.pullbackDiagonalMapIdIso, AlgebraicGeometry.IsClosedImmersion, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
refine_1 :
  AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜 =
    Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
refine_2 :
  AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜 =
    Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
⊢ pullback (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜)
      (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜) ≅
    Spec
      (CommRingCat.of
        (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
          Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))

Tactic:
refine pullback.congrHom ?_ ?_ ≪≫ pullbackSpecIso (𝒜 0) (Away 𝒜 (i.2 : A)) (Away 𝒜 (j.2 : A))

Premises used: AlgebraicGeometry.pullbackSpecIso, Membership.mem, Subtype, CategoryTheory.Limits.pullback.congrHom, OfNat.ofNat, Sigma.snd, Subtype.val, HomogeneousLocalization.Away
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
refine_1 :
  Eq.{u_2 + 1} (α :=
    Spec (CommRingCat.of (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
    (Spec.map
      (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
    (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
⊢ AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜 =
    Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))

Tactic:
simp [affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayι_toSpecZero]

Premises used: AlgebraicGeometry.Proj.affineOpenCover, AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan, AlgebraicGeometry.Proj.awayι_toSpecZero
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
⊢ Eq.{u_2 + 1} (α :=
    Spec (CommRingCat.of (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
    (Spec.map
      (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
    (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
refine_2 :
  Eq.{u_2 + 1} (α :=
    Spec (CommRingCat.of (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
    (Spec.map
      (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
    (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
⊢ AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜 =
    Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))

Tactic:
simp [affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayι_toSpecZero]

Premises used: AlgebraicGeometry.Proj.affineOpenCover, AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan, AlgebraicGeometry.Proj.awayι_toSpecZero
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
⊢ Eq.{u_2 + 1} (α :=
    Spec (CommRingCat.of (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
    (Spec.map
      (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
    (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
e₁ : pullback (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜)
    (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜) ≅
  Spec
    (CommRingCat.of
      (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
        Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) :=
  congrHom ⋯ ⋯ ≪≫
    pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
      (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
e₂ : pullback (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i)
    (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j) ≅
  Spec
    (CommRingCat.of
      (Away 𝒜
        ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
    Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) →+*
  Away 𝒜 ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)) :=
  AlgHom.toRingHom
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯ :
      Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
          Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) →ₐ[↥(𝒜 0)]
        Away 𝒜
          ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
⊢ Function.Surjective (α :=
    Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
      Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
    (β :=
    Away 𝒜 ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
    (⇑F : (a : Away 𝒜 (↑i.snd : A) ⊗[↥(𝒜 0)] Away 𝒜 (↑j.snd : A)) → Away 𝒜 ((↑i.snd : A) * (↑j.snd : A)))

Tactic:
have : Function.Surjective F := lift_awayMapₐ_awayMapₐ_surjective 𝒜 i.2.2 j.2.2 rfl i.1.2
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
e₁ : pullback (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜)
    (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜) ≅
  Spec
    (CommRingCat.of
      (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
        Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) :=
  congrHom ⋯ ⋯ ≪≫
    pullbackSpecIso (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
      (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
e₂ : pullback (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i)
    (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j) ≅
  Spec
    (CommRingCat.of
      (Away 𝒜
        ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))) :=
  pullbackAwayιIso 𝒜 ⋯ ⋯ ⋯ ⋯ ⋯
F : Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
    Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) →+*
  Away 𝒜 ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)) :=
  AlgHom.toRingHom
    (Algebra.TensorProduct.lift (awayMapₐ 𝒜 ⋯ ⋯) (awayMapₐ 𝒜 ⋯ ⋯) ⋯ :
      Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
          Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) →ₐ[↥(𝒜 0)]
        Away 𝒜
          ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
this :
  Function.Surjective (α :=
    Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
      Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))
    (β :=
    Away 𝒜 ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
    (⇑F : (a : Away 𝒜 (↑i.snd : A) ⊗[↥(𝒜 0)] Away 𝒜 (↑j.snd : A)) → Away 𝒜 ((↑i.snd : A) * (↑j.snd : A)))
⊢ IsClosedImmersion.{u_2} (X :=
    Spec
      (CommRingCat.of
        (Away 𝒜
          ((↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) * (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
    (Y :=
    Spec
      (CommRingCat.of
        (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
          Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
    (Spec.map (CommRingCat.ofHom F))

Tactic:
IsClosedImmersion.spec_of_surjective
      (CommRingCat.ofHom (R := Away 𝒜 i.2.1 ⊗[𝒜 0] Away 𝒜 j.2.1) F) this

Premises used: CommRingCat.ofHom, AlgebraicGeometry.IsClosedImmersion.spec_of_surjective
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ Scheme.IsSeparated.{u_2} (Proj 𝒜)

Tactic:
(HasAffineProperty.iff_of_isAffine (P := @IsSeparated)).mp (isSeparated 𝒜)

Premises used: AlgebraicGeometry.Proj.isSeparated, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
obtain :
  ∀ (x : Finset A) (hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤)
    (hx' : ∀ i ∈ x, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n), LocallyOfFiniteType (X := Proj 𝒜) (toSpecZero 𝒜)
⊢ LocallyOfFiniteType (X := Proj 𝒜) (toSpecZero 𝒜)

Tactic:
obtain ⟨x, hx, hx'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜

Premises used: GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
hx' : ∀ i ∈ x, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n
choose :
  ∀ (d : (i : A) → i ∈ x → ℕ) (hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0) (hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)),
    LocallyOfFiniteType (X := Proj 𝒜) (toSpecZero 𝒜)
⊢ LocallyOfFiniteType (X := Proj 𝒜) (toSpecZero 𝒜)

Tactic:
choose d hd hxd using hx'
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
⊢ Eq.{u_2 + 1} (α := Subalgebra (↥(𝒜 0)) A)
    (Algebra.adjoin (↥(𝒜 0)) (Set.range (ι := ↥x) (Subtype.val (p := fun (x_1 : A) ↦ x_1 ∈ x)))) ⊤

Tactic:
simpa using hx
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
rw :
  ∀ (i : ↥x),
    LocallyOfFiniteType (X := (↑(basicOpen 𝒜 (↑i : A)) : Scheme)) (Opens.ι (basicOpen 𝒜 (↑i : A)) ≫ toSpecZero 𝒜)
⊢ LocallyOfFiniteType (X := Proj 𝒜) (toSpecZero 𝒜)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := @LocallyOfFiniteType) _
    (Proj.iSup_basicOpen_eq_top' 𝒜 (ι := x) (↑) (fun i ↦ ⟨_, hxd _ i.2⟩) (by simpa using hx))]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top, AlgebraicGeometry.Proj.iSup_basicOpen_eq_top', Exists.intro
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
rw :
  RingHom.FiniteType.{u_2, u_2} (A := (↑(CommRingCat.of ↥(𝒜 0)) : Type u_2)) (B :=
    (↑(CommRingCat.of (HomogeneousLocalization 𝒜 (Submonoid.powers (↑i : A)))) : Type u_2))
    (CommRingCat.Hom.hom (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A)))))
⊢ LocallyOfFiniteType (X := (↑(basicOpen 𝒜 (↑i : A)) : Scheme)) (Opens.ι (basicOpen 𝒜 (↑i : A)) ≫ toSpecZero 𝒜)

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso (P := @LocallyOfFiniteType)
    (Proj.basicOpenIsoSpec 𝒜 (i : A) (hxd _ i.2) (hd _ i.2).bot_lt).inv, ← Category.assoc,
    ← Proj.awayι, Proj.awayι_toSpecZero, HasRingHomProperty.Spec_iff (P := @LocallyOfFiniteType)]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Proj.awayι_toSpecZero, AlgebraicGeometry.HasRingHomProperty.Spec_iff, AlgebraicGeometry.LocallyOfFiniteType, AlgebraicGeometry.Proj.basicOpenIsoSpec, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, Subtype.val, CategoryTheory.Iso.inv, AlgebraicGeometry.Proj.awayι, Ne.bot_lt, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ RingHom.FiniteType.{u_2, u_2} (A := (↑(CommRingCat.of ↥(𝒜 0)) : Type u_2)) (B :=
    (↑(CommRingCat.of (HomogeneousLocalization 𝒜 (Submonoid.powers (↑i : A)))) : Type u_2))
    (CommRingCat.Hom.hom (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A)))))

Tactic:
HomogeneousLocalization.Away.finiteType _ _ (hxd _ i.2)

Premises used: HomogeneousLocalization, Set.Mem, RingHom.FiniteType, HomogeneousLocalization.fromZeroRingHom, Quotient, HomogeneousLocalization.Away.finiteType, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
⊢ RingHom.FiniteType.{u_2, u_2} (A := (↑(CommRingCat.of ↥(𝒜 0)) : Type u_2)) (B :=
    (↑(CommRingCat.of (HomogeneousLocalization 𝒜 (Submonoid.powers (↑i : A)))) : Type u_2))
    (CommRingCat.Hom.hom (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A)))))

Tactic:
exact HomogeneousLocalization.Away.finiteType _ _ (hxd _ i.2)

Premises used: HomogeneousLocalization.Away.finiteType, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
rw : CompactSpace.{u_2} ↥(Proj 𝒜)
⊢ QuasiCompact (X := Proj 𝒜) (toSpecZero 𝒜)

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @QuasiCompact)]

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
obtain :
  ∀ (x : Finset A) (hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤)
    (hx' : ∀ i ∈ x, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n), CompactSpace.{u_2} ↥(Proj 𝒜)
⊢ CompactSpace.{u_2} ↥(Proj 𝒜)

Tactic:
obtain ⟨x, hx, hx'⟩ := GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero 𝒜

Premises used: GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous_ne_zero
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
hx' : ∀ i ∈ x, ∃ (n : ℕ), n ≠ 0 ∧ i ∈ 𝒜 n
choose :
  ∀ (d : (i : A) → i ∈ x → ℕ) (hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0) (hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)),
    CompactSpace.{u_2} ↥(Proj 𝒜)
⊢ CompactSpace.{u_2} ↥(Proj 𝒜)

Tactic:
choose d hd hxd using hx'
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
rw : IsCompact (X := ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (Hom.opensRange (awayι 𝒜 (↑i : A) ⋯ ⋯)))
⊢ IsCompact (X := ↥(Proj 𝒜)) (TopologicalSpace.Opens.carrier (basicOpen 𝒜 (↑i : A)))

Tactic:
rw [← Proj.opensRange_awayι _ _ (hxd _ i.2) (hd _ i.2).bot_lt]

Premises used: AlgebraicGeometry.Proj.opensRange_awayι, Ne.bot_lt, Subtype.property