no goals
C : Type ?u.4131
inst✝ : Category C
X Y : PresheafedSpace C
α β : Hom X Y
w : α.base = β.base
⊢ Functor.op (Opens.map α.base) = Functor.op (Opens.map β.base)
rw [w]
case mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
β : Hom X Y
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ base _* X.presheaf
w : { base := base, c := c }.base = β.base
h :
  { base := base, c := c }.c ≫
      whiskerRight (eqToHom (_ : Functor.op (Opens.map { base := base, c := c }.base) = Functor.op (Opens.map β.base)))
        X.presheaf =
    β.c
⊢ { base := base, c := c } = β
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
α β : Hom X Y
w : α.base = β.base
h : α.c ≫ whiskerRight (eqToHom (_ : Functor.op (Opens.map α.base) = Functor.op (Opens.map β.base))) X.presheaf = β.c
⊢ α = β
rcases α with ⟨base, c⟩
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ base _* X.presheaf
base' : ↑X ⟶ ↑Y
c' : Y.presheaf ⟶ base' _* X.presheaf
w : { base := base, c := c }.base = { base := base', c := c' }.base
h :
  { base := base, c := c }.c ≫
      whiskerRight
        (eqToHom
          (_ :
            Functor.op (Opens.map { base := base, c := c }.base) =
              Functor.op (Opens.map { base := base', c := c' }.base)))
        X.presheaf =
    { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }
case mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
β : Hom X Y
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ base _* X.presheaf
w : { base := base, c := c }.base = β.base
h :
  { base := base, c := c }.c ≫
      whiskerRight (eqToHom (_ : Functor.op (Opens.map { base := base, c := c }.base) = Functor.op (Opens.map β.base)))
        X.presheaf =
    β.c
⊢ { base := base, c := c } = β
rcases β with ⟨base', c'⟩
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ base _* X.presheaf
base' : ↑X ⟶ ↑Y
c' : Y.presheaf ⟶ base' _* X.presheaf
w : base = base'
h :
  { base := base, c := c }.c ≫
      whiskerRight
        (eqToHom
          (_ :
            Functor.op (Opens.map { base := base, c := c }.base) =
              Functor.op (Opens.map { base := base', c := c' }.base)))
        X.presheaf =
    { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ base _* X.presheaf
base' : ↑X ⟶ ↑Y
c' : Y.presheaf ⟶ base' _* X.presheaf
w : { base := base, c := c }.base = { base := base', c := c' }.base
h :
  { base := base, c := c }.c ≫
      whiskerRight
        (eqToHom
          (_ :
            Functor.op (Opens.map { base := base, c := c }.base) =
              Functor.op (Opens.map { base := base', c := c' }.base)))
        X.presheaf =
    { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }
dsimp at w
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ base _* X.presheaf
h :
  { base := base, c := c }.c ≫
      whiskerRight
        (eqToHom
          (_ :
            Functor.op (Opens.map { base := base, c := c }.base) =
              Functor.op (Opens.map { base := base, c := c' }.base)))
        X.presheaf =
    { base := base, c := c' }.c
⊢ { base := base, c := c } = { base := base, c := c' }
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ base _* X.presheaf
base' : ↑X ⟶ ↑Y
c' : Y.presheaf ⟶ base' _* X.presheaf
w : base = base'
h :
  { base := base, c := c }.c ≫
      whiskerRight
        (eqToHom
          (_ :
            Functor.op (Opens.map { base := base, c := c }.base) =
              Functor.op (Opens.map { base := base', c := c' }.base)))
        X.presheaf =
    { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }
subst w
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ base _* X.presheaf
h : c ≫ whiskerRight (𝟙 (Functor.op (Opens.map base))) X.presheaf = c'
⊢ { base := base, c := c } = { base := base, c := c' }
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ base _* X.presheaf
h :
  { base := base, c := c }.c ≫
      whiskerRight
        (eqToHom
          (_ :
            Functor.op (Opens.map { base := base, c := c }.base) =
              Functor.op (Opens.map { base := base, c := c' }.base)))
        X.presheaf =
    { base := base, c := c' }.c
⊢ { base := base, c := c } = { base := base, c := c' }
dsimp at h
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ base _* X.presheaf
h : c = c'
⊢ { base := base, c := c } = { base := base, c := c' }
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ base _* X.presheaf
h : c ≫ whiskerRight (𝟙 (Functor.op (Opens.map base))) X.presheaf = c'
⊢ { base := base, c := c } = { base := base, c := c' }
erw [whiskerRight_id', comp_id] at h
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ base _* X.presheaf
⊢ { base := base, c := c } = { base := base, c := c }
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ base _* X.presheaf
h : c = c'
⊢ { base := base, c := c } = { base := base, c := c' }
subst h
no goals
case mk.mk
C : Type u_1
inst✝ : Category C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ base _* X.presheaf
⊢ { base := base, c := c } = { base := base, c := c }
rfl