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 α
⊢ ∑ v in B, degRes G v A = ∑ v in A, 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 α
⊢ (∑ v in B, ∑ w in A, if Adj G v w then 1 else 0) = ∑ v in A, degRes G v B

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

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

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

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

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

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

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

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

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

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

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

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

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