[GOAL]
C : Type u_1
inst✝ : Category.{?u.4128, u_1} C
X Y : PresheafedSpace C
α β : Hom X Y
w : α.base = β.base
⊢ (Opens.map α.base).op = (Opens.map β.base).op
[PROOFSTEP]
rw [w]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
α β : Hom X Y
w : α.base = β.base
h : α.c ≫ whiskerRight (eqToHom (_ : (Opens.map α.base).op = (Opens.map β.base).op)) X.presheaf = β.c
⊢ α = β
[PROOFSTEP]
rcases α with ⟨base, c⟩
[GOAL]
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 (_ : (Opens.map { base := base, c := c }.base).op = (Opens.map β.base).op)) X.presheaf =
    β.c
⊢ { base := base, c := c } = β
[PROOFSTEP]
rcases β with ⟨base', c'⟩
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 (_ : (Opens.map { base := base, c := c }.base).op = (Opens.map { base := base', c := c' }.base).op))
        X.presheaf =
    { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }
[PROOFSTEP]
dsimp at w
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 (_ : (Opens.map { base := base, c := c }.base).op = (Opens.map { base := base', c := c' }.base).op))
        X.presheaf =
    { base := base', c := c' }.c
⊢ { base := base, c := c } = { base := base', c := c' }
[PROOFSTEP]
subst w
[GOAL]
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 ⟶ base _* X.presheaf
h :
  { base := base, c := c }.c ≫
      whiskerRight
        (eqToHom (_ : (Opens.map { base := base, c := c }.base).op = (Opens.map { base := base, c := c' }.base).op))
        X.presheaf =
    { base := base, c := c' }.c
⊢ { base := base, c := c } = { base := base, c := c' }
[PROOFSTEP]
dsimp at h
[GOAL]
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 ⟶ base _* X.presheaf
h : c ≫ whiskerRight (𝟙 (Opens.map base).op) X.presheaf = c'
⊢ { base := base, c := c } = { base := base, c := c' }
[PROOFSTEP]
erw [whiskerRight_id', comp_id] at h
[GOAL]
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 ⟶ base _* X.presheaf
h : c = c'
⊢ { base := base, c := c } = { base := base, c := c' }
[PROOFSTEP]
subst h
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c : Y.presheaf ⟶ base _* X.presheaf
⊢ { base := base, c := c } = { base := base, c := c }
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
α β : Hom X Y
w : α.base = β.base
h : HEq α.c β.c
⊢ α = β
[PROOFSTEP]
cases α
[GOAL]
case mk
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 : HEq { base := base✝, c := c✝ }.c β.c
⊢ { base := base✝, c := c✝ } = β
[PROOFSTEP]
cases β
[GOAL]
case mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 : HEq { base := base✝¹, c := c✝¹ }.c { base := base✝, c := c✝ }.c
⊢ { base := base✝¹, c := c✝¹ } = { base := base✝, c := c✝ }
[PROOFSTEP]
congr
[GOAL]
C : Type u_1
inst✝ : Category.{?u.68893, u_1} C
X✝ Y✝ : PresheafedSpace C
x✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ x✝ = x✝
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.68893, u_1} C
X✝ Y✝ : PresheafedSpace C
x✝ : X✝ ⟶ Y✝
⊢ { base := 𝟙 ↑X✝ ≫ x✝.base, c := x✝.c ≫ (Presheaf.pushforward C x✝.base).map (𝟙 X✝.presheaf) } = x✝
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝ : Category.{?u.68893, u_1} C
X✝ Y✝ : PresheafedSpace C
x✝¹ : X✝ ⟶ Y✝
x✝ : (forget TopCat).obj ↑X✝
⊢ ↑{ base := 𝟙 ↑X✝ ≫ x✝¹.base, c := x✝¹.c ≫ (Presheaf.pushforward C x✝¹.base).map (𝟙 X✝.presheaf) }.base x✝ =
    ↑x✝¹.base x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.w
C : Type u_1
inst✝ : Category.{?u.68893, u_1} C
X✝ Y✝ : PresheafedSpace C
x✝¹ : X✝ ⟶ Y✝
x✝ : (forget TopCat).obj ↑X✝
⊢ ↑(𝟙 ↑X✝ ≫ x✝¹.base) x✝ = ↑x✝¹.base x✝
[PROOFSTEP]
simp
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.68893, u_1} C
X✝ Y✝ : PresheafedSpace C
x✝ : X✝ ⟶ Y✝
U✝ : Opens ↑↑Y✝
⊢ NatTrans.app
      ({ base := 𝟙 ↑X✝ ≫ x✝.base, c := x✝.c ≫ (Presheaf.pushforward C x✝.base).map (𝟙 X✝.presheaf) }.c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    { base := 𝟙 ↑X✝ ≫ x✝.base,
                        c := x✝.c ≫ (Presheaf.pushforward C x✝.base).map (𝟙 X✝.presheaf) }.base).op =
                (Opens.map x✝.base).op))
          X✝.presheaf)
      (op U✝) =
    NatTrans.app x✝.c (op U✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.68893, u_1} C
X✝ Y✝ : PresheafedSpace C
x✝ : X✝ ⟶ Y✝
U✝ : Opens ↑↑Y✝
⊢ NatTrans.app
      ((x✝.c ≫ (Presheaf.pushforward C x✝.base).map (𝟙 X✝.presheaf)) ≫
        whiskerRight (𝟙 (Opens.map (𝟙 ↑X✝ ≫ x✝.base)).op) X✝.presheaf)
      (op U✝) =
    NatTrans.app x✝.c (op U✝)
[PROOFSTEP]
simp only [map_id, whiskerRight_id', assoc]
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.68893, u_1} C
X✝ Y✝ : PresheafedSpace C
x✝ : X✝ ⟶ Y✝
U✝ : Opens ↑↑Y✝
⊢ NatTrans.app
      (x✝.c ≫ 𝟙 ((Presheaf.pushforward C x✝.base).obj X✝.presheaf) ≫ 𝟙 ((Opens.map (𝟙 ↑X✝ ≫ x✝.base)).op ⋙ X✝.presheaf))
      (op U✝) =
    NatTrans.app x✝.c (op U✝)
[PROOFSTEP]
erw [comp_id, comp_id]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.77226, u_1} C
X Y : PresheafedSpace 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_2, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ NatTrans.app (𝟙 X).c U = X.presheaf.map (𝟙 U)
[PROOFSTEP]
rw [id_c, map_id]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U : (Opens ↑↑X)ᵒᵖ
⊢ NatTrans.app (𝟙 X.presheaf) U = 𝟙 (X.presheaf.obj U)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.143246, u_1} C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map β.base).op.obj U = (Opens.map α.base).op.obj U
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
inst✝ : Category.{?u.143246, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y)ᵒᵖ
⊢ NatTrans.app α.c U =
    NatTrans.app β.c U ≫ X.presheaf.map (eqToHom (_ : (Opens.map β.base).op.obj U = (Opens.map α.base).op.obj U))
[PROOFSTEP]
subst h
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : PresheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y)ᵒᵖ
⊢ NatTrans.app α.c U =
    NatTrans.app α.c U ≫ X.presheaf.map (eqToHom (_ : (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
⊢ { base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } = 𝟙 X
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
x✝ : (CategoryTheory.forget TopCat).obj ↑X
⊢ ↑({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).base x✝ =
    ↑(𝟙 X).base x✝
case h.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑X
⊢ NatTrans.app
      (({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    ({ base := H.hom, c := α.inv } ≫
                        { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).base).op =
                (Opens.map (𝟙 X).base).op))
          X.presheaf)
      (op U✝) =
    NatTrans.app (𝟙 X).c (op U✝)
[PROOFSTEP]
simp only [comp_base, Iso.hom_inv_id, FunctorToTypes.map_id_apply, id_base]
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑X
⊢ NatTrans.app
      (({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    ({ base := H.hom, c := α.inv } ≫
                        { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).base).op =
                (Opens.map (𝟙 X).base).op))
          X.presheaf)
      (op U✝) =
    NatTrans.app (𝟙 X).c (op U✝)
[PROOFSTEP]
rw [NatTrans.comp_app]
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑X
⊢ NatTrans.app ({ base := H.hom, c := α.inv } ≫ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).c (op U✝) ≫
      NatTrans.app
        (whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    ({ base := H.hom, c := α.inv } ≫
                        { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom }).base).op =
                (Opens.map (𝟙 X).base).op))
          X.presheaf)
        (op U✝) =
    NatTrans.app (𝟙 X).c (op U✝)
[PROOFSTEP]
simp only [id_base, comp_obj, op_obj, comp_base, Presheaf.pushforwardObj_obj, Opens.map_comp_obj, comp_c_app, unop_op,
  Presheaf.toPushforwardOfIso_app, assoc, Iso.hom_inv_id_app, comp_id, whiskerRight_app, eqToHom_app, id_c_app, map_id,
  ← Functor.map_comp, eqToHom_trans, eqToHom_refl]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
⊢ { base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv } = 𝟙 Y
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
x✝ : (CategoryTheory.forget TopCat).obj ↑Y
⊢ ↑({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv }).base x✝ =
    ↑(𝟙 Y).base x✝
case h.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ NatTrans.app
      (({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv }).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    ({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫
                        { base := H.hom, c := α.inv }).base).op =
                (Opens.map (𝟙 Y).base).op))
          Y.presheaf)
      (op U✝) =
    NatTrans.app (𝟙 Y).c (op U✝)
