Theorem: SimpleGraph.labelledCopyCount_eq_zero (LeanCamCombi/Mathlib/Combinatorics/SimpleGraph/Containment.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ G.labelledCopyCount H = 0 ↔ ¬G ⊑ H
Tactic:
simp [labelledCopyCount, IsContained, Fintype.card_eq_zero_iff]
State after:
no goals