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

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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α)
⊢ TuranPartition M
Tactic:
contrapose h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
⊢ ¬card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
⊢ ¬card (edgeFinset (mp M)) = turanNumb M.t (Fintype.card α)
Tactic:
apply Nat.ne_of_lt
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
⊢ card (edgeFinset (mp M)) < turanNumb M.t (Fintype.card α)

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
⊢ card (edgeFinset (mp M)) < turanNumb M.t (Fintype.card α)
Tactic:
obtain ⟨N, NA, Nt, iN, le⟩ := moved M
State after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ card (edgeFinset (mp M)) < turanNumb M.t (Fintype.card α)

State before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ card (edgeFinset (mp M)) < turanNumb M.t (Fintype.card α)
Tactic:
apply (mul_lt_mul_left (by norm_num : 0 < 2)).mp
State after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ 2 * card (edgeFinset (mp M)) < 2 * turanNumb M.t (Fintype.card α)

State before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ 2 * card (edgeFinset (mp M)) < 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [← sum_degrees_eq_twice_card_edges]
State after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)

State before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
have lt := moved_max N M NA Nt iN h
State after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
lt : mpDsum M < mpDsum N
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)

State before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
lt : mpDsum M < mpDsum N
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
have le2 := turan_bound_M N
State after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
lt : mpDsum M < mpDsum N
le2 : mpDsum N ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)

State before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
lt : mpDsum M < mpDsum N
le2 : mpDsum N ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
unfold mpDsum at *
State after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v in M.A, degree (mp M) v ≤ ∑ v in N.A, degree (mp N) v
lt : ∑ v in M.A, degree (mp M) v < ∑ v in N.A, degree (mp N) v
le2 : ∑ v in N.A, degree (mp N) v ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)

State before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v in M.A, degree (mp M) v ≤ ∑ v in N.A, degree (mp N) v
lt : ∑ v in M.A, degree (mp M) v < ∑ v in N.A, degree (mp N) v
le2 : ∑ v in N.A, degree (mp N) v ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [hu] at *
State after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = univ
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v in N.A, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v in N.A, degree (mp N) v
le2 : ∑ v in N.A, degree (mp N) v ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)

State before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = univ
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v in N.A, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v in N.A, degree (mp N) v
le2 : ∑ v in N.A, degree (mp N) v ≤ 2 * turanNumb N.t (card N.A)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [NA] at *
State after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb N.t (card univ)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)

State before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : N.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb N.t (card univ)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [Nt] at *
State after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : M.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb M.t (card univ)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)

State before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : M.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb M.t (card univ)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [card_univ] at *
State after:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : M.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb M.t (Fintype.card α)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)

State before:
case h.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : univ = univ
h : ¬TuranPartition M
N : MultiPart α
NA : univ = univ
Nt : M.t = M.t
iN : TuranPartition N
le : ∑ v : α, degree (mp M) v ≤ ∑ v : α, degree (mp N) v
lt : ∑ v : α, degree (mp M) v < ∑ v : α, degree (mp N) v
le2 : ∑ v : α, degree (mp N) v ≤ 2 * turanNumb M.t (Fintype.card α)
⊢ ∑ v : α, degree (mp M) v < 2 * turanNumb M.t (Fintype.card α)
Tactic:
exact lt_of_lt_of_le lt le2
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
M : MultiPart α
hu : M.A = univ
h : ¬TuranPartition M
N : MultiPart α
NA : N.A = M.A
Nt : N.t = M.t
iN : TuranPartition N
le : mpDsum M ≤ mpDsum N
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals