internlm/Lean-Github huggingface dataset:
Theorem: MiniChess.Board.set_different
Proof state before:
n : ℕ
pos' pos : Pos n
p? : Option PPiece
b : Board n
h : pos' ≠ pos
a✝ : pos = pos'
⊢ p? = b pos'
Tactic:
simp_all
Proof state after:
no goals
Theorem: SimpleGraph.no_nbhrs
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
hA : ¬v ∈ M.A
⊢ ¬Adj (mp M) v w
Tactic:
contrapose! hA
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
hA :
  ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j,
        j ∈ range (M.t + 1) ∧
          i ≠ j ∧ (v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i)
⊢ v ∈ M.A
Theorem: SimpleGraph.no_nbhrs
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
hA :
  ∃ i,
    i ∈ range (M.t + 1) ∧
      ∃ j,
        j ∈ range (M.t + 1) ∧
          i ≠ j ∧ (v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i)
⊢ v ∈ M.A
Tactic:
obtain ⟨i, hi, j, hj, _, hv⟩ := hA
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
left✝ : i ≠ j
hv : v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i
⊢ v ∈ M.A
Theorem: SimpleGraph.no_nbhrs
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
left✝ : i ≠ j
hv : v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i
⊢ v ∈ M.A
Tactic:
cases hv with
| inl hv => exact (sub_part hi) hv.1
| inr hv =>  exact (sub_part hj) hv.1
Proof state after:
no goals
Theorem: SimpleGraph.no_nbhrs
Proof state before:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
left✝ : i ≠ j
hv : v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j
⊢ v ∈ M.A
Tactic:
exact (sub_part hi) hv.1
Proof state after:
no goals
Theorem: SimpleGraph.no_nbhrs
Proof state before:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
i : ℕ
hi : i ∈ range (M.t + 1)
j : ℕ
hj : j ∈ range (M.t + 1)
left✝ : i ≠ j
hv : v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i
⊢ v ∈ M.A
Tactic:
exact (sub_part hj) hv.1
Proof state after:
no goals
Theorem: SimpleGraph.nbhrs_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
⊢ Adj (mp M) v w → v ∈ M.A
Tactic:
intro h1
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
h1 : Adj (mp M) v w
⊢ v ∈ M.A
Theorem: SimpleGraph.nbhrs_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
h1 : Adj (mp M) v w
⊢ v ∈ M.A
Tactic:
by_contra h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
h1 : Adj (mp M) v w
h : ¬v ∈ M.A
⊢ False
Theorem: SimpleGraph.nbhrs_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
v w : α
M : MultiPart α
h1 : Adj (mp M) v w
h : ¬v ∈ M.A
⊢ False
Tactic:
exact no_nbhrs h h1
Proof state after:
no goals
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
⊢ Adj (mp M) v w → i ≠ j
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : Adj (mp M) v w
⊢ i ≠ j
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : Adj (mp M) v w
⊢ i ≠ j
Tactic:
cases' h with a ha
Proof state after:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
ha :
  a ∈ range (M.t + 1) ∧
    ∃ j,
      j ∈ range (M.t + 1) ∧
        a ≠ j ∧ (v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M a)
⊢ i ≠ j
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
ha :
  a ∈ range (M.t + 1) ∧
    ∃ j,
      j ∈ range (M.t + 1) ∧
        a ≠ j ∧ (v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M a)
⊢ i ≠ j
Tactic:
obtain ⟨har, b, hbr, abne, ab⟩ := ha
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b ∨ v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
⊢ i ≠ j
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b ∨ v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
⊢ i ≠ j
Tactic:
cases ab with
| inl ab => 
  have ai := uniq_part hi har hvi ab.1; have bj := uniq_part hj hbr hwj ab.2
  rwa [← ai, ← bj] at abne 
| inr ab => 
  have aj := uniq_part hj har hwj ab.2; have bi := uniq_part hi hbr hvi ab.1
  rw [← aj, ← bi] at abne 
  exact abne.symm
