internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.mp_cliqueFree
Proof state before:
case intro.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
ub : ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ t + 1
uni : univ = Finset.biUnion (range (M.t + 1)) fun i => MultiPart.P M i
sin : (Finset.biUnion (range (M.t + 1)) fun x => S ∩ MultiPart.P M x) = S
x : ℕ
hx : x ∈ range (M.t + 1)
y : ℕ
hy : y ∈ range (M.t + 1)
ne : x ≠ y
⊢ Disjoint (S ∩ MultiPart.P M x) (S ∩ MultiPart.P M y)
Tactic:
apply disj_of_disj_inter S S (M.disj x hx y hy ne)
Proof state after:
no goals
Theorem: SimpleGraph.mp_cliqueFree
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
this : ∃ i, i ∈ range (M.t + 1) ∧ 1 < card (S ∩ MultiPart.P M i)
⊢ False
Tactic:
obtain ⟨i, hi, hc⟩ := this
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
hc : 1 < card (S ∩ MultiPart.P M i)
⊢ False
Theorem: SimpleGraph.mp_cliqueFree
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
hc : 1 < card (S ∩ MultiPart.P M i)
⊢ False
Tactic:
rw [one_lt_card_iff] at hc
Proof state after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
hc : ∃ a b, a ∈ S ∩ MultiPart.P M i ∧ b ∈ S ∩ MultiPart.P M i ∧ a ≠ b
⊢ False
Theorem: SimpleGraph.mp_cliqueFree
Proof state before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
hc : ∃ a b, a ∈ S ∩ MultiPart.P M i ∧ b ∈ S ∩ MultiPart.P M i ∧ a ≠ b
⊢ False
Tactic:
obtain ⟨a, b, ha, hb, ne⟩ := hc
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∩ MultiPart.P M i
hb : b ∈ S ∩ MultiPart.P M i
ne : a ≠ b
⊢ False
Theorem: SimpleGraph.mp_cliqueFree
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∩ MultiPart.P M i
hb : b ∈ S ∩ MultiPart.P M i
ne : a ≠ b
⊢ False
Tactic:
rw [mem_inter] at *
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∧ a ∈ MultiPart.P M i
hb : b ∈ S ∧ b ∈ MultiPart.P M i
ne : a ≠ b
⊢ False
Theorem: SimpleGraph.mp_cliqueFree
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∧ a ∈ MultiPart.P M i
hb : b ∈ S ∧ b ∈ MultiPart.P M i
ne : a ≠ b
⊢ False
Tactic:
have nadj := not_nbhr_same_part' hi ha.2 hb.2
Proof state after:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∧ a ∈ MultiPart.P M i
hb : b ∈ S ∧ b ∈ MultiPart.P M i
ne : a ≠ b
nadj : ¬Adj (mp M) a b
⊢ False
Theorem: SimpleGraph.mp_cliqueFree
Proof state before:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
i : ℕ
hi : i ∈ range (M.t + 1)
a b : α
ha : a ∈ S ∧ a ∈ MultiPart.P M i
hb : b ∈ S ∧ b ∈ MultiPart.P M i
ne : a ≠ b
nadj : ¬Adj (mp M) a b
⊢ False
Tactic:
exact nadj (hs1 ha.1 hb.1 ne)
Proof state after:
no goals
Theorem: SimpleGraph.mp_cliqueFree
Proof state before:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ M.t + 1
Tactic:
nth_rw 2 [← card_range (M.t + 1)]
Proof state after:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ card (range (M.t + 1))
Theorem: SimpleGraph.mp_cliqueFree
Proof state before:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ card (range (M.t + 1))
Tactic:
nth_rw 1 [card_eq_sum_ones]
Proof state after:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ ∑ x in range (M.t + 1), 1
Theorem: SimpleGraph.mp_cliqueFree
Proof state before:
case ub
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
t : ℕ
M : MultiPart α
ht : M.t = t
hA : M.A = univ
S : Finset α
hs1 : Set.Pairwise (↑S) (mp M).Adj
hs2 : card S = t + 2
h : ∀ (i : ℕ), i ∈ range (M.t + 1) → card (S ∩ MultiPart.P M i) ≤ 1
⊢ ∑ i in range (M.t + 1), card (S ∩ MultiPart.P M i) ≤ ∑ x in range (M.t + 1), 1
Tactic:
apply sum_le_sum h
Proof state after:
no goals
Theorem: SimpleGraph.nbhdRes_filter
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ nbhdRes G v A = filter (fun x => Adj G v x) A
Tactic:
ext x
Proof state after:
case a
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
⊢ x ∈ nbhdRes G v A ↔ x ∈ filter (fun x => Adj G v x) A
Theorem: SimpleGraph.nbhdRes_filter
Proof state before:
case a
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
⊢ x ∈ nbhdRes G v A ↔ x ∈ filter (fun x => Adj G v x) A
Tactic:
rw [nbhdRes,mem_inter,mem_filter,mem_neighborFinset]
Proof state after:
no goals
Theorem: SimpleGraph.degRes_univ
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ degRes G v univ = degree G v
Tactic:
rw [degRes, degree]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ card (nbhdRes G v univ) = card (neighborFinset G v)
Theorem: SimpleGraph.degRes_univ
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ card (nbhdRes G v univ) = card (neighborFinset G v)
Tactic:
congr
Proof state after:
case e_s
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ nbhdRes G v univ = neighborFinset G v
Theorem: SimpleGraph.degRes_univ
Proof state before:
case e_s
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ nbhdRes G v univ = neighborFinset G v
Tactic:
rw [nbhdRes, univ_inter]
Proof state after:
no goals
Theorem: SimpleGraph.exists_max_res_deg_vertex
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A
Tactic:
obtain ⟨t, ht⟩ := max_of_nonempty (Nonempty.image hA (fun v => G.degRes v A))
Proof state after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A
Theorem: SimpleGraph.exists_max_res_deg_vertex
Proof state before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A
Tactic:
obtain ⟨a, ha1, ha2⟩:=mem_image.1 (mem_of_max ht)
Proof state after:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A
Theorem: SimpleGraph.exists_max_res_deg_vertex
Proof state before:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ ∃ v, v ∈ A ∧ maxDegRes G A = degRes G v A
Tactic:
refine ⟨a, ha1,?_⟩
Proof state after:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ maxDegRes G A = degRes G a A
Theorem: SimpleGraph.exists_max_res_deg_vertex
Proof state before:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ maxDegRes G A = degRes G a A
Tactic:
rw [maxDegRes,ht,ha2]
Proof state after:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ Option.getD (↑t) 0 = t
Theorem: SimpleGraph.exists_max_res_deg_vertex
Proof state before:
case intro.intro.intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A : Finset α
hA : Finset.Nonempty A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
a : α
ha1 : a ∈ A
ha2 : degRes G a A = t
⊢ Option.getD (↑t) 0 = t
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.degRes_le_maxDegRes
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
⊢ degRes G v A ≤ maxDegRes G A
Tactic:
obtain ⟨t, ht⟩ := Finset.max_of_mem (mem_image_of_mem (fun v => G.degRes v A) hvA)
Proof state after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
⊢ degRes G v A ≤ maxDegRes G A
Theorem: SimpleGraph.degRes_le_maxDegRes
Proof state before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
⊢ degRes G v A ≤ maxDegRes G A
Tactic:
have := mem_image_of_mem (fun v => G.degRes v A) hvA
Proof state after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
this : (fun v => degRes G v A) v ∈ image (fun v => degRes G v A) A
⊢ degRes G v A ≤ maxDegRes G A
Theorem: SimpleGraph.degRes_le_maxDegRes
Proof state before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
this : (fun v => degRes G v A) v ∈ image (fun v => degRes G v A) A
⊢ degRes G v A ≤ maxDegRes G A
Tactic:
have := Finset.le_max_of_eq this ht
Proof state after:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
this✝ : (fun v => degRes G v A) v ∈ image (fun v => degRes G v A) A
this : (fun v => degRes G v A) v ≤ t
⊢ degRes G v A ≤ maxDegRes G A
Theorem: SimpleGraph.degRes_le_maxDegRes
Proof state before:
case intro
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hvA : v ∈ A
t : ℕ
ht : Finset.max (image (fun v => degRes G v A) A) = ↑t
this✝ : (fun v => degRes G v A) v ∈ image (fun v => degRes G v A) A
this : (fun v => degRes G v A) v ≤ t
⊢ degRes G v A ≤ maxDegRes G A
Tactic:
rwa [maxDegRes, ht]
Proof state after:
no goals
Theorem: SimpleGraph.maxDegRes_sum_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
⊢ ∑ v in C, degRes G v A ≤ maxDegRes G A * card C
Tactic:
rw [card_eq_sum_ones, mul_sum, mul_one]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
⊢ ∑ v in C, degRes G v A ≤ ∑ x in C, maxDegRes G A
Theorem: SimpleGraph.maxDegRes_sum_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
⊢ ∑ v in C, degRes G v A ≤ ∑ x in C, maxDegRes G A
Tactic:
apply sum_le_sum _
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
⊢ ∀ (i : α), i ∈ C → degRes G i A ≤ maxDegRes G A
Theorem: SimpleGraph.maxDegRes_sum_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
⊢ ∀ (i : α), i ∈ C → degRes G i A ≤ maxDegRes G A
Tactic:
intro i hi
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
i : α
hi : i ∈ C
⊢ degRes G i A ≤ maxDegRes G A
Theorem: SimpleGraph.maxDegRes_sum_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
C A : Finset α
hC : C ⊆ A
i : α
hi : i ∈ C
⊢ degRes G i A ≤ maxDegRes G A
Tactic:
exact G.degRes_le_maxDegRes (hC hi)
Proof state after:
no goals
Theorem: SimpleGraph.exists_mem_nempty
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ¬nbhdRes G v A = ∅
⊢ ∃ w, w ∈ A ∧ Adj G v w
Tactic:
rw [nbhdRes] at hA
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ¬A ∩ neighborFinset G v = ∅
⊢ ∃ w, w ∈ A ∧ Adj G v w
Theorem: SimpleGraph.exists_mem_nempty
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ¬A ∩ neighborFinset G v = ∅
⊢ ∃ w, w ∈ A ∧ Adj G v w
Tactic:
contrapose! hA
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
⊢ A ∩ neighborFinset G v = ∅
Theorem: SimpleGraph.exists_mem_nempty
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
⊢ A ∩ neighborFinset G v = ∅
Tactic:
rw [eq_empty_iff_forall_not_mem]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
⊢ ∀ (x : α), ¬x ∈ A ∩ neighborFinset G v
Theorem: SimpleGraph.exists_mem_nempty
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
⊢ ∀ (x : α), ¬x ∈ A ∩ neighborFinset G v
Tactic:
intro x hx
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
x : α
hx : x ∈ A ∩ neighborFinset G v
⊢ False
Theorem: SimpleGraph.exists_mem_nempty
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
x : α
hx : x ∈ A ∩ neighborFinset G v
⊢ False
Tactic:
rw [mem_inter, mem_neighborFinset] at hx
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
x : α
hx : x ∈ A ∧ Adj G v x
⊢ False
Theorem: SimpleGraph.exists_mem_nempty
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
hA : ∀ (w : α), w ∈ A → ¬Adj G v w
x : α
hx : x ∈ A ∧ Adj G v x
⊢ False
Tactic:
exact hA x hx.1 hx.2
Proof state after:
no goals
Theorem: SimpleGraph.mem_res_nbhd_iff
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v w : α
A : Finset α
⊢ w ∈ nbhdRes G v A ↔ w ∈ A ∧ w ∈ neighborFinset G v
Tactic:
rw [nbhdRes, mem_inter]
Proof state after:
no goals
Theorem: SimpleGraph.subset_res_nbhd
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B : Finset α
v : α
A : Finset α
b : α
h : B ⊆ nbhdRes G v A
hb : b ∈ B
⊢ Adj G v b
Tactic:
exact (mem_neighborFinset _ _ _).1 ((G.mem_res_nbhd_iff _ _ _).1 (h hb)).2
Proof state after:
no goals
Theorem: SimpleGraph.not_mem_nbhd
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ ¬v ∈ neighborFinset G v
Tactic:
rw [mem_neighborFinset]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ ¬Adj G v v
Theorem: SimpleGraph.not_mem_nbhd
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
⊢ ¬Adj G v v
Tactic:
exact G.loopless v
Proof state after:
no goals
Theorem: SimpleGraph.not_mem_res_nbhd
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ ¬v ∈ nbhdRes G v A
Tactic:
rw [mem_res_nbhd_iff]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ ¬(v ∈ A ∧ v ∈ neighborFinset G v)
Theorem: SimpleGraph.not_mem_res_nbhd
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ ¬(v ∈ A ∧ v ∈ neighborFinset G v)
Tactic:
push_neg
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ v ∈ A → ¬v ∈ neighborFinset G v
Theorem: SimpleGraph.not_mem_res_nbhd
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ v ∈ A → ¬v ∈ neighborFinset G v
Tactic:
intro _
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
_✝ : v ∈ A
⊢ ¬v ∈ neighborFinset G v
Theorem: SimpleGraph.not_mem_res_nbhd
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
_✝ : v ∈ A
⊢ ¬v ∈ neighborFinset G v
Tactic:
exact G.not_mem_nbhd v
Proof state after:
no goals
Theorem: SimpleGraph.sub_res_nbhd_A
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
⊢ nbhdRes G v A ⊆ A
Tactic:
intro x
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
⊢ x ∈ nbhdRes G v A → x ∈ A
Theorem: SimpleGraph.sub_res_nbhd_A
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
⊢ x ∈ nbhdRes G v A → x ∈ A
Tactic:
rw [mem_res_nbhd_iff]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
⊢ x ∈ A ∧ x ∈ neighborFinset G v → x ∈ A
Theorem: SimpleGraph.sub_res_nbhd_A
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
⊢ x ∈ A ∧ x ∈ neighborFinset G v → x ∈ A
Tactic:
intro h
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
h : x ∈ A ∧ x ∈ neighborFinset G v
⊢ x ∈ A
Theorem: SimpleGraph.sub_res_nbhd_A
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
v : α
A : Finset α
x : α
h : x ∈ A ∧ x ∈ neighborFinset G v
⊢ x ∈ A
Tactic:
exact h.1
Proof state after:
no goals
Theorem: SimpleGraph.sum_sdf
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
C : Finset α
⊢ ∑ v in A, degRes G v C = ∑ v in B, degRes G v C + ∑ v in A \ B, degRes G v C
Tactic:
nth_rw 1 [← union_sdiff_of_subset hB]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
C : Finset α
⊢ ∑ v in B ∪ A \ B, degRes G v C = ∑ v in B, degRes G v C + ∑ v in A \ B, degRes G v C
Theorem: SimpleGraph.sum_sdf
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
C : Finset α
⊢ ∑ v in B ∪ A \ B, degRes G v C = ∑ v in B, degRes G v C + ∑ v in A \ B, degRes G v C
Tactic:
exact sum_union disjoint_sdiff
Proof state after:
no goals
Theorem: SimpleGraph.degRes_add_sub
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ degRes G v A = degRes G v B + degRes G v (A \ B)
Tactic:
simp_rw [degRes, nbhdRes]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ card (A ∩ neighborFinset G v) = card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)