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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
⊢ neighborFinset (mp M) v = M.A \ MultiPart.P M i
Tactic:
ext
State after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ neighborFinset (mp M) v ↔ a✝ ∈ M.A \ MultiPart.P M i

State before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ neighborFinset (mp M) v ↔ a✝ ∈ M.A \ MultiPart.P M i
Tactic:
constructor
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ neighborFinset (mp M) v → a✝ ∈ M.A \ MultiPart.P M i

case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ M.A \ MultiPart.P M i → a✝ ∈ neighborFinset (mp M) v

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ neighborFinset (mp M) v → a✝ ∈ M.A \ MultiPart.P M i
Tactic:
rw [mem_neighborFinset]
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ Adj (mp M) v a✝ → a✝ ∈ M.A \ MultiPart.P M i

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ Adj (mp M) v a✝ → a✝ ∈ M.A \ MultiPart.P M i
Tactic:
intro h
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) v a✝
⊢ a✝ ∈ M.A \ MultiPart.P M i

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) v a✝
⊢ a✝ ∈ M.A \ MultiPart.P M i
Tactic:
rw [adj_comm] at h
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ a✝ ∈ M.A \ MultiPart.P M i

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ a✝ ∈ M.A \ MultiPart.P M i
Tactic:
rw [mem_sdiff]
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ a✝ ∈ M.A ∧ ¬a✝ ∈ MultiPart.P M i

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ a✝ ∈ M.A ∧ ¬a✝ ∈ MultiPart.P M i
Tactic:
refine' ⟨nbhrs_imp h, _⟩
State after:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ ¬a✝ ∈ MultiPart.P M i

State before:
case a.mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
h : Adj (mp M) a✝ v
⊢ ¬a✝ ∈ MultiPart.P M i
Tactic:
exact not_nbhr_same_part hv.1 hv.2 h.symm
State after:
no goals

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ M.A \ MultiPart.P M i → a✝ ∈ neighborFinset (mp M) v
Tactic:
rw [mem_neighborFinset]
State after:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ M.A \ MultiPart.P M i → Adj (mp M) v a✝

State before:
case a.mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v : α
M : MultiPart α
hv : i ∈ range (M.t + 1) ∧ v ∈ MultiPart.P M i
a✝ : α
⊢ a✝ ∈ M.A \ MultiPart.P M i → Adj (mp M) v a✝
Tactic:
exact nbhr_diff_parts hv.1 hv.2
State after:
no goals