-- Set-theoretic functions and bijections
-- 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.Set.Function
import Cumulus.Relation
import Nat.Foundation

predicate InjectiveBetween (f A B : Set) := FunctionBetween(f, A, B) ∧ (∀ x ∈ A, ∀ y ∈ A, ∀ z ∈ B, relates(f, x, z) → relates(f, y, z) → x = y)
predicate SurjectiveBetween (f A B : Set) := FunctionBetween(f, A, B) ∧ (∀ y ∈ B, ∃ x ∈ A, relates(f, x, y))
predicate BijectiveBetween (f A B : Set) := InjectiveBetween(f, A, B) ∧ SurjectiveBetween(f, A, B)
predicate TotalBetween (f A B : Set) := ∀ x ∈ A, ∃ y ∈ B, relates(f, x, y)

-- Graph of the identity function on A.
def identity (A : Set) : Set := { p ∈ A × A | ∃ x ∈ A, p = (x ↦ x) }

-- The constant graph from A to B with value y.
def constantFunction (A B y : Set) : Set :=
  { p ∈ A × B | ∃ x ∈ A, p = (x ↦ y) }

-- Graph of g after f. Explicit carrier sets keep every comprehension bounded.
def compose (g f A B C : Set) : Set := { p ∈ A × C | ∃ x ∈ A, ∃ y ∈ C, p = (x ↦ y) ∧ ∃ z ∈ B, relates(f, x, z) ∧ relates(g, z, y) }

-- Pair two functions pointwise over their common domain.
def pairFunctions (f g A B C : Set) : Set :=
  { p ∈ A × (B × C) |
    ∃ x ∈ A, p = (x ↦ (f(x), g(x))) }

def adjoinMap (f a b : Set) : Set := insert((a ↦ b), f)

theorem adjoinMap.membership (p f a b : Set)
  shows p ∈ adjoinMap(f, a, b) ↔ (p = (a ↦ b) ∨ p ∈ f)
proof
  simp [adjoinMap, insert.membership]

theorem constantFunction.relates (A B x y : Set)
  requires xInA : x ∈ A
  requires yInB : y ∈ B
  shows relates(constantFunction(A, B, y), x, y)
proof
  simp [relates, constantFunction.membership, product.pair]

instance constantFunction.function (A B y : Set)
  requires yInB : y ∈ B
  shows constantFunction(A, B, y) : A → B
proof
  constructor
    intros p member
    obtain ⟨bounded, witnesses⟩ := constantFunction.membership.forward with member
    exact bounded
  . constructor
      intros x first xFirst second xSecond
      unfold relates at xFirst
      obtain ⟨_, i, iInA, firstShape⟩ := constantFunction.membership.forward with xFirst
      unfold relates at xSecond
      obtain ⟨_, j, jInA, secondShape⟩ := constantFunction.membership.forward with xSecond
      obtain ⟨_, firstEqual⟩ := orderedPair.injective with firstShape
      obtain ⟨_, secondEqual⟩ := orderedPair.injective with secondShape
      rw [firstEqual, secondEqual]
      rfl
    . intros x xInA
      refine ⟨y, yInB, (constantFunction.relates with xInA, yInB)⟩

theorem FunctionBetween.relation (f A B : Set)
  requires h : f : A → B
  shows RelationBetween(f, A, B)
proof
  simp [FunctionBetween]

theorem FunctionBetween.bounds (f A B x y : Set)
  requires h : f : A → B
  requires hxy : relates(f, x, y)
  shows x ∈ A ∧ y ∈ B
proof
  have relation := FunctionBetween.relation with h
  exact RelationBetween.bounds with relation, hxy

theorem FunctionBetween.member_shape (f A B p : Set)
  requires h : f : A → B
  requires hp : p ∈ f
  shows ∃ x ∈ A, ∃ y ∈ B, p = (x, y) ∧ relates(f, x, y)
proof
  have relation := FunctionBetween.relation with h
  unfold RelationBetween at relation
  have bounded := relation with p, hp
  obtain ⟨bound, x, hx, y, hy, shape⟩ := product.membership.forward with bounded
  refine ⟨x, hx, y, hy, shape, ?_⟩
  unfold relates
  rwa ← shape

theorem FunctionBetween.functional (f A B : Set)
  requires h : f : A → B
  shows Functional(f)
proof
  simp [FunctionBetween]

theorem FunctionBetween.empty (C : Set)
  shows ∅ : ∅ → C
proof
  simp [FunctionBetween, RelationBetween, Subset, Functional, relates, set.empty]

theorem FunctionBetween.exists_value (f A B x : Set)
  requires h : f : A → B
  requires hx : x ∈ A
  shows ∃ y ∈ B, relates(f, x, y)
proof
  simp [FunctionBetween]

theorem FunctionBetween.total (f A B : Set)
  requires h : f : A → B
  shows TotalBetween(f, A, B)
proof
  simp [FunctionBetween, TotalBetween]

theorem FunctionBetween.foundation (f A B : Set)
  requires h : f : A → B
  shows functionOn(f, A, B)
