-- Prepending a fixed entry to the lists of a set is an injection, so a
-- cons image of a finite set is finite and has the size of its source
-- 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.List.ConsImage
import Basic
import Cardinal.NaturalSum

-- The cons map ys ↦ x :: ys onto the cons image.
defgraph consMap (x S : Set) (ys ∈ S) : consImage(x, S) := x :: ys
proof
  apply consImage.membership.backward
  refine ⟨ys, member, rfl⟩

theorem consMap.injective (x S : Set)
  shows InjectiveBetween(consMap(x, S), S, consImage(x, S))
proof
  have function := consMap.function at x, S
  constructor
  . exact function
  . intros u hu v hv z hz huz hvz
    have uValue := FunctionBetween.apply_value with function, hu, huz
    have vValue := FunctionBetween.apply_value with function, hv, hvz
    have uShape := consMap.value at x, S, u with hu
    have vShape := consMap.value at x, S, v with hv
    have equal : x :: u = x :: v
      rw [← uShape, ← vShape, uValue, vValue]
      rfl
    have parts := List.inductive.injective.cons with equal
    exact parts.right

theorem consMap.image (x S : Set)
  shows functionImage(consMap(x, S), S, consImage(x, S)) = consImage(x, S)
proof
  ext zs
  constructor
  . intro hz
    have parts := functionImage.membership.forward with hz
    exact parts.left
  . intro hz
    obtain ⟨ys, hy, shape⟩ := consImage.membership.forward with hz
    apply functionImage.membership.backward
    constructor
    . exact hz
    . witness ys
      constructor
      . exact hy
      . rw ← shape
        symm
        exact consMap.value at x, S, ys with hy

theorem consImage.finite (x S : Set)
  requires finite : Finite(S)
  shows Finite(consImage(x, S))
proof
  have function := consMap.function at x, S
  have reflexive := Subset.reflexive at S
  have image := Finite.function_image with function, finite, reflexive
  rwa consMap.image at image

theorem consImage.cardinality (x S : Set)
  requires finite : Finite(S)
  shows cardinality(consImage(x, S)) = cardinality(S)
proof
  have injective := consMap.injective at x, S
  have reflexive := Subset.reflexive at S
  have image := cardinality.injective_image with injective, reflexive, finite
  rwa consMap.image at image