Erdos494 (https://www.erdosproblems.com/494)

494.lean

import Mathlib

open Filter

namespace Erdos494

/--
For a finite set $A \subset \mathbb{C}$ and $k \ge 1$, define $A_k$ as a multiset consisting of
all sums of $k$ distinct elements of $A$.
-/
noncomputable def erdos494_A_k (A : Finset ℂ) (k : ℕ) : Multiset ℂ :=
  ((A.powersetCard k).val.map (fun s => s.sum id))

def erdos_494_unique (k : ℕ) (card : ℕ) :=
  ∀ A B : Finset ℂ, A.card = card → A.card = B.card → erdos494_A_k A k = erdos494_A_k B k → A = B

/--
Selfridge and Straus [SeSt58] showed that the conjecture is true when $k = 2$ and
$|A| \ne 2^l$ for $l \ge 0$.
They also gave counterexamples when $k = 2$ and $|A| = 2^l$.
-/
theorem erdos_494.variant.k_eq_2_card_not_pow_two :
    ∀ card : ℕ, (¬∃ l : ℕ, card = 2 ^ l) → erdos_494_unique 2 card := by
  sorry

theorem erdos_494.variant.k_eq_2_card_pow_two :
    ∀ card : ℕ, (∃ l : ℕ, card = 2 ^ l) → ¬erdos_494_unique 2 card := by
  sorry

/--
Selfridge and Straus [SeSt58] also showed that the conjecture is true when
1) $k = 3$ and $|A| > 6$ or
2) $k = 4$ and $|A| > 12$.
More generally, they proved that $A$ is determined by $A_k$ (and $|A|$) if $|A|$ is divisible by
a prime greater than $k$.
-/
theorem erdos_494.variant.k_eq_3_card_gt_6 :
    ∀ card : ℕ, 6 < card → erdos_494_unique 3 card := by
  sorry

theorem erdos_494.variant.k_eq_4_card_gt_12 :
    ∀ card : ℕ, 12 < card → erdos_494_unique 4 card := by
  sorry

theorem erdos_494.variant.card_divisible_by_prime_gt_k :
    ∀ (k card : ℕ), ∃ p : ℕ, p.Prime ∧ k < p ∧ p ∣ card → erdos_494_unique k card := by
  sorry

/--
Kruyt noted that the conjecture fails when $|A| = k$, by rotating $A$ around an appropriate point.
-/
theorem erdos_494.variant.k_eq_card :
    ∀ k : ℕ, 2 < k → ¬erdos_494_unique k k := by
  sorry

/--
Similarly, Tao noted that the conjecture fails when $|A| = 2k$, by taking $A$ to be a set of
the total sum 0 and considering $-A$.
-/
theorem erdos_494.variant.card_eq_2k :
    ∀ k : ℕ, 2 < k → ¬erdos_494_unique k (2 * k) := by
  sorry

/--
Gordon, Fraenkel, and Straus [GRS62] proved that the claim is true for all $k > 2$ when
$|A|$ is sufficiently large.
-/
theorem erdos_494.variant.gordon_fraenkel_straus :
    ∀ k : ℕ, 2 < k → (∀ᶠ card in atTop, erdos_494_unique k card) := by
  sorry

/--
A version in [Er61] by Erdős is product instead of sum, which is false.
Counterexample (by Steinerberger): consider $k = 3$ and let
$A = \{1, \zeta_6, \zeta_6^2, \zeta_6^4\}$ and $B = \{1, \zeta_6^2, \zeta_6^3, \zeta_6^4\}$.
-/
noncomputable def erdos494_A_k_prod (A : Finset ℂ) (k : ℕ) : Multiset ℂ :=
  ((A.powersetCard k).val.map (fun s => s.prod id))

theorem erdos_494.variant.product :
    ∃ (A B : Finset ℂ), A.card = B.card ∧ erdos494_A_k_prod A 3 = erdos494_A_k_prod B 3 ∧
    A ≠ B := by
  sorry

end Erdos494

494_aristotle.lean

/-
This file was edited by Aristotle.

Lean version: leanprover/lean4:v4.24.0
Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7
This project request had uuid:

The following was proved by Aristotle:

- theorem erdos_494.variant.k_eq_2_card_not_pow_two :
    ∀ card : ℕ, (¬∃ l : ℕ, card = 2 ^ l) → erdos_494_unique 2 card

- theorem erdos_494.variant.k_eq_2_card_pow_two :
    ∀ card : ℕ, (∃ l : ℕ, card = 2 ^ l) → ¬erdos_494_unique 2 card

- theorem erdos_494.variant.card_divisible_by_prime_gt_k :
    ∀ (k card : ℕ), ∃ p : ℕ, p.Prime ∧ k < p ∧ p ∣ card → erdos_494_unique k card
-/

import Mathlib


open Filter

namespace Erdos494

/--
For a finite set $A \subset \mathbb{C}$ and $k \ge 1$, define $A_k$ as a multiset consisting of
all sums of $k$ distinct elements of $A$.
-/
noncomputable def erdos494_A_k (A : Finset ℂ) (k : ℕ) : Multiset ℂ :=
  ((A.powersetCard k).val.map (fun s => s.sum id))

def erdos_494_unique (k : ℕ) (card : ℕ) :=
  ∀ A B : Finset ℂ, A.card = card → A.card = B.card → erdos494_A_k A k = erdos494_A_k B k → A = B

/-
Selfridge and Straus [SeSt58] showed that the conjecture is true when $k = 2$ and
$|A| \ne 2^l$ for $l \ge 0$.
They also gave counterexamples when $k = 2$ and $|A| = 2^l$.
-/
noncomputable section AristotleLemmas

/-
Define `expsum` as the sum of exponentials $\sum_{a \in A} e^{az}$.
-/
noncomputable def Erdos494.expsum (A : Finset ℂ) (z : ℂ) : ℂ := ∑ a ∈ A, Complex.exp (a * z)

/-
The square of the exponential sum is equal to the exponential sum at $2z$ plus twice the sum of exponentials of pair sums.
-/
lemma Erdos494.expsum_sq (A : Finset ℂ) (z : ℂ) :
    (Erdos494.expsum A z) ^ 2 = Erdos494.expsum A (2 * z) + 2 * ∑ s ∈ A.powersetCard 2, Complex.exp (s.sum id * z) := by
  -- Expand the square of the exponential sum.
  have h_expand : (∑ a ∈ A, Complex.exp (a * z))^2 = ∑ a ∈ A, Complex.exp (2 * a * z) + 2 * ∑ a ∈ A, ∑ b ∈ A, (if a ≠ b then Complex.exp ((a + b) * z) else 0) / 2 := by
    norm_num [ pow_two, Finset.sum_add_distrib, mul_add, add_mul, mul_assoc, Finset.mul_sum _ _ _, Finset.sum_mul _ _ _, Complex.exp_add ];
    norm_num [ Finset.sum_ite, Finset.filter_ne, two_mul ];
    simp +decide [ ← Finset.sum_add_distrib, ← Complex.exp_add ];
    exact Finset.sum_congr rfl fun x hx => by rw [ ← Finset.sum_erase_add _ _ hx ] ; simp +decide [ add_comm ] ;
  -- Recognize that the double sum over pairs (a, b) with a ≠ b is equivalent to the sum over all 2-element subsets of A.
  have h_double_sum : ∑ a ∈ A, ∑ b ∈ A, (if a ≠ b then Complex.exp ((a + b) * z) else 0) = ∑ s ∈ Finset.powersetCard 2 A, ∑ a ∈ s, ∑ b ∈ s, (if a ≠ b then Complex.exp ((a + b) * z) else 0) := by
    have h_pairwise : ∑ a ∈ A, ∑ b ∈ A, (if a ≠ b then Complex.exp ((a + b) * z) else 0) = ∑ s ∈ Finset.powersetCard 2 A, ∑ a ∈ s, ∑ b ∈ s, (if a ≠ b then Complex.exp ((a + b) * z) else 0) := by
      have h_partition : ∀ a ∈ A, ∑ b ∈ A, (if a ≠ b then Complex.exp ((a + b) * z) else 0) = ∑ s ∈ Finset.powersetCard 2 A, (if a ∈ s then ∑ b ∈ s, (if a ≠ b then Complex.exp ((a + b) * z) else 0) else 0) := by
        intros a ha
        have h_partition : ∑ b ∈ A, (if a ≠ b then Complex.exp ((a + b) * z) else 0) = ∑ s ∈ Finset.powersetCard 2 A, (if a ∈ s then ∑ b ∈ s, (if a ≠ b then Complex.exp ((a + b) * z) else 0) else 0) := by
          have h_partition : Finset.filter (fun b => a ≠ b) A = Finset.biUnion (Finset.powersetCard 2 A) (fun s => if a ∈ s then s.erase a else ∅) := by
            ext b;
            simp +zetaDelta at *;
            constructor;
            · exact fun h => ⟨ { a, b }, ⟨ by aesop_cat, by aesop_cat ⟩, by aesop_cat ⟩;
            · aesop
          rw [ ← Finset.sum_filter, h_partition, Finset.sum_biUnion ];
          · refine' Finset.sum_congr rfl fun s hs => _;
            split_ifs <;> simp_all +decide [ Finset.sum_ite, Finset.filter_ne ];
          · intro s hs t ht hst; simp_all +decide [ Finset.disjoint_left ] ;
            split_ifs <;> simp_all +decide [ Finset.subset_iff ];
            intro x hx₁ hx₂ hx₃; have := Finset.eq_of_subset_of_card_le ( Finset.insert_subset hx₂ ( Finset.singleton_subset_iff.mpr ‹a ∈ s› ) ) ; have := Finset.eq_of_subset_of_card_le ( Finset.insert_subset hx₃ ( Finset.singleton_subset_iff.mpr ‹a ∈ t› ) ) ; aesop;
        convert h_partition using 1
      rw [ Finset.sum_congr rfl h_partition, Finset.sum_comm ];
      refine' Finset.sum_congr rfl fun s hs => _;
      rw [ ← Finset.sum_filter ] ; congr ; ext ; aesop;
    convert h_pairwise using 1;
  -- Notice that $\sum_{a \in s} \sum_{b \in s} (if a \neq b then \exp((a + b)z) else 0)$ simplifies to $\exp((a + b)z)$ for each $s \in \text{powersetCard } 2 A$.
  have h_inner_sum : ∀ s ∈ Finset.powersetCard 2 A, ∑ a ∈ s, ∑ b ∈ s, (if a ≠ b then Complex.exp ((a + b) * z) else 0) = 2 * Complex.exp ((s.sum id) * z) := by
    intro s hs; rw [ Finset.mem_powersetCard ] at hs; rcases Finset.card_eq_two.mp hs.2 with ⟨ a, b, ha, hb, hab ⟩ ; simp +decide [ *, Finset.sum_pair ] ; ring;
    rw [ if_neg ha.symm ] ; ring;
  unfold Erdos494.Erdos494.expsum; simp_all +decide [ Finset.sum_div _ _ _, mul_assoc, mul_left_comm, div_eq_mul_inv ] ;
  simp_all +decide [ Finset.sum_ite, Finset.mul_sum _ _ _, mul_assoc, mul_comm, mul_left_comm ];
  simp_all +decide [ ← Finset.sum_mul _ _ _ ];
  rw [ Finset.sum_mul _ _ _ ] ; exact Finset.sum_congr rfl fun x hx => by rw [ h_inner_sum x ( Finset.mem_powersetCard.mp hx |>.1 ) ( Finset.mem_powersetCard.mp hx |>.2 ) ] ; ring;

