Ramsey lemma

lemma ramsey_lemma {C : Type} {cs : Set C} {φ : ℕ → ℕ} {col : ℕ → ℕ → C}    (h_fin : cs.Finite) (h_mono : StrictMono φ) (h_col : ∀ i j, i < j → col (φ i) (φ j) ∈ cs) :    ∃ c ∈ cs, ∃ σ : ℕ → ℕ, StrictMono σ ∧ ∀ i j, i < j → col (φ (σ i)) (φ (σ j)) = c := by  let Vertex := ↑(Set.range φ)  have : Infinite Vertex := by refine Infinite.to_subtype (strict_mono_infinite h_mono)  let Color := {c // c ∈ cs}  have : Finite Color := by exact h_fin  have φ' := Equiv.ofInjective φ <| StrictMono.injective h_mono  let color (e : Finset Vertex) : Color :=    let ns := e.image φ'.invFun    if h_2 : ns.card = 2 then      have h_ne : ns.Nonempty := by apply Finset.card_ne_zero.mp ; simp [h_2]      ⟨col (φ (ns.min' h_ne)) (φ (ns.max' h_ne)), by        obtain ⟨x, y, h_xy, h_ns⟩ := Finset.card_eq_two.mp h_2        simp [h_ns, h_col (min x y) (max x y) (by simp [h_xy.symm])]⟩    else ⟨col (φ 0) (φ 1), by exact h_col 0 1 (by omega)⟩  obtain ⟨c, vs, h_inf_vs, h_col_vs⟩ := inf_graph_ramsey color  use ↑c ; constructor  · exact Subtype.coe_prop c  let ns := φ' ⁻¹' vs  have h_inf_ns : ns.Infinite := by    apply Infinite.preimage h_inf_vs    exact subset_range_of_surjective φ'.surjective vs  obtain ⟨σ, h_mono_σ, h_ns⟩ := infinite_strict_mono h_inf_ns  use σ ; simp [h_mono_σ] ; intro i j h_ij  obtain ⟨rfl⟩ := h_col_vs {φ' (σ i), φ' (σ j)} (by    apply Finset.card_pair ; by_contra h_contra    have := StrictMono.injective h_mono_σ <| φ'.injective h_contra ; omega  ) (by    simp [insert_subset_iff] ; constructor    · have h_i : σ i ∈ ns := by simp [← h_ns]      unfold ns at h_i ; rwa [← mem_preimage]    · have h_j : σ j ∈ ns := by simp [← h_ns]      unfold ns at h_j ; rwa [← mem_preimage])  have h_2 : Finset.card {σ i, σ j} = 2 := by    apply Finset.card_pair ; by_contra h_contra    have := StrictMono.injective h_mono_σ h_contra ; omega  have h_ij_σ := h_mono_σ h_ij  simp [color, h_2, min_eq_left_of_lt h_ij_σ, max_eq_right_of_lt h_ij_σ]