Erdős #1 — largest 3-element sum-distinct subset of [1,N] (N≥4)

import Mathlib

open Filter
open scoped Topology Real

abbrev IsSumDistinctSet (A : Finset ℕ) (N : ℕ) : Prop :=
    A ⊆ Finset.Icc 1 N ∧ (fun (⟨S, _⟩ : A.powerset) => S.sum id).Injective

theorem erdos1_least_N_3 :
    IsLeast { N | ∃ A, IsSumDistinctSet A N ∧ A.card = 3 } 4 := by
  refine ⟨⟨{1, 2, 4}, ?_⟩, ?_⟩
  · simp
    refine ⟨by decide, ?_⟩
    let P := Finset.powerset {1, 2, 4}
    have : Finset.univ.image (fun p : P ↦ ∑ x ∈ p, x) = {0, 1, 2, 4, 3, 5, 6, 7} := by
      refine Finset.ext_iff.mpr (fun n => ?_)
      simp [show P = {{}, {1}, {2}, {4}, {1, 2}, {1, 4}, {2, 4}, {1, 2, 4}} by decide]
      omega
    rw [← Set.injOn_univ, ← Finset.coe_univ]
    have : (Finset.univ.image (fun p : P ↦ ∑ x ∈ p.1, x)).card = (Finset.univ (α := P)).card := by
      rw [this]; aesop
    exact Finset.injOn_of_card_image_eq this
  · simp [mem_lowerBounds]
    intro n S h h_inj hcard3
    by_contra hn
    interval_cases n; aesop; aesop
    · have := Finset.card_le_card h
      aesop
    · absurd h_inj
      rw [(Finset.subset_iff_eq_of_card_le (Nat.le_of_eq (by rw [hcard3]; decide))).mp h]
      decide