proof
  rcases h with ⟨relation, functional, total⟩
  constructor
  . intros input hInput
    specialize total with input, hInput
    obtain ⟨output, outputB, mapped⟩ := total
    witness output
    constructor
    exact outputB
    constructor
    exact mapped
    intros other mappedOther
    specialize functional with input, output, mapped, other, mappedOther
    rw functional
    rfl
  . intros p hp
    unfold RelationBetween at relation
    specialize relation with p, hp
    obtain ⟨bounded, x, hxA, y, hyB, shape⟩ := product.membership.forward with relation
    refine ⟨x, y, hxA, hyB, shape⟩

theorem FunctionBetween.apply_value (f A B x y : Set)
  requires h : f : A → B
  requires hx : x ∈ A
  requires hxy : relates(f, x, y)
  shows f(x) = y
proof
  apply function.apply at f, A, B, x, y
  constructor
  . have foundation := FunctionBetween.foundation at f, A, B
    exact foundation with h
  refine ⟨hx, hxy⟩

theorem FunctionBetween.apply_closed (f A B x : Set)
  requires function : f : A → B
  requires input : x ∈ A
  shows f(x) ∈ B
proof
  obtain ⟨y, output, mapped⟩ := FunctionBetween.exists_value with function, input
  have value := FunctionBetween.apply_value with function, input, mapped
  rwa value

theorem constantFunction.apply (A B x y : Set)
  requires xInA : x ∈ A
  requires yInB : y ∈ B
  shows apply(constantFunction(A, B, y), x) = y
proof
  have function := constantFunction.function at A, B, y with yInB
  have mapped := constantFunction.relates with xInA, yInB
  exact FunctionBetween.apply_value with function, xInA, mapped

theorem FunctionBetween.relates_apply (f A B x : Set)
  requires function : f : A → B
  requires input : x ∈ A
  shows relates(f, x, f(x))
proof
  obtain ⟨y, output, mapped⟩ := FunctionBetween.exists_value with function, input
  have value := FunctionBetween.apply_value with function, input, mapped
  rwa value

-- A graph can be given a smaller codomain once all its values are
-- known to lie there. This is particularly useful for sequences in a set.
theorem FunctionBetween.codomain_of_values (f A B C : Set)
  requires function : f : A → B
  requires values : ∀ x ∈ A, f(x) ∈ C
  shows f : A → C
proof
  constructor
    intros p member
    obtain ⟨x, memberA, y, memberB, shape, related⟩ := FunctionBetween.member_shape with function, member
    have value := FunctionBetween.apply_value with function, memberA, related
    have memberC := values with x, memberA
    rw value at memberC
    rw shape
    exact product.pair with memberA, memberC
  . constructor
    . exact FunctionBetween.functional with function
    . intros x memberA
      refine ⟨f(x), (values with x, memberA), (FunctionBetween.relates_apply with function, memberA)⟩

theorem pairFunctions.relates (f g A B C x : Set)
  requires fFunction : f : A → B
  requires gFunction : g : A → C
  requires input : x ∈ A
  shows relates(pairFunctions(f, g, A, B, C), x,
    (f(x), g(x)))
proof
  have fValue := FunctionBetween.apply_closed with fFunction, input
  have gValue := FunctionBetween.apply_closed with gFunction, input
  have pairValue := product.pair with fValue, gValue
  unfold relates
  apply pairFunctions.membership.backward
  constructor
  . exact product.pair at x, (f(x), g(x)), A, B × C with
      input, pairValue
  . refine ⟨x, input, rfl⟩

instance pairFunctions.function (f g A B C : Set)
  requires fFunction : f : A → B
  requires gFunction : g : A → C
  shows pairFunctions(f, g, A, B, C) : A → B × C
proof
  constructor
    intros p member
    obtain ⟨bounded, witnesses⟩ := pairFunctions.membership.forward with member
    exact bounded
  . constructor
      intros x y xy z xz
      unfold relates at xy
      obtain ⟨_, a, aInA, firstShape⟩ := pairFunctions.membership.forward with xy
      unfold relates at xz
      obtain ⟨_, b, bInA, secondShape⟩ := pairFunctions.membership.forward with xz
      obtain ⟨sameA, shapeY⟩ := orderedPair.injective with firstShape
      obtain ⟨sameB, shapeZ⟩ := orderedPair.injective with secondShape
      cc
    . intros x input
      have fValue := FunctionBetween.apply_closed with fFunction, input
      have gValue := FunctionBetween.apply_closed with gFunction, input
      refine ⟨(f(x), g(x)), (product.pair with fValue, gValue), (pairFunctions.relates with fFunction, gFunction, input)⟩

theorem pairFunctions.apply (f g A B C x : Set)
  requires fFunction : f : A → B
  requires gFunction : g : A → C
  requires input : x ∈ A
  shows apply(pairFunctions(f, g, A, B, C), x) =
    (f(x), g(x))
proof
  have function := pairFunctions.function with fFunction, gFunction
  have mapped := pairFunctions.relates with fFunction, gFunction, input
  exact FunctionBetween.apply_value with function, input, mapped

theorem Functional.unique (f x y z : Set)
  requires hf : Functional(f)
  requires hxy : relates(f, x, y)
  requires hxz : relates(f, x, z)
  shows y = z
proof
  exact hf with x, y, hxy, z, hxz

theorem TotalBetween.predecessor (f A : Set, n : Nat)
  requires h : TotalBetween(f, succ(n), A)
  shows TotalBetween(f, n, A)
proof
  simp [TotalBetween]

theorem identity.relation (A : Set)
  shows RelationBetween(identity(A), A, A)
proof
  simp [RelationBetween, Subset]

theorem identity.relates (x A : Set)
  requires hx : x ∈ A
  shows relates(identity(A), x, x)
proof
  simp [relates, identity.membership, product.pair]

theorem identity.total (A : Set)
  shows TotalBetween(identity(A), A, A)
proof
  simp [TotalBetween, identity.relates]

theorem identity.functional (A : Set)
  shows Functional(identity(A))
proof
  intros x y hxy z hxz
  unfold relates at hxy
  simp [identity] at hxy
  rcases hxy with ⟨hxyProduct, a, haA, hxyPair⟩
  unfold relates at hxz
  simp [identity] at hxz
  rcases hxz with ⟨hxzProduct, b, hbA, hxzPair⟩
  obtain ⟨hxa, hya⟩ := orderedPair.injective with hxyPair
  obtain ⟨hxb, hzb⟩ := orderedPair.injective with hxzPair
  rw [hya, hzb]
  rwa ← hxa

instance identity.function (A : Set)
  shows identity(A) : A → A
proof
  constructor
  exact identity.relation
  constructor
  exact identity.functional
  exact identity.total at A

theorem identity.apply (x A : Set)
  requires member : x ∈ A
  shows apply(identity(A), x) = x
proof
  have function := identity.function at A
  have mapped := identity.relates with member
  exact FunctionBetween.apply_value with function, member, mapped

theorem identity.injective (A : Set)
  shows InjectiveBetween(identity(A), A, A)
proof
  constructor
  exact identity.function
  intros x hx y hy z hz hxz hyz
  unfold relates at hxz
  simp [identity] at hxz
  rcases hxz with ⟨hxzProduct, a, haA, hxzPair⟩
  obtain ⟨hxa, hza⟩ := orderedPair.injective with hxzPair
  unfold relates at hyz
  simp [identity] at hyz
  rcases hyz with ⟨hyzProduct, b, hbA, hyzPair⟩
  obtain ⟨hyb, hzb⟩ := orderedPair.injective with hyzPair
  rw [hxa, hyb]
  rwa ← hza

theorem identity.surjective (A : Set)
  shows SurjectiveBetween(identity(A), A, A)
proof
  simp [SurjectiveBetween, identity.function, identity.relates]

theorem identity.bijective (A : Set)
  shows BijectiveBetween(identity(A), A, A)
proof
  refine ⟨identity.injective at A, identity.surjective at A⟩

theorem compose.relation (g f A B C : Set)
  shows RelationBetween(compose(g, f, A, B, C), A, C)
proof
  simp [RelationBetween, Subset]

theorem compose.relates (g f A B C x z y : Set)
  requires hx : x ∈ A
  requires hz : z ∈ B
  requires hy : y ∈ C
  requires hf : relates(f, x, z)
  requires hg : relates(g, z, y)
  shows relates(compose(g, f, A, B, C), x, y)
proof
  unfold relates
  apply compose.membership.backward
  constructor
  exact product.pair with hx, hy
  refine ⟨x, hx, y, hy, rfl, z, hz, hf, hg⟩

theorem compose.total (g f A B C : Set)
  requires hf : f : A → B
  requires hg : g : B → C
  shows TotalBetween(compose(g, f, A, B, C), A, C)
proof
  intros x hx
  obtain ⟨z, hzB, hfxz⟩ := FunctionBetween.exists_value with hf, hx
  obtain ⟨y, hyC, hgzy⟩ := FunctionBetween.exists_value with hg, hzB
  witness y
  constructor
  exact hyC
  exact compose.relates with hx, hzB, hyC, hfxz, hgzy

theorem compose.functional (g f A B C : Set)
  requires hf : f : A → B
  requires hg : g : B → C
  shows Functional(compose(g, f, A, B, C))
proof
  intros x y hxy z hxz
  unfold relates at hxy
  simp [compose] at hxy
  rcases hxy with ⟨hxyProduct, x1, hx1A, y1, hy1C, hpair1, m, hmB, hfxm, hgmy⟩
  obtain ⟨hxx1, hyy1⟩ := orderedPair.injective with hpair1
  rw ← hxx1 at hfxm
  rw ← hyy1 at hgmy
  unfold relates at hxz
  simp [compose] at hxz
  rcases hxz with ⟨hxzProduct, x2, hx2A, z2, hz2C, hpair2, n, hnB, hfxn, hgnz⟩
  obtain ⟨hxx2, hzz2⟩ := orderedPair.injective with hpair2
  rw ← hxx2 at hfxn
  rw ← hzz2 at hgnz
  have fUnique := FunctionBetween.functional with hf, x, m, hfxm, n, hfxn
  rw ← fUnique at hgnz
  have gUnique := FunctionBetween.functional with hg
  exact gUnique with m, y, hgmy, z, hgnz

