-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem card_interedges_add_card_interedges_compl (h : Disjoint s t) :
    #(G.interedges s t) + #(Gᶜ.interedges s t) = #s * #t

Proof state:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
this : filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t) = filter (fun e => ¬G.Adj e.1 e.2) (s ×ˢ t)
⊢ Disjoint (filter (fun e => G.Adj e.1 e.2) (s ×ˢ t)) (filter (fun e => ¬G.Adj e.1 e.2) (s ×ˢ t))

Tactic:
exact disjoint_filter.2 fun _ _ ↦ Classical.not_not.2

Result:
no goals

Proof state:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x.1 ∈ s ∧ x.2 ∈ t
⊢ Gᶜ.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2

Tactic:
rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)]

Result:
no goals

Proof state:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
this : filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t) = filter (fun e => ¬G.Adj e.1 e.2) (s ×ˢ t)
⊢ #(filter (fun e => G.Adj e.1 e.2) (s ×ˢ t)) + #(filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t)) = #(s ×ˢ t)

Tactic:
rw [this, ← card_union_of_disjoint, filter_union_filter_neg_eq]

Result:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
this : filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t) = filter (fun e => ¬G.Adj e.1 e.2) (s ×ˢ t)
⊢ Disjoint (filter (fun e => G.Adj e.1 e.2) (s ×ˢ t)) (filter (fun e => ¬G.Adj e.1 e.2) (s ×ˢ t))

Proof state:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ #(G.interedges s t) + #(Gᶜ.interedges s t) = #s * #t

Tactic:
rw [← card_product, interedges_def, interedges_def]

Result:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ #(filter (fun e => G.Adj e.1 e.2) (s ×ˢ t)) + #(filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t)) = #(s ×ˢ t)

Proof state:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x ∈ s ×ˢ t
⊢ Gᶜ.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2

Tactic:
rw [mem_product] at hx

Result:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x.1 ∈ s ∧ x.2 ∈ t
⊢ Gᶜ.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2

Proof state:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ #(filter (fun e => G.Adj e.1 e.2) (s ×ˢ t)) + #(filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t)) = #(s ×ˢ t)

Tactic:
have : {e ∈ s ×ˢ t | Gᶜ.Adj e.1 e.2} = {e ∈ s ×ˢ t | ¬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)]

Result:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
this : filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t) = filter (fun e => ¬G.Adj e.1 e.2) (s ×ˢ t)
⊢ #(filter (fun e => G.Adj e.1 e.2) (s ×ˢ t)) + #(filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t)) = #(s ×ˢ t)

Proof state:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
⊢ filter (fun e => Gᶜ.Adj e.1 e.2) (s ×ˢ t) = filter (fun e => ¬G.Adj e.1 e.2) (s ×ˢ t)

Tactic:
refine filter_congr fun x hx ↦ ?_

Result:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
h : Disjoint s t
x : α × α
hx : x ∈ s ×ˢ t
⊢ Gᶜ.Adj x.1 x.2 ↔ ¬G.Adj x.1 x.2