internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.turan_imm_imp_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
⊢ (¬¬Balanced M.t fun i => card (MultiPart.P M i)) → card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
Tactic:
rw [Classical.not_not]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
⊢ (Balanced M.t fun i => card (MultiPart.P M i)) → card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
Theorem: SimpleGraph.turan_imm_imp_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
⊢ (Balanced M.t fun i => card (MultiPart.P M i)) → card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
Tactic:
intro iM
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
Theorem: SimpleGraph.turan_imm_imp_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ card (edgeFinset (mp M)) = turanNumb t (Fintype.card α)
Tactic:
apply (mul_right_inj' (by norm_num : 2 ≠ 0)).mp
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ 2 * card (edgeFinset (mp M)) = 2 * turanNumb t (Fintype.card α)
Theorem: SimpleGraph.turan_imm_imp_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ 2 * card (edgeFinset (mp M)) = 2 * turanNumb t (Fintype.card α)
Tactic:
rw [← sum_degrees_eq_twice_card_edges, ← hu, ← ht]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ ∑ v in M.A, degree (mp M) v = 2 * turanNumb M.t (Fintype.card α)
Theorem: SimpleGraph.turan_imm_imp_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ ∑ v in M.A, degree (mp M) v = 2 * turanNumb M.t (Fintype.card α)
Tactic:
rw [mp_deg_sum_sq, ← card_univ, ← hu]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ card M.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = 2 * turanNumb M.t (card M.A)
Theorem: SimpleGraph.turan_imm_imp_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ card M.A ^ 2 - ∑ i in range (M.t + 1), card (MultiPart.P M i) ^ 2 = 2 * turanNumb M.t (card M.A)
Tactic:
simp only [← bal_turan_bd (turan_bal iM), sumSq, add_tsub_cancel_left]
Proof state after:
no goals
Theorem: SimpleGraph.turan_imm_imp_eq
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
hu : M.A = univ
ht : M.t = t
iM : Balanced M.t fun i => card (MultiPart.P M i)
⊢ 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: SimpleGraph.mp_com
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
⊢ ∀ (v : α), v ∈ C → degRes (mp (minsert M h)) v M.A = card M.A
Tactic:
intro v hv
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ degRes (mp (minsert M h)) v M.A = card M.A
Theorem: SimpleGraph.mp_com
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ degRes (mp (minsert M h)) v M.A = card M.A
Tactic:
rw [degRes]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ card (nbhdRes (mp (minsert M h)) v M.A) = card M.A
Theorem: SimpleGraph.mp_com
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ card (nbhdRes (mp (minsert M h)) v M.A) = card M.A
Tactic:
congr
Proof state after:
case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ nbhdRes (mp (minsert M h)) v M.A = M.A
Theorem: SimpleGraph.mp_com
Proof state before:
case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
⊢ nbhdRes (mp (minsert M h)) v M.A = M.A
Tactic:
ext a
Proof state after:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ nbhdRes (mp (minsert M h)) v M.A ↔ a ∈ M.A
Theorem: SimpleGraph.mp_com
Proof state before:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ nbhdRes (mp (minsert M h)) v M.A ↔ a ∈ M.A
Tactic:
rw [mem_res_nbhd_iff]
Proof state after:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ M.A ∧ a ∈ neighborFinset (mp (minsert M h)) v ↔ a ∈ M.A
Theorem: SimpleGraph.mp_com
Proof state before:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ M.A ∧ a ∈ neighborFinset (mp (minsert M h)) v ↔ a ∈ M.A
Tactic:
simp only [mem_neighborFinset, mem_range, Ne.def, exists_prop, and_iff_left_iff_imp]
Proof state after:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ M.A →
    ∃ i,
      i < (minsert M h).t + 1 ∧
        ∃ j,
          j < (minsert M h).t + 1 ∧
            ¬i = j ∧
              (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
                v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)
Theorem: SimpleGraph.mp_com
Proof state before:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
⊢ a ∈ M.A →
    ∃ i,
      i < (minsert M h).t + 1 ∧
        ∃ j,
          j < (minsert M h).t + 1 ∧
            ¬i = j ∧
              (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
                v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)
Tactic:
intro ha
Proof state after:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
⊢ ∃ i,
    i < (minsert M h).t + 1 ∧
      ∃ j,
        j < (minsert M h).t + 1 ∧
          ¬i = j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)
Theorem: SimpleGraph.mp_com
Proof state before:
case e_s.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
⊢ ∃ i,
    i < (minsert M h).t + 1 ∧
      ∃ j,
        j < (minsert M h).t + 1 ∧
          ¬i = j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)
Tactic:
obtain ⟨j, hjr, hjm⟩ := inv_part ha
Proof state after:
case e_s.a.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ∃ i,
    i < (minsert M h).t + 1 ∧
      ∃ j,
        j < (minsert M h).t + 1 ∧
          ¬i = j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)
Theorem: SimpleGraph.mp_com
Proof state before:
case e_s.a.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ∃ i,
    i < (minsert M h).t + 1 ∧
      ∃ j,
        j < (minsert M h).t + 1 ∧
          ¬i = j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ a ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) i)
Tactic:
use j
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < (minsert M h).t + 1 ∧
    ∃ j_1,
      j_1 < (minsert M h).t + 1 ∧
        ¬j = j_1 ∧
          (v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) j_1 ∨
            v ∈ MultiPart.P (minsert M h) j_1 ∧ a ∈ MultiPart.P (minsert M h) j)
Theorem: SimpleGraph.mp_com
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < (minsert M h).t + 1 ∧
    ∃ j_1,
      j_1 < (minsert M h).t + 1 ∧
        ¬j = j_1 ∧
          (v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) j_1 ∨
            v ∈ MultiPart.P (minsert M h) j_1 ∧ a ∈ MultiPart.P (minsert M h) j)
Tactic:
rw [insert_t]
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1 ∧
    ∃ j_1,
      j_1 < M.t + 1 + 1 ∧
        ¬j = j_1 ∧
          (v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) j_1 ∨
            v ∈ MultiPart.P (minsert M h) j_1 ∧ a ∈ MultiPart.P (minsert M h) j)
Theorem: SimpleGraph.mp_com
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1 ∧
    ∃ j_1,
      j_1 < M.t + 1 + 1 ∧
        ¬j = j_1 ∧
          (v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) j_1 ∨
            v ∈ MultiPart.P (minsert M h) j_1 ∧ a ∈ MultiPart.P (minsert M h) j)
Tactic:
refine' ⟨_, _, _, _, _⟩
Proof state after:
case h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1

case h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ℕ

case h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ?h.refine'_2 < M.t + 1 + 1

case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ¬j = ?h.refine'_2

case h.refine'_5
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) ?h.refine'_2 ∨
    v ∈ MultiPart.P (minsert M h) ?h.refine'_2 ∧ a ∈ MultiPart.P (minsert M h) j
Theorem: SimpleGraph.mp_com
Proof state before:
case h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1
Tactic:
rw [mem_range] at *
Proof state after:
case h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j < M.t + 1
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1
Theorem: SimpleGraph.mp_com
Proof state before:
case h.refine'_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j < M.t + 1
hjm : a ∈ MultiPart.P M j
⊢ j < M.t + 1 + 1
Tactic:
apply hjr.trans (lt_succ_self _)
Proof state after:
no goals
Theorem: SimpleGraph.mp_com
Proof state before:
case h.refine'_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ℕ
Tactic:
exact M.t + 1
Proof state after:
no goals
Theorem: SimpleGraph.mp_com
Proof state before:
case h.refine'_3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ M.t + 1 < M.t + 1 + 1
Tactic:
exact lt_succ_self _
Proof state after:
no goals
Theorem: SimpleGraph.mp_com
Proof state before:
case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ ¬j = M.t + 1
Tactic:
intro eq
Proof state after:
case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
eq : j = M.t + 1
⊢ False
Theorem: SimpleGraph.mp_com
Proof state before:
case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
eq : j = M.t + 1
⊢ False
Tactic:
rw [eq] at hjr
Proof state after:
case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : M.t + 1 ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
eq : j = M.t + 1
⊢ False
Theorem: SimpleGraph.mp_com
Proof state before:
case h.refine'_4
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : M.t + 1 ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
eq : j = M.t + 1
⊢ False
Tactic:
exact not_mem_range_self hjr
Proof state after:
no goals
Theorem: SimpleGraph.mp_com
Proof state before:
case h.refine'_5
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ v ∈ MultiPart.P (minsert M h) j ∧ a ∈ MultiPart.P (minsert M h) (M.t + 1) ∨
    v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h) j
