-- The strong form of the Banach–Tarski paradox: the ball is
-- equidecomposable with the disjoint union of two copies of itself
-- 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.Geometry.BanachTarski.Strong
import Geometry.BanachTarski
import Algebra.Group.Paradox.SchroederBernstein

-- The ball embeds in the two balls as a subset, the two balls embed in
-- the ball through the part proved in Geometry.BanachTarski, and the
-- Banach–Schröder–Bernstein theorem turns the two embeddings into a
-- decomposition.
theorem banachTarski.two_balls
  shows Equidecomposable(motionAction, Motions, ℝ³, unitBall,
      unitBall ∪ shiftedBall)
proof
  have action := motionAction.action
  obtain ⟨C, boundedC, part⟩ := banachTarski.two_balls_part
  have shiftedSubset : shiftedBall ⊆ ℝ³
    rw shiftedBall.graph
    exact translate.subset at motionAction, ℝ³,
      (matrixRing(realRing, 3)[1], farPoint), unitBall
  have unionSubset := union2.subset with unitBall.subset, shiftedSubset
  have left := union2.subset_left at unitBall, shiftedBall
  have forward :
      Embeds(motionAction, Motions, ℝ³, unitBall, unitBall ∪ shiftedBall) :=
    Embeds.of_subset with action, unitBall.subset, left
  have back := Equidecomposable.symmetric with action, part
  have backward :
      Embeds(motionAction, Motions, ℝ³, unitBall ∪ shiftedBall, unitBall) :=
    Embeds.of_equidecomposable with action, boundedC, back
  exact Equidecomposable.of_embeddings with action, unitBall.subset,
    unionSubset, forward, backward