Theorem: SimpleGraph.nbhr_diff_parts (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 ∈ M.A \ MultiPart.P M i
⊢ Adj (mp M) v w
Tactic:
rw [mem_sdiff] at 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
hw : w ∈ M.A ∧ ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w

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 ∈ M.A ∧ ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w
Tactic:
cases' hw with hA hni
State after:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hA : w ∈ M.A
hni : ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w

State before:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hA : w ∈ M.A
hni : ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w
Tactic:
rw [M.uni] at hA
State after:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hA : w ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
hni : ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w

State before:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hA : w ∈ Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
hni : ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w
Tactic:
rw [mem_biUnion] at hA
State after:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hA : ∃ a, a ∈ range (M.t + 1) ∧ w ∈ MultiPart.P M a
hni : ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w

State before:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hA : ∃ a, a ∈ range (M.t + 1) ∧ w ∈ MultiPart.P M a
hni : ¬w ∈ MultiPart.P M i
⊢ Adj (mp M) v w
Tactic:
obtain ⟨j, hj1, hj2⟩ := hA
State after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hni : ¬w ∈ MultiPart.P M i
j : ℕ
hj1 : j ∈ range (M.t + 1)
hj2 : w ∈ MultiPart.P M j
⊢ Adj (mp M) v w

State before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hni : ¬w ∈ MultiPart.P M i
j : ℕ
hj1 : j ∈ range (M.t + 1)
hj2 : w ∈ MultiPart.P M j
⊢ Adj (mp M) v w
Tactic:
refine' mp_imp_adj hi hj1 hv hj2 _
State after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hni : ¬w ∈ MultiPart.P M i
j : ℕ
hj1 : j ∈ range (M.t + 1)
hj2 : w ∈ MultiPart.P M j
⊢ i ≠ j

State before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hni : ¬w ∈ MultiPart.P M i
j : ℕ
hj1 : j ∈ range (M.t + 1)
hj2 : w ∈ MultiPart.P M j
⊢ i ≠ j
Tactic:
intro h
State after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hni : ¬w ∈ MultiPart.P M i
j : ℕ
hj1 : j ∈ range (M.t + 1)
hj2 : w ∈ MultiPart.P M j
h : i = j
⊢ False

State before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
hni : ¬w ∈ MultiPart.P M i
j : ℕ
hj1 : j ∈ range (M.t + 1)
hj2 : w ∈ MultiPart.P M j
h : i = j
⊢ False
Tactic:
rw [h] at hni
State after:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
j : ℕ
hni : ¬w ∈ MultiPart.P M j
hj1 : j ∈ range (M.t + 1)
hj2 : w ∈ MultiPart.P M j
h : i = j
⊢ False

State before:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hv : v ∈ MultiPart.P M i
j : ℕ
hni : ¬w ∈ MultiPart.P M j
hj1 : j ∈ range (M.t + 1)
hj2 : w ∈ MultiPart.P M j
h : i = j
⊢ False
Tactic:
exact hni hj2
State after:
no goals