-- Uncountability of the Dedekind reals - Final
-- 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.Real.Uncountable.Final
import Encoding
import Cardinal.Countable

-- The Cantor-space embedding X ↦ cantorReal(X).
def cantorEmbedding : Set :=
  { p ∈ 𝒫(ℕ) × ℝ | ∃ X ∈ 𝒫(ℕ), p = (X ↦ cantorReal(X)) }

theorem cantorEmbedding.relates (X A : Set)
  shows relates(cantorEmbedding, X, A) ↔
    (X ∈ 𝒫(ℕ) ∧ A = cantorReal(X))
proof
  constructor
  . intro related
    unfold relates at related
    simp [cantorEmbedding.membership] at related
    rcases related with ⟨bounded, Y, yInPower, shape⟩
    obtain ⟨xShape, aShape⟩ := orderedPair.injective with shape
    constructor
    . rw xShape
      exact yInPower
    . rw xShape
      exact aShape
  . intro data
    rcases data with ⟨xInPower, rfl⟩
    unfold relates
    apply cantorEmbedding.membership.backward
    constructor
    . apply product.pair at X, cantorReal(X), 𝒫(ℕ), ℝ
      . exact xInPower
      . exact cantorReal.real at X
    . witness X
      constructor
      . exact xInPower
      . rfl

theorem cantorEmbedding.total
  shows TotalBetween(cantorEmbedding, 𝒫(ℕ), ℝ)
proof
  intros X xInPower
  witness cantorReal(X)
  constructor
  . exact cantorReal.real at X
  . apply cantorEmbedding.relates.backward at X, cantorReal(X)
    constructor
    . exact xInPower
    . rfl

theorem cantorEmbedding.functional
  shows Functional(cantorEmbedding)
proof
  intros X A xA B xB
  have first := cantorEmbedding.relates.forward with xA
  have second := cantorEmbedding.relates.forward with xB
  rcases first with ⟨_, aShape⟩
  rcases second with ⟨_, bShape⟩
  have reverseB : cantorReal(X) = B
    rw bShape
    rfl
  calc
    A = cantorReal(X) := aShape
    _ = B := reverseB

theorem cantorEmbedding.function
  shows cantorEmbedding : 𝒫(ℕ) → ℝ
proof
  constructor
    intros p member
    obtain ⟨bounded, witnesses⟩ := cantorEmbedding.membership.forward with member
    exact bounded
  . constructor
    . exact cantorEmbedding.functional
    . exact cantorEmbedding.total

theorem cantorEmbedding.injective
  shows InjectiveBetween(cantorEmbedding, 𝒫(ℕ), ℝ)
proof
  constructor
  . exact cantorEmbedding.function
  . intros X xInPower Y yInPower A aInReal xMaps yMaps
    have xData := cantorEmbedding.relates.forward with xMaps
    have yData := cantorEmbedding.relates.forward with yMaps
    rcases xData with ⟨_, xShape⟩
    rcases yData with ⟨_, yShape⟩
    have reverseX : cantorReal(X) = A
      rw xShape
      rfl
    have sameReals : cantorReal(X) = cantorReal(Y)
      calc
        cantorReal(X) = A := reverseX
        _ = cantorReal(Y) := yShape
    have subsetX := powerset.membership_iff.forward with xInPower
    have subsetY := powerset.membership_iff.forward with yInPower
    exact cantorReal.injective with subsetX, subsetY, sameReals

theorem reals.uncountable
  shows Uncountable(ℝ)
proof
  unfold Uncountable
  intro countable
  obtain ⟨f, realsIntoNaturals⟩ := countable
  have powersetIntoReals := cantorEmbedding.injective
  have composite := compose.injective with powersetIntoReals, realsIntoNaturals
  exact powerset.naturals_not_injects_into_naturals with composite