[PROOFSTEP]
dsimp
[GOAL]
case w.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
x✝ : (CategoryTheory.forget TopCat).obj ↑Y
⊢ ↑(H.inv ≫ H.hom) x✝ = ↑(𝟙 ↑Y) x✝
case h.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ NatTrans.app
      (({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv }).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    ({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫
                        { base := H.hom, c := α.inv }).base).op =
                (Opens.map (𝟙 Y).base).op))
          Y.presheaf)
      (op U✝) =
    NatTrans.app (𝟙 Y).c (op U✝)
[PROOFSTEP]
rw [H.inv_hom_id]
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ NatTrans.app
      (({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv }).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    ({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫
                        { base := H.hom, c := α.inv }).base).op =
                (Opens.map (𝟙 Y).base).op))
          Y.presheaf)
      (op U✝) =
    NatTrans.app (𝟙 Y).c (op U✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ NatTrans.app
      (({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv }).c ≫
        whiskerRight (eqToHom (_ : (Opens.map (H.inv ≫ H.hom)).op = (Opens.map (𝟙 ↑Y)).op)) Y.presheaf)
      (op U✝) =
    NatTrans.app (𝟙 Y).c (op U✝)
[PROOFSTEP]
rw [NatTrans.comp_app]
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ NatTrans.app ({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv }).c (op U✝) ≫
      NatTrans.app (whiskerRight (eqToHom (_ : (Opens.map (H.inv ≫ H.hom)).op = (Opens.map (𝟙 ↑Y)).op)) Y.presheaf)
        (op U✝) =
    NatTrans.app (𝟙 Y).c (op U✝)
[PROOFSTEP]
simp only [Presheaf.pushforwardObj_obj, op_obj, Opens.map_comp_obj, comp_obj, comp_c_app, unop_op,
  Presheaf.toPushforwardOfIso_app, whiskerRight_app, eqToHom_app, assoc, id_c_app, map_id]
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ NatTrans.app α.inv (op U✝) ≫
      X.presheaf.map
          (eqToHom
            (_ :
              op ((Opens.map H.hom).obj U✝) =
                op
                  {
                    carrier :=
                      ↑H.hom ⁻¹'
                        ↑(op
                              { carrier := ↑H.inv ⁻¹' ↑(op ((Opens.map H.hom).obj U✝)).unop,
                                is_open' := (_ : IsOpen (↑H.inv ⁻¹' ↑(op ((Opens.map H.hom).obj U✝)).unop)) }).unop,
                    is_open' :=
                      (_ :
                        IsOpen
                          (↑H.hom ⁻¹'
                            ↑(op
                                  { carrier := ↑H.inv ⁻¹' ↑(op ((Opens.map H.hom).obj U✝)).unop,
                                    is_open' :=
                                      (_ : IsOpen (↑H.inv ⁻¹' ↑(op ((Opens.map H.hom).obj U✝)).unop)) }).unop)) })) ≫
        NatTrans.app α.hom (op ((Opens.map H.inv).obj ((Opens.map H.hom).obj U✝))) ≫
          Y.presheaf.map
            (eqToHom (_ : (Opens.map (H.inv ≫ H.hom)).op.obj (op U✝) = (Opens.map (𝟙 ↑Y)).op.obj (op U✝))) =
    𝟙 (Y.presheaf.obj (op U✝))
[PROOFSTEP]
rw [← α.hom.naturality, Presheaf.pushforwardObj_map, eqToHom_map, eqToHom_map, eqToHom_map, eqToHom_trans_assoc,
  eqToHom_refl, id_comp]
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.204326, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : H.hom _* X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ NatTrans.app α.inv (op U✝) ≫ NatTrans.app α.hom (op ((Opens.map (𝟙 ↑Y)).obj U✝)) = 𝟙 (Y.presheaf.obj (op U✝))
[PROOFSTEP]
apply Iso.inv_hom_id_app
[GOAL]
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
⊢ H.hom.c ≫ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c = 𝟙 Y.presheaf
[PROOFSTEP]
ext U
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ NatTrans.app (H.hom.c ≫ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c) (op U) =
    NatTrans.app (𝟙 Y.presheaf) (op U)
[PROOFSTEP]
rw [NatTrans.comp_app]
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ NatTrans.app H.hom.c (op U) ≫ NatTrans.app (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c) (op U) =
    NatTrans.app (𝟙 Y.presheaf) (op U)
[PROOFSTEP]
simpa using congr_arg (fun f => f ≫ eqToHom _) (congr_app H.inv_hom_id (op U))
[GOAL]
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
⊢ Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c ≫ H.hom.c = 𝟙 (H.hom.base _* X.presheaf)
[PROOFSTEP]
ext U
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ NatTrans.app (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c ≫ H.hom.c) (op U) =
    NatTrans.app (𝟙 (H.hom.base _* X.presheaf)) (op U)
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ NatTrans.app (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c ≫ H.hom.c) (op U) =
    NatTrans.app (𝟙 (H.hom.base _* X.presheaf)) (op U)
[PROOFSTEP]
rw [NatTrans.comp_app, NatTrans.id_app]
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ NatTrans.app (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c) (op U) ≫ NatTrans.app H.hom.c (op U) =
    𝟙 ((H.hom.base _* X.presheaf).obj (op U))
[PROOFSTEP]
simp only [Presheaf.pushforwardObj_obj, op_obj, Presheaf.pushforwardToOfIso_app, Iso.symm_inv, mapIso_hom, forget_map,
  Iso.symm_hom, mapIso_inv, unop_op, eqToHom_map, assoc]
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ NatTrans.app H.inv.c (op ((Opens.map H.hom.base).obj U)) ≫
      eqToHom
          (_ :
            Y.presheaf.obj (op ((Opens.map H.inv.base).obj ((Opens.map H.hom.base).obj U))) = Y.presheaf.obj (op U)) ≫
        NatTrans.app H.hom.c (op U) =
    𝟙 (X.presheaf.obj (op ((Opens.map H.hom.base).obj U)))
[PROOFSTEP]
have eq₁ := congr_app H.hom_inv_id (op ((Opens.map H.hom.base).obj U))
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  NatTrans.app (H.hom ≫ H.inv).c (op ((Opens.map H.hom.base).obj U)) =
    NatTrans.app (𝟙 X).c (op ((Opens.map H.hom.base).obj U)) ≫
      X.presheaf.map
        (eqToHom
          (_ :
            (Opens.map (𝟙 X).base).op.obj (op ((Opens.map H.hom.base).obj U)) =
              (Opens.map (H.hom ≫ H.inv).base).op.obj (op ((Opens.map H.hom.base).obj U))))
⊢ NatTrans.app H.inv.c (op ((Opens.map H.hom.base).obj U)) ≫
      eqToHom
          (_ :
            Y.presheaf.obj (op ((Opens.map H.inv.base).obj ((Opens.map H.hom.base).obj U))) = Y.presheaf.obj (op U)) ≫
        NatTrans.app H.hom.c (op U) =
    𝟙 (X.presheaf.obj (op ((Opens.map H.hom.base).obj U)))
[PROOFSTEP]
have eq₂ := H.hom.c.naturality (eqToHom (congr_obj (congr_arg Opens.map ((forget C).congr_map H.inv_hom_id.symm)) U)).op
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  NatTrans.app (H.hom ≫ H.inv).c (op ((Opens.map H.hom.base).obj U)) =
    NatTrans.app (𝟙 X).c (op ((Opens.map H.hom.base).obj U)) ≫
      X.presheaf.map
        (eqToHom
          (_ :
            (Opens.map (𝟙 X).base).op.obj (op ((Opens.map H.hom.base).obj U)) =
              (Opens.map (H.hom ≫ H.inv).base).op.obj (op ((Opens.map H.hom.base).obj U))))
eq₂ :
  Y.presheaf.map
        (eqToHom
            (_ : (Opens.map ((forget C).map (𝟙 Y))).obj U = (Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)).op ≫
      NatTrans.app H.hom.c (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    NatTrans.app H.hom.c (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      (H.hom.base _* X.presheaf).map
        (eqToHom (_ : (Opens.map ((forget C).map (𝟙 Y))).obj U = (Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)).op
⊢ NatTrans.app H.inv.c (op ((Opens.map H.hom.base).obj U)) ≫
      eqToHom
          (_ :
            Y.presheaf.obj (op ((Opens.map H.inv.base).obj ((Opens.map H.hom.base).obj U))) = Y.presheaf.obj (op U)) ≫
        NatTrans.app H.hom.c (op U) =
    𝟙 (X.presheaf.obj (op ((Opens.map H.hom.base).obj U)))
[PROOFSTEP]
rw [id_c, NatTrans.id_app, id_comp, eqToHom_map, comp_c_app] at eq₁
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  NatTrans.app H.inv.c (op ((Opens.map H.hom.base).obj U)) ≫
      NatTrans.app H.hom.c (op ((Opens.map H.inv.base).obj (op ((Opens.map H.hom.base).obj U)).unop)) =
    eqToHom
      (_ :
        X.presheaf.obj ((Opens.map (𝟙 X).base).op.obj (op ((Opens.map H.hom.base).obj U))) =
          X.presheaf.obj ((Opens.map (H.hom ≫ H.inv).base).op.obj (op ((Opens.map H.hom.base).obj U))))
eq₂ :
  Y.presheaf.map
        (eqToHom
            (_ : (Opens.map ((forget C).map (𝟙 Y))).obj U = (Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)).op ≫
      NatTrans.app H.hom.c (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    NatTrans.app H.hom.c (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      (H.hom.base _* X.presheaf).map
        (eqToHom (_ : (Opens.map ((forget C).map (𝟙 Y))).obj U = (Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)).op
⊢ NatTrans.app H.inv.c (op ((Opens.map H.hom.base).obj U)) ≫
      eqToHom
          (_ :
            Y.presheaf.obj (op ((Opens.map H.inv.base).obj ((Opens.map H.hom.base).obj U))) = Y.presheaf.obj (op U)) ≫
        NatTrans.app H.hom.c (op U) =
    𝟙 (X.presheaf.obj (op ((Opens.map H.hom.base).obj U)))
[PROOFSTEP]
rw [eqToHom_op, eqToHom_map] at eq₂
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  NatTrans.app H.inv.c (op ((Opens.map H.hom.base).obj U)) ≫
      NatTrans.app H.hom.c (op ((Opens.map H.inv.base).obj (op ((Opens.map H.hom.base).obj U)).unop)) =
    eqToHom
      (_ :
        X.presheaf.obj ((Opens.map (𝟙 X).base).op.obj (op ((Opens.map H.hom.base).obj U))) =
          X.presheaf.obj ((Opens.map (H.hom ≫ H.inv).base).op.obj (op ((Opens.map H.hom.base).obj U))))
eq₂ :
  eqToHom
        (_ :
          Y.presheaf.obj (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) =
            Y.presheaf.obj (op ((Opens.map ((forget C).map (𝟙 Y))).obj U))) ≫
      NatTrans.app H.hom.c (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    NatTrans.app H.hom.c (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      (H.hom.base _* X.presheaf).map
        (eqToHom
          (_ : op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U) = op ((Opens.map ((forget C).map (𝟙 Y))).obj U)))
⊢ NatTrans.app H.inv.c (op ((Opens.map H.hom.base).obj U)) ≫
      eqToHom
          (_ :
            Y.presheaf.obj (op ((Opens.map H.inv.base).obj ((Opens.map H.hom.base).obj U))) = Y.presheaf.obj (op U)) ≫
        NatTrans.app H.hom.c (op U) =
    𝟙 (X.presheaf.obj (op ((Opens.map H.hom.base).obj U)))
[PROOFSTEP]
erw [eq₂, reassoc_of% eq₁]
[GOAL]
case w
C : Type u_1
inst✝ : Category.{?u.217173, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
eq₁ :
  NatTrans.app H.inv.c (op ((Opens.map H.hom.base).obj U)) ≫
      NatTrans.app H.hom.c (op ((Opens.map H.inv.base).obj (op ((Opens.map H.hom.base).obj U)).unop)) =
    eqToHom
      (_ :
        X.presheaf.obj ((Opens.map (𝟙 X).base).op.obj (op ((Opens.map H.hom.base).obj U))) =
          X.presheaf.obj ((Opens.map (H.hom ≫ H.inv).base).op.obj (op ((Opens.map H.hom.base).obj U))))
eq₂ :
  eqToHom
        (_ :
          Y.presheaf.obj (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) =
            Y.presheaf.obj (op ((Opens.map ((forget C).map (𝟙 Y))).obj U))) ≫
      NatTrans.app H.hom.c (op ((Opens.map ((forget C).map (𝟙 Y))).obj U)) =
    NatTrans.app H.hom.c (op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U)) ≫
      (H.hom.base _* X.presheaf).map
        (eqToHom
          (_ : op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U) = op ((Opens.map ((forget C).map (𝟙 Y))).obj U)))
⊢ eqToHom
        (_ :
          X.presheaf.obj ((Opens.map (𝟙 X).base).op.obj (op ((Opens.map H.hom.base).obj U))) =
            X.presheaf.obj ((Opens.map (H.hom ≫ H.inv).base).op.obj (op ((Opens.map H.hom.base).obj U)))) ≫
      (H.hom.base _* X.presheaf).map
        (eqToHom
          (_ :
            op ((Opens.map ((forget C).map (H.inv ≫ H.hom))).obj U) = op ((Opens.map ((forget C).map (𝟙 Y))).obj U))) =
    𝟙 (X.presheaf.obj (op ((Opens.map H.hom.base).obj U)))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.242573, u_1} C
U✝ : TopCat
X : PresheafedSpace C
f✝ : U✝ ⟶ ↑X
h : OpenEmbedding ↑f✝
U V : (Opens ↑↑X)ᵒᵖ
f : U ⟶ V
⊢ X.presheaf.map f ≫
      (fun V => X.presheaf.map (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f✝)).counit V.unop).op) V =
    (fun V => X.presheaf.map (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f✝)).counit V.unop).op) U ≫
      X.presheaf.map ((IsOpenMap.functor (_ : IsOpenMap ↑f✝)).op.map ((Opens.map f✝).op.map f))
[PROOFSTEP]
rw [← map_comp, ← map_comp]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.242573, u_1} C
U✝ : TopCat
X : PresheafedSpace C
f✝ : U✝ ⟶ ↑X
h : OpenEmbedding ↑f✝
U V : (Opens ↑↑X)ᵒᵖ
f : U ⟶ V
⊢ X.presheaf.map (f ≫ (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f✝)).counit V.unop).op) =
    X.presheaf.map
      ((NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f✝)).counit U.unop).op ≫
        (IsOpenMap.functor (_ : IsOpenMap ↑f✝)).op.map ((Opens.map f✝).op.map f))
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
⊢ Mono (ofRestrict X hf)
[PROOFSTEP]
haveI : Mono f := (TopCat.mono_iff_injective _).mpr hf.inj
[GOAL]
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this : Mono f
⊢ Mono (ofRestrict X hf)
[PROOFSTEP]
constructor
[GOAL]
case right_cancellation
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this : Mono f
⊢ ∀ {Z : PresheafedSpace C} (g h : Z ⟶ restrict X hf), g ≫ ofRestrict X hf = h ≫ ofRestrict X hf → g = h
[PROOFSTEP]
intro Z g₁ g₂ eq
[GOAL]
case right_cancellation
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
⊢ g₁ = g₂
[PROOFSTEP]
ext1
[GOAL]
case right_cancellation.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
⊢ g₁.base = g₂.base
[PROOFSTEP]
have := congr_arg PresheafedSpace.Hom.base eq
[GOAL]
case right_cancellation.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
this : (g₁ ≫ ofRestrict X hf).base = (g₂ ≫ ofRestrict X hf).base
⊢ g₁.base = g₂.base
[PROOFSTEP]
simp only [PresheafedSpace.comp_base, PresheafedSpace.ofRestrict_base] at this
[GOAL]
case right_cancellation.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
this : g₁.base ≫ f = g₂.base ≫ f
⊢ g₁.base = g₂.base
[PROOFSTEP]
rw [cancel_mono] at this
[GOAL]
case right_cancellation.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
this : g₁.base = g₂.base
⊢ g₁.base = g₂.base
[PROOFSTEP]
exact this
[GOAL]
case right_cancellation.h
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
⊢ g₁.c ≫ whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf = g₂.c
[PROOFSTEP]
ext V
[GOAL]
case right_cancellation.h.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
⊢ NatTrans.app (g₁.c ≫ whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf) (op V) =
    NatTrans.app g₂.c (op V)
[PROOFSTEP]
have hV : (Opens.map (X.ofRestrict hf).base).obj (hf.isOpenMap.functor.obj V) = V :=
  by
  ext1
  exact Set.preimage_image_eq _ hf.inj
[GOAL]
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
⊢ (Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) = V
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
⊢ ↑((Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) = ↑V
[PROOFSTEP]
exact Set.preimage_image_eq _ hf.inj
[GOAL]
case right_cancellation.h.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
hV : (Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) = V
⊢ NatTrans.app (g₁.c ≫ whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf) (op V) =
    NatTrans.app g₂.c (op V)
[PROOFSTEP]
haveI : IsIso (hf.isOpenMap.adjunction.counit.app (unop (op (hf.isOpenMap.functor.obj V)))) :=
  NatIso.isIso_app_of_isIso (whiskerLeft hf.isOpenMap.functor hf.isOpenMap.adjunction.counit) V
[GOAL]
case right_cancellation.h.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
hV : (Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) = V
this :
  IsIso
    (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit
      (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)
⊢ NatTrans.app (g₁.c ≫ whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf) (op V) =
    NatTrans.app g₂.c (op V)
[PROOFSTEP]
have := PresheafedSpace.congr_app eq (op (hf.isOpenMap.functor.obj V))
[GOAL]
case right_cancellation.h.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
hV : (Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) = V
this✝ :
  IsIso
    (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit
      (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)
this :
  NatTrans.app (g₁ ≫ ofRestrict X hf).c (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) =
    NatTrans.app (g₂ ≫ ofRestrict X hf).c (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) ≫
      Z.presheaf.map
        (eqToHom
          (_ :
            (Opens.map (g₂ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) =
              (Opens.map (g₁ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V))))
⊢ NatTrans.app (g₁.c ≫ whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf) (op V) =
    NatTrans.app g₂.c (op V)
[PROOFSTEP]
simp only [PresheafedSpace.comp_c_app, PresheafedSpace.ofRestrict_c_app, Category.assoc, cancel_epi] at this
[GOAL]
case right_cancellation.h.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
hV : (Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) = V
this✝ :
  IsIso
    (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit
      (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)
this :
  NatTrans.app g₁.c
      (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) =
    NatTrans.app g₂.c
        (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) ≫
      Z.presheaf.map
        (eqToHom
          (_ :
            (Opens.map (g₂ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) =
              (Opens.map (g₁ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V))))
⊢ NatTrans.app (g₁.c ≫ whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf) (op V) =
    NatTrans.app g₂.c (op V)
[PROOFSTEP]
have h : _ ≫ _ = _ ≫ _ ≫ _ := congr_arg (fun f => (X.restrict hf).presheaf.map (eqToHom hV).op ≫ f) this
[GOAL]
case right_cancellation.h.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
hV : (Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) = V
this✝ :
  IsIso
    (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit
      (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)
this :
  NatTrans.app g₁.c
      (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) =
    NatTrans.app g₂.c
        (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) ≫
      Z.presheaf.map
        (eqToHom
          (_ :
            (Opens.map (g₂ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) =
              (Opens.map (g₁ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V))))
h :
  (restrict X hf).presheaf.map (eqToHom hV).op ≫
      NatTrans.app g₁.c
        (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) =
    (restrict X hf).presheaf.map (eqToHom hV).op ≫
      NatTrans.app g₂.c
          (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) ≫
        Z.presheaf.map
          (eqToHom
            (_ :
              (Opens.map (g₂ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) =
                (Opens.map (g₁ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V))))
⊢ NatTrans.app (g₁.c ≫ whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf) (op V) =
    NatTrans.app g₂.c (op V)
[PROOFSTEP]
erw [g₁.c.naturality, g₂.c.naturality_assoc] at h
[GOAL]
case right_cancellation.h.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
hV : (Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) = V
this✝ :
  IsIso
    (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit
      (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)
this :
  NatTrans.app g₁.c
      (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) =
    NatTrans.app g₂.c
        (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) ≫
      Z.presheaf.map
        (eqToHom
          (_ :
            (Opens.map (g₂ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) =
              (Opens.map (g₁ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V))))
h :
  NatTrans.app g₁.c (op V) ≫ (g₁.base _* Z.presheaf).map (eqToHom hV).op =
    NatTrans.app g₂.c (op V) ≫
      (g₂.base _* Z.presheaf).map (eqToHom hV).op ≫
        Z.presheaf.map
          (eqToHom
            (_ :
              (Opens.map (g₂ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) =
                (Opens.map (g₁ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V))))
⊢ NatTrans.app (g₁.c ≫ whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf) (op V) =
    NatTrans.app g₂.c (op V)
[PROOFSTEP]
simp only [Presheaf.pushforwardObj_map, eqToHom_op, Category.assoc, eqToHom_map, eqToHom_trans] at h
[GOAL]
case right_cancellation.h.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
hV : (Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) = V
this✝ :
  IsIso
    (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit
      (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)
this :
  NatTrans.app g₁.c
      (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) =
    NatTrans.app g₂.c
        (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) ≫
      Z.presheaf.map
        (eqToHom
          (_ :
            (Opens.map (g₂ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) =
              (Opens.map (g₁ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V))))
h :
  NatTrans.app g₁.c (op V) ≫
      eqToHom
        (_ :
          Z.presheaf.obj ((Opens.map g₁.base).op.obj (op V)) =
            Z.presheaf.obj
              ((Opens.map g₁.base).op.obj
                (op ((Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V))))) =
    NatTrans.app g₂.c (op V) ≫
      eqToHom
        (_ :
          (g₂.base _* Z.presheaf).obj (op V) =
            (g₁.base _* Z.presheaf).obj
              (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)))
⊢ NatTrans.app (g₁.c ≫ whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf) (op V) =
    NatTrans.app g₂.c (op V)
[PROOFSTEP]
rw [← IsIso.comp_inv_eq, inv_eqToHom, Category.assoc, eqToHom_trans] at h
[GOAL]
case right_cancellation.h.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
hV : (Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) = V
this✝ :
  IsIso
    (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit
      (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)
this :
  NatTrans.app g₁.c
      (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) =
    NatTrans.app g₂.c
        (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) ≫
      Z.presheaf.map
        (eqToHom
          (_ :
            (Opens.map (g₂ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) =
              (Opens.map (g₁ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V))))
h :
  NatTrans.app g₁.c (op V) ≫ eqToHom (_ : (g₁.base _* Z.presheaf).obj (op V) = (g₂.base _* Z.presheaf).obj (op V)) =
    NatTrans.app g₂.c (op V)
⊢ NatTrans.app (g₁.c ≫ whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf) (op V) =
    NatTrans.app g₂.c (op V)
[PROOFSTEP]
rw [NatTrans.comp_app]
[GOAL]
case right_cancellation.h.w
C : Type u_1
inst✝ : Category.{?u.247153, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : OpenEmbedding ↑f
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ restrict X hf
eq : g₁ ≫ ofRestrict X hf = g₂ ≫ ofRestrict X hf
V : Opens ↑↑(restrict X hf)
hV : (Opens.map (ofRestrict X hf).base).obj ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V) = V
this✝ :
  IsIso
    (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑f)).counit
      (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)
this :
  NatTrans.app g₁.c
      (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) =
    NatTrans.app g₂.c
        (op ((Opens.map (ofRestrict X hf).base).obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)).unop)) ≫
      Z.presheaf.map
        (eqToHom
          (_ :
            (Opens.map (g₂ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V)) =
              (Opens.map (g₁ ≫ ofRestrict X hf).base).op.obj (op ((IsOpenMap.functor (_ : IsOpenMap ↑f)).obj V))))
h :
  NatTrans.app g₁.c (op V) ≫ eqToHom (_ : (g₁.base _* Z.presheaf).obj (op V) = (g₂.base _* Z.presheaf).obj (op V)) =
    NatTrans.app g₂.c (op V)
⊢ NatTrans.app g₁.c (op V) ≫
      NatTrans.app (whiskerRight (eqToHom (_ : (Opens.map g₁.base).op = (Opens.map g₂.base).op)) Z.presheaf) (op V) =
    NatTrans.app g₂.c (op V)
[PROOFSTEP]
simpa using h
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
⊢ (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).presheaf = (Opens.inclusionTopIso ↑X).inv _* X.presheaf
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
⊢ (IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion ⊤))).op ⋙ X.presheaf =
    (Opens.inclusionTopIso ↑X).inv _* X.presheaf
[PROOFSTEP]
rw [Opens.inclusion_top_functor X.carrier]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
⊢ (Opens.map (Opens.inclusionTopIso ↑X).inv).op ⋙ X.presheaf = (Opens.inclusionTopIso ↑X).inv _* X.presheaf
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.265841, u_1} C
X : PresheafedSpace C
⊢ X.presheaf =
    (ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).base _*
      (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).presheaf
[PROOFSTEP]
rw [restrict_top_presheaf, ← Presheaf.Pushforward.comp_eq]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.265841, u_1} C
X : PresheafedSpace C
⊢ X.presheaf =
    ((Opens.inclusionTopIso ↑X).inv ≫ (ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).base) _* X.presheaf
[PROOFSTEP]
erw [Iso.inv_hom_id]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.265841, u_1} C
X : PresheafedSpace C
⊢ X.presheaf = 𝟙 ↑X _* X.presheaf
[PROOFSTEP]
rw [Presheaf.Pushforward.id_eq]
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
⊢ (ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).c =
    eqToHom
      (_ :
        X.presheaf =
          (ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).base _*
            (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).presheaf)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ NatTrans.app (ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).c (op U✝) =
    NatTrans.app
      (eqToHom
        (_ :
          X.presheaf =
            (ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).base _*
              (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).presheaf))
      (op U✝)
[PROOFSTEP]
dsimp [ofRestrict]
[GOAL]
case w
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ X.presheaf.map (NatTrans.app (IsOpenMap.adjunction (_ : IsOpenMap ↑(Opens.inclusion ⊤))).counit U✝).op =
    NatTrans.app
      (eqToHom
        (_ :
          X.presheaf = Opens.inclusion ⊤ _* ((IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion ⊤))).op ⋙ X.presheaf)))
      (op U✝)
[PROOFSTEP]
erw [eqToHom_map, eqToHom_app]
[GOAL]
case w.p
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ op U✝ = op ((IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion ⊤))).obj ((Opens.map (Opens.inclusion ⊤)).obj U✝))
case w.p
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ op U✝ = op ((IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion ⊤))).obj ((Opens.map (Opens.inclusion ⊤)).obj U✝))
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝ : Category.{?u.273541, u_1} C
X : PresheafedSpace C
⊢ ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)) ≫ toRestrictTop X =
    𝟙 (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)))
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝ : Category.{?u.273541, u_1} C
X : PresheafedSpace C
x✝ : (CategoryTheory.forget TopCat).obj ↑(restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)))
⊢ ↑(ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)) ≫ toRestrictTop X).base x✝ =
    ↑(𝟙 (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)))).base x✝
