case intro
α : Type u_1
ι : Sort ?u.5391
κ : ι → Sort ?u.5396
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
y : α
⊢ ↑c.toOrderHom y ∈ closed c
α : Type u_1
ι : Sort ?u.5391
κ : ι → Sort ?u.5396
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ x ∈ Set.range ↑c.toOrderHom → x ∈ closed c
rintro ⟨y, rfl⟩
no goals
case intro
α : Type u_1
ι : Sort ?u.5391
κ : ι → Sort ?u.5396
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
y : α
⊢ ↑c.toOrderHom y ∈ closed c
apply c.idempotent