instance compose.function (g f A B C : Set)
  requires hf : f : A → B
  requires hg : g : B → C
  shows compose(g, f, A, B, C) : A → C
proof
  constructor
  exact compose.relation
  constructor
  exact compose.functional with hf, hg
  exact compose.total with hf, hg

theorem compose.apply (g f A B C x : Set)
  requires fFunction : f : A → B
  requires gFunction : g : B → C
  requires input : x ∈ A
  shows apply(compose(g, f, A, B, C), x) = g(f(x))
proof
  have middle := FunctionBetween.apply_closed with fFunction, input
  have output := FunctionBetween.apply_closed with gFunction, middle
  have mappedF := FunctionBetween.relates_apply with fFunction, input
  have mappedG := FunctionBetween.relates_apply with gFunction, middle
  have mapped := compose.relates with input, middle, output, mappedF, mappedG
  have function := compose.function with fFunction, gFunction
  exact FunctionBetween.apply_value with function, input, mapped

-- Image and corestriction do not change the function graph.
def functionImage (f A B : Set) : Set := { y ∈ B | ∃ x ∈ A, y = f(x) }

theorem functionImage.subset (f A B : Set)
  shows functionImage(f, A, B) ⊆ B
proof
  simp

theorem functionImage.value (f A B x : Set)
  requires function : f : A → B
  requires hx : x ∈ A
  shows f(x) ∈ functionImage(f, A, B)
proof
  have valueIn := FunctionBetween.apply_closed with *
  exact functionImage.membership.backward with ⟨valueIn, x, hx, rfl⟩

theorem identity.inclusion (A B : Set)
  requires subset : A ⊆ B
  shows identity(A) : A → B
proof
  have function := identity.function at A
  have values : ∀ x ∈ A, identity(A)(x) ∈ B by simp [identity.apply]
  exact FunctionBetween.codomain_of_values with function, values

theorem functionImage.identity (A B : Set)
  requires subset : A ⊆ B
  shows functionImage(identity(A), A, B) = A
proof
  have function := identity.inclusion with subset
  ext x
  constructor
  . intro member
    obtain ⟨inB, a, ha, value⟩ := functionImage.membership.forward with member
    have equal := identity.apply with ha
    rw value
    rwa equal
  . intro member
    have image := functionImage.value with *
    have equal := identity.apply with member
    rwa equal at image

theorem functionImage.corestrict (f A B : Set)
  requires function : f : A → B
  shows f : A → functionImage(f, A, B)
proof
  apply FunctionBetween.codomain_of_values with function
  intros x hx
  exact functionImage.value with *

theorem functionImage.surjective (f A B : Set)
  requires function : f : A → B
  shows SurjectiveBetween(f, A, functionImage(f, A, B))
proof
  have corestricted := functionImage.corestrict with *
  unfold SurjectiveBetween
  refine ⟨corestricted, ?_⟩
  intros y hy
  obtain ⟨yIn, x, hx, shape⟩ := functionImage.membership.forward with hy
  have edge := FunctionBetween.relates_apply at f, A, B, x with *
  refine ⟨x, hx, ?_⟩
  rwa shape

theorem restrict.relates (f S x y : Set)
  shows relates(restrict(f, S), x, y) ↔ x ∈ S ∧ relates(f, x, y)
proof
  constructor
  . intro edge
    unfold relates at edge
    obtain ⟨original, u, hu, v, shape⟩ := restrict.membership.forward with edge
    have coordinates := orderedPair.injective with shape
    have member : x ∈ S by rwa coordinates.left
    refine ⟨member, ?_⟩
    exact original
  . intro data
    unfold relates
    apply restrict.membership.backward
    have original := data.right
    refine ⟨original, x, data.left, y, rfl⟩

theorem restrict.nested (f S T : Set)
  requires subset : S ⊆ T
  shows restrict(restrict(f, T), S) = restrict(f, S)
proof
  ext p
  constructor
  . intro member
    obtain ⟨inside, x, inS, y, shape⟩ := restrict.membership.forward with member
    have original := restrict.membership.forward with inside
    exact restrict.membership.backward with ⟨original.left, x, inS, y, shape⟩
  . intro member
    obtain ⟨inside, x, inS, y, shape⟩ := restrict.membership.forward with member
    have inT := subset with x, inS
    have restricted : p ∈ restrict(f, T) := restrict.membership.backward with ⟨inside, x, inT, y, shape⟩
    exact restrict.membership.backward with ⟨restricted, x, inS, y, shape⟩

theorem restrict.function (f A B S C : Set)
  requires function : f : A → B
  requires subset : S ⊆ A
  requires closed : ∀ x ∈ S, f(x) ∈ C
  shows restrict(f, S) : S → C
