𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ card (filter (fun e => Adj G e.fst e.snd) (s ×ˢ t)) + card (filter (fun e => Adj (Gᶜ) e.fst e.snd) (s ×ˢ t)) =
    card (s ×ˢ t)
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ card (interedges G s t) + card (interedges (Gᶜ) s t) = card s * card t
rw [← card_product, interedges_def, interedges_def]
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
this : filter (fun e => Adj (Gᶜ) e.fst e.snd) (s ×ˢ t) = filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t)
⊢ card (filter (fun e => Adj G e.fst e.snd) (s ×ˢ t)) + card (filter (fun e => Adj (Gᶜ) e.fst e.snd) (s ×ˢ t)) =
    card (s ×ˢ t)
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ card (filter (fun e => Adj G e.fst e.snd) (s ×ˢ t)) + card (filter (fun e => Adj (Gᶜ) e.fst e.snd) (s ×ˢ t)) =
    card (s ×ˢ t)
have : ((s ×ˢ t).filter fun e ↦ Gᶜ.Adj e.1 e.2) = (s ×ˢ t).filter fun e ↦ ¬G.Adj e.1 e.2 := by
  refine' filter_congr fun x hx ↦ _
  rw [mem_product] at hx
  rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
this : filter (fun e => Adj (Gᶜ) e.fst e.snd) (s ×ˢ t) = filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t)
⊢ Disjoint (filter (fun e => Adj G e.fst e.snd) (s ×ˢ t)) (filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t))
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
this : filter (fun e => Adj (Gᶜ) e.fst e.snd) (s ×ˢ t) = filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t)
⊢ card (filter (fun e => Adj G e.fst e.snd) (s ×ˢ t)) + card (filter (fun e => Adj (Gᶜ) e.fst e.snd) (s ×ˢ t)) =
    card (s ×ˢ t)
rw [this, ← card_union_eq, filter_union_filter_neg_eq]
no goals
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
this : filter (fun e => Adj (Gᶜ) e.fst e.snd) (s ×ˢ t) = filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t)
⊢ Disjoint (filter (fun e => Adj G e.fst e.snd) (s ×ˢ t)) (filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t))
exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x ∈ s ×ˢ t
⊢ Adj (Gᶜ) x.fst x.snd ↔ ¬Adj G x.fst x.snd
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ filter (fun e => Adj (Gᶜ) e.fst e.snd) (s ×ˢ t) = filter (fun e => ¬Adj G e.fst e.snd) (s ×ˢ t)
refine' filter_congr fun x hx ↦ _
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x.fst ∈ s ∧ x.snd ∈ t
⊢ Adj (Gᶜ) x.fst x.snd ↔ ¬Adj G x.fst x.snd
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x ∈ s ×ˢ t
⊢ Adj (Gᶜ) x.fst x.snd ↔ ¬Adj G x.fst x.snd
rw [mem_product] at hx
no goals
𝕜 : Type ?u.113206
ι : Type ?u.113209
κ : Type ?u.113212
α : Type u_1
β : Type ?u.113218
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s s₁ s₂ t t₁ t₂ : Finset α
a b : α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x.fst ∈ s ∧ x.snd ∈ t
⊢ Adj (Gᶜ) x.fst x.snd ↔ ¬Adj G x.fst x.snd
rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]