/-
If the multisets of pair sums are equal, then the sums of exponentials of pair sums are equal.
-/
lemma Erdos494.expsum_pair_sum_eq {A B : Finset ℂ} (h : Erdos494.erdos494_A_k A 2 = Erdos494.erdos494_A_k B 2) (z : ℂ) :
    ∑ s ∈ A.powersetCard 2, Complex.exp (s.sum id * z) = ∑ t ∈ B.powersetCard 2, Complex.exp (t.sum id * z) := by
  -- Since the multisets of pair sums are equal, their sums are equal.
  have h_sum_eq : Multiset.sum (Multiset.map (fun x => Complex.exp (x * z)) (erdos494_A_k A 2)) = Multiset.sum (Multiset.map (fun x => Complex.exp (x * z)) (erdos494_A_k B 2)) := by
    rw [h];
  convert h_sum_eq using 1;
  · unfold Erdos494.erdos494_A_k; aesop;
  · unfold Erdos494.erdos494_A_k; aesop;

/-
Define `powerSum` as the sum of k-th powers of elements in A.
-/
noncomputable def Erdos494.powerSum (A : Finset ℂ) (k : ℕ) : ℂ := ∑ a ∈ A, a ^ k

/-
The n-th derivative of $e^{cz}$ at 0 is $c^n$.
-/
lemma Erdos494.iteratedDeriv_exp_const_mul (c : ℂ) (n : ℕ) :
    iteratedDeriv n (fun z => Complex.exp (c * z)) 0 = c ^ n := by
  aesop

/-
The n-th derivative of `expsum A` at 0 is the n-th power sum of A.
-/
lemma Erdos494.expsum_iteratedDeriv (A : Finset ℂ) (n : ℕ) :
    iteratedDeriv n (Erdos494.expsum A) 0 = Erdos494.powerSum A n := by
  -- By definition of `Erdos494.expsum`, we have `Erdos494.expsum A = ∑ a ∈ A, Complex.exp (a * _)`.
  have h_expsum_def : Erdos494.Erdos494.expsum A = ∑ a ∈ A, fun z => Complex.exp (a * z) := by
    ext; simp +decide [ Erdos494.Erdos494.expsum ];
  -- Apply the linearity of the iterated derivative.
  have h_linear : iteratedDeriv n (∑ a ∈ A, fun z => Complex.exp (a * z)) = ∑ a ∈ A, iteratedDeriv n (fun z => Complex.exp (a * z)) := by
    induction' n with n ih generalizing A <;> simp_all +decide [ iteratedDeriv_succ ];
    ext; erw [ deriv_sum ] ; aesop;
    exact fun _ _ => DifferentiableAt.const_mul ( Complex.differentiableAt_exp.comp _ ( differentiableAt_id.const_mul _ ) ) _;
  aesop

/-
The n-th derivative of `expsum A (2z)` at 0 is $2^n$ times the n-th power sum of A.
-/
lemma Erdos494.expsum_two_mul_iteratedDeriv (A : Finset ℂ) (n : ℕ) :
    iteratedDeriv n (fun z => Erdos494.expsum A (2 * z)) 0 = (2 : ℂ) ^ n * Erdos494.powerSum A n := by
  rw [ iteratedDeriv_eq_iterate ];
  -- By definition of the exponential sum, we have:
  have h_expsum : deriv^[n] (fun z => Erdos494.Erdos494.expsum A (2 * z)) = fun z => ∑ a ∈ A, Complex.exp (a * (2 * z)) * (2 * a) ^ n := by
    induction' n with n ih;
    · aesop;
    · rw [ Function.iterate_succ_apply', ih ];
      ext; norm_num [ mul_pow, mul_assoc, mul_comm, mul_left_comm ];
      exact Finset.sum_congr rfl fun _ _ => by ring;
  simp_all +decide [ mul_pow, mul_comm, mul_left_comm, Finset.mul_sum _ _ _, Erdos494.Erdos494.powerSum ]

/-
If two finite sets of complex numbers have the same power sums for all k, they are equal.
-/
lemma Erdos494.power_sums_inj (A B : Finset ℂ) :
    (∀ k, Erdos494.powerSum A k = Erdos494.powerSum B k) → A = B := by
  intro h;
  have h_multiset : ∀ (m n : Multiset ℂ), (∀ k : ℕ, Multiset.sum (Multiset.map (fun x => x ^ k) m) = Multiset.sum (Multiset.map (fun x => x ^ k) n)) → m = n := by
    intro m n hmn
    have h_poly : ∀ p : Polynomial ℂ, Multiset.sum (Multiset.map (fun x => p.eval x) m) = Multiset.sum (Multiset.map (fun x => p.eval x) n) := by
      intro p
      have h_poly_eq : ∀ k : ℕ, Multiset.sum (Multiset.map (fun x => x ^ k) m) = Multiset.sum (Multiset.map (fun x => x ^ k) n) := by
        assumption;
      simp_all +decide [ Polynomial.eval_eq_sum_range ];
      induction' p.natDegree with d hd <;> simp_all +decide [ Finset.sum_range_succ ];
      · specialize h_poly_eq 0 ; aesop;
      · simp_all +decide [ Multiset.sum_map_mul_left, Multiset.sum_map_mul_right ];
    have h_poly_eq : ∀ x : ℂ, Multiset.count x m = Multiset.count x n := by
      intro x
      by_contra h_neq;
      -- Consider the polynomial $p(t) = \prod_{y \in m \cup n, y \neq x} (t - y)$.
      set p : Polynomial ℂ := Finset.prod (Multiset.toFinset (m + n) \ {x}) (fun y => Polynomial.X - Polynomial.C y);
      -- Since $p(x) \neq 0$, we have $p.eval x \neq 0$.
      have h_p_eval_x_ne_zero : p.eval x ≠ 0 := by
        simp [p, Polynomial.eval_prod];
        exact Finset.prod_ne_zero_iff.mpr fun y hy => sub_ne_zero_of_ne <| by aesop;
      -- Since $p(y) = 0$ for all $y \in m \cup n$ except $x$, we have $\sum_{y \in m} p(y) = p(x) \cdot \text{count}(x, m)$ and $\sum_{y \in n} p(y) = p(x) \cdot \text{count}(x, n)$.
      have h_sum_p_m : Multiset.sum (Multiset.map (fun y => p.eval y) m) = p.eval x * Multiset.count x m := by
        have h_sum_p_m : ∀ y ∈ m, p.eval y = if y = x then p.eval x else 0 := by
          intro y hy; split_ifs <;> simp_all +decide [ Polynomial.eval_prod, Finset.prod_eq_zero_iff, sub_eq_zero ] ;
          rw [ Polynomial.eval_prod, Finset.prod_eq_zero ( Finset.mem_sdiff.mpr ⟨ Multiset.mem_toFinset.mpr ( Multiset.mem_add.mpr ( Or.inl hy ) ), by aesop ⟩ ) ] ; aesop;
        rw [ Multiset.map_congr rfl h_sum_p_m ] ; norm_num [ mul_comm ];
        rw [ Multiset.sum_map_eq_nsmul_single x ] <;> aesop
      have h_sum_p_n : Multiset.sum (Multiset.map (fun y => p.eval y) n) = p.eval x * Multiset.count x n := by
        have h_sum_p_n : ∀ y ∈ n, y ≠ x → p.eval y = 0 := by
          simp +zetaDelta at *;
          exact fun y hy hyx => by rw [ Polynomial.eval_prod ] ; exact Finset.prod_eq_zero ( Finset.mem_sdiff.mpr ⟨ Finset.mem_union_right _ ( Multiset.mem_toFinset.mpr hy ), by aesop ⟩ ) ( by aesop ) ;
        have h_sum_p_n : Multiset.sum (Multiset.map (fun y => p.eval y) n) = Multiset.sum (Multiset.map (fun y => if y = x then p.eval x else 0) n) := by
          exact congr_arg _ ( Multiset.map_congr rfl fun y hy => by by_cases hyx : y = x <;> aesop );
        simp_all +decide [ mul_comm, Multiset.sum_map_mul_right ];
        have h_sum_p_n : Multiset.sum (Multiset.map (fun y => if y = x then p.eval x else 0) n) = p.eval x * Multiset.count x n := by
          rw [ mul_comm, Multiset.sum_map_eq_nsmul_single x ] <;> aesop;
        exact h_neq ( by rw [ mul_comm ] at h_sum_p_n; aesop );
      exact h_neq <| by simpa [ h_p_eval_x_ne_zero, mul_comm ] using h_sum_p_m.symm.trans ( h_poly p ) |> Eq.trans <| h_sum_p_n;
    ext x; specialize h_poly_eq x; aesop;
  exact?

/-
The n-th derivative of f(cz) at 0 is c^n times the n-th derivative of f at 0.
-/
lemma Erdos494.iteratedDeriv_comp_const_mul (f : ℂ → ℂ) (c : ℂ) (n : ℕ) :
    iteratedDeriv n (fun z => f (c * z)) 0 = c ^ n * iteratedDeriv n f 0 := by
  -- By induction on $n$, we can show that the $n$-th derivative of $f(cz)$ is $c^n$ times the $n$-th derivative of $f$ evaluated at $cz$.
  have h_ind : ∀ n : ℕ, deriv^[n] (fun z => f (c * z)) = fun z => c^n * deriv^[n] f (c * z) := by
    intro n; induction' n with n ih <;> simp_all +decide [ Function.iterate_succ_apply', mul_assoc ] ;
    ext z; by_cases hc : c = 0 <;> simp +decide [ hc, pow_succ, mul_assoc, mul_comm c ] ;
    by_cases h : DifferentiableAt ℂ ( deriv^[n] f ) ( z * c ) <;> simp_all +decide [ mul_comm c ];
    · convert HasDerivAt.deriv ( HasDerivAt.comp z ( h.hasDerivAt ) ( hasDerivAt_mul_const c ) ) using 1;
    · rw [ deriv_zero_of_not_differentiableAt ];
      · rw [ deriv_zero_of_not_differentiableAt h, MulZeroClass.zero_mul ];
      · contrapose! h;
        have h_diff : DifferentiableAt ℂ (fun x => deriv^[n] f (x * c)) (z * c / c) := by
          aesop;
        convert h_diff.comp ( z * c ) ( differentiableAt_id.div_const c ) using 1 ; aesop;
  simp +decide [ h_ind, iteratedDeriv_eq_iterate ]

