Lean4
/-- If `G` is `Kᵣ₊₂`-free and contains a `Wᵣ,ₖ` together with a vertex `x` adjacent to all but at most
two vertices of `Wᵣ,ₖ`, including all of its common clique vertices, then `G` contains a `Wᵣ,ₖ₊₁`.
-/
theorem exists_isFiveWheelLike_succ_of_not_adj_le_two (hW : ∀ ⦃y⦄, y ∈ s ∩ t → G.Adj x y)
(h2 : #({z ∈ { v } ∪ ({ w₁ } ∪ ({ w₂ } ∪ (s ∪ t))) | ¬G.Adj x z}) ≤ 2) :
∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b)) :=
by
obtain ⟨a, b, c, d, ha, haj, hb, hbj, hc, hcj, hd, hdj, hab, had, hbc, hat, hbs⟩ :=
hw.exist_not_adj_of_adj_inter hcf hW
let W := { v } ∪ ({ w₁ } ∪ ({ w₂ } ∪ (s ∪ t)))
have ⟨hca, hdb⟩ : c = a ∧ d = b := by
by_contra! hf
apply h2.not_gt <| two_lt_card_iff.2 _
by_cases h : a = c
· exact ⟨a, b, d, by grind⟩
· exact ⟨a, b, c, by grind⟩
simp_rw [hca, hdb, mem_insert] at *
have ⟨has, hbt, hav, hbv, haw, hbw⟩ : a ∈ s ∧ b ∈ t ∧ a ≠ v ∧ b ≠ v ∧ a ≠ w₂ ∧ b ≠ w₁ := by grind
have ⟨hxv, hxw₁, hxw₂⟩ : v ≠ x ∧ w₁ ≠ x ∧ w₂ ≠ x :=
by
refine ⟨?_, ?_, ?_⟩
· by_cases hax : x = a <;> rintro rfl
· grind
· exact haj <| hw.isNClique_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax
· by_cases hax : x = a <;> rintro rfl
· grind
· exact haj <| hw.isNClique_fst_left.1 (mem_insert_self ..) (mem_insert_of_mem has) hax
· by_cases hbx : x = b <;> rintro rfl
· grind
· exact hbj <| hw.isNClique_snd_right.1 (mem_insert_self ..) (mem_insert_of_mem hbt) hbx
have wa : ∀ ⦃w⦄, w ∈ W → w ≠ a → w ≠ b → G.Adj w x :=
by
intro _ hz haz hbz
by_contra! hf
apply h2.not_gt
exact
two_lt_card.2
⟨_, by simp [has, hcj], _, by simp [hbt, hdj], _, mem_filter.2 ⟨hz, by rwa [adj_comm] at hf⟩, hab, haz.symm,
hbz.symm⟩
have ⟨h1s, h2t⟩ : insert w₁ s ⊆ W ∧ insert w₂ t ⊆ W := by
grind
-- We now check that we can build a `Wᵣ,ₖ₊₁` by inserting `x` and erasing `a` and `b`
refine
⟨a, b, ⟨by grind, by grind, by grind, by grind, by grind, ?h5, ?h6, ?h7, ?h8, ?h9⟩⟩
-- Check that the new cliques are indeed cliques
case h5 =>
exact
hw.isNClique_left.insert_insert_erase has hw.notMem_left fun _ hz hZ ↦
wa ((insert_subset_insert _ fun _ hx ↦ (by simp [hx])) hz) hZ fun h ↦
hbv <| (mem_insert.1 (h ▸ hz)).resolve_right hbs
case h6 =>
exact
hw.isNClique_fst_left.insert_insert_erase has hw.fst_notMem fun _ hz hZ ↦
wa (h1s hz) hZ fun h ↦ hbw <| (mem_insert.1 (h ▸ hz)).resolve_right hbs
case h7 =>
exact
hw.isNClique_right.insert_insert_erase hbt hw.notMem_right fun _ hz hZ ↦
wa ((insert_subset_insert _ fun _ hx ↦ (by simp [hx])) hz)
(fun h ↦ hav <| (mem_insert.1 (h ▸ hz)).resolve_right hat) hZ
case h8 =>
exact
hw.isNClique_snd_right.insert_insert_erase hbt hw.snd_notMem fun _ hz hZ ↦
wa (h2t hz) (fun h ↦ haw <| (mem_insert.1 (h ▸ hz)).resolve_right hat) hZ
case h9 =>
-- Finally check that this new `IsFiveWheelLike` structure has `k + 1` common clique
-- vertices i.e. `#((insert x (s.erase a)) ∩ (insert x (s.erase b))) = k + 1`.
rw [← insert_inter_distrib, erase_inter, inter_erase, erase_eq_of_notMem <| notMem_mono inter_subset_left hbs,
erase_eq_of_notMem <| notMem_mono inter_subset_right hat, card_insert_of_notMem (fun h ↦ G.irrefl (hW h)),
hw.card_inter]
