Theorem: SimpleGraph.not_nbhr_same_part' (Turan4/Multipartite.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hw : w ∈ MultiPart.P M i
⊢ ¬Adj (mp M) v w
Tactic:
intro h1
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hw : w ∈ MultiPart.P M i
h1 : Adj (mp M) v w
⊢ False

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hw : w ∈ MultiPart.P M i
h1 : Adj (mp M) v w
⊢ False
Tactic:
contrapose hw
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
h1 : Adj (mp M) v w
hw : ¬False
⊢ ¬w ∈ MultiPart.P M i

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
h1 : Adj (mp M) v w
hw : ¬False
⊢ ¬w ∈ MultiPart.P M i
Tactic:
exact not_nbhr_same_part hi hv h1
State after:
no goals