/-
Paper to Lean · Cantor's diagonal argument
Georg Cantor, Ueber eine elementare Frage der Mannigfaltigkeitslehre (1891).

Scope: the diagonal construction for infinite sequences of two symbols.
This is a modern reconstruction of the selected argument, not the entire paper.
Lean 4.33.1; only Lean's automatically imported core library is needed.
Run: lean -DwarningAsError=true Cantor.lean
License: MIT (see the project LICENSE).
-/

namespace PaperToLean.Cantor

-- A sequence is an infinite stream of two possible symbols.
abbrev Sequence := Nat → Bool

-- Given a proposed list, flip its nth sequence's nth symbol.
def diagonal (list : Nat → Sequence) : Sequence :=
  fun n => !(list n n)

-- The new sequence differs from each listed sequence at its own index.
theorem diagonal_not_in_list (list : Nat → Sequence) (n : Nat) :
    diagonal list ≠ list n := by
  intro h
  have same := congrArg (fun sequence => sequence n) h
  change (!(list n n)) = list n n at same
  cases value : list n n <;> simp [value] at same

-- Consequently, no natural-number-indexed list contains every sequence.
theorem no_complete_list :
    ¬ ∃ list : Nat → Sequence, ∀ sequence, ∃ n, list n = sequence := by
  intro ⟨list, complete⟩
  obtain ⟨n, equal⟩ := complete (diagonal list)
  exact diagonal_not_in_list list n equal.symm

#print axioms diagonal_not_in_list
#print axioms no_complete_list

end PaperToLean.Cantor