[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
⊢ Function.Injective fun c => ↑c.toOrderHom
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ h
[GOAL]
case mk.mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
toOrderHom✝¹ : α →o α
le_closure'✝¹ : ∀ (x : α), x ≤ OrderHom.toFun toOrderHom✝¹ x
idempotent'✝¹ : ∀ (x : α), OrderHom.toFun toOrderHom✝¹ (OrderHom.toFun toOrderHom✝¹ x) = OrderHom.toFun toOrderHom✝¹ x
toOrderHom✝ : α →o α
le_closure'✝ : ∀ (x : α), x ≤ OrderHom.toFun toOrderHom✝ x
idempotent'✝ : ∀ (x : α), OrderHom.toFun toOrderHom✝ (OrderHom.toFun toOrderHom✝ x) = OrderHom.toFun toOrderHom✝ x
h :
  (fun c => ↑c.toOrderHom) { toOrderHom := toOrderHom✝¹, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹ } =
    (fun c => ↑c.toOrderHom) { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝, idempotent' := idempotent'✝ }
⊢ { toOrderHom := toOrderHom✝¹, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹ } =
    { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝, idempotent' := idempotent'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toOrderHom
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
toOrderHom✝¹ : α →o α
le_closure'✝¹ : ∀ (x : α), x ≤ OrderHom.toFun toOrderHom✝¹ x
idempotent'✝¹ : ∀ (x : α), OrderHom.toFun toOrderHom✝¹ (OrderHom.toFun toOrderHom✝¹ x) = OrderHom.toFun toOrderHom✝¹ x
toOrderHom✝ : α →o α
le_closure'✝ : ∀ (x : α), x ≤ OrderHom.toFun toOrderHom✝ x
idempotent'✝ : ∀ (x : α), OrderHom.toFun toOrderHom✝ (OrderHom.toFun toOrderHom✝ x) = OrderHom.toFun toOrderHom✝ x
h :
  (fun c => ↑c.toOrderHom) { toOrderHom := toOrderHom✝¹, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹ } =
    (fun c => ↑c.toOrderHom) { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝, idempotent' := idempotent'✝ }
⊢ toOrderHom✝¹ = toOrderHom✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
c₁ : α → α
monotone'✝¹ : Monotone c₁
le_closure'✝¹ : ∀ (x : α), x ≤ OrderHom.toFun { toFun := c₁, monotone' := monotone'✝¹ } x
idempotent'✝¹ :
  ∀ (x : α),
    OrderHom.toFun { toFun := c₁, monotone' := monotone'✝¹ }
        (OrderHom.toFun { toFun := c₁, monotone' := monotone'✝¹ } x) =
      OrderHom.toFun { toFun := c₁, monotone' := monotone'✝¹ } x
c₂ : α → α
monotone'✝ : Monotone c₂
le_closure'✝ : ∀ (x : α), x ≤ OrderHom.toFun { toFun := c₂, monotone' := monotone'✝ } x
idempotent'✝ :
  ∀ (x : α),
    OrderHom.toFun { toFun := c₂, monotone' := monotone'✝ }
        (OrderHom.toFun { toFun := c₂, monotone' := monotone'✝ } x) =
      OrderHom.toFun { toFun := c₂, monotone' := monotone'✝ } x
h :
  ↑{ toOrderHom := { toFun := c₁, monotone' := monotone'✝¹ }, le_closure' := le_closure'✝¹,
        idempotent' := idempotent'✝¹ } =
    ↑{ toOrderHom := { toFun := c₂, monotone' := monotone'✝ }, le_closure' := le_closure'✝,
        idempotent' := idempotent'✝ }
⊢ { toOrderHom := { toFun := c₁, monotone' := monotone'✝¹ }, le_closure' := le_closure'✝¹,
      idempotent' := idempotent'✝¹ } =
    { toOrderHom := { toFun := c₂, monotone' := monotone'✝ }, le_closure' := le_closure'✝, idempotent' := idempotent'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ x ∈ Set.range ↑c → x ∈ closed c
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case intro
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
y : α
⊢ ↑c y ∈ closed c
[PROOFSTEP]
apply c.idempotent
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c : ClosureOperator α
x y : α
hy : closed c y
⊢ ↑c x ≤ y ↔ x ≤ y
[PROOFSTEP]
rw [← c.closure_eq_self_of_mem_closed hy, ← le_closure_iff]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c✝ c : ClosureOperator α
⊢ c =
    mk₃ (↑c) (closed c) (_ : ∀ (x : α), x ≤ ↑c x) (_ : ∀ (x : α), ↑c x ∈ closed c)
      (_ : ∀ (x y : α), x ≤ y → closed c y → ↑c x ≤ y)
[PROOFSTEP]
ext
[GOAL]
case a.h
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝¹ inst✝ : PartialOrder α
c✝ c : ClosureOperator α
x✝ : α
⊢ ↑c x✝ =
    ↑(mk₃ (↑c) (closed c) (_ : ∀ (x : α), x ≤ ↑c x) (_ : ∀ (x : α), ↑c x ∈ closed c)
          (_ : ∀ (x y : α), x ≤ y → closed c y → ↑c x ≤ y))
      x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ ↑c (x ⊔ ↑c y) = ↑c (x ⊔ y)
[PROOFSTEP]
rw [sup_comm, closure_sup_closure_left, sup_comm (a := x)]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : SemilatticeSup α
c : ClosureOperator α
x y : α
⊢ ↑c (↑c x ⊔ ↑c y) = ↑c (x ⊔ y)
[PROOFSTEP]
rw [closure_sup_closure_left, closure_sup_closure_right]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
u : β → α
l : LowerAdjoint u
l₁ : α → β
gc'✝¹ : GaloisConnection l₁ u
l₂ : α → β
gc'✝ : GaloisConnection l₂ u
h : { toFun := l₁, gc' := gc'✝¹ }.toFun = { toFun := l₂, gc' := gc'✝ }.toFun
⊢ { toFun := l₁, gc' := gc'✝¹ } = { toFun := l₂, gc' := gc'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ x ∈ toFun l s ↔ ∀ (S : α), s ⊆ ↑S → x ∈ S
[PROOFSTEP]
simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← l.le_iff_subset]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
s : Set β
x : β
⊢ toFun l {x} ≤ toFun l s ↔ ∀ (S : α), toFun l s ≤ S → toFun l {x} ≤ S
[PROOFSTEP]
exact ⟨fun h S => h.trans, fun h => h _ le_rfl⟩
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝ : SetLike α β
l : LowerAdjoint SetLike.coe
x y : α
⊢ toFun l (↑(toFun l ↑x) ∪ ↑(toFun l ↑y)) = toFun l (↑x ∪ ↑y)
[PROOFSTEP]
rw [closure_union_closure_right, closure_union_closure_left]
[GOAL]
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ GaloisConnection.closureOperator (_ : GaloisConnection (ClosureOperator.toClosed c) Subtype.val) = c
[PROOFSTEP]
ext x
[GOAL]
case a.h
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
β : Type u_4
inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ ↑(GaloisConnection.closureOperator (_ : GaloisConnection (ClosureOperator.toClosed c) Subtype.val)) x = ↑c x
[PROOFSTEP]
rfl
