split_ifs with h1 h2 h3
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
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