[PROOFSTEP]
rfl
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.273541, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)))
⊢ NatTrans.app
      ((ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)) ≫ toRestrictTop X).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map (ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)) ≫ toRestrictTop X).base).op =
                (Opens.map (𝟙 (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)))).base).op))
          (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).presheaf)
      (op U✝) =
    NatTrans.app (𝟙 (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)))).c (op U✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.273541, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)))
⊢ NatTrans.app
      ((ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)) ≫ toRestrictTop X).c ≫
        whiskerRight (𝟙 (Opens.map (Opens.inclusion ⊤ ≫ (Opens.inclusionTopIso ↑X).inv)).op)
          ((IsOpenMap.functor (_ : IsOpenMap ↑(Opens.inclusion ⊤))).op ⋙ X.presheaf))
      (op U✝) =
    NatTrans.app (𝟙 (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)))).c (op U✝)
[PROOFSTEP]
erw [comp_c, toRestrictTop_c, whiskerRight_id', comp_id, ofRestrict_top_c, eqToHom_map, eqToHom_trans, eqToHom_refl]
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.273541, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)))
⊢ NatTrans.app (𝟙 (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).presheaf) (op U✝) =
    NatTrans.app (𝟙 (restrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)))).c (op U✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.273541, u_1} C
X : PresheafedSpace C
⊢ toRestrictTop X ≫ ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤)) = 𝟙 X
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝ : Category.{?u.273541, u_1} C
X : PresheafedSpace C
x✝ : (CategoryTheory.forget TopCat).obj ↑X
⊢ ↑(toRestrictTop X ≫ ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).base x✝ = ↑(𝟙 X).base x✝
[PROOFSTEP]
rfl
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.273541, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ NatTrans.app
      ((toRestrictTop X ≫ ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map (toRestrictTop X ≫ ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).base).op =
                (Opens.map (𝟙 X).base).op))
          X.presheaf)
      (op U✝) =
    NatTrans.app (𝟙 X).c (op U✝)
[PROOFSTEP]
dsimp
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.273541, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ NatTrans.app
      ((toRestrictTop X ≫ ofRestrict X (_ : OpenEmbedding ↑(Opens.inclusion ⊤))).c ≫
        whiskerRight (𝟙 (Opens.map ((Opens.inclusionTopIso ↑X).inv ≫ Opens.inclusion ⊤)).op) X.presheaf)
      (op U✝) =
    NatTrans.app (𝟙 X).c (op U✝)
[PROOFSTEP]
erw [comp_c, ofRestrict_top_c, toRestrictTop_c, eqToHom_map, whiskerRight_id', comp_id, eqToHom_trans, eqToHom_refl]
[GOAL]
case h.w
C : Type u_1
inst✝ : Category.{?u.273541, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ NatTrans.app (𝟙 X.presheaf) (op U✝) = NatTrans.app (𝟙 X).c (op U✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.293007, u_1} C
D : Type u_2
inst✝ : Category.{?u.293014, u_2} D
F : C ⥤ D
X : PresheafedSpace C
⊢ { obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
          map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
      (𝟙 X) =
    𝟙
      ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
            map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
        X)
[PROOFSTEP]
ext U
[GOAL]
case w.w
C : Type u_1
inst✝¹ : Category.{?u.293007, u_1} C
D : Type u_2
inst✝ : Category.{?u.293014, u_2} D
F : C ⥤ D
X : PresheafedSpace C
U :
  (forget TopCat).obj
    ↑({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
            map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
        X)
⊢ ↑({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
            (𝟙 X)).base
      U =
    ↑(𝟙
            ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                  map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
              X)).base
      U
case h.w
C : Type u_1
inst✝¹ : Category.{?u.293007, u_1} C
D : Type u_2
inst✝ : Category.{?u.293014, u_2} D
F : C ⥤ D
X : PresheafedSpace C
U :
  Opens
    ↑↑({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
              map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
          X)
⊢ NatTrans.app
      (({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
            (𝟙 X)).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                            map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
                        (𝟙 X)).base).op =
                (Opens.map
                    (𝟙
                        ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                              map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
                          X)).base).op))
          ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                  map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
              X).presheaf)
      (op U) =
    NatTrans.app
      (𝟙
          ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
            X)).c
      (op U)