proof
  have relation := FunctionBetween.relation with function
  have functional := FunctionBetween.functional with function
  unfold FunctionBetween
  refine ⟨?_, ⟨?_, ?_⟩⟩
    intros p hp
    obtain ⟨original, x, hx, y, shape⟩ := restrict.membership.forward with hp
    have xIn := subset with x, hx
    have edge : relates(f, x, y)
      unfold relates
      rwa ← shape
    have value := FunctionBetween.apply_value with *
    have yIn := closed with x, hx
    rw value at yIn
    rw shape
    exact product.pair with *
    intros x y left z right
    have first := restrict.relates.forward with left
    have second := restrict.relates.forward with right
    exact Functional.unique with functional, first.right, second.right
  . intros x hx
    have xIn := subset with x, hx
    have yIn := closed with x, hx
    have edge := FunctionBetween.relates_apply with *
    refine ⟨f(x), yIn, ?_⟩
    exact restrict.relates.backward with ⟨hx, edge⟩

theorem restrict.apply (f A B S C x : Set)
  requires function : f : A → B
  requires subset : S ⊆ A
  requires closed : ∀ x ∈ S, f(x) ∈ C
  requires hx : x ∈ S
  shows restrict(f, S)(x) = f(x)
proof
  have restricted := restrict.function with *
  have xIn := subset with x, hx
  have original := FunctionBetween.relates_apply at f, A, B, x with *
  have edge : relates(restrict(f, S), x, f(x)) := restrict.relates.backward with ⟨hx, original⟩
  exact FunctionBetween.apply_value with *

-- Restricting only the domain needs no extra codomain closure obligation.
theorem restrict.domain_function (f A B S : Set)
  requires function : f : A → B
  requires subset : S ⊆ A
  shows restrict(f, S) : S → B
proof
  have closed : ∀ x ∈ S, f(x) ∈ B
    intros x hx
    have member := subset with x, hx
    exact FunctionBetween.apply_closed with function, member
  exact restrict.function with function, subset, closed

theorem restrict.domain_apply (f A B S x : Set)
  requires function : f : A → B
  requires subset : S ⊆ A
  requires member : x ∈ S
  shows restrict(f, S)(x) = f(x)
proof
  have closed : ∀ y ∈ S, f(y) ∈ B
    intros y hy
    have inA := subset with y, hy
    exact FunctionBetween.apply_closed with function, inA
  exact restrict.apply with function, subset, closed, member

-- Functions with the same domain and pointwise values are the same graph.
theorem FunctionBetween.subset_of_agree (f g A B : Set)
  requires hf : f : A → B
  requires hg : g : A → B
  requires same : ∀ x ∈ A, f(x) = g(x)
  shows f ⊆ g
proof
  intros p hp
  obtain ⟨x, hx, y, hy, shape, edge⟩ := FunctionBetween.member_shape with hf, hp
  have value := FunctionBetween.apply_value with *
  have equal := same with x, hx
  have image := FunctionBetween.relates_apply at g, A, B, x with *
  have result : relates(g, x, y) by cc
  unfold relates at result
  rwa shape

theorem FunctionBetween.ext (f g A B : Set)
  requires hf : f : A → B
  requires hg : g : A → B
  requires same : ∀ x ∈ A, f(x) = g(x)
  shows f = g
proof
  have fg := FunctionBetween.subset_of_agree with hf, hg, same
  have reversed : ∀ x ∈ A, g(x) = f(x) by simp
  have gf := FunctionBetween.subset_of_agree with hg, hf, reversed
  ext p
  simp

theorem compose.identity_left (f A B : Set)
  requires hf : f : A → B
  shows compose(identity(B), f, A, B, B) = f
proof
  ext p
  constructor
  intro hp
  simp [compose] at hp
  rcases hp with ⟨_, x, hxA, y, hyB, hpair, z, hzB, hfxz, hidzy⟩
  have self := identity.relates with hzB
  have unique := identity.functional at B with z, y, hidzy, z, self
  unfold relates at hfxz
  rw hpair
  rwa unique
  intro hp
  obtain ⟨x2, hxA, y2, hyB, hpair, hrel⟩ := FunctionBetween.member_shape with hf, hp
  have hid := identity.relates with hyB
  have composed := compose.relates with hxA, hyB, hyB, hrel, hid
  unfold relates at composed
  rwa ← hpair at composed

theorem compose.identity_right (f A B : Set)
  requires hf : f : A → B
  shows compose(f, identity(A), A, A, B) = f
proof
  ext p
  constructor
  intro hp
  simp [compose] at hp
  rcases hp with ⟨_, x, hxA, y, hyB, hpair, z, hzA, hidxz, hfzy⟩
  have self := identity.relates with hxA
  have unique := identity.functional at A with x, z, hidxz, x, self
  rw hpair
  rwa unique at hfzy
  intro hp
  obtain ⟨x2, hxA, y2, hyB, hpair, hrel⟩ := FunctionBetween.member_shape with hf, hp
  have hid := identity.relates with hxA
  have composed := compose.relates with hxA, hxA, hyB, hid, hrel
  unfold relates at composed
  rwa ← hpair at composed

theorem Injective.function (f A B : Set)
  requires h : InjectiveBetween(f, A, B)
  shows f : A → B
proof
  rcases h with ⟨fn, injective⟩
  exact fn

theorem Surjective.function (f A B : Set)
  requires h : SurjectiveBetween(f, A, B)
  shows f : A → B
proof
  rcases h with ⟨fn, surjective⟩
  exact fn

