-- The continuous image of a compact set is compact: pull a cover back,
-- take a finite subcover, and push each member forward through a chosen
-- original. The choice of originals is the one use of choice in the
-- compactness development
-- 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.Topology.CompactImage
import Compact
import Set.Choice

defgraph originalMap (f X C F : Set) (U ∈ F) : C := choose(originals(f, X, C, U))
requires inside : F ⊆ preimages(f, X, C)
proof
  have hU := inside with U, assumption
  obtain ⟨V, hV, shape⟩ := preimages.membership.forward with hU
  have original : V ∈ originals(f, X, C, U) := originals.membership.backward with ⟨hV, shape⟩
  have inhabited : Nonempty(originals(f, X, C, U)) := ⟨V, original⟩
  have chosen := choose.member with inhabited
  have parts := originals.membership.forward with chosen
  exact parts.left

theorem IsCompact.image (f X T Y S A : Set)
  requires continuous : ContinuousMap(f, X, T, Y, S)
  requires compact : IsCompact(X, T, A)
  shows IsCompact(Y, S, functionImage(f, A, Y))
proof
  have function := continuous.left
  constructor
  . exact functionImage.subset at f, A, Y
  . intros D cover
    have pulledOpen : preimages(f, X, D) ⊆ T
      intros U hU
      obtain ⟨V, hV, shape⟩ := preimages.membership.forward with hU
      rw ← shape
      exact continuous.right with V, (cover.left with V, hV)
    have pulledCover : A ⊆ ⋃(preimages(f, X, D))
      intros a ha
      have haX := compact.left with a, ha
      have value := FunctionBetween.apply_closed with function, haX
      have imageMember : f(a) ∈ functionImage(f, A, Y) by simp [functionImage.membership]
      have covered := cover.right with f(a), imageMember
      obtain ⟨V, hV, inV⟩ := union.membership.forward with covered
      have member : functionPreimage(f, X, V) ∈ preimages(f, X, D) := preimages.membership.backward with ⟨V, hV, rfl⟩
      have inPreimage : a ∈ functionPreimage(f, X, V) := functionPreimage.membership.backward with ⟨haX, inV⟩
      exact union.contains with member, inPreimage
    obtain ⟨F, hF, finiteF, coveredA⟩ := compact.right with preimages(f, X, D), ⟨pulledOpen, pulledCover⟩
    have graph := originalMap.function with hF
    witness functionImage(originalMap(f, X, D, F), F, D)
    refine ⟨(functionImage.subset at originalMap(f, X, D, F), F, D), (Finite.function_image with graph, finiteF, (Subset.reflexive at F)), ?_⟩
    intros y hy
    simp [functionImage.membership] at hy
    obtain ⟨hyY, a, ha, shape⟩ := hy
    have covered := coveredA with a, ha
    obtain ⟨U, hU, haU⟩ := union.membership.forward with covered
    have value := originalMap.value with hF
    have hUP := hF with U, hU
    obtain ⟨V, hV, preimageShape⟩ := preimages.membership.forward with hUP
    have member : V ∈ originals(f, X, D, U) := originals.membership.backward with ⟨hV, preimageShape⟩
    have inhabited : Nonempty(originals(f, X, D, U)) := ⟨V, member⟩
    have chosen := choose.member with inhabited
    have chosenParts := originals.membership.forward with chosen
    rw ← value at chosenParts
    have inChosen : a ∈ functionPreimage(f, X, originalMap(f, X, D, F)(U)) by rwa chosenParts.right
    have hit := functionPreimage.membership.forward with inChosen
    have chosenMember : originalMap(f, X, D, F)(U) ∈ functionImage(originalMap(f, X, D, F), F, D)
      have closed := FunctionBetween.apply_closed with graph, hU
      simp [functionImage.membership]
      constructor
      . exact closed
      . witness U
        constructor
        . exact hU
        . rfl
    rw shape
    exact union.contains with chosenMember, hit.right