[PROOFSTEP]
rfl
[GOAL]
case h.w
C : Type u_1
inst✝¹ : Category.{?u.293007, u_1} C
D : Type u_2
inst✝ : Category.{?u.293014, u_2} D
F : C ⥤ D
X : PresheafedSpace C
U :
  Opens
    ↑↑({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
              map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
          X)
⊢ NatTrans.app
      (({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
            (𝟙 X)).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                            map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
                        (𝟙 X)).base).op =
                (Opens.map
                    (𝟙
                        ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                              map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
                          X)).base).op))
          ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                  map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
              X).presheaf)
      (op U) =
    NatTrans.app
      (𝟙
          ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
            X)).c
      (op U)
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.293007, u_1} C
D : Type u_2
inst✝ : Category.{?u.293014, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
          map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
      (f ≫ g) =
    { obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
            map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
        f ≫
      { obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
            map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
        g
[PROOFSTEP]
ext U
[GOAL]
case w.w
C : Type u_1
inst✝¹ : Category.{?u.293007, u_1} C
D : Type u_2
inst✝ : Category.{?u.293014, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
U :
  (forget TopCat).obj
    ↑({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
            map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
        X✝)
⊢ ↑({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
            (f ≫ g)).base
      U =
    ↑({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                  map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
              f ≫
            { obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                  map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
              g).base
      U
case h.w
C : Type u_1
inst✝¹ : Category.{?u.293007, u_1} C
D : Type u_2
inst✝ : Category.{?u.293014, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
U :
  Opens
    ↑↑({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
              map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
          Z✝)
⊢ NatTrans.app
      (({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
            (f ≫ g)).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                            map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
                        (f ≫ g)).base).op =
                (Opens.map
                    ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                              map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
                          f ≫
                        { obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                              map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
                          g).base).op))
          ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                  map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
              X✝).presheaf)
      (op U) =
    NatTrans.app
      ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
            f ≫
          { obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
            g).c
      (op U)
[PROOFSTEP]
rfl
[GOAL]
case h.w
C : Type u_1
inst✝¹ : Category.{?u.293007, u_1} C
D : Type u_2
inst✝ : Category.{?u.293014, u_2} D
F : C ⥤ D
X✝ Y✝ Z✝ : PresheafedSpace C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
U :
  Opens
    ↑↑({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
              map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
          Z✝)
⊢ NatTrans.app
      (({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
            (f ≫ g)).c ≫
        whiskerRight
          (eqToHom
            (_ :
              (Opens.map
                    ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                            map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
                        (f ≫ g)).base).op =
                (Opens.map
                    ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                              map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
                          f ≫
                        { obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                              map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
                          g).base).op))
          ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                  map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.obj
              X✝).presheaf)
      (op U) =
    NatTrans.app
      ({ obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
            f ≫
          { obj := fun X => { carrier := ↑X, presheaf := X.presheaf ⋙ F },
                map := fun {X Y} f => { base := f.base, c := whiskerRight f.c F } }.map
            g).c
      (op U)
[PROOFSTEP]
simp


[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
F G : L →ᴸ L'
h_fun : F.onFunction = G.onFunction
h_rel : F.onRelation = G.onRelation
⊢ F = G
[PROOFSTEP]
cases' F with Ff Fr
[GOAL]
case mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
G : L →ᴸ L'
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = G.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = G.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = G
[PROOFSTEP]
cases' G with Gf Gr
[GOAL]
case mk.mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
Gf : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Gr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = { onFunction := Gf, onRelation := Gr }
[PROOFSTEP]
simp only [mk.injEq]
[GOAL]
case mk.mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
Gf : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Gr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ Ff = Gf ∧ Fr = Gr
[PROOFSTEP]
exact And.intro h_fun h_rel
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
F : L →ᴸ L'
⊢ LHom.id L' ∘ᴸ F = F
[PROOFSTEP]
cases F
[GOAL]
case mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
onFunction✝ : ⦃n : ℕ⦄ → Functions L n → Functions L' n
onRelation✝ : ⦃n : ℕ⦄ → Relations L n → Relations L' n
⊢ LHom.id L' ∘ᴸ { onFunction := onFunction✝, onRelation := onRelation✝ } =
    { onFunction := onFunction✝, onRelation := onRelation✝ }
[PROOFSTEP]
rfl
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
F : L →ᴸ L'
⊢ F ∘ᴸ LHom.id L = F
[PROOFSTEP]
cases F
[GOAL]
case mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
onFunction✝ : ⦃n : ℕ⦄ → Functions L n → Functions L' n
onRelation✝ : ⦃n : ℕ⦄ → Relations L n → Relations L' n
⊢ { onFunction := onFunction✝, onRelation := onRelation✝ } ∘ᴸ LHom.id L =
    { onFunction := onFunction✝, onRelation := onRelation✝ }
[PROOFSTEP]
rfl
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁵ : Structure L M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : Structure L M
inst✝³ : Structure L' M
inst✝² : Structure L'' M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
f : Functions (Language.sum L L'') n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Functions L n✝), funMap (onFunction (LHom.sumElim ϕ ψ) (Sum.inl val)) x✝ = funMap (Sum.inl val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁵ : Structure L M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : Structure L M
inst✝³ : Structure L' M
inst✝² : Structure L'' M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
f : Functions (Language.sum L L'') n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Functions L'' n✝), funMap (onFunction (LHom.sumElim ϕ ψ) (Sum.inr val)) x✝ = funMap (Sum.inr val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁵ : Structure L M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : Structure L M
inst✝³ : Structure L' M
inst✝² : Structure L'' M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
R : Relations (Language.sum L L'') n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Relations L n✝), RelMap (onRelation (LHom.sumElim ϕ ψ) (Sum.inl val)) x✝ = RelMap (Sum.inl val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁵ : Structure L M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : Structure L M
inst✝³ : Structure L' M
inst✝² : Structure L'' M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
R : Relations (Language.sum L L'') n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Relations L'' n✝), RelMap (onRelation (LHom.sumElim ϕ ψ) (Sum.inr val)) x✝ = RelMap (Sum.inr val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁶ : Structure L M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : Structure L M
inst✝⁴ : Structure L' M
inst✝³ : Structure L₁ M
inst✝² : Structure L₂ M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
f : Functions (Language.sum L L₁) n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Functions L n✝), funMap (onFunction (sumMap ϕ ψ) (Sum.inl val)) x✝ = funMap (Sum.inl val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁶ : Structure L M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : Structure L M
inst✝⁴ : Structure L' M
inst✝³ : Structure L₁ M
inst✝² : Structure L₂ M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
f : Functions (Language.sum L L₁) n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Functions L₁ n✝), funMap (onFunction (sumMap ϕ ψ) (Sum.inr val)) x✝ = funMap (Sum.inr val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁶ : Structure L M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : Structure L M
inst✝⁴ : Structure L' M
inst✝³ : Structure L₁ M
inst✝² : Structure L₂ M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
R : Relations (Language.sum L L₁) n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Relations L n✝), RelMap (onRelation (sumMap ϕ ψ) (Sum.inl val)) x✝ = RelMap (Sum.inl val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁶ : Structure L M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : Structure L M
inst✝⁴ : Structure L' M
inst✝³ : Structure L₁ M
inst✝² : Structure L₂ M
inst✝¹ : IsExpansionOn ϕ M
inst✝ : IsExpansionOn ψ M
n✝ : ℕ
R : Relations (Language.sum L L₁) n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : Relations L₁ n✝), RelMap (onRelation (sumMap ϕ ψ) (Sum.inr val)) x✝ = RelMap (Sum.inr val) x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
⊢ IsExpansionOn ϕ M
[PROOFSTEP]
letI := ϕ.defaultExpansion M
[GOAL]
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
⊢ IsExpansionOn ϕ M
[PROOFSTEP]
refine' ⟨fun {n} f xs => _, fun {n} r xs => _⟩
[GOAL]
case refine'_1
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
f : Functions L n
xs : Fin n → M
⊢ funMap (LHom.onFunction ϕ f) xs = funMap f xs
[PROOFSTEP]
have hf : ϕ.onFunction f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f := ⟨f, rfl⟩
[GOAL]
case refine'_1
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
f : Functions L n
xs : Fin n → M
hf : LHom.onFunction ϕ f ∈ Set.range fun f => LHom.onFunction ϕ f
⊢ funMap (LHom.onFunction ϕ f) xs = funMap f xs
[PROOFSTEP]
refine' (dif_pos hf).trans _
[GOAL]
case refine'_1
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
f : Functions L n
xs : Fin n → M
hf : LHom.onFunction ϕ f ∈ Set.range fun f => LHom.onFunction ϕ f
⊢ funMap (Exists.choose hf) xs = funMap f xs
[PROOFSTEP]
rw [h.onFunction hf.choose_spec]
[GOAL]
case refine'_2
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
r : Relations L n
xs : Fin n → M
⊢ RelMap (LHom.onRelation ϕ r) xs = RelMap r xs
[PROOFSTEP]
have hr : ϕ.onRelation r ∈ Set.range fun r : L.Relations n => ϕ.onRelation r := ⟨r, rfl⟩
[GOAL]
case refine'_2
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
r : Relations L n
xs : Fin n → M
hr : LHom.onRelation ϕ r ∈ Set.range fun r => LHom.onRelation ϕ r
⊢ RelMap (LHom.onRelation ϕ r) xs = RelMap r xs
[PROOFSTEP]
refine' (dif_pos hr).trans _
[GOAL]
case refine'_2
L : Language
L' : Language
M✝ : Type w
inst✝⁴ : Structure L M✝
ϕ✝ : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : Functions L' n) → Decidable (f ∈ Set.range fun f => LHom.onFunction ϕ f)
inst✝² : (n : ℕ) → (r : Relations L' n) → Decidable (r ∈ Set.range fun r => LHom.onRelation ϕ r)
h : LHom.Injective ϕ
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : Structure L M
this : Structure L' M := defaultExpansion ϕ M
n : ℕ
r : Relations L n
xs : Fin n → M
hr : LHom.onRelation ϕ r ∈ Set.range fun r => LHom.onRelation ϕ r
⊢ RelMap (Exists.choose hr) xs = RelMap r xs
[PROOFSTEP]
rw [h.onRelation hr.choose_spec]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ LHom.comp (LHom.comp e.invLHom e'.invLHom) (LHom.comp e'.toLHom e.toLHom) = LHom.id L
[PROOFSTEP]
rw [LHom.comp_assoc, ← LHom.comp_assoc e'.invLHom, e'.left_inv, LHom.id_comp, e.left_inv]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ LHom.comp (LHom.comp e'.toLHom e.toLHom) (LHom.comp e.invLHom e'.invLHom) = LHom.id L''
[PROOFSTEP]
rw [LHom.comp_assoc, ← LHom.comp_assoc e.toLHom, e.right_inv, LHom.id_comp, e'.right_inv]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type u'
⊢ card (constantsOn α) = #α
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
⊢ LHom.IsExpansionOn (LHom.constantsOnMap f) M
[PROOFSTEP]
letI := constantsOn.structure fα
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this : Structure (constantsOn α) M := constantsOn.structure fα
⊢ LHom.IsExpansionOn (LHom.constantsOnMap f) M
[PROOFSTEP]
letI := constantsOn.structure fβ
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this✝ : Structure (constantsOn α) M := constantsOn.structure fα
this : Structure (constantsOn β) M := constantsOn.structure fβ
⊢ LHom.IsExpansionOn (LHom.constantsOnMap f) M
[PROOFSTEP]
exact ⟨fun {n} => Nat.casesOn n (fun F _x => (congr_fun h F : _)) fun n F => isEmptyElim F, fun R => isEmptyElim R⟩
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
⊢ card (L[[α]]) = lift (card L) + lift #α
[PROOFSTEP]
rw [withConstants, card_sum, card_constantsOn]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
ie : IsEmpty α
⊢ LHom.comp (LHom.sumElim (LHom.id L) (LHom.ofIsEmpty (constantsOn α) L)) (lhomWithConstants L α) = LHom.id L
[PROOFSTEP]
rw [lhomWithConstants, LHom.sumElim_comp_inl]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
ie : IsEmpty α
⊢ LHom.comp (lhomWithConstants L α) (LHom.sumElim (LHom.id L) (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id (L[[α]])
[PROOFSTEP]
simp only [LHom.comp_sumElim, lhomWithConstants, LHom.comp_id]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
ie : IsEmpty α
⊢ LHom.sumElim LHom.sumInl (LHom.comp LHom.sumInl (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id (L[[α]])
[PROOFSTEP]
exact _root_.trans (congr rfl (Subsingleton.elim _ _)) LHom.sumElim_inl_inr
[GOAL]
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
β : Type u_1
f : α → β
⊢ comp (lhomWithConstantsMap L f) LHom.sumInl = lhomWithConstants L β
[PROOFSTEP]
ext
[GOAL]
case h_fun.h.h
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
β : Type u_1
f : α → β
x✝¹ : ℕ
x✝ : Functions L x✝¹
⊢ onFunction (comp (lhomWithConstantsMap L f) LHom.sumInl) x✝ = onFunction (lhomWithConstants L β) x✝
[PROOFSTEP]
rfl
[GOAL]
case h_rel.h.h
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
α : Type w'
β : Type u_1
f : α → β
x✝¹ : ℕ
x✝ : Relations L x✝¹
⊢ onRelation (comp (lhomWithConstantsMap L f) LHom.sumInl) x✝ = onRelation (lhomWithConstants L β) x✝
[PROOFSTEP]
rfl
[GOAL]
L : Language
L' : Language
M : Type w
inst✝¹ : Structure L M
α : Type u_1
inst✝ : Structure (constantsOn α) M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) x = ↑(Language.con L a)
[PROOFSTEP]
rw [Unique.eq_default x]
[GOAL]
L : Language
L' : Language
M : Type w
inst✝¹ : Structure L M
α : Type u_1
inst✝ : Structure (constantsOn α) M
a : α
x : Fin 0 → M
⊢ funMap (Sum.inr a) default = ↑(Language.con L a)
[PROOFSTEP]
exact (LHom.sumInr : constantsOn α →ᴸ L.sum _).map_onFunction _ _