-- Monotone maps between ordered sets, Galois connections, and closure
-- operators
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Lattice.Monotone
import Complete

predicate IsMonotoneMap (f A r B s : Set) :=
  FunctionBetween(f, A, B) ∧
  (∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → relates(s, f(x), f(y)))

predicate IsAntitoneMap (f A r B s : Set) :=
  FunctionBetween(f, A, B) ∧
  (∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → relates(s, f(y), f(x)))

-- A Galois connection: f is left adjoint to g.
predicate IsGaloisConnection (f A r g B s : Set) :=
  FunctionBetween(f, A, B) ∧ FunctionBetween(g, B, A) ∧
  (∀ x ∈ A, ∀ y ∈ B, (relates(s, f(x), y) ↔ relates(r, x, g(y))))

predicate IsClosureOperator (c A r : Set) :=
  FunctionBetween(c, A, A) ∧
  (∀ x ∈ A, relates(r, x, c(x))) ∧
  (∀ x ∈ A, ∀ y ∈ A, relates(r, x, y) → relates(r, c(x), c(y))) ∧
  (∀ x ∈ A, c(c(x)) = c(x))

-- Monotone maps

theorem IsMonotoneMap.function (f A r B s : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  shows f : A → B
proof
  simp [IsMonotoneMap]

theorem IsMonotoneMap.preserves (f A r B s x y : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hxy : relates(r, x, y)
  shows relates(s, f(x), f(y))
proof
  rcases h with ⟨function, monotone⟩
  exact monotone with x, hx, y, hy, hxy

theorem IsMonotoneMap.apply_member (f A r B s x : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  requires hx : x ∈ A
  shows f(x) ∈ B
proof
  exact FunctionBetween.apply_closed with (IsMonotoneMap.function with h), hx

theorem IsAntitoneMap.function (f A r B s : Set)
  requires h : IsAntitoneMap(f, A, r, B, s)
  shows f : A → B
proof
  simp [IsAntitoneMap]

theorem IsAntitoneMap.reverses (f A r B s x y : Set)
  requires h : IsAntitoneMap(f, A, r, B, s)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hxy : relates(r, x, y)
  shows relates(s, f(y), f(x))
proof
  rcases h with ⟨function, antitone⟩
  exact antitone with x, hx, y, hy, hxy

theorem IsMonotoneMap.identity (A r : Set)
  shows IsMonotoneMap(identity(A), A, r, A, r)
proof
  constructor
  . exact identity.function at A
  . intros x hx y hy hxy
    have valueX := identity.apply with hx
    have valueY := identity.apply with hy
    rw [valueX, valueY]
    exact hxy

theorem IsMonotoneMap.compose (f g A r B s C t : Set)
  requires hf : IsMonotoneMap(f, A, r, B, s)
  requires hg : IsMonotoneMap(g, B, s, C, t)
  shows IsMonotoneMap(compose(g, f, A, B, C), A, r, C, t)
proof
  have fFunction := IsMonotoneMap.function with hf
  have gFunction := IsMonotoneMap.function with hg
  constructor
  . exact compose.function with fFunction, gFunction
  . intros x hx y hy hxy
    have valueX := compose.apply with fFunction, gFunction, hx
    have valueY := compose.apply with fFunction, gFunction, hy
    rw [valueX, valueY]
    have fxB := FunctionBetween.apply_closed with fFunction, hx
    have fyB := FunctionBetween.apply_closed with fFunction, hy
    have mapped := IsMonotoneMap.preserves with hf, hx, hy, hxy
    exact IsMonotoneMap.preserves with hg, fxB, fyB, mapped

theorem IsMonotoneMap.converse (f A r B s : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  shows IsMonotoneMap(f, A, converse(r, A, A), B, converse(s, B, B))
proof
  have function := IsMonotoneMap.function with h
  constructor
  . exact function
  . intros x hx y hy hxy
    have yx := converse.reflects with hxy
    have mapped := IsMonotoneMap.preserves with h, hy, hx, yx
    have fxB := FunctionBetween.apply_closed with function, hx
    have fyB := FunctionBetween.apply_closed with function, hy
    exact converse.relates with fyB, fxB, mapped

theorem IsAntitoneMap.monotone_converse (f A r B s : Set)
  requires h : IsAntitoneMap(f, A, r, B, s)
  shows IsMonotoneMap(f, A, r, B, converse(s, B, B))
proof
  have function := IsAntitoneMap.function with h
  constructor
  . exact function
  . intros x hx y hy hxy
    have reversed := IsAntitoneMap.reverses with h, hx, hy, hxy
    have fxB := FunctionBetween.apply_closed with function, hx
    have fyB := FunctionBetween.apply_closed with function, hy
    exact converse.relates with fyB, fxB, reversed

theorem OrderEmbedding.monotone (f A r B s : Set)
  requires h : OrderEmbedding(f, A, r, B, s)
  shows IsMonotoneMap(f, A, r, B, s)
proof
  rcases h with ⟨injective, ordered⟩
  have function := Injective.function with injective
  constructor
  . exact function
  . intros x hx y hy hxy
    have fxB := FunctionBetween.apply_closed with function, hx
    have fyB := FunctionBetween.apply_closed with function, hy
    have mapX := FunctionBetween.relates_apply with function, hx
    have mapY := FunctionBetween.relates_apply with function, hy
    have preserved := ordered with x, hx, y, hy, f(x), fxB, f(y), fyB, mapX,
        mapY
    exact preserved.forward with hxy

theorem OrderEmbedding.reflects (f A r B s x y : Set)
  requires h : OrderEmbedding(f, A, r, B, s)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hxy : relates(s, f(x), f(y))
  shows relates(r, x, y)
proof
  rcases h with ⟨injective, ordered⟩
  have function := Injective.function with injective
  have fxB := FunctionBetween.apply_closed with function, hx
  have fyB := FunctionBetween.apply_closed with function, hy
  have mapX := FunctionBetween.relates_apply with function, hx
  have mapY := FunctionBetween.relates_apply with function, hy
  have preserved := ordered with x, hx, y, hy, f(x), fxB, f(y), fyB, mapX, mapY
  exact preserved.backward with hxy

theorem OrderIsomorphism.monotone (f A r B s : Set)
  requires h : OrderIsomorphism(f, A, r, B, s)
  shows IsMonotoneMap(f, A, r, B, s)
proof
  exact OrderEmbedding.monotone with (OrderIsomorphism.embedding with h)

-- Chains and bounds under a monotone map

theorem IsMonotoneMap.chain (f A r B s C : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  requires chain : Chain(A, r, C)
  shows Chain(B, s, functionImage(f, C, B))
proof
  rcases chain with ⟨bounded, comparable⟩
  constructor
  . exact functionImage.subset at f, C, B
  . intros u hu v hv
    obtain ⟨uB, x, hx, rfl⟩ := functionImage.membership.forward with hu
    obtain ⟨vB, y, hy, rfl⟩ := functionImage.membership.forward with hv
    have xA := bounded with x, hx
    have yA := bounded with y, hy
    have cases := comparable with x, hx, y, hy
    cases cases with xy | yx
    . left
      exact IsMonotoneMap.preserves with h, xA, yA, xy
    . right
      exact IsMonotoneMap.preserves with h, yA, xA, yx

theorem IsMonotoneMap.image_upper (f A r B s S u : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  requires bound : UpperBound(A, r, S, u)
  shows UpperBound(B, s, functionImage(f, S, B), f(u))
proof
  have uA := UpperBound.member with bound
  have bounded := UpperBound.subset with bound
  refine ⟨(IsMonotoneMap.apply_member with h, uA), (functionImage.subset at f,
      S, B), ?_⟩
  intros v hv
  obtain ⟨vB, x, hx, rfl⟩ := functionImage.membership.forward with hv
  have above := UpperBound.above with bound, hx
  exact IsMonotoneMap.preserves with h, (bounded with x, hx), uA, above

theorem IsMonotoneMap.image_lower (f A r B s S l : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  requires bound : LowerBound(A, r, S, l)
  shows LowerBound(B, s, functionImage(f, S, B), f(l))
proof
  have lA := LowerBound.member with bound
  have bounded := LowerBound.subset with bound
  refine ⟨(IsMonotoneMap.apply_member with h, lA), (functionImage.subset at f,
      S, B), ?_⟩
  intros v hv
  obtain ⟨vB, x, hx, rfl⟩ := functionImage.membership.forward with hv
  have below := LowerBound.below with bound, hx
  exact IsMonotoneMap.preserves with h, lA, (bounded with x, hx), below

theorem IsMonotoneMap.image_supremum_le (f A r B s S u v : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  requires hu : Supremum(A, r, S, u)
  requires hv : Supremum(B, s, functionImage(f, S, B), v)
  shows relates(s, v, f(u))
proof
  have uA := Supremum.member with hu
  have bound := IsMonotoneMap.image_upper with h, (Supremum.upper with hu)
  exact Supremum.least with hv, (IsMonotoneMap.apply_member with h, uA), bound

theorem IsMonotoneMap.image_infimum_ge (f A r B s S l m : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  requires hl : Infimum(A, r, S, l)
  requires hm : Infimum(B, s, functionImage(f, S, B), m)
  shows relates(s, f(l), m)
proof
  have lA := Infimum.member with hl
  have bound := IsMonotoneMap.image_lower with h, (Infimum.lower with hl)
  exact Infimum.greatest with hm, (IsMonotoneMap.apply_member with h, lA), bound

theorem IsMonotoneMap.join_le (f A r B s x y : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  requires source : IsLattice(A, r)
  requires target : IsLattice(B, s)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows relates(s, join(B, s, f(x), f(y)), f(join(A, r, x, y)))
proof
  have joinA := join.member with source, hx, hy
  have fxB := IsMonotoneMap.apply_member with h, hx
  have fyB := IsMonotoneMap.apply_member with h, hy
  have fJ := IsMonotoneMap.apply_member with h, joinA
  have xJ := IsMonotoneMap.preserves with h, hx, joinA,
      (join.upper_left with source, hx, hy)
  have yJ := IsMonotoneMap.preserves with h, hy, joinA,
      (join.upper_right with source, hx, hy)
  exact join.least with target, fxB, fyB, fJ, xJ, yJ

theorem IsMonotoneMap.meet_ge (f A r B s x y : Set)
  requires h : IsMonotoneMap(f, A, r, B, s)
  requires source : IsLattice(A, r)
  requires target : IsLattice(B, s)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows relates(s, f(meet(A, r, x, y)), meet(B, s, f(x), f(y)))
proof
  have meetA := meet.member with source, hx, hy
  have fxB := IsMonotoneMap.apply_member with h, hx
  have fyB := IsMonotoneMap.apply_member with h, hy
  have fM := IsMonotoneMap.apply_member with h, meetA
  have mX := IsMonotoneMap.preserves with h, meetA, hx,
      (meet.lower_left with source, hx, hy)
  have mY := IsMonotoneMap.preserves with h, meetA, hy,
      (meet.lower_right with source, hx, hy)
  exact meet.greatest with target, fxB, fyB, fM, mX, mY

-- Galois connections

theorem IsGaloisConnection.lower_function (f A r g B s : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  shows f : A → B
proof
  simp [IsGaloisConnection]

theorem IsGaloisConnection.upper_function (f A r g B s : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  shows g : B → A
proof
  simp [IsGaloisConnection]

theorem IsGaloisConnection.adjunction (f A r g B s x y : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  requires hx : x ∈ A
  requires hy : y ∈ B
  shows relates(s, f(x), y) ↔ relates(r, x, g(y))
proof
  rcases h with ⟨fFunction, gFunction, adjoint⟩
  exact adjoint with x, hx, y, hy

theorem IsGaloisConnection.unit (f A r g B s x : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  requires target : IsPartialOrder(B, s)
  requires hx : x ∈ A
  shows relates(r, x, g(f(x)))
proof
  have reflexive := IsPartialOrder.reflexive with target
  have fxB := FunctionBetween.apply_closed with
      (IsGaloisConnection.lower_function with h), hx
  have adjoint := IsGaloisConnection.adjunction with h, hx, fxB
  exact adjoint.forward with (reflexive with f(x), fxB)

theorem IsGaloisConnection.counit (f A r g B s y : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  requires source : IsPartialOrder(A, r)
  requires hy : y ∈ B
  shows relates(s, f(g(y)), y)
proof
  have reflexive := IsPartialOrder.reflexive with source
  have gyA := FunctionBetween.apply_closed with
      (IsGaloisConnection.upper_function with h), hy
  have adjoint := IsGaloisConnection.adjunction with h, gyA, hy
  exact adjoint.backward with (reflexive with g(y), gyA)

theorem IsGaloisConnection.lower_monotone (f A r g B s : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  requires source : IsPartialOrder(A, r)
  requires target : IsPartialOrder(B, s)
  shows IsMonotoneMap(f, A, r, B, s)
proof
  have transitive := IsPartialOrder.transitive with source
  have fFunction := IsGaloisConnection.lower_function with h
  have gFunction := IsGaloisConnection.upper_function with h
  constructor
  . exact fFunction
  . intros x hx y hy hxy
    have fyB := FunctionBetween.apply_closed with fFunction, hy
    have gfyA := FunctionBetween.apply_closed with gFunction, fyB
    have unit := IsGaloisConnection.unit with h, target, hy
    have below := transitive with x, hx, y, hy, g(f(y)), gfyA, hxy, unit
    have adjoint := IsGaloisConnection.adjunction with h, hx, fyB
    exact adjoint.backward with below

theorem IsGaloisConnection.upper_monotone (f A r g B s : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  requires source : IsPartialOrder(A, r)
  requires target : IsPartialOrder(B, s)
  shows IsMonotoneMap(g, B, s, A, r)
proof
  have transitive := IsPartialOrder.transitive with target
  have fFunction := IsGaloisConnection.lower_function with h
  have gFunction := IsGaloisConnection.upper_function with h
  constructor
  . exact gFunction
  . intros x hx y hy hxy
    have gxA := FunctionBetween.apply_closed with gFunction, hx
    have fgxB := FunctionBetween.apply_closed with fFunction, gxA
    have counit := IsGaloisConnection.counit with h, source, hx
    have below := transitive with f(g(x)), fgxB, x, hx, y, hy, counit, hxy
    have adjoint := IsGaloisConnection.adjunction with h, gxA, hy
    exact adjoint.forward with below

theorem IsGaloisConnection.lower_upper_lower (f A r g B s x : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  requires source : IsPartialOrder(A, r)
  requires target : IsPartialOrder(B, s)
  requires hx : x ∈ A
  shows f(g(f(x))) = f(x)
proof
  have antisymmetric := IsPartialOrder.antisymmetric with target
  have fFunction := IsGaloisConnection.lower_function with h
  have gFunction := IsGaloisConnection.upper_function with h
  have fxB := FunctionBetween.apply_closed with fFunction, hx
  have gfxA := FunctionBetween.apply_closed with gFunction, fxB
  have fgfxB := FunctionBetween.apply_closed with fFunction, gfxA
  have below := IsGaloisConnection.counit with h, source, fxB
  have unit := IsGaloisConnection.unit with h, target, hx
  have monotone := IsGaloisConnection.lower_monotone with h, source, target
  have above := IsMonotoneMap.preserves with monotone, hx, gfxA, unit
  exact antisymmetric with f(g(f(x))), fgfxB, f(x), fxB, below, above

theorem IsGaloisConnection.upper_lower_upper (f A r g B s y : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  requires source : IsPartialOrder(A, r)
  requires target : IsPartialOrder(B, s)
  requires hy : y ∈ B
  shows g(f(g(y))) = g(y)
proof
  have antisymmetric := IsPartialOrder.antisymmetric with source
  have fFunction := IsGaloisConnection.lower_function with h
  have gFunction := IsGaloisConnection.upper_function with h
  have gyA := FunctionBetween.apply_closed with gFunction, hy
  have fgyB := FunctionBetween.apply_closed with fFunction, gyA
  have gfgyA := FunctionBetween.apply_closed with gFunction, fgyB
  have above := IsGaloisConnection.unit with h, target, gyA
  have counit := IsGaloisConnection.counit with h, source, hy
  have monotone := IsGaloisConnection.upper_monotone with h, source, target
  have below := IsMonotoneMap.preserves with monotone, fgyB, hy, counit
  exact antisymmetric with g(f(g(y))), gfgyA, g(y), gyA, below, above

theorem IsGaloisConnection.identity (A r : Set)
  shows IsGaloisConnection(identity(A), A, r, identity(A), A, r)
proof
  refine ⟨identity.function at A, identity.function at A, ?_⟩
  intros x hx y hy
  have valueX := identity.apply with hx
  have valueY := identity.apply with hy
  rw [valueX, valueY]
  constructor
  . intro related
    exact related
  . intro related
    exact related

theorem IsGaloisConnection.compose (f A r g B s k C t l : Set)
  requires first : IsGaloisConnection(f, A, r, g, B, s)
  requires second : IsGaloisConnection(k, B, s, l, C, t)
  shows
    IsGaloisConnection(compose(k, f, A, B, C), A, r, compose(g, l, C, B, A), C, t)
proof
  have fFunction := IsGaloisConnection.lower_function with first
  have gFunction := IsGaloisConnection.upper_function with first
  have kFunction := IsGaloisConnection.lower_function with second
  have lFunction := IsGaloisConnection.upper_function with second
  refine ⟨(compose.function with fFunction, kFunction),
      (compose.function with lFunction, gFunction), ?_⟩
  intros x hx z hz
  have valueX := compose.apply with fFunction, kFunction, hx
  have valueZ := compose.apply with lFunction, gFunction, hz
  rw [valueX, valueZ]
  have fxB := FunctionBetween.apply_closed with fFunction, hx
  have lzB := FunctionBetween.apply_closed with lFunction, hz
  have outer := IsGaloisConnection.adjunction with second, fxB, hz
  have inner := IsGaloisConnection.adjunction with first, hx, lzB
  constructor
  . intro related
    exact inner.forward with (outer.forward with related)
  . intro related
    exact outer.backward with (inner.backward with related)

-- The left adjoint preserves suprema and the right adjoint preserves infima.

theorem IsGaloisConnection.lower_supremum (f A r g B s S u : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  requires source : IsPartialOrder(A, r)
  requires target : IsPartialOrder(B, s)
  requires hu : Supremum(A, r, S, u)
  shows Supremum(B, s, functionImage(f, S, B), f(u))
proof
  have monotone := IsGaloisConnection.lower_monotone with h, source, target
  have gFunction := IsGaloisConnection.upper_function with h
  have uA := Supremum.member with hu
  have bounded := Supremum.subset with hu
  constructor
  . exact IsMonotoneMap.image_upper with monotone, (Supremum.upper with hu)
  . intros b hb bound
    have gbA := FunctionBetween.apply_closed with gFunction, hb
    have lifted : UpperBound(A, r, S, g(b))
      refine ⟨gbA, bounded, ?_⟩
      intros x hx
      have xA := bounded with x, hx
      have fxB := IsMonotoneMap.apply_member with monotone, xA
      have imageMember : f(x) ∈ functionImage(f, S, B) :=
        functionImage.membership.backward with ⟨fxB, x, hx, rfl⟩
      have above := UpperBound.above with bound, imageMember
      have adjoint := IsGaloisConnection.adjunction with h, xA, hb
      exact adjoint.forward with above
    have below := Supremum.least with hu, gbA, lifted
    have adjoint := IsGaloisConnection.adjunction with h, uA, hb
    exact adjoint.backward with below

theorem IsGaloisConnection.upper_infimum (f A r g B s T v : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  requires source : IsPartialOrder(A, r)
  requires target : IsPartialOrder(B, s)
  requires hv : Infimum(B, s, T, v)
  shows Infimum(A, r, functionImage(g, T, A), g(v))
proof
  have monotone := IsGaloisConnection.upper_monotone with h, source, target
  have fFunction := IsGaloisConnection.lower_function with h
  have vB := Infimum.member with hv
  have bounded := Infimum.subset with hv
  constructor
  . exact IsMonotoneMap.image_lower with monotone, (Infimum.lower with hv)
  . intros a ha bound
    have faB := FunctionBetween.apply_closed with fFunction, ha
    have lifted : LowerBound(B, s, T, f(a))
      refine ⟨faB, bounded, ?_⟩
      intros y hy
      have yB := bounded with y, hy
      have gyA := IsMonotoneMap.apply_member with monotone, yB
      have imageMember : g(y) ∈ functionImage(g, T, A) :=
        functionImage.membership.backward with ⟨gyA, y, hy, rfl⟩
      have below := LowerBound.below with bound, imageMember
      have adjoint := IsGaloisConnection.adjunction with h, ha, yB
      exact adjoint.backward with below
    have above := Infimum.greatest with hv, faB, lifted
    have adjoint := IsGaloisConnection.adjunction with h, ha, vB
    exact adjoint.forward with above

-- Closure operators

theorem IsClosureOperator.function (c A r : Set)
  requires h : IsClosureOperator(c, A, r)
  shows c : A → A
proof
  simp [IsClosureOperator]

theorem IsClosureOperator.extensive (c A r x : Set)
  requires h : IsClosureOperator(c, A, r)
  requires hx : x ∈ A
  shows relates(r, x, c(x))
proof
  rcases h with ⟨function, extensive, monotone, idempotent⟩
  exact extensive with x, hx

theorem IsClosureOperator.monotone (c A r : Set)
  requires h : IsClosureOperator(c, A, r)
  shows IsMonotoneMap(c, A, r, A, r)
proof
  rcases h with ⟨function, extensive, monotone, idempotent⟩
  refine ⟨function, monotone⟩

theorem IsClosureOperator.idempotent (c A r x : Set)
  requires h : IsClosureOperator(c, A, r)
  requires hx : x ∈ A
  shows c(c(x)) = c(x)
proof
  rcases h with ⟨function, extensive, monotone, idempotent⟩
  exact idempotent with x, hx

theorem IsClosureOperator.apply_member (c A r x : Set)
  requires h : IsClosureOperator(c, A, r)
  requires hx : x ∈ A
  shows c(x) ∈ A
proof
  exact FunctionBetween.apply_closed with (IsClosureOperator.function with h),
    hx

theorem IsClosureOperator.identity (A r : Set)
  requires order : IsPartialOrder(A, r)
  shows IsClosureOperator(identity(A), A, r)
proof
  have reflexive := IsPartialOrder.reflexive with order
  refine ⟨identity.function at A, ?_, ?_, ?_⟩
  . intros x hx
    have valueX := identity.apply with hx
    rw valueX
    exact reflexive with x, hx
  . intros x hx y hy hxy
    have valueX := identity.apply with hx
    have valueY := identity.apply with hy
    rw [valueX, valueY]
    exact hxy
  . intros x hx
    have valueX := identity.apply with hx
    rw valueX
    rw valueX
    rfl

theorem IsClosureOperator.le_iff (c A r x y : Set)
  requires h : IsClosureOperator(c, A, r)
  requires order : IsPartialOrder(A, r)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows relates(r, x, c(y)) ↔ relates(r, c(x), c(y))
proof
  have transitive := IsPartialOrder.transitive with order
  have monotone := IsClosureOperator.monotone with h
  have cxA := IsClosureOperator.apply_member with h, hx
  have cyA := IsClosureOperator.apply_member with h, hy
  constructor
  . intro below
    have mapped := IsMonotoneMap.preserves with monotone, hx, cyA, below
    have twice := IsClosureOperator.idempotent with h, hy
    rw twice at mapped
    exact mapped
  . intro below
    have extensive := IsClosureOperator.extensive with h, hx
    exact transitive with x, hx, c(x), cxA, c(y), cyA, extensive, below

theorem IsGaloisConnection.closure (f A r g B s : Set)
  requires h : IsGaloisConnection(f, A, r, g, B, s)
  requires source : IsPartialOrder(A, r)
  requires target : IsPartialOrder(B, s)
  shows IsClosureOperator(compose(g, f, A, B, A), A, r)
proof
  have fFunction := IsGaloisConnection.lower_function with h
  have gFunction := IsGaloisConnection.upper_function with h
  have lower := IsGaloisConnection.lower_monotone with h, source, target
  have upper := IsGaloisConnection.upper_monotone with h, source, target
  have composite := IsMonotoneMap.compose with lower, upper
  refine ⟨(compose.function with fFunction, gFunction), ?_, ?_, ?_⟩
  . intros x hx
    have valueX := compose.apply with fFunction, gFunction, hx
    rw valueX
    exact IsGaloisConnection.unit with h, target, hx
  . intros x hx y hy hxy
    exact IsMonotoneMap.preserves with composite, hx, hy, hxy
  . intros x hx
    have fxB := FunctionBetween.apply_closed with fFunction, hx
    have gfxA := FunctionBetween.apply_closed with gFunction, fxB
    have valueX := compose.apply with fFunction, gFunction, hx
    have valueTwice := compose.apply with fFunction, gFunction, gfxA
    rw valueX
    rw valueTwice
    exact IsGaloisConnection.upper_lower_upper with h, source, target, fxB