/-
The Leibniz rule for iterated derivatives of a product of smooth functions.
-/
lemma Erdos494.iteratedDeriv_mul (f g : ℂ → ℂ) (n : ℕ)
    (hf : ContDiff ℂ ⊤ f) (hg : ContDiff ℂ ⊤ g) :
    iteratedDeriv n (f * g) = fun z => ∑ k ∈ Finset.range (n + 1), (Nat.choose n k : ℂ) * iteratedDeriv k f z * iteratedDeriv (n - k) g z := by
  induction' n with n ih generalizing f g;
  · aesop;
  · -- Apply the product rule to each term in the sum.
    have h_prod_rule : deriv (fun z => ∑ k ∈ Finset.range (n + 1), Nat.choose n k * iteratedDeriv k f z * iteratedDeriv (n - k) g z) = fun z => ∑ k ∈ Finset.range (n + 1), Nat.choose n k * iteratedDeriv (k + 1) f z * iteratedDeriv (n - k) g z + ∑ k ∈ Finset.range (n + 1), Nat.choose n k * iteratedDeriv k f z * iteratedDeriv (n - k + 1) g z := by
      ext z;
      convert HasDerivAt.deriv ( HasDerivAt.sum fun i hi => ?_ ) using 1;
      congr! 1;
      exact?;
      rw [ ← Finset.sum_add_distrib ];
      convert HasDerivAt.mul ( HasDerivAt.mul ( hasDerivAt_const _ _ ) ( hasDerivAt_deriv_iff.mpr _ ) ) ( hasDerivAt_deriv_iff.mpr _ ) using 1;
      · norm_num [ iteratedDeriv_succ ];
      · apply_rules [ ContDiff.differentiable_iteratedDeriv, hf, hg ];
        exact WithTop.coe_lt_top _;
      · apply_rules [ ContDiff.differentiable_iteratedDeriv, hf, hg ];
        exact WithTop.coe_lt_top _;
    rw [ iteratedDeriv_succ ];
    ext z; rw [ ih f g hf hg, h_prod_rule ] ; rw [ Finset.sum_range_succ, Finset.sum_range_succ' ] ; simp +decide [ Nat.choose_succ_succ, mul_assoc, mul_comm, mul_left_comm, Finset.sum_add_distrib ] ;
    rw [ Finset.sum_range_succ, Finset.sum_range_succ' ] ; simp +decide [ mul_add, add_mul, mul_assoc, mul_comm, mul_left_comm, Finset.sum_add_distrib ];
    rw [ show ( ∑ x ∈ Finset.range n, iteratedDeriv ( x + 1 ) f z * ( iteratedDeriv ( n - ( x + 1 ) + 1 ) g z * ( n.choose ( x + 1 ) : ℂ ) ) ) = ∑ x ∈ Finset.range n, iteratedDeriv ( n - x ) g z * ( iteratedDeriv ( x + 1 ) f z * ( n.choose ( x + 1 ) : ℂ ) ) from Finset.sum_congr rfl fun x hx => by rw [ tsub_add_eq_add_tsub ( by linarith [ Finset.mem_range.mp hx ] ) ] ; simp +decide [ mul_assoc, mul_comm, mul_left_comm ] ] ; ring

/-
If the first m-1 derivatives of f at 0 vanish, then (fg)^(m)(0) = f^(m)(0) g(0).
-/
lemma Erdos494.iteratedDeriv_mul_eq_of_vanish (f g : ℂ → ℂ) (m : ℕ)
    (hf : ContDiff ℂ ⊤ f) (hg : ContDiff ℂ ⊤ g)
    (h_vanish : ∀ k < m, iteratedDeriv k f 0 = 0) :
    iteratedDeriv m (f * g) 0 = (iteratedDeriv m f 0) * (g 0) := by
  rw [ iteratedDeriv_mul _ _ ];
  · simp +decide [ Finset.sum_range_succ, h_vanish ];
    exact Finset.sum_eq_zero fun k hk => by rw [ h_vanish k ( Finset.mem_range.mp hk ) ] ; ring;
  · exact hf;
  · assumption

end AristotleLemmas

theorem erdos_494.variant.k_eq_2_card_not_pow_two :
    ∀ card : ℕ, (¬∃ l : ℕ, card = 2 ^ l) → erdos_494_unique 2 card := by
  intro card hnot_pow_two
  intro A B hA_card hB_card hsum_eq
  by_contra hneq;
  -- Let $m$ be the minimal $k$ such that $powerSum A k \neq powerSum B k$.
  obtain ⟨m, hm⟩ : ∃ m : ℕ, (Erdos494.powerSum A m ≠ Erdos494.powerSum B m) ∧ (∀ k < m, Erdos494.powerSum A k = Erdos494.powerSum B k) := by
    have h_exists_m : ∃ m : ℕ, Erdos494.powerSum A m ≠ Erdos494.powerSum B m := by
      exact not_forall.mp fun h => hneq <| Erdos494.power_sums_inj A B h;
    exact ⟨ Nat.find h_exists_m, Nat.find_spec h_exists_m, fun k hk => by aesop ⟩;
  -- Differentiate the functional equation $m$ times at $z=0$.
  have h_diff : (iteratedDeriv m (fun z => (Erdos494.expsum A z - Erdos494.expsum B z) * (Erdos494.expsum A z + Erdos494.expsum B z)) 0) = (iteratedDeriv m (fun z => Erdos494.expsum A (2 * z) - Erdos494.expsum B (2 * z)) 0) := by
    congr with z;
    have := Erdos494.expsum_sq A z; have := Erdos494.expsum_sq B z; have := Erdos494.expsum_pair_sum_eq hsum_eq z; ring_nf at *; aesop;
  -- By `iteratedDeriv_mul_eq_of_vanish`, this equals `(iteratedDeriv m h 0) * (f_A(0) + f_B(0))`.
  have h_lhs : (iteratedDeriv m (fun z => (Erdos494.expsum A z - Erdos494.expsum B z) * (Erdos494.expsum A z + Erdos494.expsum B z)) 0) = (iteratedDeriv m (fun z => Erdos494.expsum A z - Erdos494.expsum B z) 0) * (Erdos494.expsum A 0 + Erdos494.expsum B 0) := by
    apply Erdos494.iteratedDeriv_mul_eq_of_vanish;
    · exact ContDiff.sub ( ContDiff.sum fun _ _ => Complex.contDiff_exp.comp ( contDiff_const.mul contDiff_id ) ) ( ContDiff.sum fun _ _ => Complex.contDiff_exp.comp ( contDiff_const.mul contDiff_id ) );
    · exact ContDiff.add ( ContDiff.sum fun _ _ => Complex.contDiff_exp.comp ( contDiff_const.mul contDiff_id ) ) ( ContDiff.sum fun _ _ => Complex.contDiff_exp.comp ( contDiff_const.mul contDiff_id ) );
    · intro k hk; have := hm.2 k hk; simp_all +decide [ sub_eq_iff_eq_add ] ;
      -- By `expsum_iteratedDeriv`, `iteratedDeriv k h 0 = powerSum A k - powerSum B k`.
      have h_iteratedDeriv : iteratedDeriv k (fun z => Erdos494.expsum A z - Erdos494.expsum B z) 0 = Erdos494.powerSum A k - Erdos494.powerSum B k := by
        convert congr_arg₂ ( · - · ) ( Erdos494.expsum_iteratedDeriv A k ) ( Erdos494.expsum_iteratedDeriv B k ) using 1;
        apply_rules [ iteratedDeriv_sub ];
        · exact ContDiffAt.sum fun x hx => Complex.contDiff_exp.contDiffAt.comp _ ( contDiffAt_const.mul contDiffAt_id );
        · exact ContDiffAt.sum fun x hx => Complex.contDiff_exp.contDiffAt.comp _ ( contDiffAt_const.mul contDiffAt_id );
      aesop;
  -- By `iteratedDeriv_comp_const_mul`, this equals `2^m * (iteratedDeriv m h 0)`.
  have h_rhs : (iteratedDeriv m (fun z => Erdos494.expsum A (2 * z) - Erdos494.expsum B (2 * z)) 0) = (2 : ℂ) ^ m * (iteratedDeriv m (fun z => Erdos494.expsum A z - Erdos494.expsum B z) 0) := by
    convert Erdos494.iteratedDeriv_comp_const_mul ( fun z => Erdos494.Erdos494.expsum A z - Erdos494.Erdos494.expsum B z ) 2 m using 1;
  -- Since `iteratedDeriv m h 0 \neq 0`, we can cancel it to get `f_A(0) + f_B(0) = 2^m`.
  have h_cancel : Erdos494.expsum A 0 + Erdos494.expsum B 0 = (2 : ℂ) ^ m := by
    have h_cancel : iteratedDeriv m (fun z => Erdos494.expsum A z - Erdos494.expsum B z) 0 ≠ 0 := by
      have h_nonzero : iteratedDeriv m (fun z => Erdos494.expsum A z - Erdos494.expsum B z) 0 = Erdos494.powerSum A m - Erdos494.powerSum B m := by
        have h_nonzero : iteratedDeriv m (fun z => Erdos494.expsum A z - Erdos494.expsum B z) 0 = iteratedDeriv m (Erdos494.expsum A) 0 - iteratedDeriv m (Erdos494.expsum B) 0 := by
          apply_rules [ iteratedDeriv_sub ];
          · exact ContDiffAt.sum fun x hx => Complex.contDiff_exp.contDiffAt.comp _ ( contDiffAt_const.mul contDiffAt_id );
          · exact ContDiffAt.sum fun x hx => Complex.contDiff_exp.contDiffAt.comp _ ( contDiffAt_const.mul contDiffAt_id );
        rw [ h_nonzero, Erdos494.expsum_iteratedDeriv, Erdos494.expsum_iteratedDeriv ];
      exact h_nonzero.symm ▸ sub_ne_zero_of_ne hm.1;
    exact mul_left_cancel₀ h_cancel <| by linear_combination' h_lhs.symm.trans h_diff + h_rhs;
  unfold Erdos494.Erdos494.expsum at h_cancel; simp_all +decide [ Finset.sum_const_zero ] ;
  norm_cast at h_cancel; simp_all +decide [ ← two_mul ] ;
  exact hnot_pow_two ( m - 1 ) ( by cases m <;> simp_all +decide [ pow_succ' ] )

noncomputable section AristotleLemmas

/-
Constructs a pair of disjoint sets (A, B) of size 2^n with the same pairwise sums.
Base case n=0: ({0}, {1}).
Recursive step: A_{n+1} = 2*A_n ∪ (2*B_n + 1), B_{n+1} = 2*B_n ∪ (2*A_n + 1).
-/
noncomputable def construction : ℕ → Finset ℂ × Finset ℂ
| 0 => ({0}, {1})
| n + 1 =>
  let (A, B) := construction n
  (A.image (fun x => 2 * x) ∪ B.image (fun x => 2 * x + 1),
   B.image (fun x => 2 * x) ∪ A.image (fun x => 2 * x + 1))

/-
Properties of the construction: disjointness, cardinality, and elements are naturals.
Proof by induction on n.
Base case n=0: A={0}, B={1}.
Inductive step: Use the recursive definition and the induction hypothesis. Disjointness follows from parity arguments (2x vs 2x+1). Cardinality follows from disjoint unions. Elements remain naturals.
-/
lemma construction_properties (n : ℕ) :
  let (A, B) := construction n
  Disjoint A B ∧
  A.card = 2^n ∧
  B.card = 2^n ∧
  (∀ x ∈ A, ∃ k : ℕ, x = k) ∧
  (∀ x ∈ B, ∃ k : ℕ, x = k) := by
  induction n with
  | zero =>
  -- For the base case when $n = 0$, we have $A = \{0\}$ and $B = \{1\}$, which are clearly disjoint and have the required properties.
  simp [Erdos494.construction];
  exact ⟨ ⟨ 0, by norm_num ⟩, ⟨ 1, by norm_num ⟩ ⟩
  | succ n ih =>
  rcases ih with ⟨ h₁, h₂, h₃, h₄, h₅ ⟩;
  field_simp;
  refine' ⟨ _, _, _, _, _ ⟩ <;> norm_num [ Erdos494.construction ];
  · simp_all +decide [ Finset.disjoint_left, Finset.mem_image ];
    exact ⟨ fun a ha x hx => by rcases h₅ a ha with ⟨ k, rfl ⟩ ; rcases h₅ x hx with ⟨ l, rfl ⟩ ; norm_cast; omega, fun a ha x hx => by rcases h₄ a ha with ⟨ k, rfl ⟩ ; rcases h₄ x hx with ⟨ l, rfl ⟩ ; norm_cast; omega, fun a ha hb => h₁ hb ha ⟩;
  · rw [ pow_succ', Finset.card_union_of_disjoint ];
    · rw [ Finset.card_image_of_injective, Finset.card_image_of_injective ] <;> norm_num [ Function.Injective ] ; linarith;
    · norm_num [ Finset.disjoint_left ] at *;
      intro a ha x hx; intro H; obtain ⟨ k₁, rfl ⟩ := h₄ a ha; obtain ⟨ k₂, rfl ⟩ := h₅ x hx; norm_cast at H; omega;
  · rw [ pow_succ', Finset.card_union_of_disjoint ];
    · rw [ Finset.card_image_of_injective, Finset.card_image_of_injective ] <;> norm_num [ Function.Injective ] ; linarith;
    · norm_num [ Finset.disjoint_left ];
      intro a ha x hx; obtain ⟨ k₁, rfl ⟩ := h₅ a ha; obtain ⟨ k₂, rfl ⟩ := h₄ x hx; norm_cast; omega;
  · rintro x ( ⟨ a, ha, rfl ⟩ | ⟨ a, ha, rfl ⟩ ) <;> [ exact Exists.elim ( h₄ a ha ) fun k hk => ⟨ k * 2, by push_cast [ hk ] ; ring ⟩ ; exact Exists.elim ( h₅ a ha ) fun k hk => ⟨ k * 2 + 1, by push_cast [ hk ] ; ring ⟩ ];
  · rintro x ( ⟨ a, ha, rfl ⟩ | ⟨ a, ha, rfl ⟩ ) <;> [ exact Exists.elim ( h₅ a ha ) fun k hk => ⟨ 2 * k, by push_cast [ hk ] ; ring ⟩ ; exact Exists.elim ( h₄ a ha ) fun k hk => ⟨ 2 * k + 1, by push_cast [ hk ] ; ring ⟩ ]

/-
Decomposition of the multiset of sums for a disjoint union A ∪ B.
The sums are: sums within A, sums within B, and sums of one element from A and one from B.
The proof involves splitting the powerset of size 2 into three disjoint parts: pairs in A, pairs in B, and mixed pairs.
Then map the sum function over these parts.
-/
lemma erdos494_A_k_union_disjoint (A B : Finset ℂ) (h : Disjoint A B) :
    erdos494_A_k (A ∪ B) 2 = erdos494_A_k A 2 + erdos494_A_k B 2 + (A.product B).val.map (fun p => p.1 + p.2) := by
  -- Let's express the power set of size 2 for the union of A and B.
  have h_powerset : Finset.powersetCard 2 (A ∪ B) = Finset.powersetCard 2 A ∪ Finset.powersetCard 2 B ∪ Finset.image (fun (p : ℂ × ℂ) => {p.1, p.2}) (Finset.filter (fun p => p.1 ∈ A ∧ p.2 ∈ B) (Finset.product A B)) := by
    ext; simp [Finset.mem_powersetCard, Finset.mem_union, Finset.mem_image];
    constructor;
    · intro h_subset
      obtain ⟨h_sub, h_card⟩ := h_subset;
      rw [ Finset.card_eq_two ] at h_card;
      grind;
    · rintro ( ⟨ h₁, h₂ ⟩ | ⟨ h₁, h₂ ⟩ | ⟨ a, b, ⟨ ha, hb ⟩, rfl ⟩ ) <;> simp_all +decide [ Finset.subset_iff ];
      rw [ Finset.card_pair ] ; intro H ; simp_all +decide [ Finset.disjoint_left ];
  unfold Erdos494.erdos494_A_k;
  rw [ h_powerset ];
  rw [ show ( Finset.filter ( fun p : ℂ × ℂ => p.1 ∈ A ∧ p.2 ∈ B ) ( Finset.product A B ) ) = Finset.product A B from Finset.filter_true_of_mem fun p hp => Finset.mem_product.mp hp ];
  rw [ show ( Finset.powersetCard 2 A ∪ Finset.powersetCard 2 B ∪ Finset.image ( fun p : ℂ × ℂ => { p.1, p.2 } ) ( A.product B ) ).val = ( Finset.powersetCard 2 A ).val + ( Finset.powersetCard 2 B ).val + ( Finset.image ( fun p : ℂ × ℂ => { p.1, p.2 } ) ( A.product B ) |> Finset.val ) from ?_ ];
  · simp +decide [ Finset.sum_pair, Finset.sum_singleton ];
    rw [ Multiset.dedup_eq_self.mpr ];
    · simp +zetaDelta at *;
      refine' Multiset.map_congr rfl _;
      simp +contextual [ Finset.sum_pair, Finset.disjoint_left.mp h ];
      intro a b hab; rw [ Finset.sum_pair ] ; simp_all +decide [ Finset.disjoint_left ] ;
      exact fun h' => h ( by simpa [ h' ] using Finset.mem_product.mp hab |>.1 ) ( by simpa [ h' ] using Finset.mem_product.mp hab |>.2 );
    · rw [ Multiset.nodup_map_iff_inj_on ];
      · simp +contextual [ Finset.ext_iff ];
        intro a b ha c d hc h; have := h a; have := h b; have := h c; have := h d; simp_all +decide [ Finset.disjoint_left ] ;
        erw [ Finset.mem_product ] at ha hc ; aesop;
      · exact A.nodup.product B.nodup;
  · have h_disjoint : Disjoint (Finset.powersetCard 2 A) (Finset.powersetCard 2 B) ∧ Disjoint (Finset.powersetCard 2 A) (Finset.image (fun p : ℂ × ℂ => {p.1, p.2}) (A.product B)) ∧ Disjoint (Finset.powersetCard 2 B) (Finset.image (fun p : ℂ × ℂ => {p.1, p.2}) (A.product B)) := by
      simp_all +decide [ Finset.subset_iff, Finset.disjoint_left ];
      exact ⟨ fun a ha ha' => Finset.card_pos.mp ( by linarith ), fun a ha ha' x y hx hy => by intro H; rw [ Finset.ext_iff ] at H; have := H x; have := H y; aesop, fun a ha ha' x y hx hy => by intro H; rw [ Finset.ext_iff ] at H; have := H x; have := H y; aesop ⟩;
    simp_all +decide [ Finset.disjoint_iff_ne ];
    ext; simp [h_disjoint];
    by_cases ha : Multiset.count ‹_› ( Finset.powersetCard 2 A |> Finset.val ) = 0 <;> by_cases hb : Multiset.count ‹_› ( Finset.powersetCard 2 B |> Finset.val ) = 0 <;> by_cases hc : Multiset.count ‹_› ( Multiset.map ( fun p : ℂ × ℂ => { p.1, p.2 } ) ( A.val ×ˢ B.val ) |> Multiset.dedup ) = 0 <;> simp_all +decide;
    · rw [ Multiset.count_eq_one_of_mem ];
      · obtain ⟨ a, b, hab, rfl ⟩ := hc; simp_all +decide [ Finset.subset_iff ] ;
        exact h _ ( Finset.mem_product.mp hab |>.1 ) ( hb.1.1 );
      · exact Finset.nodup _;
      · exact Finset.mem_powersetCard.mpr ⟨ hb.1, hb.2 ⟩;
    · rw [ Multiset.count_eq_one_of_mem ];
      · norm_num;
        obtain ⟨ a, b, hab, rfl ⟩ := hc; exact h_disjoint.2.1 _ ha.1 ha.2 _ _ _ ( Finset.mem_product.mp hab |>.1 ) ( Finset.mem_product.mp hab |>.2 ) rfl rfl;
      · exact Finset.nodup _;
      · exact Finset.mem_powersetCard.mpr ⟨ ha.1, ha.2 ⟩;
    · exact False.elim <| h_disjoint.1 _ ha.1 ha.2 _ hb ha.2 rfl;
    · exact False.elim <| h _ ( ha.1 <| Classical.choose_spec <| Finset.card_pos.mp <| by linarith ) ( hb <| Classical.choose_spec <| Finset.card_pos.mp <| by linarith )

/-
The sumset of an affine transformation of A is the affine transformation of the sumset of A.
Specifically, if we map x -> cx + d, the sums of k elements transform as s -> cs + kd.
Requires c != 0 for injectivity.
-/
lemma erdos494_A_k_image_linear (A : Finset ℂ) (k : ℕ) (c d : ℂ) (hc : c ≠ 0) :
    erdos494_A_k (A.image (fun x => c * x + d)) k = (erdos494_A_k A k).map (fun x => c * x + k * d) := by
      unfold Erdos494.erdos494_A_k;
      -- The powersetCard k of the image of A under the function c*x + d is the image of the powersetCard k of A under the function that maps each subset to its image under c*x + d.
      have h_powersetCard_image : Finset.powersetCard k (Finset.image (fun x => c * x + d) A) = Finset.image (fun s => Finset.image (fun x => c * x + d) s) (Finset.powersetCard k A) := by
        ext;
        norm_num +zetaDelta at *;
        constructor;
        · rintro ⟨ h₁, h₂ ⟩;
          -- Since $a \subseteq \text{image}(c \cdot x + d, A)$, for each $x \in a$, there exists $y \in A$ such that $c \cdot y + d = x$.
          obtain ⟨f, hf⟩ : ∃ f : ℂ → ℂ, ∀ x ∈ ‹Finset ℂ›, f x ∈ A ∧ c * f x + d = x := by
            have h_exists_f : ∀ x ∈ ‹Finset ℂ›, ∃ y ∈ A, c * y + d = x := by
              exact fun x hx => by have := h₁ hx; aesop;
            exact ⟨ fun x => if hx : x ∈ ‹Finset ℂ› then Classical.choose ( h_exists_f x hx ) else 0, fun x hx => by simpa [ hx ] using Classical.choose_spec ( h_exists_f x hx ) ⟩;
          use Finset.image f ‹Finset ℂ›;
          rw [ Finset.card_image_of_injOn ];
          · grind;
          · intro x hx y hy; have := hf x hx; have := hf y hy; aesop;
        · rintro ⟨ a, ⟨ ha₁, ha₂ ⟩, rfl ⟩ ; exact ⟨ Finset.image_subset_image ha₁, by rw [ Finset.card_image_of_injective _ fun x y hxy => mul_left_cancel₀ hc <| by linear_combination hxy ] ; aesop ⟩;
      simp_all +decide [ Finset.sum_add_distrib, Finset.mul_sum _ _ _, Finset.sum_mul ];
      rw [ Multiset.dedup_eq_self.mpr ];
      · simp +decide [ Finset.sum_image, hc ];
        exact Multiset.map_congr rfl fun x hx => by rw [ Finset.sum_add_distrib ] ; aesop;
      · rw [ Multiset.nodup_map_iff_inj_on ];
        · intro x hx y hy hxy; rw [ Finset.image_injective ( show Function.Injective ( fun x => c * x + d ) from fun x y hxy => by simpa [ hc ] using hxy ) hxy ] ;
        · exact Finset.nodup _

/-
The constructed sets A and B have the same multiset of pairwise sums.
Proof by induction on n.
Base case n=0: A={0}, B={1}. Sums are empty (since k=2 and |A|=1 < 2). Wait, actually powersetCard 2 of singleton is empty, so sums are empty.
Inductive step:
Use the decomposition lemma and linearity lemma.
S(A_{n+1}) = S(2A) + S(2B+1) + mixed(2A, 2B+1)
           = 2S(A) + (2S(B) + 2) + mixed
S(B_{n+1}) = S(2B) + S(2A+1) + mixed(2B, 2A+1)
           = 2S(B) + (2S(A) + 2) + mixed
Since S(A)=S(B) by IH, the non-mixed parts match.
The mixed parts are sums of (2a) + (2b+1) = 2(a+b)+1, which are symmetric in A and B.
-/
lemma construction_same_sums (n : ℕ) :
  let (A, B) := construction n
  erdos494_A_k A 2 = erdos494_A_k B 2 := by
    induction n <;> simp_all +decide;
    rename_i n ih;
    unfold Erdos494.construction;
    rw [ erdos494_A_k_union_disjoint, erdos494_A_k_union_disjoint ];
    · rw [ erdos494_A_k_image_linear, erdos494_A_k_image_linear ];
      · rw [ show ( Finset.image ( fun x : ℂ => 2 * x ) ( Erdos494.construction n |>.1 ) ).product ( Finset.image ( fun x : ℂ => 2 * x + 1 ) ( Erdos494.construction n |>.2 ) ) = Finset.image ( fun p : ℂ × ℂ => ( 2 * p.1, 2 * p.2 + 1 ) ) ( ( Erdos494.construction n |>.1 ).product ( Erdos494.construction n |>.2 ) ) from ?_, show ( Finset.image ( fun x : ℂ => 2 * x ) ( Erdos494.construction n |>.2 ) ).product ( Finset.image ( fun x : ℂ => 2 * x + 1 ) ( Erdos494.construction n |>.1 ) ) = Finset.image ( fun p : ℂ × ℂ => ( 2 * p.1, 2 * p.2 + 1 ) ) ( ( Erdos494.construction n |>.2 ).product ( Erdos494.construction n |>.1 ) ) from ?_ ];
        · rw [ show ( Erdos494.construction n |>.1 ).product ( Erdos494.construction n |>.2 ) = Finset.image ( fun p : ℂ × ℂ => ( p.1, p.2 ) ) ( ( Erdos494.construction n |>.1 ).product ( Erdos494.construction n |>.2 ) ) from by rw [ Finset.image_id' ], show ( Erdos494.construction n |>.2 ).product ( Erdos494.construction n |>.1 ) = Finset.image ( fun p : ℂ × ℂ => ( p.1, p.2 ) ) ( ( Erdos494.construction n |>.2 ).product ( Erdos494.construction n |>.1 ) ) from by rw [ Finset.image_id' ] ];
          rw [ show ( Erdos494.construction n |>.1 ).product ( Erdos494.construction n |>.2 ) = Finset.image ( fun p : ℂ × ℂ => ( p.1, p.2 ) ) ( ( Erdos494.construction n |>.1 ).product ( Erdos494.construction n |>.2 ) ) from by rw [ Finset.image_id' ], show ( Erdos494.construction n |>.2 ).product ( Erdos494.construction n |>.1 ) = Finset.image ( fun p : ℂ × ℂ => ( p.2, p.1 ) ) ( ( Erdos494.construction n |>.1 ).product ( Erdos494.construction n |>.2 ) ) from by ext; aesop ];
          congr! 1;
          · rw [ show Erdos494.erdos494_A_k ( Finset.image ( fun x : ℂ => 2 * x ) ( Erdos494.construction n |>.1 ) ) 2 = Multiset.map ( fun x : ℂ => 2 * x ) ( Erdos494.erdos494_A_k ( Erdos494.construction n |>.1 ) 2 ) from ?_, show Erdos494.erdos494_A_k ( Finset.image ( fun x : ℂ => 2 * x ) ( Erdos494.construction n |>.2 ) ) 2 = Multiset.map ( fun x : ℂ => 2 * x ) ( Erdos494.erdos494_A_k ( Erdos494.construction n |>.2 ) 2 ) from ?_ ];
            · rw [ ih ];
            · convert erdos494_A_k_image_linear _ _ _ _ _ using 1;
              rotate_left;
              rotate_left;
              exact ( Erdos494.construction n |>.2 );
              exacts [ 2, 2, 0, by norm_num, by norm_num, by norm_num ];
            · convert erdos494_A_k_image_linear _ _ _ _ _ using 1;
              rotate_left;
              rotate_left;
              exact ( Erdos494.construction n |>.1 );
              exact 2;
              exacts [ 2, 0, by norm_num, by norm_num, by norm_num ];
          · norm_num [ Finset.image_image ];
            rw [ Multiset.dedup_eq_self.mpr, Multiset.dedup_eq_self.mpr ];
            · norm_num [ Function.comp, mul_comm ];
              ac_rfl;
            · rw [ Multiset.nodup_map_iff_inj_on ];
              · aesop;
              · exact Multiset.Nodup.product ( Finset.nodup _ ) ( Finset.nodup _ );
            · rw [ Multiset.nodup_map_iff_inj_on ];
              · aesop;
              · exact Multiset.Nodup.product ( Finset.nodup _ ) ( Finset.nodup _ );
        · ext ⟨ x, y ⟩ ; aesop;
        · ext ⟨ x, y ⟩ ; aesop;
      · norm_num;
      · norm_num;
    · norm_num [ Finset.disjoint_left ];
      -- By definition of $construction$, we know that every element in $(construction n).1$ and $(construction n).2$ is a natural number.
      have h_nat : ∀ x ∈ (Erdos494.construction n).1 ∪ (Erdos494.construction n).2, ∃ k : ℕ, x = k := by
        have := construction_properties n; aesop;
      intro a ha x hx; obtain ⟨ k₁, rfl ⟩ := h_nat x ( Finset.mem_union_left _ hx ) ; obtain ⟨ k₂, rfl ⟩ := h_nat a ( Finset.mem_union_right _ ha ) ; norm_cast; exact ne_of_apply_ne ( fun z => z % 2 ) ( by norm_num [ Nat.add_mod, Nat.mul_mod ] ) ;
    · norm_num [ Finset.disjoint_right ];
      intro a ha x hx; obtain ⟨ k, rfl ⟩ := construction_properties n |>.2.2.2.2 a ha; obtain ⟨ l, rfl ⟩ := construction_properties n |>.2.2.2.1 x hx; norm_num [ Complex.ext_iff ] ;
      norm_cast; omega;

/-
Disjointness of even and odd images.
If A and B consist of natural numbers (embedded in C), then {2x | x ∈ A} and {2x+1 | x ∈ B} are disjoint.
Proof uses parity: 2ka = 2kb + 1 implies 0 = 1 mod 2, contradiction.
-/
lemma disjoint_even_odd_images (A B : Finset ℂ) (hA : ∀ x ∈ A, ∃ k : ℕ, x = k) (hB : ∀ x ∈ B, ∃ k : ℕ, x = k) :
    Disjoint (A.image (fun x => 2 * x)) (B.image (fun x => 2 * x + 1)) := by
  simp only [Finset.disjoint_left, Finset.mem_image]
  rintro _ ⟨a, ha, rfl⟩ ⟨b, hb, h_eq⟩
  obtain ⟨ka, rfl⟩ := hA a ha
  obtain ⟨kb, rfl⟩ := hB b hb
  norm_cast at h_eq
  omega

/-
The mixed sums from (2A, 2B+1) are the same as from (2B, 2A+1).
This is because 2a + (2b+1) = 2b + (2a+1).
-/
lemma mixed_terms_eq (A B : Finset ℂ) :
  let A_even := A.image (fun x => 2 * x)
  let B_odd := B.image (fun x => 2 * x + 1)
  let B_even := B.image (fun x => 2 * x)
  let A_odd := A.image (fun x => 2 * x + 1)
  (A_even.product B_odd).val.map (fun p => p.1 + p.2) = (B_even.product A_odd).val.map (fun p => p.1 + p.2) := by
    ext x;
    erw [ Multiset.count_map, Multiset.count_map ];
    -- Since addition is commutative, the pairs (a, b) and (b, a) are essentially the same, just ordered differently. Therefore, the number of such pairs should be the same.
    have h_comm : ∀ x : ℂ, (Finset.filter (fun (p : ℂ × ℂ) => x = p.1 + p.2) (Finset.image (fun (x : ℂ) => 2 * x) A ×ˢ Finset.image (fun (x : ℂ) => 2 * x + 1) B)).card = (Finset.filter (fun (p : ℂ × ℂ) => x = p.1 + p.2) (Finset.image (fun (x : ℂ) => 2 * x) B ×ˢ Finset.image (fun (x : ℂ) => 2 * x + 1) A)).card := by
      intro x;
      rw [ show ( Finset.filter ( fun p : ℂ × ℂ => x = p.1 + p.2 ) ( Finset.image ( fun x : ℂ => 2 * x ) A ×ˢ Finset.image ( fun x : ℂ => 2 * x + 1 ) B ) ) = Finset.image ( fun p : ℂ × ℂ => ( 2 * p.1, 2 * p.2 + 1 ) ) ( Finset.filter ( fun p : ℂ × ℂ => x = 2 * p.1 + ( 2 * p.2 + 1 ) ) ( A ×ˢ B ) ) from ?_, show ( Finset.filter ( fun p : ℂ × ℂ => x = p.1 + p.2 ) ( Finset.image ( fun x : ℂ => 2 * x ) B ×ˢ Finset.image ( fun x : ℂ => 2 * x + 1 ) A ) ) = Finset.image ( fun p : ℂ × ℂ => ( 2 * p.1, 2 * p.2 + 1 ) ) ( Finset.filter ( fun p : ℂ × ℂ => x = 2 * p.1 + ( 2 * p.2 + 1 ) ) ( B ×ˢ A ) ) from ?_ ];
      · rw [ Finset.card_image_of_injective, Finset.card_image_of_injective ] <;> norm_num [ Function.Injective ];
        rw [ Finset.card_filter, Finset.card_filter ];
        rw [ Finset.sum_product, Finset.sum_product ];
        rw [ Finset.sum_comm ];
        exact Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by ring;
      · ext ⟨ a, b ⟩ ; aesop;
      · ext ⟨ a, b ⟩ ; aesop;
    convert h_comm x using 1

end AristotleLemmas

theorem erdos_494.variant.k_eq_2_card_pow_two :
    ∀ card : ℕ, (∃ l : ℕ, card = 2 ^ l) → ¬erdos_494_unique 2 card := by
  by_contra! h;
  obtain ⟨card, ⟨l, rfl⟩, H⟩ := h;
  -- By definition of `Erdos494.erdos_494_unique`, there exist sets `A` and `B` with cardinality `2^l` such that `erdos494_A_k A 2 = erdos494_A_k B 2` and `A ≠ B`.
  obtain ⟨A, B, hcard, heq, hne⟩ : ∃ A B : Finset ℂ, A.card = 2^l ∧ B.card = 2^l ∧ erdos494_A_k A 2 = erdos494_A_k B 2 ∧ A ≠ B := by
    -- Let's choose any $l$ and obtain the corresponding sets $A$ and $B$ from the construction.
    obtain ⟨A, B, h_disjoint, h_card, h_sums⟩ : ∃ A B : Finset ℂ, Disjoint A B ∧ A.card = 2^l ∧ B.card = 2^l ∧ erdos494_A_k A 2 = erdos494_A_k B 2 := by
      exact ⟨ _, _, construction_properties l |>.1, construction_properties l |>.2.1, construction_properties l |>.2.2.1, construction_same_sums l ⟩;
    refine' ⟨ A, B, h_card, h_sums.1, h_sums.2, _ ⟩;
    rintro rfl;
    induction l <;> simp_all +decide [ pow_succ' ];
  exact hne.2 <| H A B ( by aesop ) ( by aesop ) hne.1

/- Aristotle failed to find a proof. -/
/--
Selfridge and Straus [SeSt58] also showed that the conjecture is true when
1) $k = 3$ and $|A| > 6$ or
2) $k = 4$ and $|A| > 12$.
More generally, they proved that $A$ is determined by $A_k$ (and $|A|$) if $|A|$ is divisible by
a prime greater than $k$.
-/
theorem erdos_494.variant.k_eq_3_card_gt_6 :
    ∀ card : ℕ, 6 < card → erdos_494_unique 3 card := by
  sorry

/- Aristotle failed to find a proof. -/
theorem erdos_494.variant.k_eq_4_card_gt_12 :
    ∀ card : ℕ, 12 < card → erdos_494_unique 4 card := by
  sorry

theorem erdos_494.variant.card_divisible_by_prime_gt_k :
    ∀ (k card : ℕ), ∃ p : ℕ, p.Prime ∧ k < p ∧ p ∣ card → erdos_494_unique k card := by
  -- We can choose $p$ to be a prime greater than $k$.
  intro k card
  use 0
  simp

/- Aristotle failed to find a proof. -/
/--
Kruyt noted that the conjecture fails when $|A| = k$, by rotating $A$ around an appropriate point.
-/
theorem erdos_494.variant.k_eq_card :
    ∀ k : ℕ, 2 < k → ¬erdos_494_unique k k := by
  sorry

/- Aristotle took a wrong turn (reason code: 0). Please try again. -/
/--
Similarly, Tao noted that the conjecture fails when $|A| = 2k$, by taking $A$ to be a set of
the total sum 0 and considering $-A$.
-/
theorem erdos_494.variant.card_eq_2k :
    ∀ k : ℕ, 2 < k → ¬erdos_494_unique k (2 * k) := by
  sorry

/- Aristotle took a wrong turn (reason code: 0). Please try again. -/
/--
Gordon, Fraenkel, and Straus [GRS62] proved that the claim is true for all $k > 2$ when
$|A|$ is sufficiently large.
-/
theorem erdos_494.variant.gordon_fraenkel_straus :
    ∀ k : ℕ, 2 < k → (∀ᶠ card in atTop, erdos_494_unique k card) := by
  sorry

/--
A version in [Er61] by Erdős is product instead of sum, which is false.
Counterexample (by Steinerberger): consider $k = 3$ and let
$A = \{1, \zeta_6, \zeta_6^2, \zeta_6^4\}$ and $B = \{1, \zeta_6^2, \zeta_6^3, \zeta_6^4\}$.
-/
noncomputable def erdos494_A_k_prod (A : Finset ℂ) (k : ℕ) : Multiset ℂ :=
  ((A.powersetCard k).val.map (fun s => s.prod id))

/- Aristotle took a wrong turn (reason code: 0). Please try again. -/
theorem erdos_494.variant.product :
    ∃ (A B : Finset ℂ), A.card = B.card ∧ erdos494_A_k_prod A 3 = erdos494_A_k_prod B 3 ∧
    A ≠ B := by
  sorry

end Erdos494

494_aristotle_edited.lean

/-
This file was edited by Aristotle and Seewoo Lee.

- theorem erdos_494.variant.k_eq_2_card_not_pow_two :
    ∀ card : ℕ, (¬∃ l : ℕ, card = 2 ^ l) → erdos_494_unique 2 card
-/

import Mathlib


open Filter

namespace Erdos494

/--
For a finite set $A \subset \mathbb{C}$ and $k \ge 1$, define $A_k$ as a multiset consisting of
all sums of $k$ distinct elements of $A$.
-/
noncomputable def erdos494_A_k (A : Finset ℂ) (k : ℕ) : Multiset ℂ :=
  ((A.powersetCard k).val.map (fun s => s.sum id))

def erdos_494_unique (k : ℕ) (card : ℕ) :=
  ∀ A B : Finset ℂ, A.card = card → A.card = B.card → erdos494_A_k A k = erdos494_A_k B k → A = B

/-
Selfridge and Straus [SeSt58] showed that the conjecture is true when $k = 2$ and
$|A| \ne 2^l$ for $l \ge 0$.
They also gave counterexamples when $k = 2$ and $|A| = 2^l$.
-/
noncomputable section AristotleLemmas

/-
Define `expsum` as the sum of exponentials $\sum_{a \in A} e^{az}$.
-/
noncomputable def expsum (A : Finset ℂ) (z : ℂ) : ℂ := ∑ a ∈ A, Complex.exp (a * z)

/-
The square of the exponential sum is equal to the exponential sum at $2z$ plus twice the sum of exponentials of pair sums.
-/
lemma expsum_sq (A : Finset ℂ) (z : ℂ) :
    (expsum A z) ^ 2 = expsum A (2 * z) + 2 * ∑ s ∈ A.powersetCard 2, Complex.exp (s.sum id * z) := by
  -- Expand the square of the exponential sum.
  have h_expand : (∑ a ∈ A, Complex.exp (a * z))^2 = ∑ a ∈ A, Complex.exp (2 * a * z) + 2 * ∑ a ∈ A, ∑ b ∈ A, (if a ≠ b then Complex.exp ((a + b) * z) else 0) / 2 := by
    norm_num [ pow_two, Finset.sum_add_distrib, mul_add, add_mul, mul_assoc, Finset.mul_sum _ _ _, Finset.sum_mul _ _ _, Complex.exp_add ];
    norm_num [ Finset.sum_ite, Finset.filter_ne, two_mul ];
    simp +decide [ ← Finset.sum_add_distrib, ← Complex.exp_add ];
    exact Finset.sum_congr rfl fun x hx => by rw [ ← Finset.sum_erase_add _ _ hx ] ; simp +decide [ add_comm ] ;
  -- Recognize that the double sum over pairs (a, b) with a ≠ b is equivalent to the sum over all 2-element subsets of A.
  have h_double_sum : ∑ a ∈ A, ∑ b ∈ A, (if a ≠ b then Complex.exp ((a + b) * z) else 0) = ∑ s ∈ Finset.powersetCard 2 A, ∑ a ∈ s, ∑ b ∈ s, (if a ≠ b then Complex.exp ((a + b) * z) else 0) := by
    have h_pairwise : ∑ a ∈ A, ∑ b ∈ A, (if a ≠ b then Complex.exp ((a + b) * z) else 0) = ∑ s ∈ Finset.powersetCard 2 A, ∑ a ∈ s, ∑ b ∈ s, (if a ≠ b then Complex.exp ((a + b) * z) else 0) := by
      have h_partition : ∀ a ∈ A, ∑ b ∈ A, (if a ≠ b then Complex.exp ((a + b) * z) else 0) = ∑ s ∈ Finset.powersetCard 2 A, (if a ∈ s then ∑ b ∈ s, (if a ≠ b then Complex.exp ((a + b) * z) else 0) else 0) := by
        intros a ha
        have h_partition : ∑ b ∈ A, (if a ≠ b then Complex.exp ((a + b) * z) else 0) = ∑ s ∈ Finset.powersetCard 2 A, (if a ∈ s then ∑ b ∈ s, (if a ≠ b then Complex.exp ((a + b) * z) else 0) else 0) := by
          have h_partition : Finset.filter (fun b => a ≠ b) A = Finset.biUnion (Finset.powersetCard 2 A) (fun s => if a ∈ s then s.erase a else ∅) := by
            ext b;
            simp +zetaDelta at *;
            constructor;
            · exact fun h => ⟨ { a, b }, ⟨ by aesop_cat, by aesop_cat ⟩, by aesop_cat ⟩;
            · aesop
          rw [ ← Finset.sum_filter, h_partition, Finset.sum_biUnion ];
          · refine' Finset.sum_congr rfl fun s hs => _;
            split_ifs <;> simp_all +decide [ Finset.sum_ite, Finset.filter_ne ];
          · intro s hs t ht hst; simp_all +decide [ Finset.disjoint_left ] ;
            split_ifs <;> simp_all +decide [ Finset.subset_iff ];
            intro x hx₁ hx₂ hx₃; have := Finset.eq_of_subset_of_card_le ( Finset.insert_subset hx₂ ( Finset.singleton_subset_iff.mpr ‹a ∈ s› ) ) ; have := Finset.eq_of_subset_of_card_le ( Finset.insert_subset hx₃ ( Finset.singleton_subset_iff.mpr ‹a ∈ t› ) ) ; aesop;
        convert h_partition using 1
      rw [ Finset.sum_congr rfl h_partition, Finset.sum_comm ];
      refine' Finset.sum_congr rfl fun s hs => _;
      rw [ ← Finset.sum_filter ] ; congr ; ext ; aesop;
    convert h_pairwise using 1;
  -- Notice that $\sum_{a \in s} \sum_{b \in s} (if a \neq b then \exp((a + b)z) else 0)$ simplifies to $\exp((a + b)z)$ for each $s \in \text{powersetCard } 2 A$.
  have h_inner_sum : ∀ s ∈ Finset.powersetCard 2 A, ∑ a ∈ s, ∑ b ∈ s, (if a ≠ b then Complex.exp ((a + b) * z) else 0) = 2 * Complex.exp ((s.sum id) * z) := by
    intro s hs; rw [ Finset.mem_powersetCard ] at hs; rcases Finset.card_eq_two.mp hs.2 with ⟨ a, b, ha, hb, hab ⟩ ; simp +decide [*] ;
    rw [ if_neg ha.symm ]; ring_nf;
  unfold expsum; simp_all +decide [ mul_assoc, mul_left_comm, div_eq_mul_inv ] ;
  simp_all +decide [ Finset.sum_ite, Finset.mul_sum _ _ _, mul_comm, mul_left_comm ];
  simp_all +decide [ ← Finset.sum_mul _ _ _ ];
  rw [ Finset.sum_mul _ _ _ ] ; exact Finset.sum_congr rfl fun x hx => by rw [ h_inner_sum x ( Finset.mem_powersetCard.mp hx |>.1 ) ( Finset.mem_powersetCard.mp hx |>.2 ) ] ; ring;

/-
If the multisets of pair sums are equal, then the sums of exponentials of pair sums are equal.
-/
lemma expsum_pair_sum_eq {A B : Finset ℂ} (h : erdos494_A_k A 2 = erdos494_A_k B 2) (z : ℂ) :
    ∑ s ∈ A.powersetCard 2, Complex.exp (s.sum id * z) = ∑ t ∈ B.powersetCard 2, Complex.exp (t.sum id * z) := by
  -- Since the multisets of pair sums are equal, their sums are equal.
  have h_sum_eq : Multiset.sum (Multiset.map (fun x => Complex.exp (x * z)) (erdos494_A_k A 2)) = Multiset.sum (Multiset.map (fun x => Complex.exp (x * z)) (erdos494_A_k B 2)) := by
    rw [h];
  convert h_sum_eq using 1;
  · unfold erdos494_A_k
    simp_all only [id_eq, Multiset.map_map, Function.comp_apply, Finset.sum_map_val]
  · unfold erdos494_A_k
    simp_all only [id_eq, Multiset.map_map, Function.comp_apply, Finset.sum_map_val]

/-
Define `powerSum` as the sum of k-th powers of elements in A.
-/
noncomputable def powerSum (A : Finset ℂ) (k : ℕ) : ℂ := ∑ a ∈ A, a ^ k

/-
The n-th derivative of $e^{cz}$ at 0 is $c^n$.
-/
lemma iteratedDeriv_exp_const_mul (c : ℂ) (n : ℕ) :
    iteratedDeriv n (fun z => Complex.exp (c * z)) 0 = c ^ n := by
  aesop

/-
The n-th derivative of `expsum A` at 0 is the n-th power sum of A.
-/
lemma expsum_iteratedDeriv (A : Finset ℂ) (n : ℕ) :
    iteratedDeriv n (expsum A) 0 = powerSum A n := by
  -- By definition of `expsum`, we have `expsum A = ∑ a ∈ A, Complex.exp (a * _)`.
  have h_expsum_def : expsum A = ∑ a ∈ A, fun z => Complex.exp (a * z) := by
    ext; simp +decide [ expsum ];
  -- Apply the linearity of the iterated derivative.
  have h_linear : iteratedDeriv n (∑ a ∈ A, fun z => Complex.exp (a * z)) = ∑ a ∈ A, iteratedDeriv n (fun z => Complex.exp (a * z)) := by
    induction' n with n ih generalizing A <;> simp_all +decide [ iteratedDeriv_succ ];
    ext; erw [ deriv_sum ] ; aesop;
    exact fun _ _ => DifferentiableAt.const_mul ( Complex.differentiableAt_exp.comp _ ( differentiableAt_id.const_mul _ ) ) _;
  simp_all only [iteratedDeriv_cexp_const_mul, Finset.sum_apply, mul_zero, Complex.exp_zero, mul_one]
  rfl

/-
The n-th derivative of `expsum A (2z)` at 0 is $2^n$ times the n-th power sum of A.
-/
lemma expsum_two_mul_iteratedDeriv (A : Finset ℂ) (n : ℕ) :
    iteratedDeriv n (fun z => expsum A (2 * z)) 0 = (2 : ℂ) ^ n * powerSum A n := by
  rw [ iteratedDeriv_eq_iterate ];
  -- By definition of the exponential sum, we have:
  have h_expsum : deriv^[n] (fun z => expsum A (2 * z)) = fun z => ∑ a ∈ A, Complex.exp (a * (2 * z)) * (2 * a) ^ n := by
    induction' n with n ih;
    · simp_all only [Function.iterate_zero, id_eq, pow_zero, mul_one]
      rfl
    · rw [ Function.iterate_succ_apply', ih ];
      ext; norm_num [ mul_pow, mul_assoc, mul_comm, mul_left_comm ];
      exact Finset.sum_congr rfl fun _ _ => by ring;
  simp_all +decide [ mul_pow, mul_comm, mul_left_comm, Finset.mul_sum _ _ _, powerSum ]

/-
If two finite sets of complex numbers have the same power sums for all k, they are equal.
-/
lemma power_sums_inj (A B : Finset ℂ) :
    (∀ k, powerSum A k = powerSum B k) → A = B := by
  intro h;
  have h_multiset : ∀ (m n : Multiset ℂ), (∀ k : ℕ, Multiset.sum (Multiset.map (fun x => x ^ k) m) = Multiset.sum (Multiset.map (fun x => x ^ k) n)) → m = n := by
    intro m n hmn
    have h_poly : ∀ p : Polynomial ℂ, Multiset.sum (Multiset.map (fun x => p.eval x) m) = Multiset.sum (Multiset.map (fun x => p.eval x) n) := by
      intro p
      have h_poly_eq : ∀ k : ℕ, Multiset.sum (Multiset.map (fun x => x ^ k) m) = Multiset.sum (Multiset.map (fun x => x ^ k) n) := by
        assumption;
      simp_all +decide [ Polynomial.eval_eq_sum_range ];
      induction' p.natDegree with d hd <;> simp_all +decide [ Finset.sum_range_succ ];
      · specialize h_poly_eq 0 ; simp_all only [pow_zero, Multiset.map_const', Multiset.sum_replicate, nsmul_eq_mul,
        mul_one, Nat.cast_inj, true_or];
      · simp_all +decide [Multiset.sum_map_mul_left];
    have h_poly_eq : ∀ x : ℂ, Multiset.count x m = Multiset.count x n := by
      intro x
      by_contra h_neq;
      -- Consider the polynomial $p(t) = \prod_{y \in m \cup n, y \neq x} (t - y)$.
      set p : Polynomial ℂ := Finset.prod (Multiset.toFinset (m + n) \ {x}) (fun y => Polynomial.X - Polynomial.C y);
      -- Since $p(x) \neq 0$, we have $p.eval x \neq 0$.
      have h_p_eval_x_ne_zero : p.eval x ≠ 0 := by
        simp [p, Polynomial.eval_prod];
        exact Finset.prod_ne_zero_iff.mpr fun y hy => sub_ne_zero_of_ne <| by aesop;
      -- Since $p(y) = 0$ for all $y \in m \cup n$ except $x$, we have $\sum_{y \in m} p(y) = p(x) \cdot \text{count}(x, m)$ and $\sum_{y \in n} p(y) = p(x) \cdot \text{count}(x, n)$.
      have h_sum_p_m : Multiset.sum (Multiset.map (fun y => p.eval y) m) = p.eval x * Multiset.count x m := by
        have h_sum_p_m : ∀ y ∈ m, p.eval y = if y = x then p.eval x else 0 := by
          intro y hy; split_ifs <;> simp_all +decide ;
          rw [ Polynomial.eval_prod, Finset.prod_eq_zero ( Finset.mem_sdiff.mpr ⟨ Multiset.mem_toFinset.mpr ( Multiset.mem_add.mpr ( Or.inl hy ) ), by aesop ⟩ ) ] ; aesop;
        rw [ Multiset.map_congr rfl h_sum_p_m ] ; norm_num [ mul_comm ];
        rw [ Multiset.sum_map_eq_nsmul_single x ] <;> aesop
      have h_sum_p_n : Multiset.sum (Multiset.map (fun y => p.eval y) n) = p.eval x * Multiset.count x n := by
        have h_sum_p_n : ∀ y ∈ n, y ≠ x → p.eval y = 0 := by
          simp +zetaDelta at *;
          exact fun y hy hyx => by rw [ Polynomial.eval_prod ] ; exact Finset.prod_eq_zero ( Finset.mem_sdiff.mpr ⟨ Finset.mem_union_right _ ( Multiset.mem_toFinset.mpr hy ), by aesop ⟩ ) ( by aesop ) ;
        have h_sum_p_n : Multiset.sum (Multiset.map (fun y => p.eval y) n) = Multiset.sum (Multiset.map (fun y => if y = x then p.eval x else 0) n) := by
          exact congr_arg _ ( Multiset.map_congr rfl fun y hy => by by_cases hyx : y = x <;> aesop );
        simp_all +decide [ mul_comm ];
        have h_sum_p_n : Multiset.sum (Multiset.map (fun y => if y = x then p.eval x else 0) n) = p.eval x * Multiset.count x n := by
          rw [ mul_comm, Multiset.sum_map_eq_nsmul_single x ] <;> aesop;
        exact h_neq ( by rw [ mul_comm ] at h_sum_p_n; aesop );
      exact h_neq <| by simpa [ h_p_eval_x_ne_zero, mul_comm ] using h_sum_p_m.symm.trans ( h_poly p ) |> Eq.trans <| h_sum_p_n;
    ext x; specialize h_poly_eq x; aesop;
  exact Finset.val_inj.mp (h_multiset A.val B.val h)

/-
The n-th derivative of f(cz) at 0 is c^n times the n-th derivative of f at 0.
-/
lemma iteratedDeriv_comp_const_mul (f : ℂ → ℂ) (c : ℂ) (n : ℕ) :
    iteratedDeriv n (fun z => f (c * z)) 0 = c ^ n * iteratedDeriv n f 0 := by
  -- By induction on $n$, we can show that the $n$-th derivative of $f(cz)$ is $c^n$ times the $n$-th derivative of $f$ evaluated at $cz$.
  have h_ind : ∀ n : ℕ, deriv^[n] (fun z => f (c * z)) = fun z => c^n * deriv^[n] f (c * z) := by
    intro n; induction' n with n ih <;> simp_all +decide [Function.iterate_succ_apply'] ;
    ext z; by_cases hc : c = 0 <;> simp +decide [ hc, pow_succ, mul_assoc, mul_comm c ] ;
    by_cases h : DifferentiableAt ℂ ( deriv^[n] f ) ( z * c ) <;> simp_all +decide [ mul_comm c ];
    · convert HasDerivAt.deriv ( HasDerivAt.comp z ( h.hasDerivAt ) ( hasDerivAt_mul_const c ) ) using 1;
    · rw [ deriv_zero_of_not_differentiableAt ];
      · rw [ deriv_zero_of_not_differentiableAt h, MulZeroClass.zero_mul ];
      · contrapose! h
        have h_diff : DifferentiableAt ℂ (fun x => deriv^[n] f (x * c)) (z * c / c) := by aesop
        convert h_diff.comp ( z * c ) ( differentiableAt_id.div_const c ) using 1 ; aesop;
  simp +decide [ h_ind, iteratedDeriv_eq_iterate ]

/-
The Leibniz rule for iterated derivatives of a product of smooth functions.
-/
lemma iteratedDeriv_mul (f g : ℂ → ℂ) (n : ℕ)
    (hf : ContDiff ℂ ⊤ f) (hg : ContDiff ℂ ⊤ g) :
    iteratedDeriv n (f * g) = fun z => ∑ k ∈ Finset.range (n + 1), (Nat.choose n k : ℂ) * iteratedDeriv k f z * iteratedDeriv (n - k) g z := by
  induction' n with n ih generalizing f g;
  · aesop;
  · -- Apply the product rule to each term in the sum.
    have h_prod_rule : deriv (fun z => ∑ k ∈ Finset.range (n + 1), Nat.choose n k * iteratedDeriv k f z * iteratedDeriv (n - k) g z) = fun z => ∑ k ∈ Finset.range (n + 1), Nat.choose n k * iteratedDeriv (k + 1) f z * iteratedDeriv (n - k) g z + ∑ k ∈ Finset.range (n + 1), Nat.choose n k * iteratedDeriv k f z * iteratedDeriv (n - k + 1) g z := by
      ext z;
      convert HasDerivAt.deriv ( HasDerivAt.sum fun i hi => ?_ ) using 1;
      congr! 1;
      exact
        Eq.symm
          (Finset.sum_fn (Finset.range (n + 1)) fun c a ↦
            ↑(n.choose c) * iteratedDeriv c f a * iteratedDeriv (n - c) g a);
      rw [ ← Finset.sum_add_distrib ];
      convert HasDerivAt.mul ( HasDerivAt.mul ( hasDerivAt_const _ _ ) ( hasDerivAt_deriv_iff.mpr _ ) ) ( hasDerivAt_deriv_iff.mpr _ ) using 1;
      · norm_num [ iteratedDeriv_succ ];
      · apply_rules [ ContDiff.differentiable_iteratedDeriv, hf, hg ];
        exact WithTop.coe_lt_top _;
      · apply_rules [ ContDiff.differentiable_iteratedDeriv, hf, hg ];
        exact WithTop.coe_lt_top _;
    rw [ iteratedDeriv_succ ];
    ext z; rw [ ih f g hf hg, h_prod_rule ] ; rw [ Finset.sum_range_succ, Finset.sum_range_succ' ] ; simp +decide [Nat.choose_succ_succ,
      mul_assoc, mul_comm] ;
    rw [ Finset.sum_range_succ, Finset.sum_range_succ' ] ; simp +decide [mul_add, mul_comm,
      Finset.sum_add_distrib];
    rw [ show ( ∑ x ∈ Finset.range n, iteratedDeriv ( x + 1 ) f z * ( iteratedDeriv ( n - ( x + 1 ) + 1 ) g z * ( n.choose ( x + 1 ) : ℂ ) ) ) = ∑ x ∈ Finset.range n, iteratedDeriv ( n - x ) g z * ( iteratedDeriv ( x + 1 ) f z * ( n.choose ( x + 1 ) : ℂ ) ) from Finset.sum_congr rfl fun x hx => by rw [ tsub_add_eq_add_tsub ( by linarith [ Finset.mem_range.mp hx ] ) ] ; simp +decide [mul_left_comm] ] ; ring

/-
If the first m-1 derivatives of f at 0 vanish, then (fg)^(m)(0) = f^(m)(0) g(0).
-/
lemma iteratedDeriv_mul_eq_of_vanish (f g : ℂ → ℂ) (m : ℕ)
    (hf : ContDiff ℂ ⊤ f) (hg : ContDiff ℂ ⊤ g)
    (h_vanish : ∀ k < m, iteratedDeriv k f 0 = 0) :
    iteratedDeriv m (f * g) 0 = (iteratedDeriv m f 0) * (g 0) := by
  rw [ iteratedDeriv_mul _ _ ];
  · simp +decide [Finset.sum_range_succ];
    exact Finset.sum_eq_zero fun k hk => by rw [ h_vanish k ( Finset.mem_range.mp hk ) ] ; ring;
  · exact hf
  · exact hg

end AristotleLemmas

theorem erdos_494.variant.k_eq_2_card_not_pow_two :
    ∀ card : ℕ, (¬∃ l : ℕ, card = 2 ^ l) → erdos_494_unique 2 card := by
  intro card hnot_pow_two A B hA_card hB_card hsum_eq
  by_contra hneq;
  -- Let $m$ be the minimal $k$ such that $powerSum A k \neq powerSum B k$.
  obtain ⟨m, hm⟩ : ∃ m : ℕ, (powerSum A m ≠ powerSum B m) ∧ (∀ k < m, powerSum A k = powerSum B k) := by
    have h_exists_m : ∃ m : ℕ, powerSum A m ≠ powerSum B m := by
      exact not_forall.mp fun h => hneq <| power_sums_inj A B h;
    exact ⟨ Nat.find h_exists_m, Nat.find_spec h_exists_m, fun k hk => by aesop ⟩;
  -- Differentiate the functional equation $m$ times at $z=0$.
  have h_diff : (iteratedDeriv m (fun z => (expsum A z - expsum B z) * (expsum A z + expsum B z)) 0) = (iteratedDeriv m (fun z => expsum A (2 * z) - expsum B (2 * z)) 0) := by
    congr with z;
    have := expsum_sq A z; have := expsum_sq B z; have := expsum_pair_sum_eq hsum_eq z; ring_nf at *; aesop;
  -- By `iteratedDeriv_mul_eq_of_vanish`, this equals `(iteratedDeriv m h 0) * (f_A(0) + f_B(0))`.
  have h_lhs : (iteratedDeriv m (fun z => (expsum A z - expsum B z) * (expsum A z + expsum B z)) 0) = (iteratedDeriv m (fun z => expsum A z - expsum B z) 0) * (expsum A 0 + expsum B 0) := by
    apply Erdos494.iteratedDeriv_mul_eq_of_vanish;
    · exact ContDiff.sub ( ContDiff.sum fun _ _ => Complex.contDiff_exp.comp ( contDiff_const.mul contDiff_id ) ) ( ContDiff.sum fun _ _ => Complex.contDiff_exp.comp ( contDiff_const.mul contDiff_id ) );
    · exact ContDiff.add ( ContDiff.sum fun _ _ => Complex.contDiff_exp.comp ( contDiff_const.mul contDiff_id ) ) ( ContDiff.sum fun _ _ => Complex.contDiff_exp.comp ( contDiff_const.mul contDiff_id ) );
    · intro k hk; have := hm.2 k hk;
      -- By `expsum_iteratedDeriv`, `iteratedDeriv k h 0 = powerSum A k - powerSum B k`.
      have h_iteratedDeriv : iteratedDeriv k (fun z => expsum A z - expsum B z) 0 = powerSum A k - powerSum B k := by
        convert congr_arg₂ ( · - · ) ( expsum_iteratedDeriv A k ) ( expsum_iteratedDeriv B k ) using 1;
        apply_rules [ iteratedDeriv_sub ];
        · exact ContDiffAt.sum fun x hx => Complex.contDiff_exp.contDiffAt.comp _ ( contDiffAt_const.mul contDiffAt_id );
        · exact ContDiffAt.sum fun x hx => Complex.contDiff_exp.contDiffAt.comp _ ( contDiffAt_const.mul contDiffAt_id );
      aesop;
  -- By `iteratedDeriv_comp_const_mul`, this equals `2^m * (iteratedDeriv m h 0)`.
  have h_rhs : (iteratedDeriv m (fun z => expsum A (2 * z) - expsum B (2 * z)) 0) = (2 : ℂ) ^ m * (iteratedDeriv m (fun z => expsum A z - expsum B z) 0) := by
    convert Erdos494.iteratedDeriv_comp_const_mul ( fun z => expsum A z - expsum B z ) 2 m using 1;
  -- Since `iteratedDeriv m h 0 \neq 0`, we can cancel it to get `f_A(0) + f_B(0) = 2^m`.
  have h_cancel : expsum A 0 + expsum B 0 = (2 : ℂ) ^ m := by
    have h_cancel : iteratedDeriv m (fun z => expsum A z - expsum B z) 0 ≠ 0 := by
      have h_nonzero : iteratedDeriv m (fun z => expsum A z - expsum B z) 0 = powerSum A m - powerSum B m := by
        have h_nonzero : iteratedDeriv m (fun z => expsum A z - expsum B z) 0 = iteratedDeriv m (expsum A) 0 - iteratedDeriv m (expsum B) 0 := by
          apply_rules [ iteratedDeriv_sub ];
          · exact ContDiffAt.sum fun x hx => Complex.contDiff_exp.contDiffAt.comp _ ( contDiffAt_const.mul contDiffAt_id );
          · exact ContDiffAt.sum fun x hx => Complex.contDiff_exp.contDiffAt.comp _ ( contDiffAt_const.mul contDiffAt_id );
        rw [ h_nonzero, expsum_iteratedDeriv, expsum_iteratedDeriv ];
      exact h_nonzero.symm ▸ sub_ne_zero_of_ne hm.1;
    exact mul_left_cancel₀ h_cancel <| by linear_combination' h_lhs.symm.trans h_diff + h_rhs;
  unfold expsum at h_cancel; simp_all +decide;
  norm_cast at h_cancel; simp_all +decide [ ← two_mul ] ;
  exact hnot_pow_two ( m - 1 ) ( by cases m <;> simp_all +decide [ pow_succ' ] )

end Erdos494