internlm/Lean-Github huggingface dataset:
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
⊢ card (A ∩ neighborFinset G v) = card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)
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 α
v : α
hB : B ⊆ A
⊢ card ((B ∪ A \ B) ∩ neighborFinset G v) = card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)
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
⊢ card ((B ∪ A \ B) ∩ neighborFinset G v) = card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)
Tactic:
rw [inter_distrib_right B (A \ B) _]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
v : α
hB : B ⊆ A
⊢ card (B ∩ neighborFinset G v ∪ A \ B ∩ neighborFinset G v) =
    card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)
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
⊢ card (B ∩ neighborFinset G v ∪ A \ B ∩ neighborFinset G v) =
    card (B ∩ neighborFinset G v) + card (A \ B ∩ neighborFinset G v)
Tactic:
exact card_disjoint_union (sdiff_inter_disj A B _)
Proof state after:
no goals
Theorem: SimpleGraph.degRes_add_sum
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
hB : B ⊆ A
⊢ ∑ v in C, degRes G v A = ∑ v in C, degRes G v B + ∑ v in C, degRes G v (A \ B)
Tactic:
rw [← sum_add_distrib]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
hB : B ⊆ A
⊢ ∑ v in C, degRes G v A = ∑ x in C, (degRes G x B + degRes G x (A \ B))
Theorem: SimpleGraph.degRes_add_sum
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
hB : B ⊆ A
⊢ ∑ v in C, degRes G v A = ∑ x in C, (degRes G x B + degRes G x (A \ B))
Tactic:
exact sum_congr rfl fun _ _ => G.degRes_add_sub hB
Proof state after:
no goals
Theorem: SimpleGraph.degRes_add'
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
v : α
h : Disjoint A B
⊢ degRes G v (A ∪ B) = degRes G v A + degRes G v B
Tactic:
rw [degRes, nbhdRes,inter_distrib_right]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
v : α
h : Disjoint A B
⊢ card (A ∩ neighborFinset G v ∪ B ∩ neighborFinset G v) = degRes G v A + degRes G v B
Theorem: SimpleGraph.degRes_add'
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
v : α
h : Disjoint A B
⊢ card (A ∩ neighborFinset G v ∪ B ∩ neighborFinset G v) = degRes G v A + degRes G v B
Tactic:
exact card_disjoint_union (disj_of_inter_disj _ _ h)
Proof state after:
no goals
Theorem: SimpleGraph.degRes_add_sum'
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
h : Disjoint A B
⊢ ∑ v in C, degRes G v (A ∪ B) = ∑ v in C, degRes G v A + ∑ v in C, degRes G v B
Tactic:
rw [← sum_add_distrib]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
h : Disjoint A B
⊢ ∑ v in C, degRes G v (A ∪ B) = ∑ x in C, (degRes G x A + degRes G x B)
Theorem: SimpleGraph.degRes_add_sum'
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B C : Finset α
h : Disjoint A B
⊢ ∑ v in C, degRes G v (A ∪ B) = ∑ x in C, (degRes G x A + degRes G x B)
Tactic:
exact sum_congr rfl fun _ _ => G.degRes_add' h
Proof state after:
no goals
Theorem: SimpleGraph.bip_count_help
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
⊢ ∑ v in B, degRes G v (A \ B) = ∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0
Tactic:
simp only [degRes_ones]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
⊢ ∑ x in B, ∑ x in nbhdRes G x (A \ B), 1 = ∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0
Theorem: SimpleGraph.bip_count_help
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
⊢ ∑ x in B, ∑ x in nbhdRes G x (A \ B), 1 = ∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0
Tactic:
congr
Proof state after:
case e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
⊢ (fun x => ∑ x in nbhdRes G x (A \ B), 1) = fun v => ∑ w in A \ B, if Adj G v w then 1 else 0
Theorem: SimpleGraph.bip_count_help
Proof state before:
case e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
⊢ (fun x => ∑ x in nbhdRes G x (A \ B), 1) = fun v => ∑ w in A \ B, if Adj G v w then 1 else 0
Tactic:
ext x
Proof state after:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ ∑ x in nbhdRes G x (A \ B), 1 = ∑ w in A \ B, if Adj G x w then 1 else 0
Theorem: SimpleGraph.bip_count_help
Proof state before:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ ∑ x in nbhdRes G x (A \ B), 1 = ∑ w in A \ B, if Adj G x w then 1 else 0
Tactic:
simp only [sum_const, Algebra.id.smul_eq_mul, mul_one, sum_boole, cast_id]
Proof state after:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ card (nbhdRes G x (A \ B)) = card (filter (fun x_1 => Adj G x x_1) (A \ B))
Theorem: SimpleGraph.bip_count_help
Proof state before:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ card (nbhdRes G x (A \ B)) = card (filter (fun x_1 => Adj G x x_1) (A \ B))
Tactic:
congr
Proof state after:
case e_f.h.e_s
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ nbhdRes G x (A \ B) = filter (fun x_1 => Adj G x x_1) (A \ B)
Theorem: SimpleGraph.bip_count_help
Proof state before:
case e_f.h.e_s
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x : α
⊢ nbhdRes G x (A \ B) = filter (fun x_1 => Adj G x x_1) (A \ B)
Tactic:
ext
Proof state after:
case e_f.h.e_s.a
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x a✝ : α
⊢ a✝ ∈ nbhdRes G x (A \ B) ↔ a✝ ∈ filter (fun x_1 => Adj G x x_1) (A \ B)
Theorem: SimpleGraph.bip_count_help
Proof state before:
case e_f.h.e_s.a
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
A B : Finset α
x a✝ : α
⊢ a✝ ∈ nbhdRes G x (A \ B) ↔ a✝ ∈ filter (fun x_1 => Adj G x x_1) (A \ B)
Tactic:
rw [mem_res_nbhd_iff, mem_filter, mem_neighborFinset]
Proof state after:
no goals
Theorem: SimpleGraph.bip_count
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
⊢ ∑ v in B, degRes G v (A \ B) = ∑ v in A \ B, degRes G v B
Tactic:
rw [G.bip_count_help]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
⊢ (∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0) = ∑ v in A \ B, degRes G v B
Theorem: SimpleGraph.bip_count
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
⊢ (∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0) = ∑ v in A \ B, degRes G v B
Tactic:
have := _root_.sdiff_sdiff_eq_self hB
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
⊢ (∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0) = ∑ v in A \ B, degRes G v B
Theorem: SimpleGraph.bip_count
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
⊢ (∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0) = ∑ v in A \ B, degRes G v B
Tactic:
nth_rw 4 [←this ]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
⊢ (∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0) = ∑ v in A \ B, degRes G v (A \ (A \ B))
Theorem: SimpleGraph.bip_count
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
⊢ (∑ v in B, ∑ w in A \ B, if Adj G v w then 1 else 0) = ∑ v in A \ B, degRes G v (A \ (A \ B))
Tactic:
rw [G.bip_count_help, this, sum_comm]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
⊢ (∑ y in A \ B, ∑ x in B, if Adj G x y then 1 else 0) = ∑ v in A \ B, ∑ w in B, if Adj G v w then 1 else 0
Theorem: SimpleGraph.bip_count
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
⊢ (∑ y in A \ B, ∑ x in B, if Adj G x y then 1 else 0) = ∑ v in A \ B, ∑ w in B, if Adj G v w then 1 else 0
Tactic:
congr
Proof state after:
case e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
⊢ (fun y => ∑ x in B, if Adj G x y then 1 else 0) = fun v => ∑ w in B, if Adj G v w then 1 else 0
Theorem: SimpleGraph.bip_count
Proof state before:
case e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
⊢ (fun y => ∑ x in B, if Adj G x y then 1 else 0) = fun v => ∑ w in B, if Adj G v w then 1 else 0
Tactic:
ext y
Proof state after:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y : α
⊢ (∑ x in B, if Adj G x y then 1 else 0) = ∑ w in B, if Adj G y w then 1 else 0
Theorem: SimpleGraph.bip_count
Proof state before:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y : α
⊢ (∑ x in B, if Adj G x y then 1 else 0) = ∑ w in B, if Adj G y w then 1 else 0
Tactic:
congr
Proof state after:
case e_f.h.e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y : α
⊢ (fun x => if Adj G x y then 1 else 0) = fun w => if Adj G y w then 1 else 0
Theorem: SimpleGraph.bip_count
Proof state before:
case e_f.h.e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y : α
⊢ (fun x => if Adj G x y then 1 else 0) = fun w => if Adj G y w then 1 else 0
Tactic:
ext x
Proof state after:
case e_f.h.e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
⊢ (if Adj G x y then 1 else 0) = if Adj G y x then 1 else 0
Theorem: SimpleGraph.bip_count
Proof state before:
case e_f.h.e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
⊢ (if Adj G x y then 1 else 0) = if Adj G y x then 1 else 0
Tactic:
split_ifs with h1 h2 h3
Proof state after:
case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : Adj G x y
h2 : Adj G y x
⊢ 1 = 1

