-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem right_triangle (R : CommRingCat) :
    identityToΓSpec.app (Spec.toLocallyRingedSpace.obj <| op R) ≫
        Spec.toLocallyRingedSpace.map (SpecΓIdentity.inv.app R).op =
      𝟙 _

Proof state:
case w.w
R : CommRingCat
p : PrimeSpectrum ↑R
⊢ (ConcreteCategory.hom
        (((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec.base ≫
          (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base))
      p =
    (ConcreteCategory.hom (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).base) p

Tactic:
dsimp

Result:
case w.w
R : CommRingCat
p : PrimeSpectrum ↑R
⊢ (TopCat.Hom.hom (Spec.topMap (toSpecΓ R))) ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p) = p

Proof state:
case w.w
R : CommRingCat
p : PrimeSpectrum ↑R
x : ↑R
⊢ x ∈
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)))
          ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p)).asIdeal ↔
    x ∈ p.asIdeal

Tactic:
rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff ((structureSheaf R).presheaf.stalk p)
    p.asIdeal x]

Result:
case w.w
R : CommRingCat
p : PrimeSpectrum ↑R
x : ↑R
⊢ x ∈
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)))
          ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p)).asIdeal ↔
    (algebraMap ↑R ↑((structureSheaf ↑R).presheaf.stalk p)) x ∈
      IsLocalRing.maximalIdeal ↑((structureSheaf ↑R).presheaf.stalk p)

Proof state:
case w.w
R : CommRingCat
p : PrimeSpectrum ↑R
⊢ (TopCat.Hom.hom (Spec.topMap (toSpecΓ R))) ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p) = p

Tactic:
refine PrimeSpectrum.ext (Ideal.ext fun x => ?_)

Result:
case w.w
R : CommRingCat
p : PrimeSpectrum ↑R
x : ↑R
⊢ x ∈
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)))
          ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p)).asIdeal ↔
    x ∈ p.asIdeal

Proof state:
case h
R : CommRingCat
⊢ ∀ (r : ↑(unop (op ((𝟭 CommRingCat).obj R)))),
    (SpecΓIdentity.inv.app R).op.unop ≫
        ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).presheaf.map (homOfLE ⋯).op =
      toOpen (↑(unop (op ((𝟭 CommRingCat).obj R)))) (basicOpen r) ≫
        (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).c.app (op (basicOpen r))

Tactic:
intro r

Result:
case h
R : CommRingCat
r : ↑(unop (op ((𝟭 CommRingCat).obj R)))
⊢ (SpecΓIdentity.inv.app R).op.unop ≫
      ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).presheaf.map (homOfLE ⋯).op =
    toOpen (↑(unop (op ((𝟭 CommRingCat).obj R)))) (basicOpen r) ≫
      (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).c.app (op (basicOpen r))

Proof state:
R : CommRingCat
⊢ identityToΓSpec.app (Spec.toLocallyRingedSpace.obj (op R)) ≫
      Spec.toLocallyRingedSpace.map (SpecΓIdentity.inv.app R).op =
    𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))

Tactic:
apply LocallyRingedSpace.comp_ring_hom_ext

Result:
case w
R : CommRingCat
⊢ ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec.base ≫
      (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base =
    (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).base

case h
R : CommRingCat
⊢ ∀ (r : ↑(unop (op ((𝟭 CommRingCat).obj R)))),
    (SpecΓIdentity.inv.app R).op.unop ≫
        ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).presheaf.map (homOfLE ⋯).op =
      toOpen (↑(unop (op ((𝟭 CommRingCat).obj R)))) (basicOpen r) ≫
        (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).c.app (op (basicOpen r))

Proof state:
case w
R : CommRingCat
⊢ ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec.base ≫
      (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base =
    (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).base

Tactic:
ext (p : PrimeSpectrum R)

Result:
case w.w
R : CommRingCat
p : PrimeSpectrum ↑R
⊢ (ConcreteCategory.hom
        (((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec.base ≫
          (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).base))
      p =
    (ConcreteCategory.hom (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).base) p

Proof state:
case w.w
R : CommRingCat
p : PrimeSpectrum ↑R
x : ↑R
⊢ x ∈
      ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)))
          ((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase) p)).asIdeal ↔
    (algebraMap ↑R ↑((structureSheaf ↑R).presheaf.stalk p)) x ∈
      IsLocalRing.maximalIdeal ↑((structureSheaf ↑R).presheaf.stalk p)

Tactic:
rfl

Result:
no goals

Proof state:
case h
R : CommRingCat
r : ↑(unop (op ((𝟭 CommRingCat).obj R)))
⊢ (SpecΓIdentity.inv.app R).op.unop ≫
      ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).presheaf.map (homOfLE ⋯).op =
    toOpen (↑(unop (op ((𝟭 CommRingCat).obj R)))) (basicOpen r) ≫
      (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).c.app (op (basicOpen r))

Tactic:
apply toOpen_res

Result:
no goals