case a.h
α : Type u_1
ι : Sort ?u.34522
κ : ι → Sort ?u.34527
β : Type ?u.34530
inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ ↑(GaloisConnection.closureOperator (_ : GaloisConnection (ClosureOperator.toClosed c) Subtype.val)).toOrderHom x =
    ↑c.toOrderHom x
α : Type u_1
ι : Sort ?u.34522
κ : ι → Sort ?u.34527
β : Type ?u.34530
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ GaloisConnection.closureOperator (_ : GaloisConnection (ClosureOperator.toClosed c) Subtype.val) = c
ext x
no goals
case a.h
α : Type u_1
ι : Sort ?u.34522
κ : ι → Sort ?u.34527
β : Type ?u.34530
inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ ↑(GaloisConnection.closureOperator (_ : GaloisConnection (ClosureOperator.toClosed c) Subtype.val)).toOrderHom x =
    ↑c.toOrderHom x
rfl