∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V]
  [inst_1 : DecidableRel G.Adj], G.IsExtremal H.Free → G.edgeFinset.card = SimpleGraph.extremalNumber (Fintype.card V) H