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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
⊢ v ∈ C → w ∈ C → ¬Adj (mp (minsert M h)) v w
Tactic:
intro hv hw
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
⊢ ¬Adj (mp (minsert M h)) v w

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
⊢ ¬Adj (mp (minsert M h)) v w
Tactic:
have vin := insert_P' M h v hv
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ ¬Adj (mp (minsert M h)) v w

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Tactic:
have win := insert_P' M h w hw
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ ¬Adj (mp (minsert M h)) v w

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Tactic:
have := self_mem_range_succ (M.t + 1)
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
this : M.t + 1 ∈ range (M.t + 1 + 1)
⊢ ¬Adj (mp (minsert M h)) v w

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
this : M.t + 1 ∈ range (M.t + 1 + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Tactic:
rw [← insert_t M h] at this
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
⊢ ¬Adj (mp (minsert M h)) v w

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
win : w ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
⊢ ¬Adj (mp (minsert M h)) v w
Tactic:
contrapose win
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
win : ¬¬Adj (mp (minsert M h)) v w
⊢ ¬w ∈ MultiPart.P (minsert M h) (M.t + 1)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
win : ¬¬Adj (mp (minsert M h)) v w
⊢ ¬w ∈ MultiPart.P (minsert M h) (M.t + 1)
Tactic:
push_neg at win
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
win :
  ∃ i,
    i ∈ range ((minsert M h).t + 1) ∧
      ∃ j,
        j ∈ range ((minsert M h).t + 1) ∧
          i ≠ j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ w ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) i)
⊢ ¬w ∈ MultiPart.P (minsert M h) (M.t + 1)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
C : Finset α
v w : α
M : MultiPart α
h : Disjoint M.A C
hv : v ∈ C
hw : w ∈ C
vin : v ∈ MultiPart.P (minsert M h) (M.t + 1)
this : (minsert M h).t ∈ range ((minsert M h).t + 1)
win :
  ∃ i,
    i ∈ range ((minsert M h).t + 1) ∧
      ∃ j,
        j ∈ range ((minsert M h).t + 1) ∧
          i ≠ j ∧
            (v ∈ MultiPart.P (minsert M h) i ∧ w ∈ MultiPart.P (minsert M h) j ∨
              v ∈ MultiPart.P (minsert M h) j ∧ w ∈ MultiPart.P (minsert M h) i)
⊢ ¬w ∈ MultiPart.P (minsert M h) (M.t + 1)
Tactic:
exact not_nbhr_same_part this vin win
State after:
no goals