case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : Adj G x y
h2 : ¬Adj G y x
⊢ False

case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : ¬Adj G x y
h3 : Adj G y x
⊢ False

case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : ¬Adj G x y
h3 : ¬Adj G y x
⊢ 0 = 0
Theorem: SimpleGraph.bip_count
Proof state before:
case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : Adj G x y
h2 : Adj G y x
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.bip_count
Proof state before:
case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : Adj G x y
h2 : ¬Adj G y x
⊢ False
Tactic:
rw [adj_comm] at h1
Proof state after:
case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : Adj G y x
h2 : ¬Adj G y x
⊢ False
Theorem: SimpleGraph.bip_count
Proof state before:
case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : Adj G y x
h2 : ¬Adj G y x
⊢ False
Tactic:
exact h2 h1
Proof state after:
no goals
Theorem: SimpleGraph.bip_count
Proof state before:
case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : ¬Adj G x y
h3 : Adj G y x
⊢ False
Tactic:
rw [adj_comm] at h1
Proof state after:
case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : ¬Adj G y x
h3 : Adj G y x
⊢ False
Theorem: SimpleGraph.bip_count
Proof state before:
case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : ¬Adj G y x
h3 : Adj G y x
⊢ False
Tactic:
exact h1 h3
Proof state after:
no goals
Theorem: SimpleGraph.bip_count
Proof state before:
case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
hB : B ⊆ A
this : A \ (A \ B) = B
y x : α
h1 : ¬Adj G x y
h3 : ¬Adj G y x
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.bip_count_help'
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ ∑ v in B, degRes G v A = ∑ v in B, ∑ w in A, if Adj G v w then 1 else 0
Tactic:
simp_rw [degRes_ones]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ ∑ x in B, ∑ x in nbhdRes G x A, 1 = ∑ v in B, ∑ w in A, if Adj G v w then 1 else 0
Theorem: SimpleGraph.bip_count_help'
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ ∑ x in B, ∑ x in nbhdRes G x A, 1 = ∑ v in B, ∑ w in A, if Adj G v w then 1 else 0
Tactic:
congr
Proof state after:
case e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (fun x => ∑ x in nbhdRes G x A, 1) = fun v => ∑ w in A, if Adj G v w then 1 else 0
Theorem: SimpleGraph.bip_count_help'
Proof state before:
case e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (fun x => ∑ x in nbhdRes G x A, 1) = fun v => ∑ w in A, if Adj G v w then 1 else 0
Tactic:
ext x
Proof state after:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
x : α
⊢ ∑ x in nbhdRes G x A, 1 = ∑ w in A, if Adj G x w then 1 else 0
Theorem: SimpleGraph.bip_count_help'
Proof state before:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
x : α
⊢ ∑ x in nbhdRes G x A, 1 = ∑ w in A, if Adj G x w then 1 else 0
Tactic:
rw [nbhdRes_filter,sum_filter]
Proof state after:
no goals
Theorem: SimpleGraph.bip_count'
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ ∑ v in B, degRes G v A = ∑ v in A, degRes G v B
Tactic:
rw [G.bip_count_help' ]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (∑ v in B, ∑ w in A, if Adj G v w then 1 else 0) = ∑ v in A, degRes G v B
Theorem: SimpleGraph.bip_count'
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (∑ v in B, ∑ w in A, if Adj G v w then 1 else 0) = ∑ v in A, degRes G v B
Tactic:
rw [G.bip_count_help']
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (∑ v in B, ∑ w in A, if Adj G v w then 1 else 0) = ∑ v in A, ∑ w in B, if Adj G v w then 1 else 0
Theorem: SimpleGraph.bip_count'
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (∑ v in B, ∑ w in A, if Adj G v w then 1 else 0) = ∑ v in A, ∑ w in B, if Adj G v w then 1 else 0
Tactic:
rw [sum_comm]
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (∑ y in A, ∑ x in B, if Adj G x y then 1 else 0) = ∑ v in A, ∑ w in B, if Adj G v w then 1 else 0
Theorem: SimpleGraph.bip_count'
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (∑ y in A, ∑ x in B, if Adj G x y then 1 else 0) = ∑ v in A, ∑ w in B, if Adj G v w then 1 else 0
Tactic:
congr
Proof state after:
case e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (fun y => ∑ x in B, if Adj G x y then 1 else 0) = fun v => ∑ w in B, if Adj G v w then 1 else 0
Theorem: SimpleGraph.bip_count'
Proof state before:
case e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
⊢ (fun y => ∑ x in B, if Adj G x y then 1 else 0) = fun v => ∑ w in B, if Adj G v w then 1 else 0
Tactic:
ext y
Proof state after:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y : α
⊢ (∑ x in B, if Adj G x y then 1 else 0) = ∑ w in B, if Adj G y w then 1 else 0
Theorem: SimpleGraph.bip_count'
Proof state before:
case e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y : α
⊢ (∑ x in B, if Adj G x y then 1 else 0) = ∑ w in B, if Adj G y w then 1 else 0
Tactic:
congr
Proof state after:
case e_f.h.e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y : α
⊢ (fun x => if Adj G x y then 1 else 0) = fun w => if Adj G y w then 1 else 0
Theorem: SimpleGraph.bip_count'
Proof state before:
case e_f.h.e_f
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y : α
⊢ (fun x => if Adj G x y then 1 else 0) = fun w => if Adj G y w then 1 else 0
Tactic:
ext x
Proof state after:
case e_f.h.e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
⊢ (if Adj G x y then 1 else 0) = if Adj G y x then 1 else 0
Theorem: SimpleGraph.bip_count'
Proof state before:
case e_f.h.e_f.h
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
⊢ (if Adj G x y then 1 else 0) = if Adj G y x then 1 else 0
Tactic:
split_ifs with h1 h2 h3
Proof state after:
case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : Adj G x y
h2 : Adj G y x
⊢ 1 = 1

case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : Adj G x y
h2 : ¬Adj G y x
⊢ False

case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : ¬Adj G x y
h3 : Adj G y x
⊢ False

case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : ¬Adj G x y
h3 : ¬Adj G y x
⊢ 0 = 0
Theorem: SimpleGraph.bip_count'
Proof state before:
case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : Adj G x y
h2 : Adj G y x
⊢ 1 = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.bip_count'
Proof state before:
case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : Adj G x y
h2 : ¬Adj G y x
⊢ False
Tactic:
rw [adj_comm] at h1
Proof state after:
case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : Adj G y x
h2 : ¬Adj G y x
⊢ False
Theorem: SimpleGraph.bip_count'
Proof state before:
case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : Adj G y x
h2 : ¬Adj G y x
⊢ False
Tactic:
exact h2 h1
Proof state after:
no goals
Theorem: SimpleGraph.bip_count'
Proof state before:
case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : ¬Adj G x y
h3 : Adj G y x
⊢ False
Tactic:
rw [adj_comm] at h1
Proof state after:
case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : ¬Adj G y x
h3 : Adj G y x
⊢ False
Theorem: SimpleGraph.bip_count'
Proof state before:
case pos
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : ¬Adj G y x
h3 : Adj G y x
⊢ False
Tactic:
exact h1 h3
Proof state after:
no goals
Theorem: SimpleGraph.bip_count'
Proof state before:
case neg
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A : Finset α
y x : α
h1 : ¬Adj G x y
h3 : ¬Adj G y x
⊢ 0 = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: SimpleGraph.sum_res_le
Proof state before:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
⊢ ∑ v in C, degRes G v B ≤ ∑ v in C, degRes G v A
Tactic:
apply sum_le_sum _
Proof state after:
α : Type u_1
G : SimpleGraph α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
B A C : Finset α
hB : B ⊆ A
⊢ ∀ (i : α), i ∈ C → degRes G i B ≤ degRes G i A