internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.mp_int_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∑ v in C, degRes (mp (minsert M h)) v C = 0
Tactic:
simp only [sum_eq_zero_iff]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∀ (x : α), x ∈ C → degRes (mp (minsert M h)) x C = 0
Theorem: SimpleGraph.mp_int_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∀ (x : α), x ∈ C → degRes (mp (minsert M h)) x C = 0
Tactic:
intro x hx
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
x : α
hx : x ∈ C
⊢ degRes (mp (minsert M h)) x C = 0
Theorem: SimpleGraph.mp_int_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
x : α
hx : x ∈ C
⊢ degRes (mp (minsert M h)) x C = 0
Tactic:
exact mp_int_degRes M h x hx
Proof state after:
no goals
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in (minsert M h).A, degRes (mp (minsert M h)) v (minsert M h).A
Tactic:
set H : SimpleGraph α := mp (minsert M h) with hH
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in (minsert M h).A, degRes (mp (minsert M h)) v (minsert M h).A
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in (minsert M h).A, degRes (mp (minsert M h)) v (minsert M h).A
Tactic:
simp [insert_AB]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C = ∑ x in M.A ∪ C, degRes (mp (minsert M h)) x (M.A ∪ C)
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C = ∑ x in M.A ∪ C, degRes (mp (minsert M h)) x (M.A ∪ C)
Tactic:
rw [sum_union h]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ x in M.A, degRes (mp (minsert M h)) x (M.A ∪ C) + ∑ x in C, degRes (mp (minsert M h)) x (M.A ∪ C)
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ x in M.A, degRes (mp (minsert M h)) x (M.A ∪ C) + ∑ x in C, degRes (mp (minsert M h)) x (M.A ∪ C)
Tactic:
rw [H.degRes_add_sum' h, H.degRes_add_sum' h]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in M.A, degRes H v M.A + ∑ v in M.A, degRes H v C + (∑ v in C, degRes H v M.A + ∑ v in C, degRes H v C)
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in M.A, degRes H v M.A + ∑ v in M.A, degRes H v C + (∑ v in C, degRes H v M.A + ∑ v in C, degRes H v C)
Tactic:
rw [add_assoc, mp_int_sum M h, add_zero]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in M.A, degRes H v M.A + (∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A)
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + 2 * card M.A * card C =
    ∑ v in M.A, degRes H v M.A + (∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A)
Tactic:
rw [←add_assoc, card_eq_sum_ones C, mul_sum]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + ∑ x in C, 2 * card M.A * 1 =
    ∑ v in M.A, degRes H v M.A + ∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ v in M.A, degRes (mp M) v M.A + ∑ x in C, 2 * card M.A * 1 =
    ∑ v in M.A, degRes H v M.A + ∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A
Tactic:
rw [mp_old_sum M h,add_assoc, add_right_inj,mul_one]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ x in C, 2 * card M.A = ∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ x in C, 2 * card M.A = ∑ v in M.A, degRes H v C + ∑ v in C, degRes H v M.A
Tactic:
rw [ H.bip_count',← sum_add_distrib]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ x in C, 2 * card M.A = ∑ x in C, (degRes H x M.A + degRes H x M.A)
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∑ x in C, 2 * card M.A = ∑ x in C, (degRes H x M.A + degRes H x M.A)
Tactic:
apply sum_congr rfl
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∀ (x : α), x ∈ C → 2 * card M.A = degRes H x M.A + degRes H x M.A
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
⊢ ∀ (x : α), x ∈ C → 2 * card M.A = degRes H x M.A + degRes H x M.A
Tactic:
intro x hx
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
x : α
hx : x ∈ C
⊢ 2 * card M.A = degRes H x M.A + degRes H x M.A
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
x : α
hx : x ∈ C
⊢ 2 * card M.A = degRes H x M.A + degRes H x M.A
Tactic:
rw [(by norm_num : 2 = 1 + 1), add_mul, one_mul]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
x : α
hx : x ∈ C
⊢ card M.A + card M.A = degRes H x M.A + degRes H x M.A
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
x : α
hx : x ∈ C
⊢ card M.A + card M.A = degRes H x M.A + degRes H x M.A
Tactic:
rw [mp_com M h x hx]
Proof state after:
no goals
Theorem: SimpleGraph.mp_count
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
H : SimpleGraph α := mp (minsert M h)
hH : H = mp (minsert M h)
x : α
hx : x ∈ C
⊢ 2 = 1 + 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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)
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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)
Proof 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)
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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)
Theorem: SimpleGraph.mp_cliqueFree
Proof 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)
Proof 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)
Theorem: SimpleGraph.mp_cliqueFree
Proof 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
Proof 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)