-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem isIso_ΓSpec_adjunction_unit_app_basicOpen {X : Scheme} [CompactSpace X]
    [QuasiSeparatedSpace X] (f : X.presheaf.obj (op ⊤)) :
    IsIso ((ΓSpec.adjunction.unit.app X).c.app (op (PrimeSpectrum.basicOpen f)))

Proof state:
case inst.refine_2
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsQuasiSeparated ⊤.carrier

Tactic:
exact isQuasiSeparated_univ

Result:
no goals

Proof state:
case inst.refine_1
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsCompact ⊤.carrier

Tactic:
exact isCompact_univ

Result:
no goals

Proof state:
case inst
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsLocalization ?M ↑(((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).presheaf.obj (op (PrimeSpectrum.basicOpen f)))

Tactic:
exact StructureSheaf.IsLocalization.to_basicOpen _ _

Result:
no goals

Proof state:
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsIso ((ΓSpec.adjunction.unit.app X).c.app (op (PrimeSpectrum.basicOpen f)))

Tactic:
refine @IsIso.of_isIso_comp_right _ _ _ _ _ _ (X.presheaf.map
  (eqToHom (Scheme.toSpecΓ_preimage_basicOpen _ _).symm).op) _ ?_

Result:
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsIso ((ΓSpec.adjunction.unit.app X).c.app (op (PrimeSpectrum.basicOpen f)) ≫ X.presheaf.map (eqToHom ⋯).op)

Proof state:
case inst
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsLocalization (Submonoid.powers f) ↑(X.presheaf.obj (op (((𝟭 Scheme).obj X).basicOpen f)))

Tactic:
refine is_localization_basicOpen_of_qcqs ?_ ?_ _

Result:
case inst.refine_1
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsCompact ⊤.carrier

case inst.refine_2
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsQuasiSeparated ⊤.carrier

Proof state:
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom
        ((ΓSpec.adjunction.unit.app X).c.app (op (PrimeSpectrum.basicOpen f)) ≫ X.presheaf.map (eqToHom ⋯).op))

Tactic:
apply (config := { allowSynthFailures := true }) IsLocalization.bijective

Result:
case inst
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsLocalization ?M ↑(((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).presheaf.obj (op (PrimeSpectrum.basicOpen f)))

case inst
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsLocalization ?M ↑(X.presheaf.obj (op (((𝟭 Scheme).obj X).basicOpen f)))

case hf
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ (ConcreteCategory.hom
          ((ΓSpec.adjunction.unit.app X).c.app (op (PrimeSpectrum.basicOpen f)) ≫ X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ?R ↑(((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).presheaf.obj (op (PrimeSpectrum.basicOpen f)))) =
    algebraMap ?R ↑(X.presheaf.obj (op (((𝟭 Scheme).obj X).basicOpen f)))

case R
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ Type ?u.251231

case inst
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ CommSemiring ?R

case M
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ Submonoid ?R

case inst
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ Algebra ?R ↑(((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).presheaf.obj (op (PrimeSpectrum.basicOpen f)))

case inst
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ Algebra ?R ↑(X.presheaf.obj (op (((𝟭 Scheme).obj X).basicOpen f)))

Proof state:
case hf
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ (ConcreteCategory.hom
          ((ΓSpec.adjunction.unit.app X).c.app (op (PrimeSpectrum.basicOpen f)) ≫ X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ↑(unop (Scheme.Γ.rightOp.obj X))
        ↑(((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).presheaf.obj (op (PrimeSpectrum.basicOpen f)))) =
    algebraMap ↑(unop (Scheme.Γ.rightOp.obj X)) ↑(X.presheaf.obj (op (((𝟭 Scheme).obj X).basicOpen f)))

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, RingHom.algebraMap_toAlgebra,
  ← Functor.map_comp]

Result:
no goals

Proof state:
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ IsIso ((ΓSpec.adjunction.unit.app X).c.app (op (PrimeSpectrum.basicOpen f)) ≫ X.presheaf.map (eqToHom ⋯).op)

Tactic:
rw [ConcreteCategory.isIso_iff_bijective]

Result:
X : Scheme
inst✝¹ : CompactSpace ↑↑X.toPresheafedSpace
inst✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op ⊤))
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom
        ((ΓSpec.adjunction.unit.app X).c.app (op (PrimeSpectrum.basicOpen f)) ≫ X.presheaf.map (eqToHom ⋯).op))