-- Mathlib/Geometry/RingedSpace/PresheafedSpace.lean
theorem Hom.ext {X Y : PresheafedSpace C} (α β : Hom X Y) (w : α.base = β.base)
    (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
α β : X.Hom Y
w : α.base = β.base
h : α.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
⊢ α = β

Tactic:
rcases α with ⟨base, c⟩

Result:
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
β : X.Hom Y
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
w : { base := base, c := c }.base = β.base
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
⊢ { base := base, c := c } = β

Proof state:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
base' : ↑X ⟶ ↑Y
c' : Y.presheaf ⟶ (Presheaf.pushforward C base').obj X.presheaf
w : base = base'
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }

Tactic:
subst w

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base, c := c' }.c
⊢ { base := base, c := c } = { base := base, c := c' }

Proof state:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : c = c'
⊢ { base := base, c := c } = { base := base, c := c' }

Tactic:
subst h

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
⊢ { base := base, c := c } = { base := base, c := c }

Proof state:
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
β : X.Hom Y
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
w : { base := base, c := c }.base = β.base
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = β.c
⊢ { base := base, c := c } = β

Tactic:
rcases β with ⟨base', c'⟩

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
base' : ↑X ⟶ ↑Y
c' : Y.presheaf ⟶ (Presheaf.pushforward C base').obj X.presheaf
w : { base := base, c := c }.base = { base := base', c := c' }.base
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }

Proof state:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : c ≫ whiskerRight (𝟙 (Opens.map base).op) X.presheaf = c'
⊢ { base := base, c := c } = { base := base, c := c' }

Tactic:
erw [whiskerRight_id', comp_id] at h

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : c = c'
⊢ { base := base, c := c } = { base := base, c := c' }

Proof state:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base, c := c' }.c
⊢ { base := base, c := c } = { base := base, c := c' }

Tactic:
dsimp at h

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : c ≫ whiskerRight (𝟙 (Opens.map base).op) X.presheaf = c'
⊢ { base := base, c := c } = { base := base, c := c' }

Proof state:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
base' : ↑X ⟶ ↑Y
c' : Y.presheaf ⟶ (Presheaf.pushforward C base').obj X.presheaf
w : { base := base, c := c }.base = { base := base', c := c' }.base
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }

Tactic:
dsimp at w

Result:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
base' : ↑X ⟶ ↑Y
c' : Y.presheaf ⟶ (Presheaf.pushforward C base').obj X.presheaf
w : base = base'
h : { base := base, c := c }.c ≫ whiskerRight (eqToHom ⋯) X.presheaf = { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }

Proof state:
C : Type u_1
inst✝ : Category.{?u.3872, u_1} C
X Y : PresheafedSpace C
α β : X.Hom Y
w : α.base = β.base
⊢ (Opens.map α.base).op = (Opens.map β.base).op

Tactic:
rw [w]

Result:
no goals

Proof state:
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
⊢ { base := base, c := c } = { base := base, c := c }

Tactic:
rfl

Result:
no goals