Theorem: SimpleGraph.bip_count (Turan4/NbhdRes.lean)

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]
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

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
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

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 ]
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))

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]
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals