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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
⊢ M.A = univ → card (edgeFinset (mp M)) ≤ turanNumb M.t (Fintype.card α)
Tactic:
intro hA
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ card (edgeFinset (mp M)) ≤ turanNumb M.t (Fintype.card α)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ card (edgeFinset (mp M)) ≤ turanNumb M.t (Fintype.card α)
Tactic:
apply (mul_le_mul_left (by norm_num : 0 < 2)).mp
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ 2 * card (edgeFinset (mp M)) ≤ 2 * turanNumb M.t (Fintype.card α)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ 2 * card (edgeFinset (mp M)) ≤ 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [← sum_degrees_eq_twice_card_edges]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Tactic:
have := turan_bound_M M
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : mpDsum M ≤ 2 * turanNumb M.t (card M.A)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : mpDsum M ≤ 2 * turanNumb M.t (card M.A)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Tactic:
unfold mpDsum at this
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : ∑ v in M.A, degree (mp M) v ≤ 2 * turanNumb M.t (card M.A)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : ∑ v in M.A, degree (mp M) v ≤ 2 * turanNumb M.t (card M.A)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [hA] at this
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (card univ)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
this : ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (card univ)
⊢ ∑ v : α, degree (mp M) v ≤ 2 * turanNumb M.t (Fintype.card α)
Tactic:
rwa [card_univ] at this
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hA : M.A = univ
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals