Theorem: SimpleGraph.disjoint_ind (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Basic.lean)

State before:
α : Type u_1
β : Type u_2
G H : SimpleGraph α
s✝ : Set (Sym2 α)
s t : Set α
a b : α
h : Disjoint s t
⊢ Disjoint (G.ind s) (G.ind t)
Tactic:
rw [disjoint_iff, ← ind_inter, disjoint_iff_inter_eq_empty.1 h, ind_empty]
State after:
no goals