[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝ : OpenNhds x
⊢ x✝ ≤ x✝
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝ : OpenNhds x
⊢ x✝.obj ≤ x✝.obj
[PROOFSTEP]
exact le_rfl
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝² x✝¹ x✝ : OpenNhds x
⊢ x✝² ≤ x✝¹ → x✝¹ ≤ x✝ → x✝² ≤ x✝
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝² x✝¹ x✝ : OpenNhds x
⊢ x✝².obj ≤ x✝¹.obj → x✝¹.obj ≤ x✝.obj → x✝².obj ≤ x✝.obj
[PROOFSTEP]
exact le_trans
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝ : OpenNhds x
⊢ x✝ ≤ ⊤
[PROOFSTEP]
dsimp [LE.le]
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
x✝ : OpenNhds x
⊢ x✝.obj ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : (OpenNhds x)ᵒᵖ
⊢ (map (𝟙 X) x).obj U.unop = U.unop
[PROOFSTEP]
simp
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : (OpenNhds x)ᵒᵖ
⊢ (map (𝟙 X) x).op.obj U = U
[PROOFSTEP]
simp
[GOAL]
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (inclusion (↑f x) ⋙ Opens.map f).obj U ≅ (map f x ⋙ inclusion x).obj U
[PROOFSTEP]
constructor
[GOAL]
case hom_inv_id
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ autoParam (?hom ≫ ?inv = 𝟙 ((inclusion (↑f x) ⋙ Opens.map f).obj U)) _auto✝
case inv_hom_id
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ autoParam (?inv ≫ ?hom = 𝟙 ((map f x ⋙ inclusion x).obj U)) _auto✝
case hom
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (inclusion (↑f x) ⋙ Opens.map f).obj U ⟶ (map f x ⋙ inclusion x).obj U
case inv
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (map f x ⋙ inclusion x).obj U ⟶ (inclusion (↑f x) ⋙ Opens.map f).obj U
[PROOFSTEP]
rfl
[GOAL]
case inv_hom_id
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ autoParam (?inv ≫ ?hom = 𝟙 ((map f x ⋙ inclusion x).obj U)) _auto✝
case hom
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (inclusion (↑f x) ⋙ Opens.map f).obj U ⟶ (map f x ⋙ inclusion x).obj U
case inv
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (map f x ⋙ inclusion x).obj U ⟶ (inclusion (↑f x) ⋙ Opens.map f).obj U
[PROOFSTEP]
rfl
[GOAL]
case hom
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (inclusion (↑f x) ⋙ Opens.map f).obj U ⟶ (map f x ⋙ inclusion x).obj U
case inv
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (map f x ⋙ inclusion x).obj U ⟶ (inclusion (↑f x) ⋙ Opens.map f).obj U
[PROOFSTEP]
exact 𝟙 _
[GOAL]
case inv
X Y : TopCat
f : X ⟶ Y
x : ↑X
U : OpenNhds (↑f x)
⊢ (map f x ⋙ inclusion x).obj U ⟶ (inclusion (↑f x) ⋙ Opens.map f).obj U
[PROOFSTEP]
exact 𝟙 _
