-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem comp_ring_hom_ext {X : LocallyRingedSpace.{u}} {R : CommRingCat.{u}} {f : R ⟶ Γ.obj (op X)}
    {β : X ⟶ Spec.locallyRingedSpaceObj R}
    (w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base)
    (h :
      ∀ r : R,
        f ≫ X.presheaf.map (homOfLE le_top : (Opens.map β.base).obj (basicOpen r) ⟶ _).op =
          toOpen R (basicOpen r) ≫ β.c.app (op (basicOpen r))) :
    X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β

Proof state:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
⊢ ∀ (r : ↑R),
    let U := basicOpen r;
    (toOpen (↑R) U ≫ (Hom.toShHom (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)

Tactic:
intro r U

Result:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (toOpen (↑R) U ≫ (Hom.toShHom (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) =
    toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)

Proof state:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      X.presheaf.map ((X.toΓSpecMapBasicOpen ((CommRingCat.Hom.hom f) r)).leTop.op ≫ eqToHom ⋯) =
    toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)

Tactic:
exact h r

Result:
no goals

Proof state:
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
⊢ X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β

Tactic:
ext1

Result:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
⊢ Hom.toShHom (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f) = Hom.toShHom β

Proof state:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
⊢ Hom.toShHom (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f) = Hom.toShHom β

Tactic:
refine Spec.basicOpen_hom_ext w ?_

Result:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
⊢ ∀ (r : ↑R),
    let U := basicOpen r;
    (toOpen (↑R) U ≫ (Hom.toShHom (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)

Proof state:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      (toOpen (↑(Γ.obj (op X))) ((Opens.comap (PrimeSpectrum.comap (CommRingCat.Hom.hom f))) U) ≫
          X.toΓSpec.c.app (op ((Opens.map (Spec.locallyRingedSpaceMap f).base).obj (unop (op U))))) ≫
        X.presheaf.map (eqToHom ⋯) =
    toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)

Tactic:
erw [toΓSpecSheafedSpace_app_spec, ← X.presheaf.map_comp]

Result:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
      X.presheaf.map ((X.toΓSpecMapBasicOpen ((CommRingCat.Hom.hom f) r)).leTop.op ≫ eqToHom ⋯) =
    toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)

Proof state:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (toOpen (↑R) U ≫
        (Spec.locallyRingedSpaceMap f).c.app (op U) ≫
          X.toΓSpec.c.app (op ((Opens.map (Spec.locallyRingedSpaceMap f).base).obj (unop (op U))))) ≫
      X.presheaf.map (eqToHom ⋯) =
    toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)

Tactic:
erw [toOpen_comp_comap_assoc]

Result:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (CommRingCat.ofHom (CommRingCat.Hom.hom f) ≫
        toOpen (↑(Γ.obj (op X))) ((Opens.comap (PrimeSpectrum.comap (CommRingCat.Hom.hom f))) U) ≫
          X.toΓSpec.c.app (op ((Opens.map (Spec.locallyRingedSpaceMap f).base).obj (unop (op U))))) ≫
      X.presheaf.map (eqToHom ⋯) =
    toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)

Proof state:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (toOpen (↑R) U ≫ (Hom.toShHom (X.toΓSpec ≫ Spec.locallyRingedSpaceMap f)).c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) =
    toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)

Tactic:
rw [LocallyRingedSpace.comp_c_app]

Result:
case h
X : LocallyRingedSpace
R : CommRingCat
f : R ⟶ Γ.obj (op X)
β : X ⟶ Spec.locallyRingedSpaceObj R
w : X.toΓSpec.base ≫ (Spec.locallyRingedSpaceMap f).base = β.base
h : ∀ (r : ↑R), f ≫ X.presheaf.map (homOfLE ⋯).op = toOpen (↑R) (basicOpen r) ≫ β.c.app (op (basicOpen r))
r : ↑R
U : Opens (PrimeSpectrum ↑R) := basicOpen r
⊢ (toOpen (↑R) U ≫
        (Spec.locallyRingedSpaceMap f).c.app (op U) ≫
          X.toΓSpec.c.app (op ((Opens.map (Spec.locallyRingedSpaceMap f).base).obj (unop (op U))))) ≫
      X.presheaf.map (eqToHom ⋯) =
    toOpen (↑R) U ≫ (Hom.toShHom β).c.app (op U)