[GOAL]
C : Type u_1
inst✝ : Category.{?u.34375, u_1} C
⊢ Category.{?u.34397, max (max (?u.34414 + 1) ?u.34375) u_1} (InducedCategory (PresheafedSpace C) toPresheafedSpace)
[PROOFSTEP]
infer_instance
  -- Porting note: adding an ext lemma.
  -- See https://github.com/leanprover-community/mathlib4/issues/5229
[GOAL]
C : Type u_1
inst✝ : Category.{?u.34683, u_1} C
X Y : SheafedSpace C
α β : X ⟶ Y
w : α.base = β.base
⊢ (Opens.map α.base).op = (Opens.map β.base).op
[PROOFSTEP]
rw [w]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.158005, u_1} C
X : SheafedSpace C
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ X.presheaf.obj U = ((𝟙 X).base _* X.presheaf).obj U
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : SheafedSpace C
U : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
⊢ NatTrans.app (𝟙 X).c U =
    eqToHom (_ : X.presheaf.obj U = X.presheaf.obj ((Opens.map (𝟙 ↑X.toPresheafedSpace)).op.obj U))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝ : Category.{?u.162894, u_1} C
X Y : SheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map β.base).op.obj U = (Opens.map α.base).op.obj U
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
inst✝ : Category.{?u.162894, u_1} C
X Y : SheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U
[PROOFSTEP]
rfl
