case h.h
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U)) ↔ x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
⊢ (IsOpenMap.functor hf).obj ((map f).obj U) = (IsOpenMap.functor hf).obj ⊤ ⊓ U
ext
case h.h.mp
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U)) → x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)

case h.h.mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U) → x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U))
case h.h
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U)) ↔ x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
constructor
case h.h.mp.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
x : (forget TopCat).obj X
hx : x ∈ ↑((map f).obj U)
⊢ (forget TopCat).map f x ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
case h.h.mp
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U)) → x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
rintro ⟨x, hx, rfl⟩
no goals
case h.h.mp.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
x : (forget TopCat).obj X
hx : x ∈ ↑((map f).obj U)
⊢ (forget TopCat).map f x ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U)
exact ⟨⟨x, trivial, rfl⟩, hx⟩
case h.h.mpr.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
x : (forget TopCat).obj X
hx : (forget TopCat).map f x ∈ ↑U
⊢ (forget TopCat).map f x ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U))
case h.h.mpr
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
x✝ : ↑Y
⊢ x✝ ∈ ↑((IsOpenMap.functor hf).obj ⊤ ⊓ U) → x✝ ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U))
rintro ⟨⟨x, -, rfl⟩, hx⟩
no goals
case h.h.mpr.intro.intro.intro
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ((forget TopCat).map f)
U : Opens ↑Y
x : (forget TopCat).obj X
hx : (forget TopCat).map f x ∈ ↑U
⊢ (forget TopCat).map f x ∈ ↑((IsOpenMap.functor hf).obj ((map f).obj U))
exact ⟨x, hx, rfl⟩