Proof state after:
no goals
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b
⊢ i ≠ j
Tactic:
have ai := uniq_part hi har hvi ab.1
Proof state after:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b
ai : i = a
⊢ i ≠ j
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b
ai : i = a
⊢ i ≠ j
Tactic:
have bj := uniq_part hj hbr hwj ab.2
Proof state after:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b
ai : i = a
bj : j = b
⊢ i ≠ j
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
case intro.intro.intro.intro.intro.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M a ∧ w ∈ MultiPart.P M b
ai : i = a
bj : j = b
⊢ i ≠ j
Tactic:
rwa [← ai, ← bj] at abne
Proof state after:
no goals
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
⊢ i ≠ j
Tactic:
have aj := uniq_part hj har hwj ab.2
Proof state after:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
⊢ i ≠ j
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
⊢ i ≠ j
Tactic:
have bi := uniq_part hi hbr hvi ab.1
Proof state after:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
bi : i = b
⊢ i ≠ j
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : a ≠ b
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
bi : i = b
⊢ i ≠ j
Tactic:
rw [← aj, ← bi] at abne
Proof state after:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : j ≠ i
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
bi : i = b
⊢ i ≠ j
Theorem: SimpleGraph.mp_adj_imp
Proof state before:
case intro.intro.intro.intro.intro.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
a : ℕ
har : a ∈ range (M.t + 1)
b : ℕ
hbr : b ∈ range (M.t + 1)
abne : j ≠ i
ab : v ∈ MultiPart.P M b ∧ w ∈ MultiPart.P M a
aj : j = a
bi : i = b
⊢ i ≠ j
Tactic:
exact abne.symm
Proof state after:
no goals
Theorem: SimpleGraph.mp_imp_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
⊢ i ≠ j → Adj (mp M) v w
Tactic:
intro h
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ Adj (mp M) v w
Theorem: SimpleGraph.mp_imp_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ Adj (mp M) v w
Tactic:
refine' ⟨i, hi, j, hj, h, _⟩
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i
Theorem: SimpleGraph.mp_imp_adj
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j ∨ v ∈ MultiPart.P M j ∧ w ∈ MultiPart.P M i
Tactic:
left
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j
Theorem: SimpleGraph.mp_imp_adj
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
i j : ℕ
v w : α
M : MultiPart α
hi : i ∈ range (M.t + 1)
hj : j ∈ range (M.t + 1)
hvi : v ∈ MultiPart.P M i
hwj : w ∈ MultiPart.P M j
h : i ≠ j
⊢ v ∈ MultiPart.P M i ∧ w ∈ MultiPart.P M j
Tactic:
exact ⟨hvi, hwj⟩
Proof state after:
no goals
Theorem: SimpleGraph.not_nbhr_same_part
Proof 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
⊢ Adj (mp M) v w → ¬w ∈ MultiPart.P M i
Tactic:
intro h1
Proof 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
⊢ ¬w ∈ MultiPart.P M i
Theorem: SimpleGraph.not_nbhr_same_part
Proof 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
⊢ ¬w ∈ MultiPart.P M i
Tactic:
by_contra h
Proof 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
h : w ∈ MultiPart.P M i
⊢ False
Theorem: SimpleGraph.not_nbhr_same_part
Proof 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
h : w ∈ MultiPart.P M i
⊢ False
Tactic:
apply mp_adj_imp hi hi hv h h1
Proof 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
h : w ∈ MultiPart.P M i
⊢ i = i
Theorem: SimpleGraph.not_nbhr_same_part
Proof 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
h : w ∈ MultiPart.P M i
⊢ i = i
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.not_nbhr_same_part'
Proof 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
Proof 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
Theorem: SimpleGraph.not_nbhr_same_part'
Proof 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
Proof 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
Theorem: SimpleGraph.not_nbhr_same_part'
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.nbhr_diff_parts
Proof 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
Proof 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
Theorem: SimpleGraph.nbhr_diff_parts
Proof 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
Proof 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
Theorem: SimpleGraph.nbhr_diff_parts
Proof 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
Proof 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
Theorem: SimpleGraph.nbhr_diff_parts
Proof 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
Proof 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
Theorem: SimpleGraph.nbhr_diff_parts
Proof 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
Proof 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
Theorem: SimpleGraph.nbhr_diff_parts
Proof 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 _
Proof 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
Theorem: SimpleGraph.nbhr_diff_parts
Proof 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
Proof 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
Theorem: SimpleGraph.nbhr_diff_parts
Proof 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
Proof 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
Theorem: SimpleGraph.nbhr_diff_parts
Proof 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
Proof state after:
no goals
Theorem: SimpleGraph.mp_nbhd
Proof 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
Proof 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
Theorem: SimpleGraph.mp_nbhd
Proof 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
Proof 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
Theorem: SimpleGraph.mp_nbhd
Proof 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]
Proof 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
Theorem: SimpleGraph.mp_nbhd
Proof 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
Proof 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
Theorem: SimpleGraph.mp_nbhd
Proof 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
Proof 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