FormalConjectures.ErdosProblems.«949»

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Erdős Problem 949

Reference: erdosproblems.com/949

open Cardinal Filteropen scoped Pointwise Topologynamespace Erdos949

Let $S \subseteq \mathbb{R}$ be a set containing no solutions to $a + b = c$. Must there be a set $A \subseteq \mathbb{R} \setminus S$ of cardinality continuum such that $A + A \subseteq \mathbb{R}\setminus S$?

@[category research open, AMS 5]
theorem erdos_949 : answer(sorry) ↔
    ∀ S : Set ℝ, (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Sᶜ, #A = 𝔠 ∧ A + A ⊆ Sᶜ := by⊢ True ↔ ∀ (S : Set ℝ), (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ A + A ⊆ Sᶜ
  sorryAll goals completed! 🐙

Let $S\sub \mathbb{R}$ be a Sidon set. Must there be a set $A\sub \mathbb{R}∖S$ of cardinality continuum such that $A + A \sub \mathbb{R}∖S$?


@[category research solved, AMS 5]
theorem erdos_949.variants.sidon : answer(True) ↔
    ∀ S : Set ℝ, IsSidon S → ∃ A ⊆ Sᶜ, #A = 𝔠 ∧ A + A ⊆ Sᶜ := by⊢ True ↔ ∀ (S : Set ℝ), IsSidon S → ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ A + A ⊆ Sᶜ
  show True ↔ _⊢ True ↔ ∀ (S : Set ℝ), IsSidon S → ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ A + A ⊆ Sᶜ
  simp only [true_iff, Set.add_subset_iff]⊢ ∀ (S : Set ℝ), IsSidon S → ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
  rintro S hSS:Set ℝhS:IsSidon S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
  -- We case on whether `S` has cardinality the continuum or strictly less.
  obtain hS𝔠 | hS𝔠 : #S < 𝔠 ∨ #S = 𝔠 := lt_or_eq_of_le <| byS:Set ℝhS:IsSidon S⊢ #↑S ≤ 𝔠inlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ SᶜinrS:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ simpa using mk_set_le SinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ SᶜinrS:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ SᶜinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ SᶜinrS:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
  -- If `S` has cardinality strictly less than the continuum, then we pick by Zorn `A` maximal
  -- such that both `A` and `A + A` are disjoint from `S`.
  ·inlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ obtain ⟨A, ⟨hAS, hAAS⟩, hAmax⟩ := byS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ?m.62inlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
      refine zorn_subset {A ⊆ Sᶜ | ∀ x ∈ A,∀ y ∈ A, x + y ∉ S} ?_S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ∀ c ⊆ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S},
  IsChain (fun x1 x2 ↦ x1 ⊆ x2) c → ∃ ub ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}, ∀ s ∈ c, s ⊆ ubinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
      simp only [Set.ofPred_and, Set.subset_inter_iff, Set.mem_inter_iff, Set.mem_ofPred_eq, and_imp,
        and_assoc]S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ∀ c ⊆ {a | a ⊆ Sᶜ},
  c ⊆ {a | ∀ x ∈ a, ∀ y ∈ a, x + y ∉ S} →
    IsChain (fun x1 x2 ↦ x1 ⊆ x2) c → ∃ ub ⊆ Sᶜ, (∀ x ∈ ub, ∀ y ∈ ub, x + y ∉ S) ∧ ∀ s ∈ c, s ⊆ ubinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
      refine fun C hCS hSC hC ↦ ⟨_, Set.iUnion₂_subset hCS, ?_, Set.subset_iUnion₂⟩S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠C:Set (Set ℝ)hCS:C ⊆ {a | a ⊆ Sᶜ}hSC:C ⊆ {a | ∀ x ∈ a, ∀ y ∈ a, x + y ∉ S}hC:IsChain (fun x1 x2 ↦ x1 ⊆ x2) C⊢ ∀ x ∈ ⋃ i ∈ C, i, ∀ y ∈ ⋃ i ∈ C, i, x + y ∉ SinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
      simp only [Set.mem_iUnion, exists_prop, forall_exists_index, and_imp]S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠C:Set (Set ℝ)hCS:C ⊆ {a | a ⊆ Sᶜ}hSC:C ⊆ {a | ∀ x ∈ a, ∀ y ∈ a, x + y ∉ S}hC:IsChain (fun x1 x2 ↦ x1 ⊆ x2) C⊢ ∀ (x : ℝ), ∀ x_1 ∈ C, x ∈ x_1 → ∀ (y : ℝ), ∀ x_2 ∈ C, y ∈ x_2 → x + y ∉ SinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
      rintro x A hA hx y B hB hyS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠C:Set (Set ℝ)hCS:C ⊆ {a | a ⊆ Sᶜ}hSC:C ⊆ {a | ∀ x ∈ a, ∀ y ∈ a, x + y ∉ S}hC:IsChain (fun x1 x2 ↦ x1 ⊆ x2) Cx:ℝA:Set ℝhA:A ∈ Chx:x ∈ Ay:ℝB:Set ℝhB:B ∈ Chy:y ∈ B⊢ x + y ∉ SinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
      obtain ⟨D, hD, hAD, hBD⟩ := hC.directedOn _ hA _ hBS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠C:Set (Set ℝ)hCS:C ⊆ {a | a ⊆ Sᶜ}hSC:C ⊆ {a | ∀ x ∈ a, ∀ y ∈ a, x + y ∉ S}hC:IsChain (fun x1 x2 ↦ x1 ⊆ x2) Cx:ℝA:Set ℝhA:A ∈ Chx:x ∈ Ay:ℝB:Set ℝhB:B ∈ Chy:y ∈ BD:Set ℝhD:D ∈ ChAD:A ⊆ DhBD:B ⊆ D⊢ x + y ∉ SinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
      exact hSC hD _ (hAD hx) _ (hBD hy)inlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ SᶜinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
    -- By construction, `A` satisfies all properties except possibly for having size the continuum.
    refine ⟨A, hAS, ?_, hAAS⟩inlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ #↑A = 𝔠
    -- By maximality, `Sᶜ ∩ (S / 2)ᶜ ⊆ A ∪ ⋃ a ∈ A, (S - a)`.
    replace hAmax : Sᶜ ∩ ((· / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (· - a) '' ShAmaxS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' SinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑A = 𝔠
    ·hAmaxS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S simp only [Set.subset_def, Set.mem_inter_iff, Set.mem_compl_iff, Set.mem_image, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, div_eq_iff_mul_eq, mul_two, exists_eq_right',
      Set.mem_union, Set.mem_iUnion, sub_eq_iff_eq_add, exists_eq_right, exists_prop,
      or_iff_not_imp_left, and_imp]hAmaxS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∀ x ∉ S, x + x ∉ S → x ∉ A → ∃ i ∈ A, x + i ∈ S
      rintro x hxS hxxS hxAhAmaxS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ Sx:ℝhxS:x ∉ ShxxS:x + x ∉ ShxA:x ∉ A⊢ ∃ i ∈ A, x + i ∈ S
      by_contra! hxAShAmaxS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ Sx:ℝhxS:x ∉ ShxxS:x + x ∉ ShxA:x ∉ AhxAS:∀ i ∈ A, x + i ∉ S⊢ False
      refine hxA <| hAmax ?_ (Set.subset_insert ..) (Set.mem_insert ..)hAmaxS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ⊆ y → y ⊆ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ Sx:ℝhxS:x ∉ ShxxS:x + x ∉ ShxA:x ∉ AhxAS:∀ i ∈ A, x + i ∉ S⊢ (fun x ↦ x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) (insert x A)
      simpa [Set.insert_subset_iff, forall_and, add_comm _ x, *] using ⟨hxAS, hAAS⟩All goals completed! 🐙
    -- By assumption, `#(Sᶜ ∩ (S / 2)ᶜ) = 𝔠`.
    have hS𝔠' : #↑(Sᶜ ∩ ((· / 2) '' S)ᶜ) = 𝔠hS𝔠'S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠inlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠⊢ #↑A = 𝔠
    ·hS𝔠'S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠 rw [← Set.compl_union,hS𝔠'S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑(S ∪ (fun x ↦ x / 2) '' S)ᶜ = 𝔠hS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑(S ∪ (fun x ↦ x / 2) '' S) < #ℝ mk_compl_of_infinite,hS𝔠'S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #ℝ = 𝔠hS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑(S ∪ (fun x ↦ x / 2) '' S) < #ℝhS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑(S ∪ (fun x ↦ x / 2) '' S) < #ℝ mk_realhS𝔠'S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ 𝔠 = 𝔠hS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑(S ∪ (fun x ↦ x / 2) '' S) < #ℝhS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑(S ∪ (fun x ↦ x / 2) '' S) < #ℝ]hS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑(S ∪ (fun x ↦ x / 2) '' S) < #ℝ
      grw [mk_union_le,hS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑S + #↑((fun x ↦ x / 2) '' S) < #ℝ Cardinal.mk_realhS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑S + #↑((fun x ↦ x / 2) '' S) < 𝔠]hS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑S + #↑((fun x ↦ x / 2) '' S) < 𝔠
      refine add_lt_of_lt aleph0_le_continuum hS𝔠 ?_hS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑((fun x ↦ x / 2) '' S) < 𝔠
      grw [mk_image_lehS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑S < 𝔠]hS𝔠'.h2S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S⊢ #↑S < 𝔠
      exact hS𝔠All goals completed! 🐙
    -- If `#A < 𝔠`, we would then have
    -- `𝔠 = #(Sᶜ ∩ (S / 2)ᶜ) ≤ #(A ∪ ⋃ a ∈ A, (S - a)) ≤ #A + #A * #S < 𝔠`, contradiction.
    refine (mk_real ▸ mk_set_le _).eq_of_not_lt fun hA𝔠 ↦ lt_irrefl 𝔠 ?_inlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠⊢ 𝔠 < 𝔠
    calc
      𝔠 = #↑(Sᶜ ∩ ((· / 2) '' S)ᶜ) := byS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠⊢ 𝔠 = #↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) rw [hS𝔠'S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠⊢ 𝔠 = 𝔠All goals completed! 🐙]All goals completed! 🐙
      _ ≤ #↑(A ∪ ⋃ a ∈ A, (· - a) '' S) := mk_subtype_mono hAmax
      _ ≤ #A + #A * #S := byS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠⊢ #↑(A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S) ≤ #↑A + #↑A * #↑S
        obtain rfl | hA := A.eq_empty_or_nonemptyinlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠hS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hAS:∅ ⊆ SᶜhAAS:∀ x ∈ ∅, ∀ y ∈ ∅, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ ∅ ∪ ⋃ a ∈ ∅, (fun x ↦ x - a) '' ShA𝔠:#↑∅ < 𝔠⊢ #↑(∅ ∪ ⋃ a ∈ ∅, (fun x ↦ x - a) '' S) ≤ #↑∅ + #↑∅ * #↑SinrS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠hA:A.Nonempty⊢ #↑(A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S) ≤ #↑A + #↑A * #↑S
        ·inlS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠hS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hAS:∅ ⊆ SᶜhAAS:∀ x ∈ ∅, ∀ y ∈ ∅, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ ∅ ∪ ⋃ a ∈ ∅, (fun x ↦ x - a) '' ShA𝔠:#↑∅ < 𝔠⊢ #↑(∅ ∪ ⋃ a ∈ ∅, (fun x ↦ x - a) '' S) ≤ #↑∅ + #↑∅ * #↑S simpAll goals completed! 🐙
        have : Nonempty A := hA.coe_sortinrS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠hA:A.Nonemptythis:Nonempty ↑A⊢ #↑(A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' S) ≤ #↑A + #↑A * #↑S
        grw [mk_union_le,inrS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠hA:A.Nonemptythis:Nonempty ↑A⊢ #↑A + #↑(⋃ a ∈ A, (fun x ↦ x - a) '' S) ≤ #↑A + #↑A * #↑S mk_biUnion_le,inrS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠hA:A.Nonemptythis:Nonempty ↑A⊢ #↑A + #↑A * ⨆ x, #↑((fun x_1 ↦ x_1 - ↑x) '' S) ≤ #↑A + #↑A * #↑S ciSup_le fun _ ↦ mk_image_leinrS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x ↦ x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x ↦ x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠hA:A.Nonemptythis:Nonempty ↑A⊢ #↑A + #↑A * #↑S ≤ #↑A + #↑A * #↑S]All goals completed! 🐙
      _ < 𝔠 := add_lt_of_lt aleph0_le_continuum hA𝔠 <| mul_lt_of_lt aleph0_le_continuum hA𝔠 hS𝔠
  -- If `S` has cardinality the continuum, then we pick some `a ≠ 0` in `S` and set
  -- `A := (S \ {a} - a / 2) \ S`.
  have hSinf : S.Infinite := by⊢ True ↔ ∀ (S : Set ℝ), IsSidon S → ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ A + A ⊆ SᶜinrS:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ simpa using aleph0_le_continuum.trans_eq hS𝔠.symminrS:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ SᶜinrS:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
  obtain ⟨a, ha, ha₀⟩ : ∃ a ∈ S, a ≠ 0 := (hSinf.sdiff <| Set.finite_singleton 0).nonemptyinrS:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
  refine ⟨(· - a / 2) '' (S \ {a}) \ S, Set.sdiff_subset_compl .., ?_, ?_⟩inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ #↑((fun x ↦ x - a / 2) '' (S \ {a}) \ S) = 𝔠inr.refine_2S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ ∀ x ∈ (fun x ↦ x - a / 2) '' (S \ {a}) \ S, ∀ y ∈ (fun x ↦ x - a / 2) '' (S \ {a}) \ S, x + y ∈ Sᶜ
  -- Since `S` is Sidon and `a ≠ 0`, `(S - a / 2) ∩ S ⊇ (S \ {a} - a / 2) ∩ S` has at most one
  -- element. In particular, `#A = #(S \ {a} - a / 2) = #S = 𝔠` as wanted.
  ·inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ #↑((fun x ↦ x - a / 2) '' (S \ {a}) \ S) = 𝔠 rw [mk_sdiff_eq_left_of_finite' ((hSinf.sdiff <| Set.finite_singleton _).image
      sub_left_injective.injOn)inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ #↑((fun a_1 ↦ a_1 - a / 2) '' (S \ {a})) = 𝔠inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ ((fun a_1 ↦ a_1 - a / 2) '' (S \ {a}) ∩ S).Finiteinr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ #↑((fun a_1 ↦ a_1 - a / 2) '' (S \ {a})) = 𝔠inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ ((fun a_1 ↦ a_1 - a / 2) '' (S \ {a}) ∩ S).Finite]inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ #↑((fun a_1 ↦ a_1 - a / 2) '' (S \ {a})) = 𝔠inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ ((fun a_1 ↦ a_1 - a / 2) '' (S \ {a}) ∩ S).Finite
    ·inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ #↑((fun a_1 ↦ a_1 - a / 2) '' (S \ {a})) = 𝔠 simp [Cardinal.mk_image_eq sub_left_injective, *]All goals completed! 🐙
    ·inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ ((fun a_1 ↦ a_1 - a / 2) '' (S \ {a}) ∩ S).Finite refine Set.Subsingleton.finite ?_inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ ((fun a_1 ↦ a_1 - a / 2) '' (S \ {a}) ∩ S).Subsingleton
      rintro _ ⟨⟨x, ⟨hx, -⟩, rfl⟩, hxa⟩ _ ⟨⟨y, ⟨hy, -⟩, rfl⟩, hya⟩inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:(fun a_1 ↦ a_1 - a / 2) x ∈ Sy:ℝhy:y ∈ Shya:(fun a_1 ↦ a_1 - a / 2) y ∈ S⊢ (fun a_1 ↦ a_1 - a / 2) x = (fun a_1 ↦ a_1 - a / 2) y
      obtain rfl : x = y := byS:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:(fun a_1 ↦ a_1 - a / 2) x ∈ Sy:ℝhy:y ∈ Shya:(fun a_1 ↦ a_1 - a / 2) y ∈ S⊢ x = yinr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:(fun a_1 ↦ a_1 - a / 2) x ∈ Shy:x ∈ Shya:(fun a_1 ↦ a_1 - a / 2) x ∈ S⊢ (fun a_1 ↦ a_1 - a / 2) x = (fun a_1 ↦ a_1 - a / 2) x
        simpa [ha₀, eq_comm (b := x - _)] using hS _ hya _ hxa _ hx _ hy (byS:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:(fun a_1 ↦ a_1 - a / 2) x ∈ Sy:ℝhy:y ∈ Shya:(fun a_1 ↦ a_1 - a / 2) y ∈ S⊢ (fun a_1 ↦ a_1 - a / 2) y + x = (fun a_1 ↦ a_1 - a / 2) x + yinr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:(fun a_1 ↦ a_1 - a / 2) x ∈ Shy:x ∈ Shya:(fun a_1 ↦ a_1 - a / 2) x ∈ S⊢ (fun a_1 ↦ a_1 - a / 2) x = (fun a_1 ↦ a_1 - a / 2) x ringAll goals completed! 🐙inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:(fun a_1 ↦ a_1 - a / 2) x ∈ Shy:x ∈ Shya:(fun a_1 ↦ a_1 - a / 2) x ∈ S⊢ (fun a_1 ↦ a_1 - a / 2) x = (fun a_1 ↦ a_1 - a / 2) x)inr.refine_1S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:(fun a_1 ↦ a_1 - a / 2) x ∈ Shy:x ∈ Shya:(fun a_1 ↦ a_1 - a / 2) x ∈ S⊢ (fun a_1 ↦ a_1 - a / 2) x = (fun a_1 ↦ a_1 - a / 2) x
      rflAll goals completed! 🐙
  -- Since `S` is Sidon, `S \ {a} + S \ {a} - a ⊇ A + A` is disjoint from `S`, as wanted.
  ·inr.refine_2S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0⊢ ∀ x ∈ (fun x ↦ x - a / 2) '' (S \ {a}) \ S, ∀ y ∈ (fun x ↦ x - a / 2) '' (S \ {a}) \ S, x + y ∈ Sᶜ rintro _ ⟨⟨x, ⟨hx, hxa⟩, rfl⟩, -⟩ _ ⟨⟨y, ⟨hy, hya⟩, rfl⟩, -⟩ hxyinr.refine_2S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:x ∉ {a}y:ℝhy:y ∈ Shya:y ∉ {a}hxy:(fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∈ S⊢ False
    have := hS _ hx _ ha _ hy _ hxy (byS:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:x ∉ {a}y:ℝhy:y ∈ Shya:y ∉ {a}hxy:(fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∈ S⊢ x + y = a + ((fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y)inr.refine_2S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:x ∉ {a}y:ℝhy:y ∈ Shya:y ∉ {a}hxy:(fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∈ Sthis:x = a ∧ y = (fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∨ x = (fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∧ y = a⊢ False ringAll goals completed! 🐙inr.refine_2S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:x ∉ {a}y:ℝhy:y ∈ Shya:y ∉ {a}hxy:(fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∈ Sthis:x = a ∧ y = (fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∨ x = (fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∧ y = a⊢ False)inr.refine_2S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinitea:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:x ∉ {a}y:ℝhy:y ∈ Shya:y ∉ {a}hxy:(fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∈ Sthis:x = a ∧ y = (fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∨ x = (fun x ↦ x - a / 2) x + (fun x ↦ x - a / 2) y ∧ y = a⊢ False
    simp_allAll goals completed! 🐙

end Erdos949