theorem Bijective.injective (f A B : Set)
  requires h : BijectiveBetween(f, A, B)
  shows InjectiveBetween(f, A, B)
proof
  rcases h with ⟨injective, surjective⟩
  exact injective

theorem Bijective.surjective (f A B : Set)
  requires h : BijectiveBetween(f, A, B)
  shows SurjectiveBetween(f, A, B)
proof
  rcases h with ⟨injective, surjective⟩
  exact surjective

theorem Injective.cancel (f A B x y z : Set)
  requires injective : InjectiveBetween(f, A, B)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ B
  requires hxz : relates(f, x, z)
  requires hyz : relates(f, y, z)
  shows x = y
proof
  rcases injective with (fn, cancel)
  exact cancel with x, hx, y, hy, z, hz, hxz, hyz

theorem converse.function_of_bijective (f A B : Set)
  requires h : BijectiveBetween(f, A, B)
  shows converse(f, A, B) : B → A
proof
  constructor
  exact converse.relation
  constructor
  intros y x hyx z hyz
  obtain ⟨hyB, hxA⟩ := converse.bounds with hyx
  obtain ⟨hyB2, hzA⟩ := converse.bounds with hyz
  have hxy := converse.reflects with hyx
  have hzy := converse.reflects with hyz
  obtain ⟨fn, injectiveLaw⟩ := Bijective.injective with h
  exact injectiveLaw with x, hxA, z, hzA, y, hyB, hxy, hzy
  intros y hy
  obtain ⟨fn, surjectiveLaw⟩ := Bijective.surjective with h
  specialize surjectiveLaw with y, hy
  obtain ⟨preimage, hpreimageA, hpreimageY⟩ := surjectiveLaw
  witness preimage
  constructor
  exact hpreimageA
  exact converse.relates with hpreimageA, hy, hpreimageY

theorem converse.injective_of_bijective (f A B : Set)
  requires h : BijectiveBetween(f, A, B)
  shows InjectiveBetween(converse(f, A, B), B, A)
proof
  constructor
  exact converse.function_of_bijective with h
  intros y hy z hz x hx hyx hzx
  have hxy := converse.reflects with hyx
  have hxz := converse.reflects with hzx
  have injective := Bijective.injective with h
  have fn := Injective.function with injective
  have functional := FunctionBetween.functional with fn
  exact functional with x, y, hxy, z, hxz

theorem converse.surjective_of_bijective (f A B : Set)
  requires h : BijectiveBetween(f, A, B)
  shows SurjectiveBetween(converse(f, A, B), B, A)
proof
  constructor
  exact converse.function_of_bijective with h
  intros x hx
  have injective := Bijective.injective with h
  have fn := Injective.function with injective
  obtain ⟨y, hyB, hxy⟩ := FunctionBetween.exists_value with fn, hx
  witness y
  constructor
  exact hyB
  exact converse.relates with hx, hyB, hxy

theorem converse.bijective (f A B : Set)
  requires h : BijectiveBetween(f, A, B)
  shows BijectiveBetween(converse(f, A, B), B, A)
proof
  simp [BijectiveBetween, converse.injective_of_bijective, converse.surjective_of_bijective]

theorem Bijective.inverse_apply (f A B x : Set)
  requires bijective : BijectiveBetween(f, A, B)
  requires hx : x ∈ A
  shows converse(f, A, B)(f(x)) = x
proof
  have injective := Bijective.injective with bijective
  have function := Injective.function with injective
  have inverse := converse.function_of_bijective with bijective
  have fx := FunctionBetween.apply_closed with function, hx
  have edge := FunctionBetween.relates_apply with function, hx
  have reverse := converse.relates with *
  exact FunctionBetween.apply_value with *

theorem Bijective.apply_inverse (f A B y : Set)
  requires bijective : BijectiveBetween(f, A, B)
  requires hy : y ∈ B
  shows f(converse(f, A, B)(y)) = y
proof
  have injective := Bijective.injective with bijective
  have function := Injective.function with injective
  have inverse := converse.function_of_bijective with bijective
  have preimage := FunctionBetween.apply_closed with inverse, hy
  have edge := FunctionBetween.relates_apply with inverse, hy
  have original := converse.reflects with edge
  exact FunctionBetween.apply_value with *

theorem compose.factors (g f A B C x y : Set)
  requires h : relates(compose(g, f, A, B, C), x, y)
  shows ∃ z ∈ B, relates(f, x, z) ∧ relates(g, z, y)
proof
  unfold relates at h
  simp [compose.membership] at h
  rcases h with ⟨hProduct, a, haA, b, hbC, hPair, z, hzB, hfaz, hgzb⟩
  obtain (hxa, hyb) := orderedPair.injective with hPair
  rw ← hxa at hfaz
  rw ← hyb at hgzb
  refine ⟨z, hzB, hfaz, hgzb⟩

theorem compose.injective (g f A B C : Set)
  requires hf : InjectiveBetween(f, A, B)
  requires hg : InjectiveBetween(g, B, C)
  shows InjectiveBetween(compose(g, f, A, B, C), A, C)
