-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma isIso_toSpec (f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
    IsIso (toSpec 𝒜 f)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : IsIso (toSpec 𝒜 f).base
x : ↑(Proj.restrict ⋯).toTopCat
⊢ IsIso
    ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫
      («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)

Tactic:
infer_instance

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsIso (toSpec 𝒜 f)

Tactic:
haveI : IsIso (toSpec 𝒜 f).base := toSpec_base_isIso 𝒜 f_deg hm

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : IsIso (toSpec 𝒜 f).base
⊢ IsIso (toSpec 𝒜 f)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : IsIso (toSpec 𝒜 f).base
⊢ IsIso (toSpec 𝒜 f)

Tactic:
haveI (x) : IsIso ((toSpec 𝒜 f).stalkMap x) := by
  rw [stalkMap_toSpec 𝒜 f x f_deg hm]; infer_instance

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this✝ : IsIso (toSpec 𝒜 f).base
this : ∀ (x : ↑(Proj.restrict ⋯).toTopCat), IsIso (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
⊢ IsIso (toSpec 𝒜 f)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this✝ : IsIso (toSpec 𝒜 f).base
this : ∀ (x : ↑(Proj.restrict ⋯).toTopCat), IsIso (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
⊢ IsIso (toSpec 𝒜 f)

Tactic:
haveI : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f) :=
  LocallyRingedSpace.IsOpenImmersion.of_stalk_iso (toSpec 𝒜 f)
    (TopCat.homeoOfIso (asIso <| (toSpec 𝒜 f).base)).isOpenEmbedding

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this✝¹ : IsIso (toSpec 𝒜 f).base
this✝ : ∀ (x : ↑(Proj.restrict ⋯).toTopCat), IsIso (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
this : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f)
⊢ IsIso (toSpec 𝒜 f)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : IsIso (toSpec 𝒜 f).base
x : ↑(Proj.restrict ⋯).toTopCat
⊢ IsIso (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)

Tactic:
rw [stalkMap_toSpec 𝒜 f x f_deg hm]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : IsIso (toSpec 𝒜 f).base
x : ↑(Proj.restrict ⋯).toTopCat
⊢ IsIso
    ((specStalkEquiv 𝒜 f x f_deg hm).hom ≫
      («Proj».stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ≫ (Proj.restrictStalkIso ⋯ x).inv)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this✝¹ : IsIso (toSpec 𝒜 f).base
this✝ : ∀ (x : ↑(Proj.restrict ⋯).toTopCat), IsIso (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
this : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f)
⊢ IsIso (toSpec 𝒜 f)

Tactic:
exact LocallyRingedSpace.IsOpenImmersion.to_iso _

Result:
no goals