-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem isLocalization_basicOpen :
    IsLocalization.Away f Γ(X, X.basicOpen f)

Proof state:
case h.e'_3.h.h.e_i
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))
he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring
⊢ CommRingCat.Hom.hom
      (((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) ≫
        (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop).op ≫
          (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    CommRingCat.Hom.hom (StructureSheaf.toOpen (↑Γ(X, U)) (PrimeSpectrum.basicOpen f))

Tactic:
simp only [Category.assoc, ← Functor.map_comp, ← op_comp]

Result:
case h.e'_3.h.h.e_i
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))
he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring
⊢ CommRingCat.Hom.hom
      ((Scheme.ΓSpecIso Γ(X, U)).inv ≫
        (Spec Γ(X, U)).presheaf.map (eqToHom ⋯ ≫ (Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop ≫ eqToHom ⋯).op) =
    CommRingCat.Hom.hom (StructureSheaf.toOpen (↑Γ(X, U)) (PrimeSpectrum.basicOpen f))

Proof state:
case h.e'_3.h.h.e_i
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))
he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring
⊢ CommRingCat.Hom.hom
      ((Scheme.ΓSpecIso Γ(X, U)).inv ≫
        (Spec Γ(X, U)).presheaf.map (eqToHom ⋯ ≫ (Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop ≫ eqToHom ⋯).op) =
    CommRingCat.Hom.hom (StructureSheaf.toOpen (↑Γ(X, U)) (PrimeSpectrum.basicOpen f))

Tactic:
exact CommRingCat.hom_ext_iff.mp (StructureSheaf.toOpen_res _ _ _ _)

Result:
no goals

Proof state:
case h.e'_3.h.h.e_i
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))
he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring
⊢ CommRingCat.Hom.hom
      (X.presheaf.map (homOfLE ⋯).op ≫
        hU.fromSpec.c.app (op (X.basicOpen f)) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    CommRingCat.Hom.hom (StructureSheaf.toOpen (↑Γ(X, U)) (PrimeSpectrum.basicOpen f))

Tactic:
rw [hU.fromSpec.naturality_assoc, hU.fromSpec_app_self]

Result:
case h.e'_3.h.h.e_i
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))
he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring
⊢ CommRingCat.Hom.hom
      (((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) ≫
        (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE ⋯).op.unop).op ≫
          (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    CommRingCat.Hom.hom (StructureSheaf.toOpen (↑Γ(X, U)) (PrimeSpectrum.basicOpen f))

Proof state:
case h.e'_3.h.h.e_i
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))
he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring
⊢ (asIso (hU.basicOpenSectionsToAffine f)).commRingCatIsoToRingEquiv.toRingHom.comp
      (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) =
    CommRingCat.Hom.hom (StructureSheaf.toOpen (↑Γ(X, U)) (unop (op (PrimeSpectrum.basicOpen f))))

Tactic:
dsimp [CommRingCat.ofHom, RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
  basicOpenSectionsToAffine]

Result:
case h.e'_3.h.h.e_i
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))
he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring
⊢ CommRingCat.Hom.hom
      (X.presheaf.map (homOfLE ⋯).op ≫
        hU.fromSpec.c.app (op (X.basicOpen f)) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) =
    CommRingCat.Hom.hom (StructureSheaf.toOpen (↑Γ(X, U)) (PrimeSpectrum.basicOpen f))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsLocalization (Submonoid.powers f) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)

Tactic:
convert StructureSheaf.IsLocalization.to_basicOpen _ f using 1

Result:
case h.e'_3.h.h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))
he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring
⊢ ((asIso (hU.basicOpenSectionsToAffine f)).commRingCatIsoToRingEquiv.toRingHom.comp
        (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f))).toAlgebra =
    StructureSheaf.openAlgebra (↑Γ(X, U)) (op (PrimeSpectrum.basicOpen f))

Proof state:
case h.e'_3.h.h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))
he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring
⊢ ((asIso (hU.basicOpenSectionsToAffine f)).commRingCatIsoToRingEquiv.toRingHom.comp
        (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f))).toAlgebra =
    StructureSheaf.openAlgebra (↑Γ(X, U)) (op (PrimeSpectrum.basicOpen f))

Tactic:
congr 1

Result:
case h.e'_3.h.h.e_i
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
e_1✝ :
  ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))
he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring
⊢ (asIso (hU.basicOpenSectionsToAffine f)).commRingCatIsoToRingEquiv.toRingHom.comp
      (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) =
    CommRingCat.Hom.hom (StructureSheaf.toOpen (↑Γ(X, U)) (unop (op (PrimeSpectrum.basicOpen f))))

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)

Tactic:
apply
  (IsLocalization.isLocalization_iff_of_ringEquiv (Submonoid.powers f)
    (asIso <| basicOpenSectionsToAffine hU f).commRingCatIsoToRingEquiv).mpr

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : ↑Γ(X, U)
⊢ IsLocalization (Submonoid.powers f) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)