proof
  constructor
  have fFunction := Injective.function with hf
  have gFunction := Injective.function with hg
  exact compose.function with fFunction, gFunction
  intros x hx y hy w hw hxw hyw
  obtain ⟨m, hmB, hfxm, hgmw⟩ := compose.factors with hxw
  obtain ⟨n, hnB, hfyn, hgnw⟩ := compose.factors with hyw
  have middleEqual := Injective.cancel with hg, hmB, hnB, hw, hgmw, hgnw
  rw ← middleEqual at hfyn
  exact Injective.cancel with hf, hx, hy, hmB, hfxm, hfyn

theorem compose.surjective (g f A B C : Set)
  requires hf : BijectiveBetween(f, A, B)
  requires hg : BijectiveBetween(g, B, C)
  shows SurjectiveBetween(compose(g, f, A, B, C), A, C)
proof
  constructor
  have fInjective := Bijective.injective with hf
  have fFunction := Injective.function with fInjective
  have gInjective := Bijective.injective with hg
  have gFunction := Injective.function with gInjective
  exact compose.function with fFunction, gFunction
  intros y hy
  obtain (gFunction2, gOnto) := Bijective.surjective with hg
  specialize gOnto with y, hy
  obtain ⟨z, hzB, hgzy⟩ := gOnto
  obtain (fFunction2, fOnto) := Bijective.surjective with hf
  specialize fOnto with z, hzB
  obtain ⟨x, hxA, hfxz⟩ := fOnto
  witness x
  constructor
  exact hxA
  exact compose.relates with hxA, hzB, hy, hfxz, hgzy

theorem compose.bijective (g f A B C : Set)
  requires hf : BijectiveBetween(f, A, B)
  requires hg : BijectiveBetween(g, B, C)
  shows BijectiveBetween(compose(g, f, A, B, C), A, C)
proof
  --! Reduce bijectivity to its two components.
  --| The two obligations can be discharged independently.
  constructor
  . --! Injectivity
    --| Equality after composition is pulled back through g and then f.
    have fInjective := Bijective.injective with hf
    have gInjective := Bijective.injective with hg
    exact compose.injective with fInjective, gInjective
  . --! Surjectivity
    --| An output is pulled back through g and then through f.
    exact compose.surjective with hf, hg

theorem adjoinMap.relation (f A B a b : Set)
  requires hf : f : A → B
  shows RelationBetween(adjoinMap(f, a, b), insert(a, A), insert(b, B))
proof
  intros p hp
  have shape := adjoinMap.membership.forward with hp
  cases shape with newPair | oldPair
  rw newPair
  apply product.pair
  exact insert.self
  exact insert.self
  have relation := FunctionBetween.relation with hf
  unfold RelationBetween at relation
  specialize relation with p, oldPair
  obtain ⟨oldBound, x, hxA, y, hyB, pairShape⟩ := product.membership.forward with relation
  rw pairShape
  apply product.pair
  exact insert.contains with hxA
  exact insert.contains with hyB

theorem adjoinMap.relates_new (f a b : Set)
  shows relates(adjoinMap(f, a, b), a, b)
proof
  simp [relates]

theorem adjoinMap.relates_old (f a b x y : Set)
  requires h : relates(f, x, y)
  shows relates(adjoinMap(f, a, b), x, y)
proof
  simp [relates]

theorem adjoinMap.functional (f A B a b : Set)
  requires hf : f : A → B
  requires ha : ¬a ∈ A
  shows Functional(adjoinMap(f, a, b))
proof
  intros x y hxy z hxz
  unfold relates at hxy
  unfold relates at hxz
  have firstShape := adjoinMap.membership.forward with hxy
  have secondShape := adjoinMap.membership.forward with hxz
  cases firstShape with firstNew | firstOld
  . cases secondShape with secondNew | secondOld
    . obtain (xIsA, yIsB) := orderedPair.injective with firstNew
      obtain (xIsAAgain, zIsB) := orderedPair.injective with secondNew
      rw [yIsB, zIsB]
      rfl
    . obtain (xIsA, yIsB) := orderedPair.injective with firstNew
      have oldRelates := relates.backward with secondOld
      obtain (xInA, zInB) := FunctionBetween.bounds with hf, oldRelates
      rw xIsA at xInA
      contradiction
  . cases secondShape with secondNew | secondOld
    . obtain (xIsA, zIsB) := orderedPair.injective with secondNew
      have oldRelates := relates.backward with firstOld
      obtain (xInA, yInB) := FunctionBetween.bounds with hf, oldRelates
      rw xIsA at xInA
      contradiction
    . have oldFunctional := FunctionBetween.functional with hf
      have firstRelates := relates.backward with firstOld
      have secondRelates := relates.backward with secondOld
      exact oldFunctional with x, y, firstRelates, z, secondRelates

theorem adjoinMap.total (f A B a b : Set)
  requires hf : f : A → B
  shows TotalBetween(adjoinMap(f, a, b), insert(a, A), insert(b, B))
