module
public import FormalConjecturesForMathlib.Combinatorics.Ramsey
public import Mathlib.Data.Nat.Choose.Central
Erdős–Szekeres 1935 upper bound for the diagonal Ramsey number
Statement (Erdős–Szekeres 1935): For every k : ℕ, the diagonal Ramsey number satisfies
Combinatorics.hypergraphRamsey 2 k ≤ 4 ^ k.
Proof sketch. Use the symmetric recursion R(s, t) ≤ R(s-1, t) + R(s, t-1) with base
cases R(0, t) = R(s, 0) = 1. Induction on s + t then gives R(s, t) ≤ C(s+t, s); for
s = t = k this is R(k, k) ≤ C(2k, k) ≤ 4 ^ k (the Catalan-like central binomial
coefficient bound).
The whole argument is phrased directly on the Mathlib-style coloring data
c : Finset (Fin m) → Bool of 2-element subsets — no auxiliary "edge colouring" structure
is introduced.
Reference: [ES35] Erdős, P. and Szekeres, G. (1935). "A combinatorial problem in
geometry." Compositio Math. 2 , pp. 463–470.
@[ expose ] public section namespace Combinatorics namespace Diagonal
Off-diagonal Ramsey via a subset-indexed predicate
Rather than introduce an auxiliary edge-colouring structure, we phrase the off-diagonal
Ramsey statement as a property of an arbitrary Finset (Fin m) of sufficient cardinality
inside a Bool-valued coloring of all subsets of Fin m. We only ever query the coloring
on 2-element subsets. This setup matches the shape of
Combinatorics.hypergraphRamsey 2 directly.
HasRamseyProperty N s t asserts: for every m, every coloring
c : Finset (Fin m) → Bool, and every V : Finset (Fin m) with V.card ≥ N, the subset
V contains either a subset of size s whose 2-element subsets are all false-coloured,
or a subset of size t whose 2-element subsets are all true-coloured.
This is the "off-diagonal Ramsey number does not exceed N" form of the classical
Erdős–Szekeres Ramsey recurrence, packaged in the same shape used by
Combinatorics.hypergraphRamsey.
def HasRamseyProperty ( N s t : ℕ ) : Prop :=
∀ { m : ℕ } ( c : Finset ( Fin m ) → Bool ) ( V : Finset ( Fin m ) ) , N ≤ V . card →
( ∃ S ⊆ V , S . card = s ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
( ∃ S ⊆ V , S . card = t ∧ ∀ e ⊆ S , e . card = 2 → c e = true )
Monotonicity. If N ≤ N' then HasRamseyProperty N s t → HasRamseyProperty N' s t.
lemma HasRamseyProperty.mono { N N' s t : ℕ } ( hNN' : N ≤ N' ) ( h : HasRamseyProperty N s t ) :
HasRamseyProperty N' s t := by N : ℕ N' : ℕ s : ℕ t : ℕ hNN' : N ≤ N' h : HasRamseyProperty N s t ⊢ HasRamseyProperty N' s t
intro m c V hV N : ℕ N' : ℕ s : ℕ t : ℕ hNN' : N ≤ N' h : HasRamseyProperty N s t m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : N' ≤ V . card ⊢ (∃ S ⊆ V , S . card = s ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = t ∧ ∀ e ⊆ S , e . card = 2 → c e = true
exact h c V ( hNN' . trans hV ) All goals completed! 🐙
Base case s = 0. Any V contains an empty false-monochromatic set.
lemma hasRamseyProperty_zero_left ( N t : ℕ ) : HasRamseyProperty N 0 t := by N : ℕ t : ℕ ⊢ HasRamseyProperty N 0 t
intro m c V _hV N : ℕ t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) _hV : N ≤ V . card ⊢ (∃ S ⊆ V , S . card = 0 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = t ∧ ∀ e ⊆ S , e . card = 2 → c e = true
refine Or.inl ⟨ ∅ , Finset.empty_subset _ , by N : ℕ t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) _hV : N ≤ V . card ⊢ ∅ . card = 0 simp All goals completed! 🐙 , ? _ ⟩
intro e he _ N : ℕ t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) _hV : N ≤ V . card e : Finset ( Fin m ) he : e ⊆ ∅ a✝ : e . card = 2 ⊢ c e = false
have he_empty : e = ∅ := Finset.subset_empty . mp he N : ℕ t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) _hV : N ≤ V . card e : Finset ( Fin m ) he : e ⊆ ∅ a✝ : e . card = 2 he_empty : e = ∅ ⊢ c e = false
simp [ he_empty ] at * All goals completed! 🐙
Base case t = 0. Any V contains an empty true-monochromatic set.
lemma hasRamseyProperty_zero_right ( N s : ℕ ) : HasRamseyProperty N s 0 := by N : ℕ s : ℕ ⊢ HasRamseyProperty N s 0
intro m c V _hV N : ℕ s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) _hV : N ≤ V . card ⊢ (∃ S ⊆ V , S . card = s ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = 0 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
refine Or.inr ⟨ ∅ , Finset.empty_subset _ , by N : ℕ s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) _hV : N ≤ V . card ⊢ ∅ . card = 0 simp All goals completed! 🐙 , ? _ ⟩
intro e he _ N : ℕ s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) _hV : N ≤ V . card e : Finset ( Fin m ) he : e ⊆ ∅ a✝ : e . card = 2 ⊢ c e = true
have he_empty : e = ∅ := Finset.subset_empty . mp he N : ℕ s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) _hV : N ≤ V . card e : Finset ( Fin m ) he : e ⊆ ∅ a✝ : e . card = 2 he_empty : e = ∅ ⊢ c e = true
simp [ he_empty ] at * All goals completed! 🐙
A singleton has no 2-element subsets, hence is monochromatic of any colour.
lemma forall_two_subset_singleton { m : ℕ } ( v : Fin m ) ( b : Bool )
( c : Finset ( Fin m ) → Bool ) :
∀ e ⊆ ( { v } : Finset ( Fin m ) ) , e . card = 2 → c e = b := by m : ℕ v : Fin m b : Bool c : Finset ( Fin m ) → Bool ⊢ ∀ e ⊆ { v } , e . card = 2 → c e = b
intro e he hecard m : ℕ v : Fin m b : Bool c : Finset ( Fin m ) → Bool e : Finset ( Fin m ) he : e ⊆ { v } hecard : e . card = 2 ⊢ c e = b
have : e . card ≤ 1 := by m : ℕ v : Fin m b : Bool c : Finset ( Fin m ) → Bool ⊢ ∀ e ⊆ { v } , e . card = 2 → c e = b m : ℕ v : Fin m b : Bool c : Finset ( Fin m ) → Bool e : Finset ( Fin m ) he : e ⊆ { v } hecard : e . card = 2 this : e . card ≤ 1 ⊢ c e = b
have := Finset.card_le_card he m : ℕ v : Fin m b : Bool c : Finset ( Fin m ) → Bool e : Finset ( Fin m ) he : e ⊆ { v } hecard : e . card = 2 this : e . card ≤ { v } . card ⊢ e . card ≤ 1 m : ℕ v : Fin m b : Bool c : Finset ( Fin m ) → Bool e : Finset ( Fin m ) he : e ⊆ { v } hecard : e . card = 2 this : e . card ≤ 1 ⊢ c e = b
simpa using this m : ℕ v : Fin m b : Bool c : Finset ( Fin m ) → Bool e : Finset ( Fin m ) he : e ⊆ { v } hecard : e . card = 2 this : e . card ≤ 1 ⊢ c e = b m : ℕ v : Fin m b : Bool c : Finset ( Fin m ) → Bool e : Finset ( Fin m ) he : e ⊆ { v } hecard : e . card = 2 this : e . card ≤ 1 ⊢ c e = b
omega All goals completed! 🐙
Base case s = 1. Any nonempty V contains a singleton false-monochromatic set.
lemma hasRamseyProperty_one_left ( t : ℕ ) : HasRamseyProperty 1 1 t := by t : ℕ ⊢ HasRamseyProperty 1 1 t
intro m c V hV t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card ⊢ (∃ S ⊆ V , S . card = 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = t ∧ ∀ e ⊆ S , e . card = 2 → c e = true
obtain ⟨ v , hv ⟩ : V . Nonempty := Finset.card_pos . mp ( by t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card ⊢ 0 < V . card t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card v : Fin m hv : v ∈ V ⊢ (∃ S ⊆ V , S . card = 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = t ∧ ∀ e ⊆ S , e . card = 2 → c e = true omega All goals completed! 🐙 t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card v : Fin m hv : v ∈ V ⊢ (∃ S ⊆ V , S . card = 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = t ∧ ∀ e ⊆ S , e . card = 2 → c e = true ) t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card v : Fin m hv : v ∈ V ⊢ (∃ S ⊆ V , S . card = 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = t ∧ ∀ e ⊆ S , e . card = 2 → c e = true
refine Or.inl ⟨ { v } , by t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card v : Fin m hv : v ∈ V ⊢ { v } ⊆ V simpa using hv All goals completed! 🐙 , by t : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card v : Fin m hv : v ∈ V ⊢ { v } . card = 1 simp All goals completed! 🐙 , ? _ ⟩
exact forall_two_subset_singleton v false c All goals completed! 🐙
Base case t = 1. Any nonempty V contains a singleton true-monochromatic set.
lemma hasRamseyProperty_one_right ( s : ℕ ) : HasRamseyProperty 1 s 1 := by s : ℕ ⊢ HasRamseyProperty 1 s 1
intro m c V hV s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card ⊢ (∃ S ⊆ V , S . card = s ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
obtain ⟨ v , hv ⟩ : V . Nonempty := Finset.card_pos . mp ( by s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card ⊢ 0 < V . card s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card v : Fin m hv : v ∈ V ⊢ (∃ S ⊆ V , S . card = s ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true omega All goals completed! 🐙 s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card v : Fin m hv : v ∈ V ⊢ (∃ S ⊆ V , S . card = s ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true ) s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card v : Fin m hv : v ∈ V ⊢ (∃ S ⊆ V , S . card = s ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨ ∃ S ⊆ V , S . card = 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
refine Or.inr ⟨ { v } , by s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card v : Fin m hv : v ∈ V ⊢ { v } ⊆ V simpa using hv All goals completed! 🐙 , by s : ℕ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : 1 ≤ V . card v : Fin m hv : v ∈ V ⊢ { v } . card = 1 simp All goals completed! 🐙 , ? _ ⟩
exact forall_two_subset_singleton v true c All goals completed! 🐙
Pigeonhole step: splitting V \ {v} by colour. For any vertex v ∈ V, the set
V.erase v partitions into false-neighbours of v and true-neighbours of v, and the
cardinalities sum to V.card - 1.
lemma card_false_true_split { m : ℕ } ( c : Finset ( Fin m ) → Bool ) ( V : Finset ( Fin m ) )
{ v : Fin m } ( hv : v ∈ V ) :
( ( V . erase v ) . filter ( fun u => c { v , u } = false ) ) . card
+ ( ( V . erase v ) . filter ( fun u => c { v , u } = true ) ) . card = V . card - 1 := by m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
classical
have hsplit :
( ( V . erase v ) . filter ( fun u => c { v , u } = false ) ) . card
+ ( ( V . erase v ) . filter ( fun u => ¬ c { v , u } = false ) ) . card = ( V . erase v ) . card :=
Finset.card_filter_add_card_filter_not ( s := V . erase v ) ( fun u => c { v , u } = false ) m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
have hne_true : ∀ u : Fin m , ¬ ( c { v , u } = false ) ↔ c { v , u } = true := by m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1 m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
intro u m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card u : Fin m ⊢ ¬ c { v , u } = false ↔ c { v , u } = true m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
cases c { v , u } false m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card u : Fin m ⊢ ¬ false = false ↔ false = true true m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card u : Fin m ⊢ ¬ true = false ↔ true = true m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1 <;> false m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card u : Fin m ⊢ ¬ false = false ↔ false = true true m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card u : Fin m ⊢ ¬ true = false ↔ true = true m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1 simp m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1 m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
have hrw : ( ( V . erase v ) . filter ( fun u => ¬ c { v , u } = false ) ) . card
= ( ( V . erase v ) . filter ( fun u => c { v , u } = true ) ) . card := by m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1 m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
congr 1 m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true ⊢ { u ∈ V . erase v | ¬ c { v , u } = false } = { u ∈ V . erase v | c { v , u } = true } m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
ext u m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true u : Fin m ⊢ u ∈ { u ∈ V . erase v | ¬ c { v , u } = false } ↔ u ∈ { u ∈ V . erase v | c { v , u } = true } m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
simp only [ Finset.mem_filter , and_congr_right_iff ] m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true u : Fin m ⊢ u ∈ V . erase v → ( ¬ c { v , u } = false ↔ c { v , u } = true ) m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
intro _ m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true u : Fin m a✝ : u ∈ V . erase v ⊢ ¬ c { v , u } = false ↔ c { v , u } = true m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
exact hne_true u m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1 m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | ¬ c { v , u } = false } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
rw [ hrw m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1 m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1 ] at hsplit m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = V . card - 1
rw [ hsplit , m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ ( V . erase v ) . card = V . card - 1 All goals completed! 🐙 Finset.card_erase_of_mem hv m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) v : Fin m hv : v ∈ V hsplit : { u ∈ V . erase v | c { v , u } = false } . card + { u ∈ V . erase v | c { v , u } = true } . card = ( V . erase v ) . card hne_true : ∀ ( u : Fin m ), ¬ c { v , u } = false ↔ c { v , u } = true hrw : { u ∈ V . erase v | ¬ c { v , u } = false } . card = { u ∈ V . erase v | c { v , u } = true } . card ⊢ V . card - 1 = V . card - 1 All goals completed! 🐙 ] All goals completed! 🐙
Extending a b-monochromatic clique S by a vertex v that is b-adjacent to every
element of S. Parameterised over the colour b : Bool, this covers both the false and
true extension steps used in HasRamseyProperty.step.
private lemma mono_insert { m : ℕ } { c : Finset ( Fin m ) → Bool } { b : Bool }
{ S : Finset ( Fin m ) } ( hSmono : ∀ e ⊆ S , e . card = 2 → c e = b )
{ v : Fin m } ( hvAdj : ∀ u ∈ S , c { v , u } = b ) :
∀ e ⊆ insert v S , e . card = 2 → c e = b := by m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b ⊢ ∀ e ⊆ insert v S , e . card = 2 → c e = b
classical
intro e he hecard m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b e : Finset ( Fin m ) he : e ⊆ insert v S hecard : e . card = 2 ⊢ c e = b
obtain ⟨ x , y , hxy , rfl ⟩ := Finset.card_eq_two . mp hecard m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 ⊢ c { x , y } = b
have hx : x ∈ insert v S := he ( Finset.mem_insert_self _ _ ) m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S ⊢ c { x , y } = b
have hy : y ∈ insert v S :=
he ( Finset.mem_insert_of_mem ( Finset.mem_singleton . mpr rfl ) ) m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S ⊢ c { x , y } = b
rcases Finset.mem_insert . mp hx with hx_eq | hxS inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hx_eq : x = v ⊢ c { x , y } = b inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S ⊢ c { x , y } = b
· inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hx_eq : x = v ⊢ c { x , y } = b rcases Finset.mem_insert . mp hy with hy_eq | hyS inl.inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hx_eq : x = v hy_eq : y = v ⊢ c { x , y } = b inl.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hx_eq : x = v hyS : y ∈ S ⊢ c { x , y } = b
· inl.inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hx_eq : x = v hy_eq : y = v ⊢ c { x , y } = b exact ( hxy ( hx_eq . trans hy_eq . symm ) ) . elim All goals completed! 🐙
· inl.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hx_eq : x = v hyS : y ∈ S ⊢ c { x , y } = b
rw [ hx_eq inl.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hx_eq : x = v hyS : y ∈ S ⊢ c { v , y } = b inl.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hx_eq : x = v hyS : y ∈ S ⊢ c { v , y } = b ] inl.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hx_eq : x = v hyS : y ∈ S ⊢ c { v , y } = b ; exact hvAdj y hyS All goals completed! 🐙
· inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S ⊢ c { x , y } = b rcases Finset.mem_insert . mp hy with hy_eq | hyS inr.inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hy_eq : y = v ⊢ c { x , y } = b inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S ⊢ c { x , y } = b
· inr.inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hy_eq : y = v ⊢ c { x , y } = b
rw [ hy_eq , inr.inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hy_eq : y = v ⊢ c { x , v } = b inr.inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hy_eq : y = v ⊢ c { v , x } = b Finset.pair_comm inr.inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hy_eq : y = v ⊢ c { v , x } = b inr.inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hy_eq : y = v ⊢ c { v , x } = b ] inr.inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hy_eq : y = v ⊢ c { v , x } = b ; exact hvAdj x hxS All goals completed! 🐙
· inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S ⊢ c { x , y } = b
have hsub : ( { x , y } : Finset ( Fin m ) ) ⊆ S := by m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b ⊢ ∀ e ⊆ insert v S , e . card = 2 → c e = b inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b
intro z hz m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } ⊢ z ∈ S inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b
rcases Finset.mem_insert . mp hz with hz_eq | hz' inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } hz_eq : z = x ⊢ z ∈ S inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } hz' : z ∈ { y } ⊢ z ∈ S inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b
· inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } hz_eq : z = x ⊢ z ∈ S inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b rw [ hz_eq inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } hz_eq : z = x ⊢ x ∈ S inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } hz_eq : z = x ⊢ x ∈ S inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b ] inl m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } hz_eq : z = x ⊢ x ∈ S inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b ; exact hxS All goals completed! 🐙 inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b
· inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } hz' : z ∈ { y } ⊢ z ∈ S inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b rw [ Finset.mem_singleton . mp hz' inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } hz' : z ∈ { y } ⊢ y ∈ S inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } hz' : z ∈ { y } ⊢ y ∈ S inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b ] inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S z : Fin m hz : z ∈ { x , y } hz' : z ∈ { y } ⊢ y ∈ S inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b ; exact hyS inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ c { x , y } = b
have hcard2 : ( { x , y } : Finset ( Fin m ) ) . card = 2 := by m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b ⊢ ∀ e ⊆ insert v S , e . card = 2 → c e = b inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S hcard2 : { x , y } . card = 2 ⊢ c { x , y } = b
rw [ Finset.card_insert_of_notMem ( by m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ x ∉ { y } inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S hcard2 : { x , y } . card = 2 ⊢ c { x , y } = b simpa using hxy All goals completed! 🐙 inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S hcard2 : { x , y } . card = 2 ⊢ c { x , y } = b ) , Finset.card_singleton m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S ⊢ 1 + 1 = 2 inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S hcard2 : { x , y } . card = 2 ⊢ c { x , y } = b ] inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S hcard2 : { x , y } . card = 2 ⊢ c { x , y } = b inr.inr m : ℕ c : Finset ( Fin m ) → Bool b : Bool S : Finset ( Fin m ) hSmono : ∀ e ⊆ S , e . card = 2 → c e = b v : Fin m hvAdj : ∀ u ∈ S , c { v , u } = b x : Fin m y : Fin m hxy : x ≠ y he : { x , y } ⊆ insert v S hecard : { x , y } . card = 2 hx : x ∈ insert v S hy : y ∈ insert v S hxS : x ∈ S hyS : y ∈ S hsub : { x , y } ⊆ S hcard2 : { x , y } . card = 2 ⊢ c { x , y } = b
exact hSmono _ hsub hcard2 All goals completed! 🐙
Recurrence. If HasRamseyProperty Ns s (t+1) and HasRamseyProperty Nt (s+1) t
hold, then HasRamseyProperty (Ns + Nt) (s+1) (t+1) holds.
This is the core Erdős–Szekeres 1935 pigeonhole step: pick any vertex v ∈ V, split
V.erase v into false-neighbours R_v and true-neighbours B_v; by pigeonhole
|R_v| ≥ Ns or |B_v| ≥ Nt. In the first case, invoke HasRamseyProperty Ns s (t+1)
on R_v: either we get a false-mono K_s on R_v (extend by v to a false-mono
K_{s+1} on V), or a true-mono K_{t+1} on R_v ⊆ V (done). The second case is
symmetric.
lemma HasRamseyProperty.step { Ns Nt s t : ℕ }
( hs : HasRamseyProperty Ns s ( t + 1 ) )
( ht : HasRamseyProperty Nt ( s + 1 ) t ) ( hNs : 1 ≤ Ns ) :
HasRamseyProperty ( Ns + Nt ) ( s + 1 ) ( t + 1 ) := by Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns ⊢ HasRamseyProperty ( Ns + Nt ) ( s + 1 ) ( t + 1 )
classical
intro m c V hV Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
have hVpos : 0 < V . card := by Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns ⊢ HasRamseyProperty ( Ns + Nt ) ( s + 1 ) ( t + 1 ) Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
have : 1 ≤ V . card := Nat.le_trans hNs ( Nat.le_trans ( Nat.le_add_right _ _ ) hV ) Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card this : 1 ≤ V . card ⊢ 0 < V . card Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
exact this Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
obtain ⟨ v , hv ⟩ := Finset.card_pos . mp hVpos Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
set R := ( V . erase v ) . filter ( fun u => c { v , u } = false ) with hR_def Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
set B := ( V . erase v ) . filter ( fun u => c { v , u } = true ) with hB_def Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
have hsplit : R . card + B . card = V . card - 1 :=
card_false_true_split c V hv Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
have hRsubV : R ⊆ V := ( Finset.filter_subset _ _ ) . trans ( Finset.erase_subset _ _ ) Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
have hBsubV : B ⊆ V := ( Finset.filter_subset _ _ ) . trans ( Finset.erase_subset _ _ ) Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
have hvnR : v ∉ R := fun h => Finset.notMem_erase _ _ ( Finset.mem_of_mem_filter _ h ) Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
have hvnB : v ∉ B := fun h => Finset.notMem_erase _ _ ( Finset.mem_of_mem_filter _ h ) Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
obtain hRcard | hRcard := le_or_gt Ns R . card inl Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true inr Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
· inl Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
rcases hs c R hRcard with ⟨ S , hSsub , hScard , hSmono ⟩ | ⟨ S , hSsub , hScard , hSmono ⟩ inl.inl Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true inl.inr Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = t + 1 hSmono : ∀ e ⊆ S , e . card = 2 → c e = true ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
· inl.inl Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
have hvS : v ∉ S := fun h => hvnR ( hSsub h ) inl.inl Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
refine Or.inl ⟨ insert v S , ? _ , ? _ , ? _ ⟩ inl.inl.refine_1 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S ⊢ insert v S ⊆ V inl.inl.refine_2 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S ⊢ ( insert v S ) . card = s + 1 inl.inl.refine_3 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S ⊢ ∀ e ⊆ insert v S , e . card = 2 → c e = false
· inl.inl.refine_1 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S ⊢ insert v S ⊆ V intro u hu inl.inl.refine_1 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S u : Fin m hu : u ∈ insert v S ⊢ u ∈ V
rcases Finset.mem_insert . mp hu with rfl | hu' inl.inl.refine_1.inl Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card S : Finset ( Fin m ) hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false u : Fin m hv : u ∈ V R : Finset ( Fin m ) := { u_1 ∈ V . erase u | c { u , u_1 } = false } hR_def : R = { u_1 ∈ V . erase u | c { u , u_1 } = false } B : Finset ( Fin m ) := { u_1 ∈ V . erase u | c { u , u_1 } = true } hB_def : B = { u_1 ∈ V . erase u | c { u , u_1 } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : u ∉ R hvnB : u ∉ B hRcard : Ns ≤ R . card hSsub : S ⊆ R hvS : u ∉ S hu : u ∈ insert u S ⊢ u ∈ V inl.inl.refine_1.inr Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S u : Fin m hu : u ∈ insert v S hu' : u ∈ S ⊢ u ∈ V
· inl.inl.refine_1.inl Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card S : Finset ( Fin m ) hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false u : Fin m hv : u ∈ V R : Finset ( Fin m ) := { u_1 ∈ V . erase u | c { u , u_1 } = false } hR_def : R = { u_1 ∈ V . erase u | c { u , u_1 } = false } B : Finset ( Fin m ) := { u_1 ∈ V . erase u | c { u , u_1 } = true } hB_def : B = { u_1 ∈ V . erase u | c { u , u_1 } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : u ∉ R hvnB : u ∉ B hRcard : Ns ≤ R . card hSsub : S ⊆ R hvS : u ∉ S hu : u ∈ insert u S ⊢ u ∈ V exact hv All goals completed! 🐙
· inl.inl.refine_1.inr Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S u : Fin m hu : u ∈ insert v S hu' : u ∈ S ⊢ u ∈ V exact hRsubV ( hSsub hu' ) All goals completed! 🐙
· inl.inl.refine_2 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S ⊢ ( insert v S ) . card = s + 1 rw [ Finset.card_insert_of_notMem hvS , inl.inl.refine_2 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S ⊢ S . card + 1 = s + 1 All goals completed! 🐙 hScard inl.inl.refine_2 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S ⊢ s + 1 = s + 1 All goals completed! 🐙 ] All goals completed! 🐙
· inl.inl.refine_3 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S ⊢ ∀ e ⊆ insert v S , e . card = 2 → c e = false apply mono_insert hSmono inl.inl.refine_3 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S ⊢ ∀ u ∈ S , c { v , u } = false
intro u hu inl.inl.refine_3 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S u : Fin m hu : u ∈ S ⊢ c { v , u } = false
have hu' : u ∈ R := hSsub hu inl.inl.refine_3 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = s hSmono : ∀ e ⊆ S , e . card = 2 → c e = false hvS : v ∉ S u : Fin m hu : u ∈ S hu' : u ∈ R ⊢ c { v , u } = false
exact ( Finset.mem_filter . mp hu' ) . 2 All goals completed! 🐙
· inl.inr Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : Ns ≤ R . card S : Finset ( Fin m ) hSsub : S ⊆ R hScard : S . card = t + 1 hSmono : ∀ e ⊆ S , e . card = 2 → c e = true ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
exact Or.inr ⟨ S , hSsub . trans hRsubV , hScard , hSmono ⟩ All goals completed! 🐙
· inr Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
rcases ht c B ( by Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns ⊢ Nt ≤ B . card lia All goals completed! 🐙 ) with ⟨ S , hSsub , hScard , hSmono ⟩ | ⟨ S , hSsub , hScard , hSmono ⟩
· inr.inl Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = s + 1 hSmono : ∀ e ⊆ S , e . card = 2 → c e = false ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
exact Or.inl ⟨ S , hSsub . trans hBsubV , hScard , hSmono ⟩ All goals completed! 🐙
· inr.inr Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
have hvS : v ∉ S := fun h => hvnB ( hSsub h ) inr.inr Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S ⊢ (∃ S ⊆ V , S . card = s + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = false ) ∨
∃ S ⊆ V , S . card = t + 1 ∧ ∀ e ⊆ S , e . card = 2 → c e = true
refine Or.inr ⟨ insert v S , ? _ , ? _ , ? _ ⟩ inr.inr.refine_1 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S ⊢ insert v S ⊆ V inr.inr.refine_2 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S ⊢ ( insert v S ) . card = t + 1 inr.inr.refine_3 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S ⊢ ∀ e ⊆ insert v S , e . card = 2 → c e = true
· inr.inr.refine_1 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S ⊢ insert v S ⊆ V intro u hu inr.inr.refine_1 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S u : Fin m hu : u ∈ insert v S ⊢ u ∈ V
rcases Finset.mem_insert . mp hu with rfl | hu' inr.inr.refine_1.inl Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card S : Finset ( Fin m ) hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true u : Fin m hv : u ∈ V R : Finset ( Fin m ) := { u_1 ∈ V . erase u | c { u , u_1 } = false } hR_def : R = { u_1 ∈ V . erase u | c { u , u_1 } = false } B : Finset ( Fin m ) := { u_1 ∈ V . erase u | c { u , u_1 } = true } hB_def : B = { u_1 ∈ V . erase u | c { u , u_1 } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : u ∉ R hvnB : u ∉ B hRcard : R . card < Ns hSsub : S ⊆ B hvS : u ∉ S hu : u ∈ insert u S ⊢ u ∈ V inr.inr.refine_1.inr Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S u : Fin m hu : u ∈ insert v S hu' : u ∈ S ⊢ u ∈ V
· inr.inr.refine_1.inl Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card S : Finset ( Fin m ) hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true u : Fin m hv : u ∈ V R : Finset ( Fin m ) := { u_1 ∈ V . erase u | c { u , u_1 } = false } hR_def : R = { u_1 ∈ V . erase u | c { u , u_1 } = false } B : Finset ( Fin m ) := { u_1 ∈ V . erase u | c { u , u_1 } = true } hB_def : B = { u_1 ∈ V . erase u | c { u , u_1 } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : u ∉ R hvnB : u ∉ B hRcard : R . card < Ns hSsub : S ⊆ B hvS : u ∉ S hu : u ∈ insert u S ⊢ u ∈ V exact hv All goals completed! 🐙
· inr.inr.refine_1.inr Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S u : Fin m hu : u ∈ insert v S hu' : u ∈ S ⊢ u ∈ V exact hBsubV ( hSsub hu' ) All goals completed! 🐙
· inr.inr.refine_2 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S ⊢ ( insert v S ) . card = t + 1 rw [ Finset.card_insert_of_notMem hvS , inr.inr.refine_2 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S ⊢ S . card + 1 = t + 1 All goals completed! 🐙 hScard inr.inr.refine_2 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S ⊢ t + 1 = t + 1 All goals completed! 🐙 ] All goals completed! 🐙
· inr.inr.refine_3 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S ⊢ ∀ e ⊆ insert v S , e . card = 2 → c e = true apply mono_insert hSmono inr.inr.refine_3 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S ⊢ ∀ u ∈ S , c { v , u } = true
intro u hu inr.inr.refine_3 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S u : Fin m hu : u ∈ S ⊢ c { v , u } = true
have hu' : u ∈ B := hSsub hu inr.inr.refine_3 Ns : ℕ Nt : ℕ s : ℕ t : ℕ hs : HasRamseyProperty Ns s ( t + 1 ) ht : HasRamseyProperty Nt ( s + 1 ) t hNs : 1 ≤ Ns m : ℕ c : Finset ( Fin m ) → Bool V : Finset ( Fin m ) hV : Ns + Nt ≤ V . card hVpos : 0 < V . card v : Fin m hv : v ∈ V R : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = false } hR_def : R = { u ∈ V . erase v | c { v , u } = false } B : Finset ( Fin m ) := { u ∈ V . erase v | c { v , u } = true } hB_def : B = { u ∈ V . erase v | c { v , u } = true } hsplit : R . card + B . card = V . card - 1 hRsubV : R ⊆ V hBsubV : B ⊆ V hvnR : v ∉ R hvnB : v ∉ B hRcard : R . card < Ns S : Finset ( Fin m ) hSsub : S ⊆ B hScard : S . card = t hSmono : ∀ e ⊆ S , e . card = 2 → c e = true hvS : v ∉ S u : Fin m hu : u ∈ S hu' : u ∈ B ⊢ c { v , u } = true
exact ( Finset.mem_filter . mp hu' ) . 2 All goals completed! 🐙
Binomial bound via Erdős–Szekeres induction.
HasRamseyProperty (Nat.choose (s + t) s) s t for all s, t.
lemma hasRamseyProperty_choose : ∀ ( s t : ℕ ) ,
HasRamseyProperty ( Nat.choose ( s + t ) s ) s t := by ⊢ ∀ ( s t : ℕ ), HasRamseyProperty ( ( s + t ) . choose s ) s t
suffices h : ∀ ( n : ℕ ) , ∀ ( s t : ℕ ) , s + t = n → HasRamseyProperty ( Nat.choose n s ) s t by h : ∀ ( n s t : ℕ ), s + t = n → HasRamseyProperty ( n . choose s ) s t ⊢ ∀ ( s t : ℕ ), HasRamseyProperty ( ( s + t ) . choose s ) s t ⊢ ∀ ( n s t : ℕ ), s + t = n → HasRamseyProperty ( n . choose s ) s t
intro s t h : ∀ ( n s t : ℕ ), s + t = n → HasRamseyProperty ( n . choose s ) s t s : ℕ t : ℕ ⊢ HasRamseyProperty ( ( s + t ) . choose s ) s t ⊢ ∀ ( n s t : ℕ ), s + t = n → HasRamseyProperty ( n . choose s ) s t
exact h ( s + t ) s t rfl ⊢ ∀ ( n s t : ℕ ), s + t = n → HasRamseyProperty ( n . choose s ) s t ⊢ ∀ ( n s t : ℕ ), s + t = n → HasRamseyProperty ( n . choose s ) s t
intro n n : ℕ ⊢ ∀ ( s t : ℕ ), s + t = n → HasRamseyProperty ( n . choose s ) s t
induction n using Nat.strong_induction_on with
| _ n ih => h n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t ⊢ ∀ ( s t : ℕ ), s + t = n → HasRamseyProperty ( n . choose s ) s t
intro s t hst h n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s : ℕ t : ℕ hst : s + t = n ⊢ HasRamseyProperty ( n . choose s ) s t
match s , t , hst with
| 0 , t , hst => n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s : ℕ t✝ : ℕ hst✝ : s + t = n t : ℕ hst : 0 + t = n ⊢ HasRamseyProperty ( n . choose 0 ) 0 t
show HasRamseyProperty ( Nat.choose n 0 ) 0 t n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s : ℕ t✝ : ℕ hst✝ : s + t = n t : ℕ hst : 0 + t = n ⊢ HasRamseyProperty ( n . choose 0 ) 0 t
rw [ Nat.choose_zero_right n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s : ℕ t✝ : ℕ hst✝ : s + t = n t : ℕ hst : 0 + t = n ⊢ HasRamseyProperty 1 0 t n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s : ℕ t✝ : ℕ hst✝ : s + t = n t : ℕ hst : 0 + t = n ⊢ HasRamseyProperty 1 0 t ] n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s : ℕ t✝ : ℕ hst✝ : s + t = n t : ℕ hst : 0 + t = n ⊢ HasRamseyProperty 1 0 t
exact HasRamseyProperty.mono ( Nat.zero_le _ ) ( hasRamseyProperty_zero_left 0 t ) All goals completed! 🐙
| s + 1 , 0 , hst => n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t : ℕ hst✝ : s + t = n s : ℕ hst : s + 1 + 0 = n ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) 0
show HasRamseyProperty ( Nat.choose n ( s + 1 ) ) ( s + 1 ) 0 n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t : ℕ hst✝ : s + t = n s : ℕ hst : s + 1 + 0 = n ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) 0
exact HasRamseyProperty.mono ( Nat.zero_le _ ) ( hasRamseyProperty_zero_right 0 ( s + 1 ) ) All goals completed! 🐙
| s + 1 , t + 1 , hst => n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
have hn_pred : n - 1 + 1 = n := by ⊢ ∀ ( s t : ℕ ), HasRamseyProperty ( ( s + t ) . choose s ) s t n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) omega n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
have hs_ih : HasRamseyProperty ( Nat.choose ( n - 1 ) s ) s ( t + 1 ) := by ⊢ ∀ ( s t : ℕ ), HasRamseyProperty ( ( s + t ) . choose s ) s t n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
apply ih ( n - 1 ) ( by n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n ⊢ n - 1 < n n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) omega All goals completed! 🐙 n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) ) s ( t + 1 )
omega n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
have ht_ih : HasRamseyProperty ( Nat.choose ( n - 1 ) ( s + 1 ) ) ( s + 1 ) t := by ⊢ ∀ ( s t : ℕ ), HasRamseyProperty ( ( s + t ) . choose s ) s t n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
apply ih ( n - 1 ) ( by n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ⊢ n - 1 < n n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) omega All goals completed! 🐙 n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) ) ( s + 1 ) t
omega n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
have hNs_pos : 1 ≤ Nat.choose ( n - 1 ) s := by ⊢ ∀ ( s t : ℕ ), HasRamseyProperty ( ( s + t ) . choose s ) s t n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
have : s ≤ n - 1 := by ⊢ ∀ ( s t : ℕ ), HasRamseyProperty ( ( s + t ) . choose s ) s t n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t this : s ≤ n - 1 ⊢ 1 ≤ ( n - 1 ) . choose s n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) omega n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t this : s ≤ n - 1 ⊢ 1 ≤ ( n - 1 ) . choose s n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t this : s ≤ n - 1 ⊢ 1 ≤ ( n - 1 ) . choose s n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
exact Nat.choose_pos this n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
have hrec : HasRamseyProperty ( Nat.choose ( n - 1 ) s + Nat.choose ( n - 1 ) ( s + 1 ) )
( s + 1 ) ( t + 1 ) := HasRamseyProperty.step hs_ih ht_ih hNs_pos n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
have hpascal : Nat.choose n ( s + 1 ) = Nat.choose ( n - 1 ) s + Nat.choose ( n - 1 ) ( s + 1 ) := by ⊢ ∀ ( s t : ℕ ), HasRamseyProperty ( ( s + t ) . choose s ) s t n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) hpascal : n . choose ( s + 1 ) = ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
conv_lhs => rw [ ← hn_pred ] n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) | ( n - 1 + 1 ) . choose ( s + 1 ) n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) hpascal : n . choose ( s + 1 ) = ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
rw [ Nat.choose_succ_succ n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) ⊢ ( n - 1 ) . choose s + ( n - 1 ) . choose s . succ = ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) hpascal : n . choose ( s + 1 ) = ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) ] n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) hpascal : n . choose ( s + 1 ) = ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) hpascal : n . choose ( s + 1 ) = ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
show HasRamseyProperty ( Nat.choose n ( s + 1 ) ) ( s + 1 ) ( t + 1 ) n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) hpascal : n . choose ( s + 1 ) = ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ⊢ HasRamseyProperty ( n . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
rw [ hpascal n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) hpascal : n . choose ( s + 1 ) = ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ⊢ HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) hpascal : n . choose ( s + 1 ) = ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ⊢ HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) ] n : ℕ ih : ∀ m < n , ∀ ( s t : ℕ ), s + t = m → HasRamseyProperty ( m . choose s ) s t s✝ : ℕ t✝ : ℕ hst✝ : s + t = n s : ℕ t : ℕ hst : s + 1 + ( t + 1 ) = n hn_pred : n - 1 + 1 = n hs_ih : HasRamseyProperty ( ( n - 1 ) . choose s ) s ( t + 1 ) ht_ih : HasRamseyProperty ( ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) t hNs_pos : 1 ≤ ( n - 1 ) . choose s hrec : HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 ) hpascal : n . choose ( s + 1 ) = ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ⊢ HasRamseyProperty ( ( n - 1 ) . choose s + ( n - 1 ) . choose ( s + 1 ) ) ( s + 1 ) ( t + 1 )
exact hrec All goals completed! 🐙 end Diagonal
Erdős–Szekeres 1935 in hypergraphRamsey form:
Combinatorics.hypergraphRamsey 2 k ≤ 4 ^ k for all k.
Proof. Diagonal.hasRamseyProperty_choose applied at s = t = k and the full vertex
set V = Finset.univ of Fin (C(2k, k)) shows that C(2k, k) is a member of the defining
set of hypergraphRamsey 2 k, hence by Nat.sInf_le we get
hypergraphRamsey 2 k ≤ C(2k, k); the central binomial bound
C(2k, k) ≤ 4 ^ k closes the result.
lemma _root_.Combinatorics.hypergraphRamsey_two_le_four_pow ( k : ℕ ) :
Combinatorics.hypergraphRamsey 2 k ≤ 4 ^ k := by k : ℕ ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
have hprop : Diagonal.HasRamseyProperty ( Nat.choose ( k + k ) k ) k k :=
Diagonal.hasRamseyProperty_choose k k k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
have hmem : Nat.choose ( k + k ) k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ) ,
∃ ( S : Finset ( Fin m ) ) , S . card = k ∧ ∃ ( color : Bool ) ,
∀ ( e : Finset ( Fin m ) ) , e ⊆ S → e . card = 2 → c e = color } := by
intro c k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool ⊢ ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
have hV : Nat.choose ( k + k ) k ≤
( Finset.univ : Finset ( Fin ( Nat.choose ( k + k ) k ) ) ) . card := by k : ℕ ⊢ hypergraphRamsey 2 k ≤ 4 ^ k k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool hV : ( k + k ) . choose k ≤ Finset.univ . card ⊢ ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
rw [ Finset.card_univ , k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool ⊢ ( k + k ) . choose k ≤ Fintype.card ( Fin ( ( k + k ) . choose k ) ) k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool hV : ( k + k ) . choose k ≤ Finset.univ . card ⊢ ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k Fintype.card_fin k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool ⊢ ( k + k ) . choose k ≤ ( k + k ) . choose k k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool hV : ( k + k ) . choose k ≤ Finset.univ . card ⊢ ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k ] k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool hV : ( k + k ) . choose k ≤ Finset.univ . card ⊢ ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool hV : ( k + k ) . choose k ≤ Finset.univ . card ⊢ ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
rcases hprop c Finset.univ hV with ⟨ S , _hSsub , hScard , hSmono ⟩ | ⟨ S , _hSsub , hScard , hSmono ⟩ inl k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool hV : ( k + k ) . choose k ≤ Finset.univ . card S : Finset ( Fin ( ( k + k ) . choose k ) ) _hSsub : S ⊆ Finset.univ hScard : S . card = k hSmono : ∀ e ⊆ S , e . card = 2 → c e = false ⊢ ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color inr k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool hV : ( k + k ) . choose k ≤ Finset.univ . card S : Finset ( Fin ( ( k + k ) . choose k ) ) _hSsub : S ⊆ Finset.univ hScard : S . card = k hSmono : ∀ e ⊆ S , e . card = 2 → c e = true ⊢ ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
· inl k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool hV : ( k + k ) . choose k ≤ Finset.univ . card S : Finset ( Fin ( ( k + k ) . choose k ) ) _hSsub : S ⊆ Finset.univ hScard : S . card = k hSmono : ∀ e ⊆ S , e . card = 2 → c e = false ⊢ ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k exact ⟨ S , hScard , false , hSmono ⟩ All goals completed! 🐙 k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
· inr k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k c : Finset ( Fin ( ( k + k ) . choose k ) ) → Bool hV : ( k + k ) . choose k ≤ Finset.univ . card S : Finset ( Fin ( ( k + k ) . choose k ) ) _hSsub : S ⊆ Finset.univ hScard : S . card = k hSmono : ∀ e ⊆ S , e . card = 2 → c e = true ⊢ ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k exact ⟨ S , hScard , true , hSmono ⟩ k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
have hle : Combinatorics.hypergraphRamsey 2 k ≤ Nat.choose ( k + k ) k := Nat.sInf_le hmem k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } hle : hypergraphRamsey 2 k ≤ ( k + k ) . choose k ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
have h2kk : Nat.choose ( k + k ) k = Nat.choose ( 2 * k ) k := by rw [ two_mul k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } hle : hypergraphRamsey 2 k ≤ ( k + k ) . choose k ⊢ ( k + k ) . choose k = ( k + k ) . choose k k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } hle : hypergraphRamsey 2 k ≤ ( k + k ) . choose k h2kk : ( k + k ) . choose k = ( 2 * k ) . choose k ⊢ hypergraphRamsey 2 k ≤ 4 ^ k ] k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } hle : hypergraphRamsey 2 k ≤ ( k + k ) . choose k h2kk : ( k + k ) . choose k = ( 2 * k ) . choose k ⊢ hypergraphRamsey 2 k ≤ 4 ^ k k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } hle : hypergraphRamsey 2 k ≤ ( k + k ) . choose k h2kk : ( k + k ) . choose k = ( 2 * k ) . choose k ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
rw [ h2kk k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } hle : hypergraphRamsey 2 k ≤ ( 2 * k ) . choose k h2kk : ( k + k ) . choose k = ( 2 * k ) . choose k ⊢ hypergraphRamsey 2 k ≤ 4 ^ k k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } hle : hypergraphRamsey 2 k ≤ ( 2 * k ) . choose k h2kk : ( k + k ) . choose k = ( 2 * k ) . choose k ⊢ hypergraphRamsey 2 k ≤ 4 ^ k ] at hle k : ℕ hprop : Diagonal.HasRamseyProperty ( ( k + k ) . choose k ) k k hmem : ( k + k ) . choose k ∈ { m | ∀ ( c : Finset ( Fin m ) → Bool ), ∃ S , S . card = k ∧ ∃ color , ∀ e ⊆ S , e . card = 2 → c e = color } hle : hypergraphRamsey 2 k ≤ ( 2 * k ) . choose k h2kk : ( k + k ) . choose k = ( 2 * k ) . choose k ⊢ hypergraphRamsey 2 k ≤ 4 ^ k
exact hle . trans ( Nat.centralBinom_le_four_pow k ) All goals completed! 🐙 end Combinatorics