internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.mp_nbhd
Proof state before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ a✝ ∈ M.A \ MultiPart.P M i
Tactic:
rw [mem_sdiff]
Proof state after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ a✝ ∈ M.A ∧ ¬a✝ ∈ MultiPart.P M i
Theorem: SimpleGraph.mp_nbhd
Proof state before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ a✝ ∈ M.A ∧ ¬a✝ ∈ MultiPart.P M i
Tactic:
refine' ⟨nbhrs_imp h, _⟩
Proof state after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ ¬a✝ ∈ MultiPart.P M i
Theorem: SimpleGraph.mp_nbhd
Proof state before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ ¬a✝ ∈ MultiPart.P M i
Tactic:
exact not_nbhr_same_part hv.1 hv.2 h.symm
Proof state after:
no goals
Theorem: SimpleGraph.mp_nbhd
Proof state before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ M.A \ MultiPart.P M i → a✝ ∈ neighborFinset (mp M) v
Tactic:
rw [mem_neighborFinset]
Proof state after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ M.A \ MultiPart.P M i → Adj (mp M) v a✝
Theorem: SimpleGraph.mp_nbhd
Proof state before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ M.A \ MultiPart.P M i → Adj (mp M) v a✝
Tactic:
exact nbhr_diff_parts hv.1 hv.2
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
⊢ degree (mp M) v = card (M.A \ MultiPart.P M i)
Tactic:
rw [degree]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
⊢ card (neighborFinset (mp M) v) = card (M.A \ MultiPart.P M i)
Theorem: SimpleGraph.mp_deg
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
⊢ card (neighborFinset (mp M) v) = card (M.A \ MultiPart.P M i)
Tactic:
rw [mp_nbhd hv]
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_diff
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
⊢ degree (mp M) v = card M.A - card (MultiPart.P M i)
Tactic:
rw [mp_deg hv]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
⊢ card (M.A \ MultiPart.P M i) = card M.A - card (MultiPart.P M i)
Theorem: SimpleGraph.mp_deg_diff
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
⊢ card (M.A \ MultiPart.P M i) = card M.A - card (MultiPart.P M i)
Tactic:
exact card_sdiff (sub_part hv.1)
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ v in M.A, degree (mp M) v = ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i)
Tactic:
nth_rw 1 [M.uni]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ v in Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i, degree (mp M) v =
    ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i)
Theorem: SimpleGraph.mp_deg_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ v in Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i, degree (mp M) v =
    ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i)
Tactic:
rw [sum_biUnion (pair_disjoint M)]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), ∑ i in MultiPart.P M x, degree (mp M) i =
    ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i)
Theorem: SimpleGraph.mp_deg_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), ∑ i in MultiPart.P M x, degree (mp M) i =
    ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i)
Tactic:
apply Finset.sum_congr rfl _
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) →
      ∑ i in MultiPart.P M x, degree (mp M) i = card (MultiPart.P M x) * card (M.A \ MultiPart.P M x)
Theorem: SimpleGraph.mp_deg_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) →
      ∑ i in MultiPart.P M x, degree (mp M) i = card (MultiPart.P M x) * card (M.A \ MultiPart.P M x)
Tactic:
intro x hx
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∑ i in MultiPart.P M x, degree (mp M) i = card (MultiPart.P M x) * card (M.A \ MultiPart.P M x)
Theorem: SimpleGraph.mp_deg_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∑ i in MultiPart.P M x, degree (mp M) i = card (MultiPart.P M x) * card (M.A \ MultiPart.P M x)
Tactic:
rw [Finset.card_eq_sum_ones, sum_mul, one_mul]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∑ i in MultiPart.P M x, degree (mp M) i = ∑ x_1 in MultiPart.P M x, card (M.A \ MultiPart.P M x)
Theorem: SimpleGraph.mp_deg_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∑ i in MultiPart.P M x, degree (mp M) i = ∑ x_1 in MultiPart.P M x, card (M.A \ MultiPart.P M x)
Tactic:
apply Finset.sum_congr rfl _
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∀ (x_1 : α), x_1 ∈ MultiPart.P M x → degree (mp M) x_1 = card (M.A \ MultiPart.P M x)
Theorem: SimpleGraph.mp_deg_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ ∀ (x_1 : α), x_1 ∈ MultiPart.P M x → degree (mp M) x_1 = card (M.A \ MultiPart.P M x)
Tactic:
intro v hv
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
v : α
hv : v ∈ MultiPart.P M x
⊢ degree (mp M) v = card (M.A \ MultiPart.P M x)
Theorem: SimpleGraph.mp_deg_sum
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
v : α
hv : v ∈ MultiPart.P M x
⊢ degree (mp M) v = card (M.A \ MultiPart.P M x)
Tactic:
exact mp_deg ⟨hx, hv⟩
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_sq'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ v in M.A, degree (mp M) v + ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = card M.A ^ 2
Tactic:
rw [mp_deg_sum M]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card M.A ^ 2
Theorem: SimpleGraph.mp_deg_sum_sq'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card M.A ^ 2
Tactic:
rw [pow_two]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card M.A * card M.A
Theorem: SimpleGraph.mp_deg_sum_sq'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card M.A * card M.A
Tactic:
nth_rw 1 [card_uni]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    (∑ i in range (M.t + 1), card (MultiPart.P M i)) * card M.A
Theorem: SimpleGraph.mp_deg_sum_sq'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    (∑ i in range (M.t + 1), card (MultiPart.P M i)) * card M.A
Tactic:
rw [← sum_add_distrib]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), (card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2) =
    (∑ i in range (M.t + 1), card (MultiPart.P M i)) * card M.A
Theorem: SimpleGraph.mp_deg_sum_sq'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), (card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2) =
    (∑ i in range (M.t + 1), card (MultiPart.P M i)) * card M.A
Tactic:
rw [sum_mul]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), (card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2) =
    ∑ x in range (M.t + 1), card (MultiPart.P M x) * card M.A
Theorem: SimpleGraph.mp_deg_sum_sq'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∑ x in range (M.t + 1), (card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2) =
    ∑ x in range (M.t + 1), card (MultiPart.P M x) * card M.A
Tactic:
refine' Finset.sum_congr rfl _
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) →
      card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2 =
        card (MultiPart.P M x) * card M.A
Theorem: SimpleGraph.mp_deg_sum_sq'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ ∀ (x : ℕ),
    x ∈ range (M.t + 1) →
      card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2 =
        card (MultiPart.P M x) * card M.A
Tactic:
intro x hx
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2 = card (MultiPart.P M x) * card M.A
Theorem: SimpleGraph.mp_deg_sum_sq'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) ^ 2 = card (MultiPart.P M x) * card M.A
Tactic:
rw [pow_two]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) * card (MultiPart.P M x) =
    card (MultiPart.P M x) * card M.A
Theorem: SimpleGraph.mp_deg_sum_sq'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * card (M.A \ MultiPart.P M x) + card (MultiPart.P M x) * card (MultiPart.P M x) =
    card (MultiPart.P M x) * card M.A
Tactic:
rw [← mul_add]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * (card (M.A \ MultiPart.P M x) + card (MultiPart.P M x)) = card (MultiPart.P M x) * card M.A
Theorem: SimpleGraph.mp_deg_sum_sq'
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
x : ℕ
hx : x ∈ range (M.t + 1)
⊢ card (MultiPart.P M x) * (card (M.A \ MultiPart.P M x) + card (MultiPart.P M x)) = card (MultiPart.P M x) * card M.A
Tactic:
rw [card_part_uni hx]
Proof state after:
no goals
Theorem: SimpleGraph.turanPartition_deg_sum_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
⊢ M.A = N.A → M.t = N.t → TuranPartition M → TuranPartition N → mpDsum M = mpDsum N
Tactic:
intro hA ht iM iN
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ mpDsum M = mpDsum N
Theorem: SimpleGraph.turanPartition_deg_sum_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ mpDsum M = mpDsum N
Tactic:
unfold mpDsum
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ ∑ v in M.A, degree (mp M) v = ∑ v in N.A, degree (mp N) v
Theorem: SimpleGraph.turanPartition_deg_sum_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ ∑ v in M.A, degree (mp M) v = ∑ v in N.A, degree (mp N) v
Tactic:
rw [mp_deg_sum_sq, mp_deg_sum_sq, hA]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ card N.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Theorem: SimpleGraph.turanPartition_deg_sum_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : TuranPartition M
iN : TuranPartition N
⊢ card N.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
rw [turanPartition_iff_not_moveable, Moveable, Classical.not_not] at *
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
⊢ card N.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Theorem: SimpleGraph.turanPartition_deg_sum_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
⊢ card N.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 =
    card N.A ^ 2 - ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
apply congr_arg _
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Theorem: SimpleGraph.turanPartition_deg_sum_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
have hN := turan_bal iN
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal N.t (card N.A) fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Theorem: SimpleGraph.turanPartition_deg_sum_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal N.t (card N.A) fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
rw [← ht, ← hA] at hN
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal M.t (card M.A) fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Theorem: SimpleGraph.turanPartition_deg_sum_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal M.t (card M.A) fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
have := bal_turan_help' (turan_bal iM) hN
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal M.t (card M.A) fun i => card (MultiPart.P N i)
this : (sumSq M.t fun i => card (MultiPart.P M i)) = sumSq M.t fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Theorem: SimpleGraph.turanPartition_deg_sum_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M N : MultiPart α
hA : M.A = N.A
ht : M.t = N.t
iM : Balanced M.t fun i => card (MultiPart.P M i)
iN : Balanced N.t fun i => card (MultiPart.P N i)
hN : Bal M.t (card M.A) fun i => card (MultiPart.P N i)
this : (sumSq M.t fun i => card (MultiPart.P M i)) = sumSq M.t fun i => card (MultiPart.P N i)
⊢ ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = ∑ i in range (N.t + 1), card (MultiPart.P N i) ^ 2
Tactic:
rwa [← ht]
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    card (MultiPart.P (move M hvi hj) i) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) i) +
      card (MultiPart.P (move M hvi hj) j) * card ((move M hvi hj).A \ MultiPart.P (move M hvi hj) j)
Tactic:
rw [move_Pcard hvi hj hvi.1, move_Pcard hvi hj hj.1, move_Pcard_sdiff hvi hj hvi.1,
  move_Pcard_sdiff hvi hj hj.1]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
⊢ card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    ((if i ≠ i ∧ i ≠ j then card (MultiPart.P M i)
        else if i = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
        if i ≠ i ∧ i ≠ j then card (M.A \ MultiPart.P M i)
        else if i = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1) +
      (if j ≠ i ∧ j ≠ j then card (MultiPart.P M j)
        else if j = i then card (MultiPart.P M i) - 1 else card (MultiPart.P M j) + 1) *
        if j ≠ i ∧ j ≠ j then card (M.A \ MultiPart.P M j)
        else if j = i then card (M.A \ MultiPart.P M i) + 1 else card (M.A \ MultiPart.P M j) - 1
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h : i ≠ i ∧ i ≠ j
h_1 : j ≠ i ∧ j ≠ j
⊢ card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j)
Tactic:
exfalso
Proof state after:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h : i ≠ i ∧ i ≠ j
h_1 : j ≠ i ∧ j ≠ j
⊢ False
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof state before:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h : i ≠ i ∧ i ≠ j
h_1 : j ≠ i ∧ j ≠ j
⊢ False
Tactic:
exact h.1 rfl
Proof state after:
no goals
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h : i ≠ i ∧ i ≠ j
h_1 : ¬(j ≠ i ∧ j ≠ j)
h_2 : j = i
⊢ card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) + card (MultiPart.P M j) * card (M.A \ MultiPart.P M j) <
    card (MultiPart.P M i) * card (M.A \ MultiPart.P M i) +
      (card (MultiPart.P M i) - 1) * (card (M.A \ MultiPart.P M i) + 1)
Tactic:
exfalso
Proof state after:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h : i ≠ i ∧ i ≠ j
h_1 : ¬(j ≠ i ∧ j ≠ j)
h_2 : j = i
⊢ False
Theorem: SimpleGraph.mp_deg_sum_move_help
Proof state before:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
j : ℕ
M : MultiPart α
hvi : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
hj : j ∈ range (M.t + 1) ∧ j ≠ i
hc : card (MultiPart.P M j) + 1 < card (MultiPart.P M i)
h : i ≠ i ∧ i ≠ j
h_1 : ¬(j ≠ i ∧ j ≠ j)
h_2 : j = i
⊢ False
Tactic:
exact h.1 rfl
Proof state after:
no goals