proof
  intros x hx
  have sourceShape := insert.membership.forward with hx
  cases sourceShape with isNew | isOld
  witness b
  constructor
  exact insert.self
  rw isNew
  exact adjoinMap.relates_new
  obtain ⟨y, hyB, hxy⟩ := FunctionBetween.exists_value with hf, isOld
  witness y
  constructor
  exact insert.contains with hyB
  exact adjoinMap.relates_old with hxy

theorem adjoinMap.function (f A B a b : Set)
  requires hf : f : A → B
  requires ha : ¬a ∈ A
  shows adjoinMap(f, a, b) : insert(a, A) → insert(b, B)
proof
  constructor
  exact adjoinMap.relation with hf
  constructor
  exact adjoinMap.functional with hf, ha
  exact adjoinMap.total at f, A, B, a, b with hf

theorem adjoinMap.injective (f A B a b : Set)
  requires hf : InjectiveBetween(f, A, B)
  requires ha : ¬a ∈ A
  requires hb : ¬b ∈ B
  shows InjectiveBetween(adjoinMap(f, a, b), insert(a, A), insert(b, B))
proof
  have oldFunction := Injective.function with hf
  constructor
  . exact adjoinMap.function with oldFunction, ha
  . intros x hx y hy z hz hxz hyz
    unfold relates at hxz
    unfold relates at hyz
    have firstShape := adjoinMap.membership.forward with hxz
    have secondShape := adjoinMap.membership.forward with hyz
    cases firstShape with firstNew | firstOld
    . cases secondShape with secondNew | secondOld
      . obtain (xIsA, zIsB) := orderedPair.injective with firstNew
        obtain (yIsA, zIsBAgain) := orderedPair.injective with secondNew
        rw [xIsA, yIsA]
        rfl
      . obtain (xIsA, zIsB) := orderedPair.injective with firstNew
        have oldRelates := relates.backward with secondOld
        obtain (yInA, zInB) := FunctionBetween.bounds with oldFunction, oldRelates
        rw zIsB at zInB
        contradiction
    . cases secondShape with secondNew | secondOld
      . obtain (yIsA, zIsB) := orderedPair.injective with secondNew
        have oldRelates := relates.backward with firstOld
        obtain (xInA, zInB) := FunctionBetween.bounds with oldFunction, oldRelates
        rw zIsB at zInB
        contradiction
      . have firstRelates := relates.backward with firstOld
        have secondRelates := relates.backward with secondOld
        have xOld := insert.membership.forward with hx
        cases xOld with xWasNew | xInA
        . rw xWasNew at firstRelates
          obtain (aInA, zBound) := FunctionBetween.bounds with oldFunction, firstRelates
          contradiction
        . have yOld := insert.membership.forward with hy
          cases yOld with yWasNew | yInA
          . rw yWasNew at secondRelates
            obtain (aInA, zBound) := FunctionBetween.bounds with oldFunction, secondRelates
            contradiction
          . have zOld := insert.membership.forward with hz
            cases zOld with zWasNew | zInB
            . rw zWasNew at firstRelates
              obtain (xBound, bInB) := FunctionBetween.bounds with oldFunction, firstRelates
              contradiction
            . exact Injective.cancel with hf, xInA, yInA, zInB, firstRelates, secondRelates

theorem adjoinMap.surjective (f A B a b : Set)
  requires hf : SurjectiveBetween(f, A, B)
  requires ha : ¬a ∈ A
  shows SurjectiveBetween(adjoinMap(f, a, b), insert(a, A), insert(b, B))
proof
  constructor
  have oldFunction := Surjective.function with hf
  exact adjoinMap.function with oldFunction, ha
  intros y hy
  have targetShape := insert.membership.forward with hy
  cases targetShape with isNew | isOld
  witness a
  constructor
  exact insert.self
  rw isNew
  exact adjoinMap.relates_new
  rcases hf with (oldFunctionAgain, oldOnto)
  specialize oldOnto with y, isOld
  obtain ⟨x, hxA, hxy⟩ := oldOnto
  witness x
  constructor
  exact insert.contains with hxA
  exact adjoinMap.relates_old with hxy

theorem adjoinMap.bijective (f A B a b : Set)
  requires hf : BijectiveBetween(f, A, B)
  requires ha : ¬a ∈ A
  requires hb : ¬b ∈ B
  shows BijectiveBetween(adjoinMap(f, a, b), insert(a, A), insert(b, B))
proof
  constructor
  . have oldInjective := Bijective.injective with hf
    exact adjoinMap.injective with oldInjective, ha, hb
  . have oldSurjective := Bijective.surjective with hf
    exact adjoinMap.surjective with oldSurjective, ha

-- Injectivity from cancellation on values.
theorem Injective.of_pointwise (f A B : Set)
  requires function : f : A → B
  requires cancel : ∀ x ∈ A, ∀ y ∈ A, f(x) = f(y) → x = y
  shows InjectiveBetween(f, A, B)
proof
  unfold InjectiveBetween
  refine ⟨function, ?_⟩
  intros x hx y hy z hz relatesX relatesY
  have valueX := FunctionBetween.apply_value with function, hx, relatesX
  have valueY := FunctionBetween.apply_value with function, hy, relatesY
  have same : f(x) = f(y)
    rw [valueX, valueY]
    rfl
  exact cancel with x, hx, y, hy, same