Tactic:
right
Proof state after:
case h.refine'_5.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h) j
Theorem: SimpleGraph.mp_com
Proof state before:
case h.refine'_5.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ v ∈ MultiPart.P (minsert M h) (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h) j
Tactic:
rw [insert_P]
Proof state after:
case h.refine'_5.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ (v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else C) ∧ a ∈ MultiPart.P (minsert M h) j
Theorem: SimpleGraph.mp_com
Proof state before:
case h.refine'_5.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
⊢ (v ∈ if M.t + 1 ≠ M.t + 1 then MultiPart.P M (M.t + 1) else C) ∧ a ∈ MultiPart.P (minsert M h) j
Tactic:
split_ifs with h
Proof state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : M.t + 1 ≠ M.t + 1
⊢ v ∈ MultiPart.P M (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h✝) j

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ C ∧ a ∈ MultiPart.P (minsert M h✝) j
Theorem: SimpleGraph.mp_com
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : M.t + 1 ≠ M.t + 1
⊢ v ∈ MultiPart.P M (M.t + 1) ∧ a ∈ MultiPart.P (minsert M h✝) j
Tactic:
exfalso
Proof state after:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : M.t + 1 ≠ M.t + 1
⊢ False
Theorem: SimpleGraph.mp_com
Proof state before:
case pos.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : M.t + 1 ≠ M.t + 1
⊢ False
Tactic:
exact h rfl
Proof state after:
no goals
Theorem: SimpleGraph.mp_com
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ C ∧ a ∈ MultiPart.P (minsert M h✝) j
Tactic:
rw [insert_P]
Proof state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ C ∧ a ∈ if j ≠ M.t + 1 then MultiPart.P M j else C
Theorem: SimpleGraph.mp_com
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ v ∈ C ∧ a ∈ if j ≠ M.t + 1 then MultiPart.P M j else C
Tactic:
refine' ⟨hv, _⟩
Proof state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ a ∈ if j ≠ M.t + 1 then MultiPart.P M j else C
Theorem: SimpleGraph.mp_com
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
⊢ a ∈ if j ≠ M.t + 1 then MultiPart.P M j else C
Tactic:
split_ifs with h_2
Proof state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j ≠ M.t + 1
⊢ a ∈ MultiPart.P M j

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : ¬j ≠ M.t + 1
⊢ a ∈ C
Theorem: SimpleGraph.mp_com
Proof state before:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j ≠ M.t + 1
⊢ a ∈ MultiPart.P M j
Tactic:
exact hjm
Proof state after:
no goals
Theorem: SimpleGraph.mp_com
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : ¬j ≠ M.t + 1
⊢ a ∈ C
Tactic:
push_neg at h_2
Proof state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ a ∈ C
Theorem: SimpleGraph.mp_com
Proof state before:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ a ∈ C
Tactic:
exfalso
Proof state after:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ False
Theorem: SimpleGraph.mp_com
Proof state before:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : j ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ False
Tactic:
rw [h_2] at hjr
Proof state after:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : M.t + 1 ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ False
Theorem: SimpleGraph.mp_com
Proof state before:
case neg.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
M : MultiPart α
h✝ : Disjoint M.A C
v : α
hv : v ∈ C
a : α
ha : a ∈ M.A
j : ℕ
hjr : M.t + 1 ∈ range (M.t + 1)
hjm : a ∈ MultiPart.P M j
h : ¬M.t + 1 ≠ M.t + 1
h_2 : j = M.t + 1
⊢ False
Tactic:
exact not_mem_range_self hjr
Proof state after:
no goals
Theorem: SimpleGraph.mp_old_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
⊢ v ∈ M.A → w ∈ M.A → (Adj (mp M) v w ↔ Adj (mp (minsert M h)) v w)
Tactic:
intro hv hw
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
⊢ Adj (mp M) v w ↔ Adj (mp (minsert M h)) v w
Theorem: SimpleGraph.mp_old_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
⊢ Adj (mp M) v w ↔ Adj (mp (minsert M h)) v w
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
⊢ Adj (mp M) v w → Adj (mp (minsert M h)) v w

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ M.A
hw : w ∈ M.A
⊢ Adj (mp (minsert M h)) v w → Adj (mp M) v w