-- Mathlib/AlgebraicGeometry/Spec.lean
theorem Spec.basicOpen_hom_ext {X : RingedSpace.{u}} {R : CommRingCat.{u}}
    {α β : X ⟶ Spec.sheafedSpaceObj R} (w : α.base = β.base)
    (h : ∀ r : R,
      let U := PrimeSpectrum.basicOpen r
      (toOpen R U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom (by rw [w])) =
        toOpen R U ≫ β.c.app (op U)) :
    α = β

Proof state:
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
r : ↑R
⊢ (α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen r)) =
    β.c.app (op (PrimeSpectrum.basicOpen r))

Tactic:
apply (StructureSheaf.to_basicOpen_epi R r).1

Result:
case h.a
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
r : ↑R
⊢ toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫
      (α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen r)) =
    toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫ β.c.app (op (PrimeSpectrum.basicOpen r))

Proof state:
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
⊢ α = β

Tactic:
ext : 1

Result:
case w
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
⊢ α.base = β.base

case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
⊢ α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c

Proof state:
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
⊢ ∀ (i : ↑R),
    (α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen i)) =
      β.c.app (op (PrimeSpectrum.basicOpen i))

Tactic:
intro r

Result:
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
r : ↑R
⊢ (α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen r)) =
    β.c.app (op (PrimeSpectrum.basicOpen r))

Proof state:
case h.a
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
r : ↑R
⊢ toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫
      (α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen r)) =
    toOpen (↑R) (PrimeSpectrum.basicOpen r) ≫ β.c.app (op (PrimeSpectrum.basicOpen r))

Tactic:
simpa using h r

Result:
no goals

Proof state:
case w
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
⊢ α.base = β.base

Tactic:
exact w

Result:
no goals

Proof state:
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
⊢ α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c

Tactic:
apply
  ((TopCat.Sheaf.pushforward _ β.base).obj X.sheaf).hom_ext _ PrimeSpectrum.isBasis_basic_opens

Result:
case h
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (toOpen (↑R) U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom ⋯) = toOpen (↑R) U ≫ β.c.app (op U)
⊢ ∀ (i : ↑R),
    (α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op (PrimeSpectrum.basicOpen i)) =
      β.c.app (op (PrimeSpectrum.basicOpen i))

Proof state:
X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.base = β.base
r : ↑R
U : TopologicalSpace.Opens (PrimeSpectrum ↑R) := PrimeSpectrum.basicOpen r
⊢ (TopologicalSpace.Opens.map α.base).op.obj (op U) = (TopologicalSpace.Opens.map β.base).op.obj (op U)

Tactic:
rw [w]

Result:
no goals