Theorem: SimpleGraph.mp_cliqueFree (Turan4/Multipartite.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
⊢ M.t = t → M.A = univ → CliqueFree (mp M) (t + 2)
Tactic:
intro ht hA
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
⊢ CliqueFree (mp M) (t + 2)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
⊢ CliqueFree (mp M) (t + 2)
Tactic:
by_contra h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
h : ¬CliqueFree (mp M) (t + 2)
⊢ False

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
h : ¬CliqueFree (mp M) (t + 2)
⊢ False
Tactic:
unfold CliqueFree at h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
h : ¬∀ (t_1 : Finset α), ¬IsNClique (mp M) (t + 2) t_1
⊢ False

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
h : ¬∀ (t_1 : Finset α), ¬IsNClique (mp M) (t + 2) t_1
⊢ False
Tactic:
push_neg at h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
h : ∃ t_1, IsNClique (mp M) (t + 2) t_1
⊢ False

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
h : ∃ t_1, IsNClique (mp M) (t + 2) t_1
⊢ False
Tactic:
obtain ⟨S, hs1, hs2⟩ := h
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : IsClique (mp M) ↑S
hs2 : card S = t + 2
⊢ False

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : IsClique (mp M) ↑S
hs2 : card S = t + 2
⊢ False
Tactic:
rw [isClique_iff] at hs1
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
⊢ False

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
⊢ False
Tactic:
suffices ∃ i ∈ range (M.t + 1), 1 < (S ∩ M.P i).card
by
  obtain ⟨i, hi, hc⟩ := this; rw [one_lt_card_iff] at hc 
  obtain ⟨a, b, ha, hb, ne⟩ := hc; rw [mem_inter] at *
  have nadj := not_nbhr_same_part' hi ha.2 hb.2
  exact nadj (hs1 ha.1 hb.1 ne)
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
⊢ ∃ i, i ∈ range (M.t + 1) ∧ 1 < card (S ∩ MultiPart.P M i)

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
⊢ ∃ i, i ∈ range (M.t + 1) ∧ 1 < card (S ∩ MultiPart.P M i)
Tactic:
by_contra h
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ¬∃ i, i ∈ range (M.t + 1) ∧ 1 < card (S ∩ MultiPart.P M i)
⊢ False

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ¬∃ i, i ∈ range (M.t + 1) ∧ 1 < card (S ∩ MultiPart.P M i)
⊢ False
Tactic:
push_neg at h
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ False

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ False
Tactic:
have ub : ∑ i in  (range (M.t + 1)), (S ∩ M.P i).card ≤ M.t + 1
State after:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ M.t + 1

case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ M.t + 1
⊢ False

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ M.t + 1
⊢ False
Tactic:
nth_rw 2 [ht] at ub
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
⊢ False

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
⊢ False
Tactic:
have uni := biUnion_parts M
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : M.A = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
⊢ False

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : M.A = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
⊢ False
Tactic:
rw [hA] at uni
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
⊢ False

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
⊢ False
Tactic:
have sin := inter_univ S
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : S ∩ univ = S
⊢ False

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : S ∩ univ = S
⊢ False
Tactic:
rw [uni, inter_biUnion] at sin
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ False

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ False
Tactic:
rw [← sin, card_biUnion] at hs2
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : ∑ u in range (M.t + 1), card (S ∩ MultiPart.P M u) = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ False

case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) → ∀ (y : ℕ), y ∈ range (M.t + 1) → x ≠ y → Disjoint (S ∩ MultiPart.P M x) (S ∩ MultiPart.P M y)

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : ∑ u in range (M.t + 1), card (S ∩ MultiPart.P M u) = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ False

case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) → ∀ (y : ℕ), y ∈ range (M.t + 1) → x ≠ y → Disjoint (S ∩ MultiPart.P M x) (S ∩ MultiPart.P M y)
Tactic:
apply not_succ_le_self _ (hs2 ▸ ub)
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) → ∀ (y : ℕ), y ∈ range (M.t + 1) → x ≠ y → Disjoint (S ∩ MultiPart.P M x) (S ∩ MultiPart.P M y)

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) → ∀ (y : ℕ), y ∈ range (M.t + 1) → x ≠ y → Disjoint (S ∩ MultiPart.P M x) (S ∩ MultiPart.P M y)
Tactic:
intro x hx y hy ne
State after:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
x : ℕ
hx : x ∈ range (M.t + 1)
y : ℕ
hy : y ∈ range (M.t + 1)
ne : x ≠ y
⊢ Disjoint (S ∩ MultiPart.P M x) (S ∩ MultiPart.P M y)

State before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
x : ℕ
hx : x ∈ range (M.t + 1)
y : ℕ
hy : y ∈ range (M.t + 1)
ne : x ≠ y
⊢ Disjoint (S ∩ MultiPart.P M x) (S ∩ MultiPart.P M y)
Tactic:
apply disj_of_disj_inter S S (M.disj x hx y hy ne)
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
this : ∃ i, i ∈ range (M.t + 1) ∧ 1 < card (S ∩ MultiPart.P M i)
⊢ False
Tactic:
obtain ⟨i, hi, hc⟩ := this
State after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
hc : 1 < card (S ∩ MultiPart.P M i)
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
hc : 1 < card (S ∩ MultiPart.P M i)
⊢ False
Tactic:
rw [one_lt_card_iff] at hc
State after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
hc : ∃ a b, a ∈ S ∩ MultiPart.P M i ∧ b ∈ S ∩ MultiPart.P M i ∧ a ≠ b
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
hc : ∃ a b, a ∈ S ∩ MultiPart.P M i ∧ b ∈ S ∩ MultiPart.P M i ∧ a ≠ b
⊢ False
Tactic:
obtain ⟨a, b, ha, hb, ne⟩ := hc
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∩ MultiPart.P M i
hb : b ∈ S ∩ MultiPart.P M i
ne : a ≠ b
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∩ MultiPart.P M i
hb : b ∈ S ∩ MultiPart.P M i
ne : a ≠ b
⊢ False
Tactic:
rw [mem_inter] at *
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∧ a ∈ MultiPart.P M i
hb : b ∈ S ∧ b ∈ MultiPart.P M i
ne : a ≠ b
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∧ a ∈ MultiPart.P M i
hb : b ∈ S ∧ b ∈ MultiPart.P M i
ne : a ≠ b
⊢ False
Tactic:
have nadj := not_nbhr_same_part' hi ha.2 hb.2
State after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∧ a ∈ MultiPart.P M i
hb : b ∈ S ∧ b ∈ MultiPart.P M i
ne : a ≠ b
nadj : ¬Adj (mp M) a b
⊢ False

State before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∧ a ∈ MultiPart.P M i
hb : b ∈ S ∧ b ∈ MultiPart.P M i
ne : a ≠ b
nadj : ¬Adj (mp M) a b
⊢ False
Tactic:
exact nadj (hs1 ha.1 hb.1 ne)
State after:
no goals

State before:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ M.t + 1
Tactic:
nth_rw 2 [← card_range (M.t + 1)]
State after:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ card (range (M.t + 1))

State before:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ card (range (M.t + 1))
Tactic:
nth_rw 1 [card_eq_sum_ones]
State after:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ ∑ x in range (M.t + 1), 1

State before:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ ∑ x in range (M.t + 1), 1
Tactic:
apply sum_le_sum h
State after:
no goals